Vor geraumer Zeit hatte ich ja erzählt, welche Maßnahmen den Browser prinzipiell etwas datensparsamer machen. Zur Zeit brause ich am liebsten mit dem Firefox von Mozilla durch den Cyberspace. Im Folgenden stelle ich vor, wie diesem Programm etwas mehr Datensparsamkeitz beibringe. In diesem Internet gibt es jedoch noch weitere Ansätze.
Die einfachste Möglichkeit, einem Browser etwas mehr Datensparsamkeit beizubringen, ist das setzen von sinnvollen Einstellungen, die zwar von Haus aus unterstützt, aber nicht voreingestellt sind.
Die wahrscheinlich leichteste Art den Browser datensparsamer zu machen ist Do Not Track. Hierbei teilt der Browser den Webseiten mit, dass der Nutzer nicht verfolgt werden soll. Aus zwei Gründen ist jedoch nicht unumstritten: Zum Einen ignorieren viele Dienste diesen Wunsch; zum Anderen setzen einige Anbieter dies um, indem sie noch immer Daten sammeln, jedoch nur keine angepasste Werbung mehr anzeigen. (Es soll sogar Menschen geben, die sich von angepasster Werbung weniger genervt fühlen.)
Wer kein Problem damit hat, dass Werbung unpassend wird, kann durch diese einfache Einstellung im Firefox wenigstens eine Anbieter dazu bringen weniger Daten zu sammeln.
Ist Do Not Track aktiviert, können Anbieter externer Inhalte noch immer sehen, von welchen Webseiten aus diese aufgerufen werden. Schlimmer noch: Die externen Inhalte können Cookies setzen, durch die das Nutzungsverhalten über Webseitengrenzen hinweg Nutzern zugeordnet werden kann.
Warum sendet der Browser überhaupt Cookies an Drittanbieter? Diese Cookies dienen nicht nur dem Verfolgen von Nutzern. Es gibt duchaus Fälle, in denen Nutzer von externen wiedererkannt werden wollen – etwa von zentralen Login-Diensten. Ein weiteres Problem ist, dass bösartige Dienste Nutzer auch ohne Cookie erkennen..
Wer kein Problem mit den geschilderten Nachteilen hat, kann Firefox leicht beibringen keine Cookies von Drittanbietern mehr anzunehmen. Übrigens kann man Firefox an dieser Stelle auch erklären, dass Cookies dann mitgensdet werden sollen, wenn sie bei einem direkten Besuch des Drittanbieters (also etwa Login über einen zentralen Dienst) gesetzt wurden.
Abgesehen von diesen Einstellungen, die Firefox von Haus aus mitbringt, gibt es auch Erweiterungen, die einige Datenschutzprobleme im Browser eindämmen.
Abgesehen von Drittanbieterinhalten setzen auch die besuchten Seiten selbst Cookies. Im Laufe der Zeit kommen so viele Cookies von vielen Webseiten zusammen. Das führt dann etwa dazu, dass Webshops bei einem zufälligen Besuch Bücher vorschlagen, die zu Angebotsaufrufen aus grauer Vorzeit passen.
Die Firefox-Erweiterung Self-Destructing Cookies tut genau das, was ihr Name verspricht: Wird ein Tab geschlossen, werden nach einer einstellbaren Zeit alle von ihr gesetzten Cookie gelöscht. Logins funktionieren daher noch, da die Cookies während des Logins ungehindert übertragen werden. Gibt es Seiten, deren Cookies auch nach dem Schließen eines Tabs oder sogar nach demm Neustart des Browsers erhalten bleiben sollen (etwa die Spracheinstellung einer Suchmaschine), kann diese Ausnahme über einen farbigen Knopf, den die Erweiterung im Browser anlegt, eingestellt werden: Grün behält die Cookies, solange sie haltbar sind, gelb löscht die Cookies beim Schließen des Browsers und rot (Voreinstellung) löscht die Cookies beim Schließen des Tabs.
Die Erweiterung RequestPolicy bietet die wahrscheinlich konsequenteste Möglichkeit, Datensparsamkeit zu erzwingen: Das Laden jeglicher externer Inhalte wird blockiert. Die meisten Seiten sehen dann ziemlich dämlich aus oder funktionieren einfach nicht mehr, weil notwendige Stylesheets oder Javascript-Bibliotheken auf externen Servern liegen. Dazu lassen sich für jede Domain mit zwei Klicks Domains Ausnahmen festlegen. Hierbei können Quellen, die immer eungebunden werden dürfen (wie etwa Videoportale), Seiten, die sämtliche Drittanbeiter verwenden dürfen (etwa Portale, die ihre Inhalte unter ständig wechselnden Adressen ablegen), und konkrete Befugnisse (etwa, dass auf images.exmaple.com gespeicherte Inhalte von example.org eingebunden werden dürfen) eingestellt werden.
Im Allgemeinen ist es ja unentscheidbar, ob eine prädikatenlogische Formel eine Tautologie ist. Wäre dies immer entscheidbar, so könnte auch entschieden werden, ob eine Instanz des Postschen Korrespondezproblems lösbar ist (indem für die Instanz eine prädikatenlogische Formel gebaut wird, die genau dann eine Tautologie ist, wenn die Instanz lösbar ist). Das das Postsche Korrespondezproblem ja unentscheidbar ist, gibt es folglich auch prädikatenlogische Formeln, für die nicht entscheiden werden kann, ob sie Tautologien sind.
Die prädikatenlogischen Formeln lassen sich jedoch etwa mit dem System F aufzählen. Es gibt außerdem Teilmengen prädikatenlogischer Formeln, für die es sogar entscheidbar ist, ob sie Tautologien sind. Hiemrmit und mit der Tablaumethode werde ich mich im Folgenden beschäftigen.
Mit der Tableaumethode lassen sich auch in der Prädikatenlogik Beweise für verschiedene Eigenschaften von Formeln führen. Dies führe ich nun mit einem Beispiel für einen Erfüllbarkeitsbeweis und mit einem Beispiel für einen Tautologiebeweis vor. Zur besseren Lesbarkeit werde ich die Formeln nummeriert statt in einem Baum aufschreiben.
An der Formel ∀ z ∃ x ∃ y p(x, y, z) zeige ich nun, wie man einen Erfüllbarkeitsbeweis mittels Tableau führen kann.
Die Formel lässt sich mit der Domäne {a} erfüllen mit einer Struktur, die ein Modell für p(a, a, a) ist (also p(a, a, a) erfüllt).
Auch Beweise, dass Formeln wie etwa ∀ x ∀ y ((p(x,y) ∧ q(x)) → ∃ y q(y)) Tautologien sind, lassen sich mit Tableau führen. Hierzu muss die gegebene Formel zunächst negiert werden:
Da 4. und 5. widersprüchlich sind, ist das Tableau abgeschlossen und die negierte Formel unerfüllbar. Daher ist die ursprüngliche Formel eine Tautologie.
Vor geraumer Zeit hatte ich ja etwas zu Theorien geschrieben. Es gibt hierzu noch eine weitere Erkenntnis, die zu Entscheidbarkeit und Aufzählbarkeit passt: Ist eine Theorie entscheidbar, so ist sie auch aufzählbar axiomatisierbar.
Nun warum ist das so? Eine Theorie ist ja aufzählbar axiomatisierbar, wenn sie sich mit einem aufzählbaren Axiomensystem erzeugen lässt. Da jede Theorie Σ gegen Folgerung abgeschlossen ist, ist die aus der Theorie erzeugte Theorie TΣ = Σ. Da eine entscheidbare Menge auch semi-entscheidbar, also aufzählbar, ist, ist die entscheidbare Theorie Σ zugleich ein aufzählbares Axiomensystem für sich selbst.
Mit System F lassen sich in der Prädikatenlogik Beweise für Folgerungen führen. Dies führe ich nun an zwei Beispielen vor.
Zum Abschluss möchte ich nun ein Beispiel für entscheidbare Mengen liefern. Betrachten wie die Theorie der Gleichheit TΣE. Diese sei durch das Axiomensystem ΣE gegeben, das Folgendes für das Gleichheitssymbol fordert: Reflexivität, Symmetrie, Transitivität und Beibehaltung der Gleichheit durch Funktionen (also: sind die Parameter zweier Funktionsaufrufe gleich, dann bilden beide auf gleiche Elemente ab). Die verwendete Signatur enthalte keine Prädikate.
Nun lässt sich ein Algorithmus finden, der für geschlossene, quantorenfreie, prädikatenfreie Formeln entscheidet, ob diese in dieser Theorie sind. Der Algorithmus arbeitet so:
Ohne mich direkt auf aktuelle Meldungen zu beziehen, finde ich, dass Datenschutz wichtig ist. Ich finde das Thema sogar so wichtig, dass ich mir von Hanna ein Symbolbild hierzu malen lassen habe. Vielen Dank dafür! Es geht hierbei nicht einfach darum, etwas zu verbergen. Es geht zum Einen darum, die Kontrolle über die eigenen Daten zu behalten. Zum Anderen geht es darum, sich bewusst zu werden, wer etwa mit Informationen über das eigene Verhalten im Web versorgt wird. Im Folgenden will ich erläutern, wie der Browser weniger „gesprächig“ über das Verhalten der Nutzer werden kann. In diesem Artikel werde ich eine grobe Übersicht über Maßnahmen und Probleme geben:
Cookies sind zunächst Datenschnipsel, die von Inhalten im Web gesetzt werden können. Der Browser sendet dann bei jeder Verbindung diejenigen Cookie mit, die von einer Website gesetzt wurden. Dies wird verwendet, um Einstellungen oder ein Identifikationsmerkmal für eingeloggte Nutzer zu übermitteln.
Kritisch ist nun eine Voreinstellung vieler Browser: Nicht nur die Seite, die gerade angezeigt wird, darf Cookies setzen und erhalten, auch etwa Bilder und andere Inhalte von externen Servern dürfen dies. Dies bedeutet, dass etwa ein soziales Netzwerk, das Knöpfchen zum Einbinden in Webseiten anbietet, Nutzer über viele verschiedene Webseiten hinweg verfolgen kann. Immer wenn der Nutzer den Knopf des sozialen Netzwerks sieht, erhält dieses den gesetzten Cookie.
Die einfache (und in vielen Browsern mögliche) Maßnahme wäre nun einfach das Unterbinden solcher Drittanbietercookies. Das Problem ist jedoch, dass einige Dienste so kontruiert sind, dass sie diese Drittanbietercookies benötigen. Daher ist es sinnvoll, wenn der Browser in solchen Fällen Ausnahmen unterstützt.
Ist mit dem Sperren von Drittanbietercookies wirklich alles getan? Hierzu ein Beispiel: Alice verwendet das soziale Netzwerk Evebook, sperrt aber Drittanbietercookies. Verwendet Alice direkt Evebook; ihr Browser sendet dabei einen Cookie und die genaue Bezeichnung des Browsers samt Versionsnummer. Evebook erhält durch den Seitenaufruf außerdem die IP-Adresse von Alice. Betrachtet sich Alice nun eine Webseite im Internet, die den „Mag ich“-Knopf von Evebook einbindet, erhält Evebook zwar keinen Cookie, aber IP-Adresse und Browserbezeichnung. Somit kann Evebook immerhin annehmen, dass wahrscheinlich Alice die Person ist, die die Seite aufruft.
Es ist also auch ohne Drittanbietercookies Dritten möglich, einen Nutzer über verschiedene Webseiten hinweg zu identifizieren. Dazu gibt es im Übrigen noch weitaus abgefahrenere Methoden als die vorgestellte. Die Drittanbieterinhalte könen außerdem Javascript-Programme sein. Der Webdienst 7-min.com, der eine Stoppuhr für Fitnessübungen anbietet, beweist eindrucksvoll, wozu Drittanbieterinhalte verwendet werden können: Nach jeder Übung wird ein Statistikdienst eines großen Suchmaschinenanbieters über den Trainingsfortschritt des Nutzers informiert.
Um nicht über Webseitengrenzen hinweg verfolgt werden zu können, wäre es nun durchaus zu überlegen nicht nur Cookies Dritter sondern gleich sämtliche Inhalte Dritter zu verbieten. Tatsächlich sähe das Web dann jedoch ziemlich kaputt aus. Viele Webanwendungen lagern etwa Bilder auf externe Server aus. Es muss also auch hier möglich sein Asunahmen zu definieren.
Wie müssen nun solche Ausnahmen aussehen? Hierzu wieder das Evebook-Beispiel: Angenommen sowohl der „Mag ich“-Knopf als auch die Logos von Evebook liegen auf „evebook-knoepfe.example“. Nun würde Alice aber erlauben wollen, dass Inhalte von „evebook-knoepfe.example“ geladen werden, um Evebook zu benutzen. Dies würde aber auch die „Mag ich“-Knöpfe umfassen und schon könnte Evebook wieder das Gewohnheiten von Alice im Web aufzeichnen.
Alice will also die Ausnahmen für einzelne Quellen und Ziele definieren: Nur Evebook selbst darf Inhalte von „evebook-knoepfe.example“ einbinden, alle anderen nicht.
Der Nachteil ist nun, dass Alice für jede Website, die sie besucht, einzeln herausfinden muss, welche Drittanbieterinhalte nötig sein. Im schlimmsten Fall muss sie dies durch Ausprobieren herausfinden und dafür eine Menge Zeit investieren.
Ein typischer Inhalt, der von Drittanbietern stammt, ist Internetwerbung. Gerade diese neigt dazu Nutzer über Webseitengrenzen hinweg zu verfolgen. Es gibt Erweiterungen und Listen, um recht effektiv Internetwerbung (und somit fragliche Inhalte Dritter). Hier ist quasi keine eigene Konfigurationsarbeit mehr nötig.
Der offensichtlichste Nachteil ist jedoch, dass es immer unerwünschte Inhalte gibt, die nicht vom Werbefilter getroffen werden, bis dafür (meist) manuell ein Filter erstellt wurde.
Es ist außerdem zu bedenken, dass das sehr strikte Blockieren von Werbung Anbietern kostenloser Inhalte schaden kann.
Eines der beliebtesten Programme zum Blockieren von Werbung steht im Moment unter heftiger Kritik. Sogar eine Schwestersendung der Tagesschau, das Nachtmagazin berichtete über den Fall.
Über die aktuelle Kritik an Werbeblockern und die Verwendung dieser werde ich demnächst etwas ausführlicher berichten.
Im Prinzip ist es ja noch nicht problematisch, wenn etwa ein soziales Netzwerk oder ein Werbeanbieter Daten sammeln kann. Problematisch wird es erst, wenn diese Daten tatsächlich Genutzt werden. Dazu gibt es den „Do-Not-Track“-Header. Dieser bittet Dienste im Web darum, den Nutzer nicht zu verfolgen.
In der Praxis verzichten einige Anbieter dann einfach auf personalisierte Inhalte. Erhoben und gespeichert werden die Daten jedoch weiterhin. Außerdem spielen nicht alle Anbieter mit.
Wer auf personalisierte Inhalte bewusst verzichten möchte, kann die „Do-Not-Track“-Option im Browser durchaus aktivieren. Ein Datenschutzallheilmittel ist die Option gewiss nicht.
Was ist eigentlich mit dem Fall, dass nicht der Dienstanbieter böse ist sondern der Feind im eigenen Netzwerk sitzt? Zum Beispiel: Alice und Bob sitzen in einem offenen (unverschlüsselten) Funknetzwerk und Alice benutzt Evebook. Nun könnte etwa Bob mit geeigneter Technik den Funkverkehr mitlesen, den Cookie zu Evebook auslesen und sich als Alice ausgeben und Unfug treiben.
Alice hat jedoch Glück: Evebook verwendet https. Die Daten zwischen dem Computern von Alice und den Servern von Evebook können also verschlüsselt werden. Was passiert aber, wenn Bob Alice einen http-Link zu Evebook unterjubelt? Dann ist die Verbindung nicht mehr verschlüsselt, die Cookies werden im Klartext übertragen und Bob kann mitlesen. Das will man nicht. Wie lassen sich nun solche http-Verbindungen verhindern?
Prädikatenlogische Theorien (erster Stufe) sind Mengen geschlossener Formeln, die auch alle, aus eben dieser Menge logisch folgerbaren Formeln enthalten. Diese Definition und die folgende Bemerkungen stammen aus den Folien (Meyer 2013) zur Vorlesung Logik. Wenn im Folgenden von Theorien und (geschlossenen) Formeln gesprochen wird, sind Formeln und Theorien über einer Signatur S gemeint.
Ich werde nun einige Beweise über Theorien und unter Verwendung der vorgestellten Definitionen vorstellen.
Sei T eine inkonsistene Theorie. Nach Definition enthält T sowohl die Formel A als auch ¬A. Somit ist T unerfüllar und jede geschlossene Formel kann daraus gefolgert werden. Nach der Defition von Theorien sind diese Formeln auch alle in der Theorie enthalten. Folglich ist jede inkonsistene Theorie gerade die Menge aller geschlossenen Formeln (einer Signatur S).
Wäre die Theorie eines Modells inkonsistent, würde sie sowohl A als auch ¬A enthalten. Dies kann jedoch nicht sein, da das Modell ja nur eine der beiden Formeln erfüllen kann und somit kann auch nur eine der beiden Formeln in der Theorie dieses Modells sein.
Wäre eine Theorie eines Modells nicht vollständig, gäbe es eine Formel A so, dass weder A noch ¬A in der Theorie sind. Erfüllt das Modell die Formel A nicht, muss es ¬A erfüllen und ¬A wäre in der Theorie des Modells.
Ist eine Theorie aufzählbar axiomatisierbar, so lässt auch durch Verwendung des deduktiven System F die Theorie selbst aufzählen. Da die Theorie vollständig ist, wird nach endlicher Zeit A oder ¬A beim Aufzählen genannt. Dann kann der Entscheidungsalgorithmus halten und entsprechend antworten.
Behauptung:Eine Theorie Σ ist vollständig ⇔ mit jeder geschlossenen Formel A ist TΣ ∪ {A} oder TΣ ∪ {¬A} inkonsistent
„⇒ “: Da die Theorie vollständig ist, betrachtet folgende Fallunterscheidung alle möglichen Fälle (für jede geschlossene Formel A):
„⇐ “: Für jede geschlossene Formel A ist TΣ ∪ {A} oder TΣ ∪ {¬A} inkonsistent.
Wer Fragen wie „Wird OpenSource verboten?“ hört, könnte meinen ich übertreibe völlig und würde antworten: „Nein, es wird nur irgendwas geändert, was nicht in deine verbohrte Ideologie passt, du Kommunist!!1!“. Ich hoffe natürlich, dass meine Befürchtungen übertrieben sind und OpenSource legal bleibt. Im Folgenden will ich jedoch erläutern, warum ich glaube, dass die EU-Kommission und das Landgericht Hamburg zur Zeit zu den Totengräbern der quelloffenen Software werden könnten.
Beginnen möchte ich mit einer Entscheidung, die die EU-Kommission demnächst treffen wird. Die einzige Quelle hierzu ist zur Zeit die „Financial Times“, die behauptet Quellen zu haben, wonach die EU die Rechtsmäßigkeit von Android prüft. Wahrscheinlich geht es um eine Kartellbeschwerde einer Organisation namens „Fair Search Europe“.
Bei dem klangvollen Namen „Fair Search“ und der zugehörige Webseite, lässt sich diese Organisation leicht für eine Bürgerrechtsbewegung halten, die das edle Ziel hat, Google fairer zu machen. Die Organisation folgt jedoch dem bewährten Prinzip einen von der Wirtschaft finanzierten Lobbyverband als Bewegung von Bürgern erscheinen zu lassen.
Hinter der genannten Organisation stehen Firmen wie Orcale, Microsoft und Nokia. Nicht nur Verschwörungstheoretiker würden annehmen, dass besagte Firmen hier nicht einfach aus edlen Motiven heraus handeln, sondern slichtweg eine konkurrierendes Mobilbetriebssystem ausschalten wollen.
Interessanter als die Herkunft der Kartellbeschwerde ist das benutzte Argument: Die Firmen beklagen sich, dass Google Android missbraucht, um eigene Dienste (Suchmaschine, Videoplattform, Navigationsdienst …) prominent zu platzieren und zu bewerben. Dies ist eine ähnliche Argumentation, wie sie schon mehrfach gegen Microsoft verwendet wurde, weil etwa „MSN“ oder der „Internet Explorer“ zu eng mit dem sog. Betriebssystem „Windows“ verwoben waren und dadurch beworben wurden.
Anders als Windows ist Android jedoch vorwiegend quelloffen. Daher ist es letztlich die Entscheidung des Herstellers des Mobilgerätes, ob die Dienste des Konzerns aus Mountainview aktiv beworben werden. Ganz böse Zungen würden sogar behaupten, dass viele Hersteller bewusst auf die Dienste von Google setzten, da Kunden genau dies erwarten und verwenden wollen.
Da nun offenbar nicht der Microsoft-Fall vorliegt, betont „Fair Search Europe“ einen weiteren Punkt: Google bietet Android „zu marktunüblichen Preisen“ an.
Wenn jetzt tatsächlich festgestellt wird, dass das kostenlose Verteilen von Android ein Handel zu „marktunüblichen Preisen“ darstellt, dann wäre dies durchaus eine Gefahr für OpenSource an sich.
Würde Google nun den Android Quelltext komplett verschlossen halten und manchen Herstellern Android als ausführbares Programm zur undurchsichtigen Bedingungen verteilen, wie es etwa bei Freeware der Fall ist, fände ich dies durchaus bedenklich. OpenSource grenzt sich in meinen Augen jedoch in zwei Punkten von Freeware ab:
Zum Einen lässt sich der Entwicklungsaufwand bei OpenSource dramatisch durch die Verwendung von vorhandenem und von der Gemeinschafte beigetragenem Quelltext enorm reduzieren. Im Extremfall stellt der Anbieter von quelloffene Software nur vorhandene Projekte mit wenig Aufwand zusammen, weswegen von einer Abgabe unter Wert gar nicht gesprochen werden kann. (Sofern der Wert der Arbeitsaufwand des Anbieters ist)
Zum Anderen wird bei OpenSource gar nicht der Quelltext oder das Programm verkauft sondern Dienstleistungen zu der Software. Das wäre etwa so, als würde „Fair Bratwurst Europe“ einen Bratwurststand verklagen, der Senf zu einem marktunüblichen Preis von 0€ zur Bratwurst „verkauft“ .
Zunächst klingt das Urteil (LG Hambug, Az.: 310 O 144/13) relativ unspektakulär: Eine quelloffene Downloadverwaltung bietet an mit RTMPE „geschützte“ Videos von einer Plattform von ProSiebenSat1 zu sichern, ProSiebenSat1 klagt dagegen und gewinnt vor dem Landgericht Hamburg. Spannend wird das ganze bei Betrachtung der Details:
Beanstandet wurde eine Entwicklerversion. Der fragliche Quelltext wurde aus der Gemeinschaft eingesandt. Der Quelltext wurde gelöscht und hat es nie in eine finale Version geschafft. Dennoch soll die Firma, die das OpenSource-Projekt betreut haftbar gemacht werden..
Warum ist es nun bedenklich, wenn das Projekt haftbar gemacht wird für fremde Quelltexte, die gleich nach Bekanntwerden gelöscht wurden? Das Problem ist hierbei die Funktionsweise solcher Projekte: Beliebige Entwickler schlagen Quelltet vor; dieser wird präsentiert, geändert und letztendlich angenommen oder abgelehnt. Ist nun der Betreuer des Projekts haftbar für (gelöschte) Zwischenversionen, so führt das dazu, dass der Quelltext im Geheimen eingereicht werden und rechtlich geprüft werden muss, bevor überhaupt öffentlich zur Diskussion gestellt werden. Dies würde sowohl den Entwicklungsprozess verlangsamen als auch die Hemmschwelle für neue Beteiligungen anheben.