seninja

Seninja - symbolisches Ausführungs -Plugin für binäre Ninja

: Starten Sie die Ausführung

: Schritt den aktuellen Zustand

: Rennen Sie bis zum Zweig

: Führen Sie den aktuellen Status bis zur aktuell ausgewählten Adresse aus

: Starten Sie eine DFS -Suche

: Starten Sie eine BFS -Suche

: Legen Sie die aktuell ausgewählte Adresse als Ziel der Suche fest

: Vermeiden Sie die aktuell ausgewählte Adresse während einer Suche

: Ziele zurücksetzen und Adressen vermeiden

: Stoppen Sie eine Suche

: Seninja zurücksetzen

Ansicht Register

Die Registeransicht kann verwendet werden, um den Wert der Register des aktiven Zustands zu visualisieren. Der Wert eines Registers kann durch Doppelklicken geändert werden. Mit dem Menü mit der rechten Maustaste ermöglicht::

• Kopieren Sie den Inhalt des Registers
• Den Wert des Registers konkretisieren
• Bewerten Sie den Wert des Registers mit dem Solver
• Symbole injizieren
• Zeigen Sie den Registerausdruck
• Stellen Sie das Register auf die Adresse eines mit der Pufferansicht erstellten Puffer

Speicheransicht

Die Speicheransicht kann verwendet werden, um den Wert eines Teils des Gedächtnisses des aktiven Zustands zu visualisieren. Durch Klicken auf "Speicher überwachen" kann der Benutzer eine Speicheradresse angeben, um zu überwachen. Das Widget zeigt 512 Bytes aus dieser Adresse. Die Speicheransicht ist in zwei Abschnitten aufgeteilt: eine Hexview und eine ASCII -Ansicht. Die Hexview zeigt den Hex -Wert jedes Byte nur, wenn das Byte zugeordnet und konkret ist. Wenn das Byte nicht kartiert ist, wird die _ angezeigt; Wenn das Byte symbolisch ist, zeigt das Widget den Charakter . .

Mit dem Menü mit der rechten Maustaste ermöglicht::

• Kopieren Sie die Auswahl (im verschiedenen Format, z. B. Little-Endian, Binary usw.)
• Den Wert der Auswahl konkretisieren
• Bewerten Sie den Wert der Auswahl mit dem Solver
• Symbole injizieren

Pufferansicht

Dieses Widget ermöglicht die Erstellung von Puffern, die symbolische Daten enthalten.

Befehlszeilen -APIs

Weitere APIs können über die Python -Hülle ausgeführt werden. Zum Beispiel können wir den Löser verwenden, um eine Bedingung für den aktuellen Zustand zu beweisen :

 > >> import borzacchiello_seninja as seninja
> >> s = seninja . get_current_state ()
> >> s . solver . satisfiable ( extra_constraints = [ s . regs . eax == 3 ])

Der Code überprüft die Befriedigung von eax == 3 angesichts der Pfadbeschränkung des aktiven Zustands.

Konsultieren Sie das Wiki, um weitere Informationen über die Befehle zu erhalten.

Einstellungen

Seninja gibt dem Benutzer die Möglichkeit, viele Teile der symbolischen Engine zu konfigurieren (z. B. Dimension von Seiten, Strategie für symbolische Speicherzugriff usw.). Auf alle verfügbaren Einstellungen können zugegriffen und geändert werden, indem Sie auf Edit/Preferences/Settings klicken und SENinja im linken Widget auswählen.

Version und Abhängigkeiten

Getestet mit

• Binärer Ninja 4.0 mit persönlicher Lizenz
• Python 3.11
• Z3 4.8.14

Damit es funktioniert, müssen Sie Z3 mit PIP: $ pip3 install z3-solver