seninja

Seninja-二进制忍者的符号执行插件

：开始执行

：踩当前状态

：运行直到分支

：执行当前状态直到当前选择的地址

：开始DFS搜索

：开始BFS搜索

：将当前选择的地址设置为搜索的目标

：避免在搜索期间选择当前选择的地址

：重置目标并避免地址

：停止搜索

：重置Seninja

注册视图

寄存器视图可用于可视化活动状态寄存器的值。可以通过双击它来修改寄存器的值。右键单击菜单允许：

• 复制寄存器的内容
• 具体化寄存器的价值
• 使用求解器评估寄存器的价值
• 注入符号
• 显示寄存器表达式
• 将寄存器设置为使用缓冲区视图创建的缓冲区的地址

内存视图

内存视图可用于可视化活动状态内存的一部分的值。通过单击“监视器内存”，用户可以指定一个内存地址以监视。小部件将从该地址开始显示512个字节。内存视图分为两个部分：六角形和ASCII视图。仅当字节被映射和混凝土时，六角形显示每个字节的十六进制值。如果字节是未盖上的，则显示符号_ ；如果字节是象征性的，则小部件显示字符. 。

右键单击菜单允许：

• 复制选择（以各种格式，例如Little-endian，二进制等）
• 具体化选择值
• 使用求解器评估选择的价值
• 注入符号

缓冲区视图

该小部件允许创建包含符号数据的缓冲区。

命令行API

可以通过Python Shell执行更多的API。例如，我们可以使用求解器证明当前状态的条件：

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

给定活动状态的路径约束，该代码将检查eax == 3的满意度。

请咨询Wiki，以获取有关命令的更多信息。

设置

Seninja使用户有可能配置符号引擎的许多部分（例如页面的维度，符号内存访问策略等）。可以通过单击Edit/Preferences/Settings并在左侧小部件中选择SENinja来访问和修改所有可用的设置。

版本和依赖项

测试

• 具有个人许可证的二进制忍者4.0
• Python 3.11
• Z3 4.8.14

为了使其正常工作，您需要使用PIP安装Z3： $ pip3 install z3-solver