Informatiker können mit der gleichen Sicherheit beweisen, dass das Programm keine Fehler enthält, wie Mathematiker Theoreme beweisen können. Diese Fortschritte werden verwendet, um die Sicherheit in einer Vielzahl von Bereichen zu verbessern, von Drohnen bis zum Internet.

Im Frühjahr 2015 versuchte ein Team von Hackern, in einen unbemannten Militärhubschrauber namens Little Bird ("Bird") einzubrechen. Der Hubschrauber befand sich ähnlich wie die bemannte Version des Lieblingsflugzeugs der US-Spezialeinheiten in Boeing in Arizona. Die Hacker hatten einen Vorsprung: Zu Beginn ihrer Arbeit hatten sie Zugriff auf eines der Subsysteme des Steuercomputers. Sie konnten nur den Hauptflugcomputer an Bord hacken und die Kontrolle über das UAV erlangen.

Zu Beginn des Projekts konnte das Hackerteam des Roten Teams ein Hubschraubersystem fast so einfach knacken wie Ihr WLAN zu Hause. In den folgenden Monaten implementierten die DARPA-Ingenieure einen neuen Sicherheitsmechanismus, ein Softwaresystem, das keiner erzwungenen Enteignung unterliegt. Die Schlüsselparameter des Little Bird-Systems können mit vorhandenen Technologien nicht geknackt werden, und sein Code kann als mathematischer Beweis herangezogen werden. Und obwohl das Team sechs Wochen lang Zugang zum UAV hatte und der Zugang zum Computersystem die Zugangsmöglichkeiten eines echten Hackerteams überstieg, konnten sie die Verteidigung des Vogels nicht knacken.

"Sie konnten den Betrieb nicht knacken oder stören", sagt Kathleen Fisher, Professor für Informatik an der Tufts University und Projektmanager für hochsichere Cyber-Militärsysteme (HACMS). "Infolgedessen standen DARPA-Vertreter auf und sagten: Meine Güte, Sie können diese Technologie tatsächlich in wichtigen Systemen einsetzen."

Technologie gegen Hacker ist ein Programmierstil, der als formale Bestätigung bezeichnet wird . Im Gegensatz zu gewöhnlichem Code, der informell geschrieben und normalerweise nur anhand seiner Leistung bewertet wird, sieht formal verifizierte Software wie ein mathematischer Beweis aus: Jede Aussage folgt logisch der vorherigen. Das gesamte Programm kann mit der gleichen Sicherheit wie ein mathematischer Satz verifiziert werden.

„Sie schreiben eine mathematische Formel, die das Verhalten eines Programms beschreibt, und verwenden ein Proof-of-Concept-Tool, das die Gültigkeit dieser Aussage testet“, sagt Brian Parno , Forscher für formale Forschung und Sicherheit bei Microsoft Research.

Der Wunsch, formal bestätigte Programme zu erstellen, bestand fast so lange wie das Gebiet der Informatik. Und dies blieb lange Zeit unmöglich, aber die Erfolge der letzten zehn Jahre auf dem Gebiet der „formalen Methoden“ haben diesen Ansatz der konventionellen Praxis näher gebracht. Heute wird die formelle Bestätigung von Software in finanzierten akademischen Gruppen, in US-Militärprojekten und in Technologieunternehmen wie Microsoft und Amazon untersucht.

Das Interesse wächst zusammen mit einer Zunahme der Anzahl wichtiger Aufgaben, die online erledigt werden. Wenn Computer zu Hause und im Büro isoliert existierten, waren Programmierfehler nur ein Ärgernis. Jetzt öffnen sie Sicherheitslücken an Computern im Netzwerk, sodass alle sachkundigen Personen in Computersysteme eindringen können.

"Im 20. Jahrhundert, als ein Programm einen Fehler hatte, war es schlimm, es konnte fallen, Gott segne sie", sagte Andrew Appel , Professor für Informatik an der Princeton University und führend in der Programmvalidierung. Aber im 21. Jahrhundert kann ein Fehler Hackern die Möglichkeit eröffnen, die Kontrolle über das Programm zu erlangen und Ihre Daten zu stehlen. Aufgrund eines erträglichen Fehlers ist es zu einer Sicherheitslücke geworden, die viel schlimmer ist “, sagt er.

Kathleen Fisher

Träume von perfekten Programmen

Im Oktober 1973 kam Edsger Dijkstra auf die Idee, fehlerfreien Code zu erstellen. Nachts, während er in einem Hotel auf einer Konferenz war, dachte er plötzlich darüber nach, wie man das Programmieren mathematischer gestalten könnte. Später erklärte er die Idee und sagte: "Mit aufgeregtem Verstand stand ich um 2:30 Uhr morgens auf und schrieb mehr als eine Stunde lang." Dieses Material war der Beginn seines fruchtbaren 1976 erschienenen Buches The Discipline of Programming, das zusammen mit der Arbeit von Charles Hoare (wie Dijkstra, der den Turing-Preis erhielt ) Ansichten zur Verwendung von Korrektheitsnachweisen beim Schreiben von Programmen definierte.

Die Informatik folgte dieser Idee jedoch nicht, hauptsächlich weil es viele Jahre lang unpraktisch oder sogar unmöglich schien, die Funktion eines Programms anhand der Regeln der formalen Logik zu bestimmen.

Eine formale Definition ist eine Möglichkeit zu bestimmen, was ein Programm speziell tut. Eine formale Bestätigung ist ein Weg, um ohne Zweifel zu beweisen, dass der Programmcode perfekt zu dieser Definition passt. Stellen Sie sich vor, Sie schreiben ein Programm für ein Robomobil, das Sie zu einem Lebensmittelgeschäft bringt. Auf der Ebene der Operationen bestimmen Sie die Bewegungen, die das Robomobil ausführen muss, um das Ziel zu erreichen - es kann sich am Anfang und Ende des Pfades drehen, verlangsamen oder beschleunigen, ein- oder ausschalten. Ihr Programm besteht aus diesen grundlegenden Vorgängen, die in der richtigen Reihenfolge angeordnet sind, sodass Sie am Ende zum Geschäft und nicht zum Flughafen kommen.

Der traditionelle Weg, um den Zustand eines Programms zu testen, ist das Testen. Programmierer geben dem Programm viele Eingabedaten (Unit-Tests), um sicherzustellen, dass es sich so verhält, wie es sollte. Wenn Ihr Programm einen Algorithmus für die Bewegung eines Robomobils definiert, können Sie dessen Fahrten zwischen vielen verschiedenen Punkten testen. Solche Tests stellen in den meisten Fällen den korrekten Betrieb von Programmen sicher, was für die meisten Anwendungen ausreichend ist. Unit-Tests garantieren jedoch nicht, dass die Software immer korrekt funktioniert - Sie können das Programm nicht mit allen möglichen Eingabedaten vergleichen. Selbst wenn der Algorithmus für alle Ziele funktioniert, besteht immer die Möglichkeit, dass er sich unter seltenen Bedingungen - oder, wie sie sagen, unter „Randbedingungen“ - anders verhält und eine Sicherheitslücke öffnet. In realen Programmen können solche Fehler einfach sein, z. B. Pufferüberläufe,Dabei kopiert das Programm etwas mehr Daten als erforderlich und überschreibt einen Teil des Computerspeichers. Dieser scheinbar harmlose Fehler ist schwer zu beseitigen und bietet ein Loch für einen Hackerangriff - ein schwaches Türscharnier, das den Weg zum Schloss öffnet.

„Irgendwo in der Software ein Loch, und das ist eine Sicherheitslücke. Es ist sehr schwierig, alle Pfade auf mögliche Eingaben zu überprüfen “, sagt Parno.

Diese Spezifikationen sind komplizierter als ein Ausflug in den Laden. Programmierer benötigen beispielsweise möglicherweise ein Programm, das das Datum des Eingangs von Dokumenten in der Reihenfolge ihres Eingangs notariell beglaubigt und anbringt. In diesem Fall sollte die Spezifikation anzeigen, dass der Zähler immer größer wird und dass das Programm niemals zulassen sollte, dass der zum Signieren verwendete Schlüssel leckt.

In der menschlichen Sprache ist dies leicht zu beschreiben. Es ist viel schwieriger, eine Spezifikation in eine formale Sprache umzuwandeln, die ein Computer versteht - was das Hauptproblem beim Schreiben von Programmen erklärt.

„Die Erstellung einer formalen Spezifikation, die für einen Computer verständlich ist, ist im Wesentlichen schwierig“, sagt Parno. "Auf der obersten Ebene ist es einfach zu sagen, dass das Passwort nicht auslaufen darf, aber Sie müssen darüber nachdenken, wie Sie daraus eine mathematische Definition machen können."

Ein weiteres Beispiel ist ein Programm, das eine Liste von Zahlen sortiert. Ein Programmierer, der versucht, eine Spezifikation für sie zu formalisieren, kann sich Folgendes einfallen lassen:

Stellen Sie für jedes Element j in der Liste sicher, dass j ≤ j + 1 ist

Aber auch in dieser formalen Spezifikation - um sicherzustellen, dass jedes Element in der Liste kleiner oder gleich dem nächsten ist - liegt ein Fehler vor. Der Programmierer geht davon aus, dass die Ausgabe die geänderte Eingabe enthält. Wenn die Liste [7, 3, 5] lautet, erwartet er, dass das Programm [3, 5, 7] zurückgibt. Die Ausgabe des Programms [1, 2] entspricht jedoch den Spezifikationen - denn „es handelt sich auch um eine sortierte Liste, aber nicht um die Liste, die Sie wahrscheinlich erwartet haben“, sagt Parno.

Mit anderen Worten, es ist schwierig, die Idee, was ein Programm tun soll, in eine formale Spezifikation umzuwandeln, die eine falsche Interpretation dessen, was Sie vom Programm erwarten, ausschließt. Das angegebene Beispiel beschreibt das einfachste Sortierprogramm. Stellen Sie sich nun eine Beschreibung von etwas viel Abstrakterem vor, wie zum Beispiel den Passwortschutz. „Was bedeutet das mathematisch? Für eine solche Definition kann es erforderlich sein, eine mathematische Beschreibung dessen zu schreiben, was es bedeutet, „ein Geheimnis zu bewahren“ oder was es bedeutet, dass der Verschlüsselungsalgorithmus sicher ist “, sagt Parno. "Wir haben all diese Probleme berücksichtigt und in ihrer Studie Fortschritte gemacht, aber ihre Implementierung kann äußerst schwierig sein."

Blockieren Sie die Sicherheit

Tatsächlich müssen sowohl Spezifikationen als auch zusätzliche Kommentare geschrieben werden, damit die Software Schlussfolgerungen über den Code ziehen kann. Ein Programm, einschließlich seiner formalen Bestätigung, kann fünfmal so groß sein wie ein reguläres Programm, das für denselben Zweck geschrieben wurde.

Diese Belastung kann mit geeigneten Tools - Programmiersprachen und Hilfsprogrammen, mit denen Programmierer kugelsichere Programme erstellen können - ein wenig verringert werden. Aber in den 1970er Jahren existierten sie nicht. „Viele Aspekte von Wissenschaft und Technologie sind damals nicht genug gewachsen, und in den 1980er Jahren hatten viele Bereiche der Informatik das Interesse daran verloren“, sagt Appel, leitender Forscher bei DeepSpec, einer formal validierten Computersystemgruppe.

Trotz der Verbesserung der Tools trat ein weiteres Hindernis bei der Bestätigung der Programme auf: Es gab keine Gewissheit, dass dies überhaupt erforderlich war. Obwohl Enthusiasten der Methode sagten, dass kleine Fehler zu großen Problemen führen können, machte der Rest auf die Tatsache aufmerksam, dass Computerprogramme im Grunde recht gut funktionieren. Manchmal stürzen sie ab, ja - aber ein wenig nicht gespeicherte Daten zu verlieren oder manchmal das System neu zu starten, scheint ein kleiner Preis zu sein, wenn man nicht jedes Programm sorgfältig in die Sprache der formalen Logik übersetzen muss. Im Laufe der Zeit begannen sogar diejenigen, die am Anfang der Programmbestätigung standen, an deren Vorteilen zu zweifeln. In den neunziger Jahren räumte sogar Hoar ein, dass Spezifikationen eine zeitaufwändige Lösung für ein nicht existierendes Problem sein könnten. 1995 schrieb er:

( ) , … , , .

Dann kam das Internet, das das Gleiche für Fehler im Code tat, die Flugreisen für Infektionen taten: Wenn alle Computer miteinander verbunden sind, können unangenehme, aber tolerante Fehler zu wachsenden Sicherheitsproblemen führen.

"Wir haben es nicht ganz verstanden", sagt Appel. "Es gibt Programme, die allen Internet-Hackern offen stehen, und wenn ein Fehler in einem solchen Programm vorliegt, kann dies zu einer Sicherheitslücke werden."

Als die Forscher begannen, die Schwere der Sicherheitsbedrohungen durch das Internet zu verstehen, stand die Programmbestätigung kurz vor der Rückkehr. Zunächst haben die Forscher Fortschritte in den grundlegenden Teilen formaler Methoden erzielt. Dies ist eine Verbesserung bei Nebenprogrammen wie Coq und Isabelle. Entwicklung logischer Systeme ( Theorie abhängiger Typen) Bereitstellung einer Entwicklungsplattform, die Computern hilft, Code zu bewerten; „Operative Semantik“ ist eine Sprache, die die richtigen Wörter enthält, um die Anforderungen des Programms auszudrücken.

„Beginnend mit der Spezifikation in der menschlichen Sprache sind Sie auf Unklarheiten gestoßen“, sagt Janette Wing , Vizepräsidentin von Microsoft Research. - Jede natürliche Sprache enthält Mehrdeutigkeiten. In der formalen Spezifikation schreiben Sie eine genaue Beschreibung auf der Grundlage der Mathematik auf, um zu erklären, was Sie vom Programm erwarten. “

Janette Wing von Microsoft Research

Darüber hinaus haben formale Methodenforscher ihre Ziele neu definiert. In den 1970er und 1980er Jahren wollten sie vollständig getestete Computersysteme entwickeln, von elektronischen Schaltkreisen bis hin zu Programmen. Heutzutage arbeiten die meisten Forscher an kleinen, aber kritischsten oder anfälligsten Teilen von Systemen - zum Beispiel Betriebssystemen oder kryptografischen Protokollen.

"Wir sagen nicht, dass wir beweisen werden, dass das gesamte System zu 100% korrekt ist, bis hin zu elektronischen Schaltkreisen", sagt Wing. - Solche Aussagen sind lächerlich. Wir sind genau in dem, was wir können oder nicht können. “

Das HACMS-Projekt zeigt, wie Sie große Sicherheitsgarantien erzielen können, indem Sie einen kleinen Teil eines Computersystems beschreiben. Das erste Ziel des Projekts war es, einen unzerbrechlichen Quadrocopter für Unterhaltung zu schaffen. Die mit dem Quadric gelieferte Software war monolithisch - das heißt, durch den Zugriff auf einen Teil davon erhielt der Hacker Zugriff auf alle anderen. Seit zwei Jahren teilt das HACMS-Team den Code im Steuercomputer in Teile.

Das Team hat die Softwarearchitektur mit den von Fisher als „Bausteine mit hohem Vertrauen“ bezeichneten Tools neu geschrieben - Tools, mit denen ein Programmierer die Reinheit des Codes nachweisen kann. Einer von ihnen liefert Beweise dafür, dass es nach dem Zugriff auf eine der Einheiten nicht möglich ist, Privilegien zu eskalieren, um die anderen zu erreichen.

Später installierten Programmierer eine solche Software auf dem „Bird“. Im Test mit dem Roten Team erhielt sie Zugang zu einem der Teile des Systems, die einen Teil des Hubschraubers steuerten, zum Beispiel die Kamera - aber nicht zu den Hauptfunktionen. Das Versagen der Hacker war mathematisch garantiert. "Sie haben auf maschinenprüfbare Weise bewiesen, dass Hacker nicht über die Systempartition hinausgehen können. Das ist also nicht überraschend", sagt Fisher. "Dies steht im Einklang mit dem Satz, aber es ist immer nützlich, einen Test durchzuführen."

Im Jahr nach dem Audit wandte DARPA die Werkzeuge und Technologien des Projekts auf andere Bereiche der Militärtechnologie an, beispielsweise Satelliten und automatische Lastwagen. Neue Initiativen fallen mit der Verbreitung der formellen Bestätigung in den letzten zehn Jahren zusammen: Jedes erfolgreiche Projekt fördert das nächste. "Ausreden über die Komplexität dieses Prinzips funktionieren nicht mehr", sagt Fisher.

Überprüfen Sie das Internet

Sicherheit und Zuverlässigkeit sind zwei der Hauptziele, die formale Methoden inspirieren. Mit jedem Tag wird der Verbesserungsbedarf immer offensichtlicher. Im Jahr 2014 eröffnete ein kleiner Softwarefehler, den eine formale Beschreibung auffangen würde, den Weg für einen Heartbleed- Fehler , der das Internet zu brechen drohte. Ein Jahr später bestätigten einige „legale“ Hacker die schlimmsten Befürchtungen hinsichtlich mit dem Internet verbundener Autos und erlangten die Fernsteuerung über den Jeep Cherokee .

Mit höheren Raten setzen sich formale Methodenforscher zunehmend ehrgeizige Ziele. Das DeepSpec-Team unter der Leitung von Appel (das ebenfalls an HACMS arbeitet) versucht, ein so komplexes, vollständig getestetes System wie einen Webserver aufzubauen. Bei Erfolg wird das Projekt, das von der State Science Foundation einen Zuschuss von 10 Millionen US-Dollar erhalten hat, viele kleinere erfolgreiche Projekte des letzten Jahrzehnts zusammenbringen. Forscher haben mehrere bewährte sichere Komponenten wie den Kernel des Betriebssystems erstellt. „Bisher wurde die Integration dieser Komponenten in spezifikationsspezifische Schnittstellen nicht durchgeführt“, sagt Appel.

Bei Microsoft Research haben Programmierer zwei ehrgeizige Projekte. Der erste, Everest, zielt darauf ab, eine validierte Version von HTTPS zu erstellen, einem Protokoll zur Sicherung von Webbrowsern, das Wing als "Achillesferse des Internets" bezeichnet.

Die zweite ist die Erstellung bestätigter Spezifikationen für komplexe cyber-physische Systeme wie UAVs. Das Projekt hat erhebliche Schwierigkeiten. Während herkömmliche Programme mit separaten, eindeutigen Schritten arbeiten, verwenden Drohnensteuerungsprogramme maschinelles Lernen, um probabilistische Entscheidungen auf der Grundlage eines kontinuierlichen Stroms von Umweltdaten zu treffen. Es ist alles andere als offensichtlich, wie logische Entscheidungen mit einem solchen Grad an Ungenauigkeit getroffen oder als formale Spezifikation beschrieben werden können. Aber erst in den letzten zehn Jahren sind die formalen Methoden ziemlich weit fortgeschritten, und Wing, der das Projekt verwaltet, glaubt optimistisch, dass die Forscher all diese Probleme lösen können.

Es ist ungebrochener Code vorhanden

Träume von perfekten Programmen

Blockieren Sie die Sicherheit

Überprüfen Sie das Internet

More articles: