Archiv für 2013-7

Mehr Datenschutz für den Browser

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:

Probleme und Maßnahmen

Drittanbietercookies

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.

Drittanbieteranfragen

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.

Inhalte Dritter grundsätzlich blockieren?

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.

Internetwerbung

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.

„Do-Not-Track“-Header

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.

https-Verbindungen

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

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.

• T_Σ ist die von Σ erzeugte Theorie, die genau aus den Folgerungen aus Σ besteht.
• Ist M eine Struktur, dann ist T_M (auch Th(M) ) die Theorie von M. Sie enthält genau die von M erfüllten (geschlossenen) Formeln
• Theorien, die sowohl die Formel A als auch ¬A enthalten, heißen inkonsistent
• Vollständig heißen Theorien, die (für jede geschlossene Formel A) A oder ¬A enthalten
• Eine Menge Ax, die eine Theorie Σ erzeugt, also T_Ax = Σ, ist deren Axiomensystem oder Axiomatisierung
  • Existiert ein solches Axiomensystem, heißt die Theorie axiomatisierbar
  • Ist ein solches Axiomensystem aufzählbar, heißt die Theorie aufzählbar axiomatisierbar
  • Ist ein solches Axiomensystem endlich, heißt die Theorie endlich axiomatisierbar

Ich werde nun einige Beweise über Theorien und unter Verwendung der vorgestellten Definitionen vorstellen.

Es gibt nur eine inkonsistente Theorie

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).

Theorien von Modellen sind vollständig und konsistent

Theorien von Modellen sind konsistent

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.

Theorien von Modellen sind vollständig

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.

Vollständige, aufzählbar axiomatisierbare Theorien sind entscheidbar

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.

Vollständigkeit und Konsistenz

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):

• A ∈ Σ: A, ¬A ∈ Σ ∪ {¬A} und daher ist T_{Σ ∪ {¬A}} inkonsistent
• ¬A ∈ Σ: A, ¬A ∈ Σ ∪ {A} und daher ist T_{Σ ∪ {A}} inkonsistent

Somit wurde gezeigt, dass mit jeder geschlossenen Formel A T_{Σ ∪ {A}} oder T_{Σ ∪ {¬A}} inkonsistent ist.

„⇐ “: Für jede geschlossene Formel A ist T_{Σ ∪ {A}} oder T_{Σ ∪ {¬A}} inkonsistent.

• T_{Σ ∪ {¬A}} ist inkonsistent: Σ ∪ {¬A} muss unerfüllbar sein. Nach Satz der Vorlesung gilt: Σ ⊧ A. Da Σ eine Theorie ist, A ∈ Σ
• T_{Σ ∪ {A}} ist inkonsistent: Σ ∪ {A} muss unerfüllbar sein. Nach Satz der Vorlesung gilt: Σ ⊧ ¬A. Da Σ eine Theorie ist, ¬A ∈ Σ

Somit wurde gezeigt, dass für jede geschlossene Formel A: A oder ¬A ∈ Σ. Σ ist also vollständig.

---