seninja

Seninja - Plugin d'exécution symbolique pour ninja binaire

: Démarrez l'exécution

: Passez l'état actuel

: courez jusqu'à la branche

: exécuter l'état actuel jusqu'à l'adresse actuellement sélectionnée

: Démarrez une recherche DFS

: Démarrez une recherche BFS

: Définissez l'adresse actuellement sélectionnée comme cible de la recherche

: Évitez l'adresse actuellement sélectionnée lors d'une recherche

: Réinitialiser les cibles et éviter les adresses

: Arrêtez une recherche

: Réinitialiser Seninja

Enregistrer la vue

La vue de registre peut être utilisée pour visualiser la valeur des registres de l'état actif. La valeur d'un registre peut être modifiée en double-cliquez dessus. Le menu de clic droit permet:

• Copiez le contenu du registre
• Concrétiser la valeur du registre
• Évaluez la valeur du registre à l'aide du solveur
• Injecter des symboles
• Afficher l'expression du registre
• Définissez le registre sur l'adresse d'un tampon créé avec la vue de tampon

Vue de mémoire

La vue de mémoire peut être utilisée pour visualiser la valeur d'une partie de la mémoire de l'état actif. En cliquant sur "Monitor Memory", l'utilisateur peut spécifier une adresse mémoire à surveiller. Le widget affichera 512 octets à partir de cette adresse. La vue de mémoire est divisée en deux sections: un hexview et une vue ASCII. L'HexView montre la valeur hexadécimale de chaque octet uniquement si l'octet est mappé et concret. Si l'octet n'est pas cartographié, le _ chargé est affiché; Si l'octet est symbolique, le widget montre le caractère . .

Le menu de clic droit permet:

• Copiez la sélection (en divers formats, par exemple Little-Endan, Binary, etc.)
• Concrétiser la valeur de la sélection
• Évaluer la valeur de la sélection à l'aide du solveur
• Injecter des symboles

Vue de tampons

Ce widget permet la création de tampons contenant des données symboliques.

API de ligne de commande

D'autres API peuvent être exécutées via le shell Python. Par exemple, nous pouvons utiliser le solveur pour prouver une condition pour l'état actuel:

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

Le code vérifiera la satisfaction de eax == 3 compte tenu de la contrainte de chemin de l'état actif.

Consultez le wiki pour avoir plus d'informations sur les commandes.

Paramètres

Seninja donne à l'utilisateur la possibilité de configurer de nombreuses parties du moteur symbolique (par exemple, dimension des pages, stratégie d'accès à la mémoire symbolique, etc.). Tous les paramètres disponibles sont accessibles et modifiés en cliquant sur Edit/Preferences/Settings et en sélectionnant SENinja dans le widget gauche.

Version et dépendances

Testé avec

• Ninja 4.0 binaire avec licence personnelle
• Python 3.11
• Z3 4.8.14

Pour le faire fonctionner, vous devez installer Z3 avec PIP: $ pip3 install z3-solver