pate
1.0.0
Dieses Repository implementiert ein Tool, um zu überprüfen, ob Patches bis zur Verfolgung von Äquivalenz (Pate) sicher sind.
Ziel ist es zu beweisen, dass Sicherheitspatches, die auf Binärdateien angewendet werden, nur schlechte Verhaltensweisen entfernen oder sie auf andere Weise genau für den Entwickler des Patchs charakterisieren. Der Verifizierer unterstützt PORPC- und AARG32 -Binärdateien (der derzeit statisch verknüpfte ELF -Binärdateien erfordert).
Der schnellste Weg, um zu beginnen, besteht darin, das Docker -Bild zu erstellen und das Tool über Docker zu verwenden. Weitere Einstellungsanweisungen finden Sie im Abschnitt Entwicklungsabschnitt unten.
Erstellen Sie zunächst das Docker -Bild mit dem Befehl:
Docker Build -Plattform Linux/AMD64. -t Pate
Führen Sie als Nächstes den Verifizierer auf einem Beispiel aus:
Docker Run - -rm -it --Platform Linux/AMD64 -v "$ (pwd)"/tests/Integration/Paket/exe:/target pate -original /target/packet.exe ---patched /target/packet.patched.exe
Der Verifizierer akzeptiert die folgenden Befehlszeilenargumente:
-h,-Helfen Sie mit, diesen Hilfstext zu zeigen
-O,-Originaler Original Binär
-p,-Patched Exe geflickt binär gepatcht
-B,-BlockInfo Dateiname Blockinformationen in Bezug auf Binärdateien
-S,-startetymbol arg starten aus der Funktion mit diesem Symbol aus der Funktion
-D,-nodiscovery entdecken Funktionspaare nicht dynamisch basierend auf
Anrufe.
-SOLVER ARG DER SMT-LOLVER, mit der die Überprüfung gelöst werden soll
Bedingungen. Einer von CVC4, Yices oder Z3
(Standard: yices)
-GOAL-Timeout arg die Auszeit zur Überprüfung der individuellen Ziele in Sekunden
(Standard: 300)
-Heuristic Timeout arg die Auszeit zur Überprüfung der heuristischen Ziele in Sekunden
(Standard: 10)
-Original-Anvill-Hinweise arg
Anvillspezifikation für die Code -Entdeckung analysieren
Hinweise
-Patched-Anvill-Hints arg
Anvillspezifikation für die Code -Entdeckung analysieren
Hinweise
-Original-probabilistische Hinweise arg
Analysieren Sie eine JSON -Datei, die eine probabilistische Funktion enthält
Name/Adresse Hinweise
-Patched-probabilistische Hinweise arg
Analysieren Sie eine JSON -Datei, die eine probabilistische Funktion enthält
Name/Adresse Hinweise
-Original-CSV-Funktions-Hinweise arg
Analysieren Sie eine CSV -Datei mit Funktionsname/Adresse
Hinweise
-Patched-CSV-Funktions-Hinweise arg
Analysieren Sie eine CSV -Datei mit Funktionsname/Adresse
Hinweise
-Original-BSI-Hinweise arg an eine JSON-Datei, die den Funktionsnamen/die Funktionsadresse enthält
Hinweise
-Patched-BSI-Hinweise arg an eine JSON-Datei, die den Funktionsnamen/die Funktionsadresse enthält
Hinweise
-No-Zwerg-Hinweise extrahieren keine Metadaten aus den Zwerginformationen in
die Binärdateien
-V,-Ausführlichkeit arg Die Ausführlichkeit der Protokollierungsausgabe (Standard: Info)
-Save-Macaw-CFGS Dir Save MacAW CFGs in das bereitgestellte Verzeichnis
-Solver-Interaktions-Datei
Speichern Sie Interaktionen mit dem SMT -Solver während des symbolischen
Ausführung dieser Datei
-Proof-Summary-Json-Datei
Eine Datei, um interessante Beweisergebnisse in JSON zu speichern
Format
-Log-Datei-Datei eine Datei zum Speichern von Debug-Protokollen auf
-E,-Errormode Arg-Verifier-Fehlerbehandlungsmodus
(Standard: throwonanyFailure)
-R,-resorable variable Ressiver-Misserfolge-Handhabungsmodus
(Standard: throwOneqrescopeFailure)
-Skip-nicht-namensfunktionen überspringen Analyse von Funktionen ohne Symbole
-Skip-Divergent-Kontroll-Fluss
<Apressierte>
-Target-äquiv-regs arg berechnen eine gleichwertige Bedingung, die ausreicht, um ausreichend zu werden
Festlegen der Gleichstellung der angegebenen Register nach der
Toplevel Entrypoint kehrt zurück. <Apressierte>
-IGNORE-SEGMENTS ARG-Überspringen von Segmenten (0-idexiert) beim Laden von ELF
-Json-Toplevel Toplevel im JSON-Output-Modus (interaktiver Modus
nur)
-Nur-Read-Segmente Arg-Marksegmente als schreibgeschützte (0-inikierte) beim Laden
ELF
-Script-Dateiname speichern MacAW-CFGs in dem bereitgestellten Verzeichnis
-Assume-Stack-SCOPE Fügen Sie zusätzliche Annahmen zum Stapelrahmen-Scoping hinzu
Während Funktionsaufrufe (unsicher)
-IGNORE-WARNINGINGS ARG erheben keine der angegebenen Warntypen
-Aufgrund der Annahme von Klassifikatorversagen immer klassifizieren Return immer Klassifikatorfehler auflösen
Funktionsrückgabe, wenn möglich.
Der Schnellstartabschnitt beschrieben einen Befehl zum Ausführen des Verifizierers in einem Testfall mit dem Docker -Container. In diesem Abschnitt werden einige nützliche Befehle für andere Szenarien behandelt.
Wenn Sie eine tar -Datei mit einem Docker -Bild des Verifiers haben, können Sie sie mit dem Befehl installieren:
Docker Load -i/path/to/pate.tar
Danach den Verifizierer über Docker ausführen:
Docker Run - -RM -it -Plattform Linux/AMD64 Pate -HELP
Um den Verifizierer mit Docker zu verwenden, ist es nützlich, ein Verzeichnis in Ihrem lokalen Dateisystem in den Docker -Container abzubilden, um Ausgabedateien zu sparen. Unter der Annahme, dass Ihre ursprünglichen und gepatmten Binärdateien original.exe bzw. patched.exe sind:
Mkdir Verifierdata
CP Original.exe Patched.exe VerifierData/
Docker Run - -RM -it -Plattform Linux/AMD64
-v `pwd`/verifierdata`:/verifierdata pate
-Original /Verifierdata/original.exe
-patched /VerifierData/patched.exe
-Proof-Summary-Json /Verifierdata/Report.json
-Log-Datei /Verifierdata/pate.log
-SAVE-MACAW-CFGS /Verifierdata /CFGS
In diesem Befehl wird der Überprüfer auf den beiden Binärdateien ausgeführt und Sie in eine Schleife für Read-Eval-Print fallen lassen, in der Sie interaktiv die Ausgabe des Verifizierers untersuchen können.
Standardmäßig beginnt der Überprüfer aus dem formalen Programmeinstiegspunkt. Dies ist oft nicht sehr nützlich (und kann für komplexe Binärdateien mit einem großen _start problematisch sein, der ein Problem für unsere Code -Entdeckung verursacht). Für Änderungen mit einem bekannten (oder zumindest erwarteten) Auswirkungenbereich ist die Analyse der betroffenen Funktionen außerdem erheblich schneller. Um stattdessen einen Analyse -Einstiegspunkt anzugeben, startet die Option -s <function_symbol> die Analyse aus der Funktion, die dem angegebenen Symbol entspricht. Beachten Sie, dass für die Binärdateien Funktionssymbole bereitgestellt werden müssen (entweder als eingebettete Debug -Symbole oder separat in einem der Hinweisformate).
Es ist zwar unangemessen, aber manchmal nützlich, einen Funktionsaufruf als No-op zu behandeln. Beispielsweise kann das Ignorieren großer Funktionen, die sich nicht geändert haben und es ist unwahrscheinlich, dass sie sich auf die Richtigkeit auswirken (z. B. große kryptografische Funktionen von vertrauenswürdigen Bibliotheken), die Leistung erheblich zu verbessern. Um diese Funktion zu verwenden, übergeben Sie eine Konfigurationsdatei mit der Option --blockinfo an den Überprüfer, um sicherzustellen, dass die Konfigurationsdatei die folgenden Anweisungen enthält:
Ignorieren Sie-Originalfunktionen = [<adresse>, ...] Ignore-Patched-functions = [<adresse>, ...]
wobei jede der Listen eine Liste von Funktionen von Funktionen ist, die ignoriert werden müssen. Während die beiden Listen separat angegeben werden, sollten sie mit ziemlicher Sicherheit zwischen den beiden Binärdateien "ausgerichtet" werden (dh eine Funktion im ursprünglichen Binärdatum bedeutet wahrscheinlich, dass die entsprechende Funktion im Patch -Binär auch ignoriert werden muss).
Der Prüfer profitiert auf zwei Arten von Zwergmetadaten:
Um Zwergmetadaten ohne IT (z. B. Binärdateien) in Binärdateien injizieren zu können, empfehlen wir die Verwendung des Zwerg-Writer-Tools. Als Beispiel für die Verwendung von dwarf-writer durch sein Docker-Bild unter der Annahme der Existenz eines Ziels ( target-binary.exe ) und Metadaten im ANVILL JSON-Format ( target-binary.exe.json ):
Docker Load -i Zwerg-Writer-Docker.tar
Mkdir DwarfwriterData
cp target-binary.exe target-binary.exe.json dwarfwriterData/
Docker Run - -rm -it -v `pwd`/dwarfwriterData:/dwarfwriterData Zwerg -Triter
-anvill /dwarfwriterData/target-binary.exe.json
/DwarfwriterData/target-binary.exe
/DwarfwriterData/target-binary-dwarf.exe
Dies erzeugt eine Version des mit Zwergmetadaten in DwarfWriterData/target-binary-dwarf.exe Metadaten.
Wenn Sie das llvm-dwarfdump -Tool haben, können Sie die generierten Zwergmetadaten verwenden. Der pate -Verifizierer nutzt automatisch die Zwergen -Metadaten -Hinweise, es sei denn, es wird angewiesen, sie zu ignorieren.
Der Verifizierer nimmt zwei Binärdateien als Eingabe auf: eine ursprüngliche Binärdehnung und ein geflicktes binär. Die Annahme ist, dass ein sicherheitsorientiertes Patch auf die ursprüngliche Binärdatei angewendet wurde, die sein Verhalten weitgehend bewahrt, aber einige unerwünschte Verhaltensweisen beheben kann. Der Überprüfer versucht dann zu beweisen, dass die beiden Binärdateien das gleiche beobachtbare Verhalten aufweisen; Wenn dies nicht der Fall ist, erzeugt es eine Differentialzusammenfassung , die die Bedingungen beschreibt, unter denen der gepatpfte Binäre ein anderes Verhalten des Originals aufweist. Auf diese Weise können Patch -Entwickler die Auswirkungen ihrer Patches auf die Programmsemantik verstehen und bewerten, ob die Auswirkungen auf die von ihnen beabsichtigten Ausführungspfade beschränkt sind.
Der Überprüfer erfordert keine manuell bereitgestellte Spezifikation von Benutzern. Stattdessen behandelt es das ursprüngliche Programm als die gewünschte Verhaltensspezifikation. Diese Anordnung macht Pate zu einem relationalen Überprüfer, da sie das gepflasterte Binärdatum auf das Original bezieht. Der Überprüfer basiert auf einer Reihe vorhandener Bibliotheken für die Erkennung von Binärcode und die symbolische Ausführung von Programmen (einschließlich Maschinencode -Programmen). Ungefährs funktioniert der Überprüfer von:
Das Pate -Tool ist in Haskell geschrieben und benötigt den GHC -Compiler (wir testen mit 9,6) und das Cabal Build -Tool zum Kompilieren. Das Gebäude aus der Quelle kann erreicht werden durch:
git clone [email protected]: Galoisinc/pate.git CD -Pastete Git Submodule Update - -Init cp cabal.project.dist cabal.project Cabal Configure PKG: Pate ./pate.sh -Help
Der Verifier erfordert, dass ein SMT -Solver im PATH verfügbar ist. Die Standardeinstellung ist yices - z3 und cvc4 können auch funktionieren, werden jedoch nicht regelmäßig mit Pate getestet.
Dieses Material basiert auf Arbeiten, die von der Defense Advanced Research Projects Agency (DARPA) und dem Naval Information Warfare Center Pacific (NIWC Pacific) unter Vertragsnummer N6001-20-C-4027 unterstützt werden. Alle Meinungen, Ergebnisse und Schlussfolgerungen oder Empfehlungen, die in diesem Material geäußert werden, sind die der Autoren und spiegeln nicht unbedingt die Ansichten des DARPA & NIWC Pacific wider.
