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