Mit DARPA: Sicherheitslücken risikofrei offenlegen

Die Offenlegung von Software-Schwachstellen ist heute oft mit Herausforderungen verbunden. Wenn es darum geht, entdeckte Bugs zu melden oder zu teilen, stehen Cybersecurity-Forscher und Software-Sicherheitsanalysten vor einem Dilemma zwischen Ethik und Effektivität. Einerseits kann die Offenlegung einer Schwachstelle die Aufmerksamkeit der Softwareentwickler erregen und eine zeitnahe Reaktion motivieren. Doch sie kann auch dazu führen, dass gegen den Forscher geklagt wird. Die öffentliche Bekanntgabe kann es böswilligen Akteuren zudem ermöglichen, die Entdeckung auszunutzen – bevor ein Patch oder eine Korrektur angewendet werden kann.

Mit anderen Worten: Für Cybersicherheitsforscher ist es eine große Herausforderung, Schwachstellen offenzulegen, ohne böswilligen Akteuren den Weg zu ebnen. Ganz besonders, wenn die Forscher sich verpflichtet fühlen, die Entdeckung von Fehlern in Fremdsoftware öffentlich zu melden, dabei jedoch nicht wollen, dass diese Informationen zu einer Waffe in den Händen von Cyberkriminellen werden.

Heutzutage kostet eine Verzögerung bei der Freigabe von Patches Millionen oder Milliarden von Dollar. Diese Verzögerung kann sogar Regierungsbehörden und den privaten Sektor von Ländern von der Größe der USA gefährden, wie es im Fall SolarWinds geschah. Daher ist es unerlässlich, Softwareentwickler dazu zu bringen, angesichts des öffentlichen Drucks Korrekturmaßnahmen zu ergreifen – und das, ohne das Risiko krimineller Aktivitäten zu erhöhen. Denn Kriminelle sind in der Lage, die offengelegten Fehler für Systemeinbrüche und Diebstahl wichtiger Daten auszunutzen.

An dieser Schaltzentrale arbeitet das Programm SIEVE (Securing Information for Encrypted Verification and Evaluation) der DARPA, der Forschungsagentur des US-Verteidigungsministeriums. Das Projekt erforscht Lösungsmöglichkeiten durch den Einsatz von so genannten Zero-Knowledge-Proofs (ZKPs) bei der Offenlegung von Sicherheitslücken.

Das Konzept ist nicht ganz neu, denn es basiert auf kryptographischen Methoden. ZKPs sind mathematisch überprüfbare Problemaussagen, die verwendet werden können, um Software oder Systeme logisch zu durchdenken. Die Beweise (Proofs) können öffentlich verwendet werden, ohne dass vertrauliche Informationen preisgegeben werden. Im Falle der Offenlegung von Schwachstellen würde dies Softwareentwicklern erlauben, die Existenz von Schwachstellen zu beweisen, ohne z.B. eine Roadmap preisgeben zu müssen, die in ungeeigneten Händen unkalkulierbaren Schaden anrichten würde.

Nach Angaben des DARPA-Projektleiters lag der Schwerpunkt der Anwendung von ZKPs vor SIEVE in der Maximierung der Geschwindigkeit der Kommunikation und der Beweisverifizierung. Neben dem Einsatz im Verteidigungsministerium selbst erfordern beispielsweise Kryptowährungs- und Blockchain-Anwendungen die Effizienz von Kommunikation und Verifikation.

Innerhalb eines Jahres haben zwei Teams des SIEVE-Programms bereits beispiellos demonstriert, dass es möglich ist, die Existenz von Schwachstellen mathematisch zu beweisen. Und das, ohne entscheidende Details der Fehler oder die Art und Weise, wie sie ausgenutzt werden können, preiszugeben. Eines der Teams, unter der Leitung von Galois, berichtete über eine Speicher-Sicherheitslücke, die im Game Boy Advance-Gerät gefunden wurde. Das Team kombinierte verschiedene Protokolle und Programmanalysen, um die Behauptungen des ZKP zu bewerten.

Speicher-Sicherheitslücken sind eine kritische Klasse von Schwachstellen, die häufig in moderner Software auftreten. In der von Galois geleiteten Demonstration war ein Schwachstellenforscher in der Lage, eine andere Partei in etwa acht Minuten interaktiv von der Existenz der spezifischen Schwachstelle zu überzeugen.

Das zweite Team von Trail of Bits-Forschern arbeitet daran, Schwachstellen auf der Ebene der Systemarchitektur zu modellieren – auf einer niedrigeren Abstraktionsebene als Galois also. Ihre erste Arbeit hat eine Möglichkeit geschaffen, reale Befehlssatzarchitekturen als boolesche Schaltungen – oder mathematische Modelle digitaler Logikschaltungen – darzustellen. Diese sind zudem mit ZKPs kompatibel, sodass Benutzer ihre Fähigkeit demonstrieren können, eine öffentliche Binärdatei in einen bestimmten bösartigen Zustand zu zwingen.

Die erste Arbeit des Teams benutzte den MSP430-Mikrocontroller, einen Mikroprozessor, der häufig in eingebetteten Systemen verwendet wird. Von dort aus fanden sie einen Weg, um eine Vielzahl gängiger Schwachstellen mathematisch darzustellen. So konnten ZKPs entwickelt werden, um die Existenz dieser Schwachstellen zu beweisen. Die Größe der ZKP-Anweisungen reichte von 86 MB bis 1,1 GB. Nun möchte das Team die Liste der Architekturen und Ausführungsumgebungen, mit denen es arbeiten kann, erweitern. Das Ziel ist es, einen Großteil der gängigen x86-Architektur einzubeziehen. Beispielsweise planen sie, ZKPs von Binärdateien aus der Cyber Grand Challenge 2016 der DARPA zu erstellen, die auf DECREE läuft ¬– einem einfachen Betriebssystem, das auf x86 basiert.

Für die DARPA-Forscher besteht das größte Hindernis für eine breitere Anwendung dieser Methode darin, einen Weg zu finden, sie in eine leicht verständliche Sprache zu übersetzen. Schließlich ist es sinnlos, präzise Beweise zu präsentieren, wenn diejenigen, die sie erhalten, nicht in der Lage sind, sie so weit zu entschlüsseln, dass sie überzeugt sind.

So funktioniert es

Zur Veranschaulichung, wie die ZKP-Methode funktioniert, dient dieses Beispiel: Es gibt eine Höhle und zwei Charaktere, A und B. Sie stehen beide vor einer Höhle, die zwei verschiedene Eingänge (1 und 2) zu zwei getrennten Pfaden hat. Im Inneren der Höhle gibt es eine Verbindung zwischen den Wegen, die nur mit einem Geheimcode geöffnet werden kann. Charakter B ist derjenige, der diesen Code hat, und Charakter A möchte sicherstellen, dass B nicht lügt.

Wie kann B beweisen, dass er den Code hat, ohne dessen Inhalt zu verraten? Die Lösung ist, dass Charakter A vor der Höhle wartet und B durch einen beliebigen Eingang (1 oder 2) vordringt. Dann, vor der Höhle, bittet Charakter A Charakter B, die Höhle auf dem anderen Weg zu verlassen. Im Besitz des Geheimcodes kann B dies ohne Probleme tun. Somit hat er den Beweis erbracht.