Mehr Sicherheit durch formale Methoden

Kryptografie ist ein Grundpfeiler der sicheren Kommunikation in der IT-Gesellschaft. Kryptografische Verfahren wie Verschlüsselung und Signaturen sorgen dafür, dass E-Mails und Messages sicher von Sender zu Empfänger gelangen oder dass Bitcoin nicht unrechtmässig den Besitzer wechseln. Die Verfahren erfordern jedoch oft Zufallszahlen von hoher Güte. Diese werden in der Regel von Pseudozufalls-generatoren (Pseudo-random Number Generators, PRNGs) erzeugt. Allerdings ist es sehr leicht, beim Implementieren von PRNGs Fehler zu machen. Als Qualitätssicherungsmaßnahme ist außerdem meistens nur manuelle Code-Inspektion etabliert.

Felix Dörre, Masterstudent in Informatik am KIT, hat bereits in seiner Bachelorarbeit ein logikbasiertes Verfahren entwickelt, welches automatisiert viele Fehler in PRNGs aufspüren kann. Dieses Verfahren hat er gemeinsam mit Vladimir Klebanov, einem wissen-
schaftlichen Mitarbeiter der Forschungsgruppe Anwendungsorientierte Formale Verifikation, in die Praxis umgesetzt. Das Software-Tool, welches dabei entstanden ist, heißt „Entroposcope“ und baut auf Techniken der formalen Verifikation auf.

Nach ersten Tests der neuen Software konnten bereits einige Fehler in etablierten Kryptobibliotheken ermittelt werden. So wurde zum Beispiel im August ein kritischer Fehler in Libgcrypt, der Kryptobibliothek hinter u.a. der Verschlüsselungssoftware GnuPG, entdeckt. „Aus den ersten 4640 Bit an Zufallszahlen lassen sich trivial die folgenden 160 Bit berechnen. Das darf nicht sein“, erklärt Vladimir Klebanov.

Inzwischen hat GnuPG auf den Bug reagiert und diesen mit einem neuen Release ausgeräumt. „Der Fehler befand sich bereits seit 18 Jahren im Code der Bibliothek und wurde auch durch mehrere externe Begutachtungen nicht entdeckt. Dies zeigt, dass unser System funktioniert und die Qualitätssicherung der PRNGs deutlich verbessern kann“, so Klebanov weiter. Auch an anderen Bibliotheken konnte Entroposcope bereits erfolgreich getestet und kleinere Fehler gefunden werden.

Am 26. Oktober wird die Veröffentlichung, welche die Methode und das Tool beschreibt, auf der Konferenz für „Computer and Communication Security (CCS)“ in Wien vorgestellt. Die CCS wird von der Association for Computing Machinery (ACM) veranstaltet und zählt weltweit zu den renommiertesten wissenschaftlichen Konferenzen im Bereich der IT-Sicherheit.
 

Felix Dörre stellte in Wien bereits die Ergebnisse seiner Bachelorarbeit vor.