Die Beweiskette steht

Im Internet werden hochsensible und vertrauliche Daten ausgetauscht. Am Zentrum für digitales Vertrauen an der ETH Zürich entwickeln Informatiker Sicherheitssysteme, denen man hundertprozentig vertrauen kann. Nun ist ihnen bei der Verifikation ein Durchbruch gelungen.

Digitale Technologie prägt unser Leben: Wir suchen im Internet nach Informationen. Wir pflegen Kontakte über E-Mail-Programme, Social-Media­-Plattformen und Nachrichtendienste. Wir bezahlen per Kreditkarte und wickeln Bankgeschäfte am Smartphone ab. Wie aber wissen wir, mit wem wir es bei solchen «Begegnungen» im digitalen Raum zu tun haben? Das ist die Frage, um die sich alles dreht im Zentrum für digitales Vertrauen an der ETH Zürich und der Universität Bonn.

«In der realen Welt sehen wir unser Gegenüber und können beispielsweise nach einem Ausweis fragen», sagt David Basin, der das von der Werner Siemens-Stiftung unterstützte Projekt gemeinsam mit seinen ETH-Kollegen Peter Müller und Adrian Perrig sowie Matthew Smith von der Universität Bonn leitet. Im Internet ist das schwieriger – hier werden Datenpakete in Form von Bits ausgetauscht.

Um die Echtheit und die Verlässlichkeit eines Absenders oder einer Webseite zu gewährleisten, setzen Informatikerinnen und Informatiker sogenannte Protokolle ein. Dabei handelt es sich um Handlungsanweisungen, die zwischen Computern, Netzwerken oder digitalen Prozessen ablaufen. «Ein kryptographisches Protokoll namens TLS sorgt beispielsweise beim E-Banking dafür, dass der Kunde oder die Kundin sicher sein kann, mit seiner oder ihrer Bank zu kommunizieren, und die Daten während der Übertragung nicht gelesen oder manipuliert werden können», erklärt David Basin.

Den Schwachstellen auf der Spur

Trotzdem werden immer wieder Systeme gehackt und Daten gestohlen. Die Forschenden am Zentrum für digitales Vertrauen arbeiten deshalb an Techniken, die künftig völlig sichere Protokolle ermöglichen. Solche Protokolle müssen nicht nur geschrieben werden, sondern es muss auch garantiert werden, dass sie keine Schwachstellen enthalten, die ein Angreifer ausnutzen könnte. «Es gibt zwei Hauptgründe, die solche Systeme angreifbar machen: technisches Versagen und menschliches Versagen», sagt Peter Müller.

Während Matthew Smith die menschliche Komponente erforscht, kümmern sich David Basin und Peter Müller darum, technische Probleme auszuschliessen. Sie benutzen dazu eine Technik namens Verifikation. Sie führen dabei automatisiert mathematische Beweise, dass eine Software die vom Entwickler vorgesehenen Eigenschaften besitzt – etwa vor Angriffen geschützt ist. «Man definiert die Menge aller möglichen Abläufe, wie zwei Parteien ein Protokoll ausführen und ein Dritter – ein Angreifer – eingreifen könnte», sagt David Basin. Diese Formalisierung, die sogenannte Semantik, erlaubt anschliessend eine mathematische Prüfung.

Schnittstelle gleich Schwachstelle

Verifikation ist aufwändig. Denn nicht nur das Protokoll selbst kann Mängel aufweisen. Fehler passieren auch, wenn ein Protokoll mittels eines Programmcodes in eine Software eingebaut wird. «Bei dieser Implementierung können Dinge vergessen gehen oder es tauchen Probleme auf, die im Protokoll selbst gar keine Rolle spielten», sagt Peter Müller. «Deshalb verifizieren wir sowohl das Protokoll als auch die Implementierung.»

Die Schnittstelle zwischen diesen beiden Schritten sei seit jeher eine Schwachstelle in der Beweisführung, dass ein Protokoll hundertprozentig korrekt ablaufe, sagt er. «An dieser Stelle gibt es bisher keine Werkzeuge, welche die Beweise überprüfen. Es waren bisher stets Menschen, die beurteilen, ob die Protokoll- und Implementierungsebene fehlerfrei ineinander übergehen – das ist fehleranfällig.»

In langwieriger Arbeit haben es die beiden Forscher und ihre Gruppen nun aber geschafft, diese beiden Ebenen mit mathematischen Beschreibungen so eng zu verknüpfen, dass diese Schwachstelle im Verifikationsbeweis vollständig eliminiert ist. «Das ist ein Durchbruch», freut sich David Basin. Und Peter Müller ergänzt: «Forschende arbeiten seit 60 Jahren an der Verifikation von Code und seit 30 Jahren an der Verifikation von Protokollen. Aber niemand hat es vor uns geschafft, die Verifikation von Protokollen und leistungsfähigen Implementierungen derart eng zu verknüpfen.»

Fehlerfrei ist nicht genug

Die Verknüpfung bedeutet faktisch eine End-zu-End-Verifikation – in der ganzen Abfolge vom Protokoll bis zum Code gibt es keinen einzigen Schritt mehr, der nicht von einem Werkzeug geprüft wurde. Trotzdem gibt es noch viel Arbeit in dem Projekt. Zum einen gelte es, die Verifikationen weiter zu automatisieren und für komplexere Implementierungen anzupassen, sagt Peter Müller.

Zum anderen ist es zwar essenziell, künftig mit den neuen Verifikationsmethoden ausschliessen zu können, dass Fehler in Protokoll und Code auftreten. «Aber Fehlerfreiheit reicht nicht», sagt David Basin. «Anwender müssen solche Sicherheitssysteme auch verstehen und ihnen vertrauen.» Wie man dieses Vertrauen gewinnt, ist deshalb die andere zentrale Frage, der die Forschenden in Zukunft nachgehen werden.