Was sind die Lücken zwischen symbolischer Ausführung und Taint-Analyse?

Question

Ich las vor kurzem ein Papiertitel "All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)" von Dr. EJ Schwartz. In dem Artikel sprach er hauptsächlich über ihre Anwendungen im Zusammenhang mit binären Sicherheitskontexten.

Ich bin neugierig auf den genauen Unterschiede zwischen dynamischer taint Analyse und vorwärts symbolischer Ausführung.

Von dem, was ich sehe, verfolgen taint Analyseinformationen von Objekt x fließen (Quelle) y (sink) zum Objekt, immer dann, wenn Information in x gespeichert übertragen wird y zu widersprechen. Das Hauptanliegen ist also, welches Objekt transitiv von der Quelle betroffen sein kann. Während die symbolische Ausführung einige Eingaben als symbolische Werte behandelt, versucht , andere Variablen mit symbolischen auszudrücken. dabei antwortet es , unter welchen Bedingungen der symbolische Eingang die nachfolgenden Programme beeinflusst.

Ich kann sehen, dass auf der Binär-Ebene, Taint-Analyse wird oft mit der Sicherheitslücke durch Rückkehr Adresse überschrieben; während symbolische Ausführung mit mehr Arten von gefährdeten Themen wie Integer-Überlauf, Laufzeitfehler Assertion, Leck Ressource (z.B. Speicherverlust, Datei-Öffnen/Schließen), Pufferüberlauf umgehen kann.

aber es scheint, dass moderne taint Analyse nicht nur beinhaltet Datenflussanalyse wird verfolgen die meisten von ihnen die Steuerfluss Bedingungen; und in mehreren Schwachstellenerkennungsszenarien wird die behaftete Eingabe auch als symbolischer Wert dargestellt und wie die symbolische Ausführung weitergegeben. Auf der anderen Seite können symbolische Ausführungs-Engines aufgrund der Einschränkungen der zugrundeliegenden Constraint-Solver und der Laufzeitumgebung nicht vollständig symbolische Werte verwenden, die durch unterschiedliche Pfadbedingungen getrennt sind. Dadurch können sie nicht den hohen Zweig oder Pfad Abdeckung wie erwartet erreichen.

So im Allgemeinen Fällen können wir sagen, dass taint Analyse ist eine Art grober symbolischer Ausführung oder symbolischer Ausführung ist eine Art präziser taint Analyse?

Answer 1

Interessante Frage! Hier ist meine 2 Cent: symbolische Ausführung verwendet eine Art von Taint-Analyse, um Pfadbeschränkungen zu konstruieren. Die symbolische Ausführung verwendet auch einen SMT/SAT-Löser, um konkrete Werte für Variablen und/oder Eingaben zu erzeugen, so dass eine bestimmte Pfadbeschränkung erfüllt ist.

Da die Taint-Analyse keinen SMT/SAT-Löser verwendet, würde ich sagen, dass es keine Art von symbolischer Ausführung ist. Vielleicht könnte man sagen, Taint-Analyse ist ein Teil der symbolischen Ausführung.

Dies ist nur eine Meinung. Bitte zögern Sie es nicht herauszufordern.

Answer 2

Ich stimme @Benny, es ist eine wirklich interessante Frage. Sie werden wahrscheinlich viel lernen, wenn Sie diese Art von Fragen formulieren und noch mehr, wenn Sie versuchen, sie zu beantworten.

würde Ich mag zu Bennys Antwort hinzufügen:

Um taint Tracking und symbolische Ausführung zu implementieren, hat man Semantik der Sprache (zum Beispiel x86-Assembler bei Binärdateien) zu definieren. Zum Beispiel muss man beschreiben, was

add eax, ebx 

'bedeutet' bedeutet, d. H. Mit dem Staat. Die Definition der Taint-Tracking-Semantik könnte vielleicht als eine Art Teilmenge der symbolischen Ausführungssemantik angesehen werden. Die Taint-Tracking-Semantik wird in der symbolischen Ausführungssemantik codiert. Der gemeinsame Teil ist

• Wenn ebx verdorben ist, dann eax verdorben ist.
• Wenn ebx symbolisch (IOW enthält eine SMT Formel, die eine oder mehr symbolischen Vars) dann eax symbolisch

Doch die Semantik für symbolische Ausführung weitere Informationen enthalten (zB der genaue arithmetische Operation): - eax ist + "was auch immer in eax vorher war" "was auch immer in ebx war, bevor"

Bitte kommentieren Sie oder korrigieren Sie mich!

Answer 3

Meiner Meinung nach müssen wir zur Beantwortung Ihrer Frage folgendes beantworten: i) Hat die symbolische Ausführung das Potenzial, alle Ausführungspfade zu finden, die die Taint-Analyse kann, und mehr; ii) Hat die Taint-Analyse das Potential, alle Ausführungspfade zu finden, die symbolische Ausführung kann, und mehr; iii) Haben beide das gleiche Potenzial, die gleichen Ausführungspfade zu finden? iv) Können beide Ausführungswege berechnen, die der andere nicht kann?

Meiner Meinung nach ist iv) korrekt, was bedeutet, dass man keine Untermenge ist. Ich stimme jedoch zu, dass es tatsächlich eine große Überschneidung gibt.

Wir können die Optionen i) und iii) eliminieren, weil die symbolische Ausführung nur brauchbare Ausführungspfade findet, während die Taint-Analyse unbrauchbare finden kann, wenn sie nicht auf Constraint-Lösungen zurückgreift.

Um Option ii) zu beseitigen, denke ich (korrigieren Sie mich, wenn ich falsch liege), dass es Ausführungspfade gibt, die symbolische Ausführung aussetzen kann und Taint-Analyse nicht kann. Zum Beispiel:

for(int i=0;i<3;i++) { 
    if(someString.charAt(i)=='4') 
     //do something 
    else 
     //do something else 
} 

In einem solchen Fall symbolische Ausführung macht alle acht möglichen Ausführungspfade, während taint Analyse (wenn ich mich nicht irre) nicht.

Answer 4

Ich denke, der wesentliche Unterschied ist, ob die Ausführung Betons oder symbolische ist ---, ob Sie in der taint Ausbreitungs interessiert sind (für ein Informationsleck oder Steuerfluss Hijack Überprüfung) auf eine einzigen konkreten Ausführung oder Wenn Sie möchten erkunden andere Möglichkeiten einer solchen Ausbreitung durch Nutzung der Macht der Löser.Der Vorteil der dynamischen Taint-Analyse ist in seinem niedrigen Overhead und somit geeignet für die Laufzeitüberwachung. Auf der anderen Seite ist die (reine/dynamische) symbolische Ausführung in der Lage, andere Pfade als den konkreten Weg zu erkunden und eignet sich somit für eine Offline-Analyse der Sicherheitseigenschaften Ihres Interesses.