seninja

Seninja - complemento de ejecución simbólica para ninja binario

: iniciar la ejecución

: paso el estado actual

: corre hasta la rama

: ejecute el estado actual hasta la dirección seleccionada actualmente

: Iniciar una búsqueda DFS

: Comience una búsqueda de BFS

: Establezca la dirección seleccionada actualmente como el objetivo de la búsqueda

: Evite la dirección seleccionada actualmente durante una búsqueda

: Restablecer objetivos y evitar direcciones

: detener una búsqueda

: restablecer seninja

Vista de registro

La vista de registro se puede utilizar para visualizar el valor de los registros del estado activo. El valor de un registro se puede modificar haciendo doble clic en él. El menú de clic derecho permite:

• Copiar el contenido del registro
• Concretizar el valor del registro
• Evaluar el valor del registro utilizando el solucionador
• Símbolos de inyección
• Mostrar la expresión de registro
• Establezca el registro en la dirección de un búfer creado con la vista del búfer

Vista de memoria

La vista de memoria se puede utilizar para visualizar el valor de una porción de memoria del estado activo. Al hacer clic en "Monitor Memory", el usuario puede especificar una dirección de memoria para monitorear. El widget mostrará 512 bytes a partir de esa dirección. La vista de memoria se divide en dos secciones: una vista hexview y una vista ASCII. El HexView muestra el valor hexadecimal de cada byte solo si el byte está asignado y concreto. Si el byte no está mapeado, se muestra el _ charactado; Si el byte es simbólico, el widget muestra el personaje . .

El menú de clic derecho permite:

• Copie la selección (en varios formatos, por ejemplo, Little-Endian, Binary, etc.)
• Concretizar el valor de la selección
• Evaluar el valor de la selección utilizando el solucionador
• Símbolos de inyección

Vista de buffers

Este widget permite la creación de buffers que contienen datos simbólicos.

API de línea de comando

Se pueden ejecutar más API a través de Python Shell. Por ejemplo, podemos usar el solucionador para probar una condición para el estado actual:

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

El Código verificará la satisfacción de eax == 3 dada la restricción de ruta del estado activo.

Consulte el wiki para tener más información sobre los comandos.

Ajustes

Seninja le da al usuario la posibilidad de configurar muchas partes del motor simbólico (por ejemplo, dimensión de páginas, estrategia de acceso a memoria simbólica, etc.). Se puede acceder y modificar todas las configuraciones disponibles haciendo clic en Edit/Preferences/Settings y seleccionando SENinja en el widget izquierdo.

Versión y dependencias

Probado con

• Ninja binario 4.0 con licencia personal
• Python 3.11
• Z3 4.8.14

Para que funcione, debe instalar Z3 con PIP: $ pip3 install z3-solver