MIT-Kurs "Computer Systems Security". Vorlesung 10: Symbolische Ausführung, Teil 1

Massachusetts Institute of Technology. Vorlesung # 6.858. "Sicherheit von Computersystemen." Nikolai Zeldovich, James Mickens. 2014 Jahr

Computer Systems Security ist ein Kurs zur Entwicklung und Implementierung sicherer Computersysteme. Die Vorträge behandeln Bedrohungsmodelle, Angriffe, die die Sicherheit gefährden, und Sicherheitstechniken, die auf jüngsten wissenschaftlichen Arbeiten basieren. Zu den Themen gehören Betriebssystemsicherheit, Funktionen, Informationsflussmanagement, Sprachsicherheit, Netzwerkprotokolle, Hardwaresicherheit und Sicherheit von Webanwendungen.

Vorlesung 1: „Einführung: Bedrohungsmodelle“ Teil 1 / Teil 2 / Teil 3
Vorlesung 2: „Kontrolle von Hackerangriffen“ Teil 1 / Teil 2 / Teil 3
Vorlesung 3: „Pufferüberläufe: Exploits und Schutz“ Teil 1 / Teil 2 / Teil 3
Vorlesung 4: „Trennung von Privilegien“ Teil 1 / Teil 2 / Teil 3
Vorlesung 5: „Woher kommen Sicherheitssysteme?“ Teil 1 / Teil 2
Vorlesung 6: „Chancen“ Teil 1 / Teil 2 / Teil 3
Vorlesung 7: „Native Client Sandbox“ Teil 1 / Teil 2 / Teil 3
Vorlesung 8: „Netzwerksicherheitsmodell“ Teil 1 / Teil 2 / Teil 3
Vorlesung 9: „Sicherheit von Webanwendungen“ Teil 1 / Teil 2 / Teil 3
Vorlesung 10: „Symbolische Ausführung“ Teil 1 / Teil 2 / Teil 3

Guten Morgen allerseits, ich bin Armando Solar-Lesam und heute werde ich einen Vortrag über symbolische Leistung halten. Wer unter den hier Anwesenden kennt diesen Begriff oder hat schon einmal davon gehört? Ich möchte nur eine Vorstellung von unserem Publikum bekommen. Also fangen wir an. Ich habe meinen Laptop mehrmals fallen lassen, daher dauert das Laden sehr lange.



Die symbolische Ausführung ist das Arbeitstier der modernen Programmanalyse. Dies ist eine der Methoden, die aus der Forschung hervorgegangen sind und dann in vielen Anwendungen eingesetzt wurden. Zum Beispiel gibt es heute bei Microsoft ein System namens SAGE, das mit vielen wichtigen Microsoft-Programmen zusammenarbeitet, die von Power Point bis Windows selbst reichen, um Sicherheitsprobleme und Schwachstellen wirklich zu finden.

Es gibt viele akademische Projekte, die einen großen Einfluss auf die reale Welt hatten, z. B. das Erkennen wichtiger Fehler in Open Source-Software mithilfe symbolischer Ausführung. Das Schöne an der symbolischen Ausführung als Technik ist, dass Sie sich im Vergleich zum Testen vorstellen können, wie sich Ihr Programm mit einem möglicherweise endlosen Satz möglicher Eingabedaten verhält. Dies ermöglicht es uns, Arrays von Eingabedaten zu untersuchen, die völlig unpraktisch und unpraktisch wären, um sie beispielsweise durch zufällige Tests zu untersuchen, selbst wenn es eine sehr große Anzahl von Testern gibt. Andererseits hat es im Vergleich zu herkömmlichen Methoden der statischen Analyse den folgenden Vorteil. Bei der Untersuchung eines Problems kann die symbolische Ausführung Eingabe und Ablaufverfolgung erstellen, einen Ausführungspfad, der in einem realen Programm ausgeführt werden kann und dieses Programm basierend auf dieser Eingabe ausführt. Danach können wir den eigentlichen Fehler identifizieren und ihn mithilfe traditioneller Debugging-Mechanismen beheben. Dies ist besonders wertvoll, wenn Sie sich in einer industriellen Entwicklungsumgebung befinden, in der Sie wahrscheinlich nicht die Zeit haben, sich um jedes kleine Problem in Ihrem Code zu kümmern.

Zum Beispiel möchten Sie wirklich in der Lage sein, zwischen echten Problemen und falsch positiven Ergebnissen zu unterscheiden. Wie funktioniert das?

Um wirklich zu verstehen, wie dies funktioniert, ist es hilfreich, mit der normalen Ausführung zu beginnen. Wenn wir die symbolische Ausführung als eine Verallgemeinerung der traditionellen, einfachen Ausführung betrachten, ist es sinnvoll zu wissen, wie sie aussieht. Daher werde ich dieses sehr einfache Programm als Illustration für viele Dinge verwenden, über die wir heute sprechen werden.



Hier haben wir einen Auszug aus einem sehr einfachen Code aus mehreren Zweigen und die Aussage, dass dies eine falsche Aussage ist, wenn unter bestimmten Bedingungen der Wert t <x ist. Wir wollen herausfinden, ob diese Aussage jemals erhoben werden kann. Das ist möglich? Gibt es Eingaben, die dazu führen, dass diese Anweisung fehlschlägt?

Eines der Dinge, die ich tun kann, ist, die Ausführung dieses Programms anhand bestimmter Werte von Eingabedaten als Beispiel zu überprüfen. Angenommen, wir verwenden Eingaben, für die X = 4 und Y = 4. Der Wert von T ist Null, wie zu Beginn des Programms angekündigt.

Bevor wir zur normalen Ausführung kommen, wollen wir herausfinden, worauf es hier ankommt. Wir müssen eine Vorstellung vom Stand des Programms haben, oder? Unabhängig davon, ob wir eine normale Ausführung oder eine symbolische Ausführung durchführen, müssen wir eine Möglichkeit haben, den Status des Programms zu charakterisieren. In diesem Fall ist es ein so einfaches Programm, dass es den Heap nicht verwendet, den Stapel nicht verwendet und es hier keine Funktionsaufrufe gibt.

Somit kann der Zustand vollständig durch diese drei Variablen charakterisiert werden, zusammen mit dem Wissen, wo ich mich im Programm befinde. Wenn ich also die Ausführung von 4, 4 und 0 beginne und zum Ende des Zweigs komme, überprüfe ich den Ausdruck: 4 ist größer als 4? Offensichtlich nicht.
Jetzt werde ich das Programm bei T = Y ausführen, dh T ist nicht mehr 0, sondern hat den Wert 4. Dies ist der aktuelle Status meines Programms, und jetzt kann ich diesen Zweig auswerten.



Stimmt es, dass T <X ist? Nein. Wir sind der Kugel ausgewichen, die Aussage false hat nicht funktioniert. Es gab keine Probleme bei dieser privaten Ausführung.

Dies sagt jedoch nichts über eine andere Ausführung aus. Wir wissen, dass mit den Werten X = 4 und Y = 4 das Programm nicht fehlschlägt. Dies sagt jedoch nichts darüber aus, was passieren wird, wenn die Eingabewerte 2 und 1 sind.



Mit diesen Eingabewerten geht die Ausführung anders. Diesmal sehen wir, dass T = X ist, und nach dem Ausführen dieser Zeile nimmt T einen Wert gleich 2 an. Gibt es Probleme bei dieser Ausführung? Wird es bei einer solchen Eingabe einen Assertionsfehler geben?

Nun, mal sehen. Wenn also T 2 und X 2 ist, dann ist T nicht weniger als X. Es scheint, dass wir der Kugel erneut ausgewichen sind. Richtig? Hier haben wir also zwei spezifische Eingabewerte, bei denen das Programm fehlerfrei arbeitet. Tatsächlich sagt es uns jedoch nichts über andere Eingabewerte aus.

Die Idee der symbolischen Ausführung ist also, dass wir über die Ausführung eines Programms mit einem Satz von Eingabedaten hinausgehen möchten. Wir möchten in der Lage sein, tatsächlich über das Verhalten des Programms zu sprechen, wenn ein sehr großer Datensatz verwendet wird, in einigen Fällen eine unendliche Anzahl möglicher Eingabewerte. Die Hauptidee davon ist wie folgt.



Für ein Programm wie dieses wird sein Zustand durch den Wert dieser drei verschiedenen Variablen bestimmt: X, Y und T und durch das Wissen, wo ich mich gerade im Programm befinde. Aber jetzt werde ich anstelle der spezifischen Werte für X und Y einen symbolischen Wert haben, nur eine Variable. Eine Variable, mit der ich diesen Wert benennen kann, den der Benutzer als Eingabe verwendet. Dies bedeutet, dass der Status meines Programms nicht mehr dadurch gekennzeichnet ist, dass Variablennamen bestimmten Werten zugeordnet werden. Dies ist nun eine Zuordnung von Variablennamen zu diesen symbolischen Werten.

Der symbolische Wert kann als Formel betrachtet werden. In diesem Fall ist die Formel für X gleich X und die Formel für Y ist einfach Y, und für T ist sie tatsächlich gleich 0. Wir wissen, dass es für jeden Eingabewert keine Rolle spielt, was Sie tun. Der Wert von T nach der ersten Anweisung ist 0.

Dort wird es jetzt interessant. Wir sind zu diesem Zweig gekommen, der besagt, dass wir in eine Richtung gehen, wenn X größer als Y ist. Wenn X kleiner oder gleich Y ist, gehen wir in die andere Richtung.

Wissen wir etwas über X und Y? Was wissen wir über sie? Zumindest kennen wir ihren Typ, wir wissen, dass sie von min int bis max int variieren werden, aber das ist alles, was wir über sie wissen. Es stellt sich heraus, dass die Informationen, die wir über sie wissen, nicht ausreichen, um zu sagen, in welche Richtung dieser Zweig gehen kann. Sie kann in jede Richtung gehen
Es gibt viele Dinge, die wir tun können, aber was können wir im Moment tun? Versuchen Sie, die wildesten Vermutungen anzustellen.



Zielgruppe: Wir können die Ausführung des Programms in beiden Zweigen verfolgen.

Professor: Ja, wir können die Fortschritte in beiden Bereichen verfolgen. Wirf eine Münze und wähle je nachdem, wie sie fällt, den einen oder anderen Zweig.

Wenn wir also beiden Zweigen folgen wollen, müssen wir zuerst dem einen und dann dem anderen folgen, oder? Angenommen, wir beginnen mit diesem Zweig - T = X. Wir wissen, dass T an diesem Ort die gleiche Bedeutung wie X hat. Wir wissen nicht, was dieser Wert ist, aber wir haben einen Namen dafür - dies ist das Skript X.



Wenn wir den entgegengesetzten Zweig nehmen, was wird dann passieren? Der Wert von T wird gleich etwas anderem sein, oder? In diesem Zweig ist der Wert von T der symbolische Wert von Y.



Was bedeutet dieser T-Wert, wenn wir an diesem Punkt im Programm angelangt sind? Vielleicht ist es X, vielleicht ist es Y. Wir wissen nicht genau, was dieser Wert ist, aber warum geben wir ihm keinen Namen? Nennen Sie es t ₀ . Und was wissen wir über t ₀ ? In welchen Fällen ist t ₀ gleich X?

Im Wesentlichen wissen wir, dass wenn X größer als Y ist, die Variable gleich X ist und wenn X kleiner oder gleich Y ist, dann ist die Variable gleich Y. Daher haben wir einen Wert, den wir definiert haben, nennen wir ihn t ₀ , und er hat diese logische Eigenschaften.



An diesem Punkt im Programm haben wir also einen Namen für den Wert von T, dies ist t ₀ . Was haben wir hier gemacht? Wir haben beide Zweige der if-Anweisung genommen und dann den symbolischen Wert berechnet, um zu sehen, unter welchen Bedingungen ein Zweig des Programms ausgeführt wird und unter welchen der andere.
Nun kommt es zu dem Punkt, dass wir fragen sollten, ob T kleiner als X sein kann. Jetzt ist der Wert von T t ₀ , und wir wollen wissen, ob es möglich ist, dass t ₀ kleiner als X ist? Erinnern Sie sich an den ersten Zweig, den wir untersucht haben - wir haben eine Frage zu X und Y gestellt und wussten nichts über sie, außer dass sie vom Typ int waren.

Aber mit t ₀ wissen wir wirklich viel darüber. Wir wissen, dass es in einigen Fällen gleich X und in einigen Fällen gleich Y sein wird. Jetzt gibt es uns eine Reihe von Gleichungen, die wir lösen können. Wir können also sagen, ob es möglich ist, dass t ₀ kleiner als X ist, wenn wir wissen, dass t ₀ alle diese Bedingungen erfüllt? Wir können dies also als Einschränkung ausdrücken und zeigen, ob es möglich ist, dass t ₀ kleiner als X ist. Und wenn X größer als Y ist, dann ist t ₀ gleich X, und wenn X kleiner als oder gleich Y ist, bedeutet dies, dass t ₀ = ist Y. Y.



Wir haben also eine Gleichung. Wenn es eine Lösung gibt, wenn es möglich ist, den Wert von t ₀ , den Wert von X und den Wert von Y zu finden, die diese Gleichung erfüllen, dann erkennen wir diese Werte, und wenn wir sie in das Programm eingeben, dann geht es bei Ausführung entlang dieses Zweigs, wenn t <x und " wird explodieren “, wenn es in die Behauptung falsch fällt.

Was haben wir hier gemacht? Wir haben das Programm ausgeführt, aber anstatt Variablennamen bestimmten Werten zuzuordnen, haben wir diesen Variablennamen symbolische Werte gegeben. Tatsächlich gaben sie ihnen andere Variablennamen. In diesem Fall sind unsere anderen Variablennamen Skript X, Skript Y, t ₀ , und außerdem haben wir eine Reihe von Gleichungen, die zeigen, wie diese Werte zusammenhängen. Wir haben eine Gleichung, die uns sagt, wie t ₀ in diesem Fall mit X und Y zusammenhängt.

Die Lösung dieser Gleichung ermöglicht es uns, die Frage zu beantworten, ob dieser Zweig ausgeführt werden kann oder nicht. Schauen Sie sich die Gleichung an - ist es möglich, diesen Zweig zu nehmen oder nicht? Es scheint nicht so, weil wir nach Fällen suchen, in denen t ₀ kleiner als X ist, aber wenn in der ersten Bedingung t ₀ = X ist, dann ist der Ausdruck t ₀ <X nicht wahr.

Dies bedeutet also, dass wenn X> Y ist, dies nicht passieren kann, weil t ₀ = X ist und es nicht gleichzeitig gleich oder kleiner als X sein kann.

Aber was passiert, wenn t ₀ = Y ist? Kann t ₀ in diesem Fall kleiner als X sein?

Nein, das kann es definitiv nicht, weil wir wissen, dass X <Y ist. Wenn also t ₀ kleiner als X ist, dann ist es auch kleiner als Y. Aber wir wissen, dass in diesem Fall t ₀ = Y. Und daher wieder kann diese Bedingung nicht erfüllt werden. Hier haben wir also eine Gleichung, die keine Lösung hat, und es spielt keine Rolle, welche Werte Sie in diese Gleichung aufnehmen.

Sie können es nicht lösen, und dies sagt uns, dass unabhängig davon, welche Eingabe X und Y wir an das Programm übergeben, es nicht den Zweig hinuntergeht, wenn t <x ist.

Beachten Sie nun, dass ich bei der Erstellung dieses Arguments hier im Grunde auf Ihre Intuition über Ganzzahlen, über mathematische Ganzzahlen hingewiesen habe. In der Praxis wissen wir, dass sich Maschinen-Ints nicht genau wie mathematische Ints verhalten. Es gibt Fälle, in denen die Gesetze für mathematische ganzzahlige Datentypen nicht auf programmatische Ints anwendbar sind.

Daher müssen wir beim Lösen dieser Gleichungen sehr vorsichtig sein, da wir uns daran erinnern müssen, dass dies nicht die ganzen Zahlen sind, über die uns in der Grundschule berichtet wurde. Dies sind die 32-Bit-Ganzzahlen, die von der Maschine verwendet werden. Und es gibt viele Fälle von Fehlern, die aufgetreten sind, weil Programmierer über ihren Code in mathematischen Ganzzahlen nachgedacht haben und nicht erkannt haben, dass es Dinge wie Überläufe gibt, die ein anderes Programmverhalten für die mathematische Eingabe verursachen können.

Eine andere Sache, die ich hier beschrieben habe, ist ein rein intuitives Argument. Ich werde Sie durch den Prozess führen und zeigen, wie man es manuell macht, aber dies ist keineswegs ein Algorithmus. Das Schöne an dieser Idee der symbolischen Ausführung ist jedoch, dass sie in einen Algorithmus codiert werden kann. Und Sie können es mechanisch lösen, was es Ihnen ermöglicht, dies nicht nur für ein 10-Zeilen-Programm, sondern für Millionen von Programmen zu tun. Auf diese Weise können wir dieselbe intuitive Argumentation verwenden, die wir in diesem Fall verwendet haben, und darüber sprechen, was passiert, wenn wir dieses Programm mit unterschiedlichen Eingabewerten ausführen. Diese Überlegungen können skaliert und auf sehr große Programme ausgedehnt werden.



Zielgruppe: Was ist, wenn das Programm die Eingabe eines bestimmten Variablentyps nicht unterstützt?

Professor: Das ist eine sehr gute Frage! Angenommen, wir haben das gleiche Programm, aber anstelle von t = x haben wir t = (x-1). Dann können wir uns intuitiv vorstellen, dass dieses Programm jetzt „explodieren“ kann, oder?



Denn wenn das Programm so läuft, ist t wirklich kleiner als x. Was wird mit einem solchen Programm passieren? Wie wird unser symbolischer Zustand aussehen? Was ist t _0, wenn x größer als y ist? Wir korrigieren die Linien in unseren Gleichungen gemäß einem anderen Wert, wenn t = (x-1). Jetzt kann das Programm fehlschlagen, und Sie gehen zum Entwickler und sagen ihm: "Hey, diese Funktion kann explodieren, wenn x größer als y ist"!

Der Entwickler sieht sich das an und sagt: „Oh, ich habe vergessen, es Ihnen zu sagen - tatsächlich wird diese Funktion niemals mit Parametern aufgerufen, bei denen x größer als y ist. "Ich habe es nur aus historischen Gründen geschrieben, also mach dir keine Sorgen, ich würde mich nicht daran erinnern, wenn du es mir nicht gesagt hättest."

Angenommen, wir gehen davon aus, dass x kleiner oder gleich y ist.



Dies ist eine Voraussetzung oder Vereinbarung für unsere Funktion. Die Funktion verspricht, etwas zu tun, aber nur, wenn der Wert diese Annahme erfüllt. Wenn es jedoch nicht zufrieden ist, heißt es in der Funktion: "Es ist mir egal, was passiert. Ich verspreche, dass es nur dann keinen Fehler geben wird, wenn diese Annahme erfüllt ist. "

Wie codieren wir diese Einschränkung, wenn wir die Gleichungen lösen? Im Wesentlichen haben wir eine Reihe von Einschränkungen, die uns sagen, ob dieser Zweig machbar ist. Zusätzlich zu den Einschränkungen müssen wir auch sicherstellen, dass die Voraussetzung oder Annahme erfüllt ist.

Die Frage ist, kann ich x und y finden, die all diese Einschränkungen erfüllen und gleichzeitig die erforderlichen Eigenschaften besitzen? Sie können sehen, dass diese Einschränkung X ≤ Y die Differenz zwischen dem Fall darstellt, in dem diese Einschränkung erfüllt ist, und dem Fall, in dem sie nicht erfüllt ist.

Dies ist ein sehr wichtiges Thema bei der Arbeit mit Analysen, insbesondere wenn Sie dies gleichzeitig auf der Ebene einzelner Funktionen tun möchten. Es ist ratsam zu wissen, was der Programmierer beim Schreiben dieser Funktion im Sinn hatte. Wenn Sie keine Ahnung von diesen Annahmen haben, denken Sie möglicherweise, dass das Programm fehlschlägt.

Wie geht das mechanisch? Dieses Problem hat zwei Aspekte. Aspekt Nummer eins - wie sind Sie auf diese Formeln gekommen?

In diesem Fall ist intuitiv klar, wie wir zu diesen Formeln gekommen sind. Wir haben sie einfach manuell zusammengestellt. Aber wie werden diese Formeln mechanisch erstellt?

Und der zweite Aspekt - wie lösen Sie diese Formeln, nachdem Sie sie haben? Ist es möglich, diese Formeln zu lösen, die beschreiben, ob Ihr Programm abstürzt oder nicht?
Beginnen wir mit der zweiten Frage. Wir können unser Problem mit diesen Formeln reduzieren, die ganzzahliges Denken und Bitvektoren enthalten. Beim Erstellen von Programmen kümmern Sie sich um Arrays, Funktionen und erhalten dadurch riesige Formeln. Ist es möglich, sie mechanisch zu lösen?



Die vielen Technologien, über die wir heute sprechen, sind praktische Werkzeuge im Zusammenhang mit den enormen Fortschritten bei der Entwicklung von Lösern für logische Fragen. Insbesondere gibt es eine sehr wichtige Klasse von Lösern, die als SMT oder "Lösbarkeitslöser modularer Theorien" bezeichnet wird. SMT-Löser ist die Lösbarkeit logischer Formeln unter Berücksichtigung der ihnen zugrunde liegenden Theorien.

Viele Leute behaupten, dass dieser Name nicht besonders gut ist, aber er wurde als der am häufigsten verwendete festgelegt.

SMT-Solver ist ein Algorithmus, aufgrund dessen diese logische Formel am Ausgang Ihnen eine von zwei Optionen bietet: Entweder erfüllt er seinen Zweck oder er erfüllt nicht. , , .

. , SMT, NP- , «» «».
, NP- ? -, ? , SMT – : « ».



, , , , : « ». , , .

27:30

MIT « ». 10: « », 2


Die Vollversion des Kurses finden Sie hier .

, . ? ? , 30% entry-level , : VPS (KVM) E5-2650 v4 (6 Cores) 10GB DDR4 240GB SSD 1Gbps $20 ? ( RAID1 RAID10, 24 40GB DDR4).

VPS (KVM) E5-2650 v4 (6 Kerne) 10 GB DDR4 240 GB SSD 1 Gbit / s bis Dezember kostenlos, wenn Sie für einen Zeitraum von sechs Monaten bezahlen, können Sie hier bestellen.

Dell R730xd 2 ? 2 Intel Dodeca-Core Xeon E5-2650v4 128GB DDR4 6x480GB SSD 1Gbps 100 $249 ! . c Dell R730xd 5-2650 v4 9000 ?