SENINJA：二进制忍者-符号执行插件的BinarY忍者反汇编-开放获取文章-版本v0.2-代码链接https://githu...

软件X 20（2022）101219原始软件出版物SENINJA：二进制忍者Luca Borzacchiello，Emilio Coppa，Camil Demetrescu意大利罗马Sapienza大学ar t i cl e i nf o文章历史记录：接收5十月2020收到修订版2021年12月16日接受2022年保留字：逆向工程符号执行网络安全a b st ra ct符号执行（Symbolic execution）是一种程序分析技术，旨在自动识别应用程序的有趣输入，使用它们来生成覆盖代码不同部分的程序执行。它被广泛用于漏洞发现和逆向工程。在本文中，我们提出SENINJA，一个符号执行插件的BinarY忍者反汇编。该工具允许用户直接在反汇编程序的用户界面中执行符号执行分析，并可用于支持各种逆向工程任务。版权所有©2022作者。由爱思唯尔公司出版这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）中找到。代码元数据当前代码版本v0.2用于此代码版本的代码/存储库的永久链接https://github.com/ElsevierSoftwareX/SOFTX-D-20-00062Code Ocean compute capsule none法律代码许可证BSD-2条款使用git的代码版本控制系统使用的软件代码语言、工具和服务编译要求、操作环境依赖性BinarY NinjaPythonBinarY Ninja v2.1.0或更高版本Z3 v4.4.1或更高版本（使用Python绑定）如果可用，链接到开发人员文档/手册https://github.com/borzacchiello/seninja/wiki问题支持电子邮件lucaborza@gmail.com1. 动机和意义软件逆向工程是从最终产品开始重建软件的操作、设计和架构的过程，例如，编译的二进制程序。这个过程通常很难，因为它涉及到分析数千行代码，这些代码是用低级语言编写的（例如，汇编），没有文档，并且经常被混淆以更难分析。尽管困难重重，但逆向工程在几种情况下至关重要：例如，在恶意软件分析和专有软件的安全评估中。虽然逆向工程主要是一项手动任务，但研究人员和开发人员已经建立了可以帮助的工具和技术来加速这个过程反汇编器是分析编译后的二进制程序的基本工具。反汇编器的工作是将编译后的二进制文件转换为人类可读的汇编代码，并将其排列在突出显示代码结构有几个可用的disassem-*通讯作者。电子邮件地址：borzacchiello@diag.uniroma1.it（Luca Borzacchiello）.https://doi.org/10.1016/j.softx.2022.101219blers [1除了反汇编程序的正常任务外，它还实现了其他类型的分析，并将其公开在一组完整且文档齐全的API中。例如，BinarYNinja执行代码提升，这是将给定架构的汇编代码转换为更高级别的中间语言（IL）。这类语言的例子是LLVM IR [6]和VEX [7]。提升简化了程序分析，因为它：(a)减少了需要由分析处理的不同（通常是冗余的）指令的数量，BinarY Ninja提升了最常见架构的指令（例如，x86，x86_64，ARM，MIPS）到LLIL（低电平IL）：图1（b）在右侧显示了BinarY Ninja在提升左侧显示的x86_64代码符号执行是在错误检测和逆向工程[8-通过在符号输入上构造表达 式 并 使 用 可 满 足 性 模 理 论 （ SMT ） 求 解 器 （ 例 如 ，[15][16][17][18][19 作为一个例子，考虑图。1（a）. 上2352-7110/©2022作者。 由Elsevier B.V.出版。这是一篇开放获取的文章，使用CC BY许可证（http://creativecommons.org/licenses/by/4.0/）。可在ScienceDirect上获得目录列表SoftwareX期刊主页：www.elsevier.com/locate/softxLuca Borzacchiello，Emilio Coppa和Camil Demetrescu软件X 20（2022）1012192[−]=-⊕̸=Fig. 1. 例如：函数authenticate。左边是函数authenticate1，而右边是符号树，它表示对这个函数进行符号探索的结果。符号执行引擎作为解释器计算函数的代码，将输入变量初始化为符号（在示例中，变量a用符号α初始化它可以假设初始区间中的任何值 0，2，321），以及构建符号表达式而不是对具体值执行计算一个状态是一个抽象对象，它保存了内存和执行路径中积累的约束。当执行命中一个分支时，如果条件涉及符号值，则执行分叉，即，符号引擎将当前状态分成两个状态。这两个状态对两个分支方向的结果进行建模（在本例中为第3生成两个状态，当α170第187章是真的分别为false）。可以分别在两个状态上继续执行。在探索期间的任何时候，在SMT求解器的帮助下，在状态中收集的约束可以用于生成输入，该输入将沿着状态的相同路径驱动具体在图1（a）中，执行树中的两个最终状态可以使用等于到α0和α17、分别请注意，因为搜索空间有232个值，所以蛮力方法将生成覆盖第6符 号 执 行 已 被证 明 是 发 现 bug 和 漏 洞 的 基 本例 如 ， 它在Windows 7的开发过程中使用，发现了几乎三分之一的模糊技术漏洞[17]。此外，它也是大多数系统的关键组件，1 为了简单起见，该函数是用C编写的;SENinja目标是二进制代码。Cyber Grand Challenge [18]，由DARPA举办的为期两年的竞赛，旨在创建用于发现、利用和修补软件漏洞的自动化工具2. 软件描述在这篇文章中，我们介绍了SENINJA，一个实现符号执行引擎作为BinarY Ninja插件的工具。SENinja评估BinarY Ninja生成的低级别IL（LLIL），并集成到BinarY Ninja用户界面（UI）中，允许用户执行符号执行，而无需切换到其他工具。 图 4给出了插件的视觉概述。2.1. 软件构架图2显示了SENINJA的架构。该工具的主要软件组件是执行器。它是一个高级接口，负责保存生成的状态，并在当前活动状态上象征性地执行指令。它与BinarY Ninja交互以获取有关二进制文件的关键信息，例如LLIL表示和内存布局。SENinja公开的命令可以通过BinarY Ninja的UI访问，这些命令都是使用这个高级接口构建的在下一节中，我们将更详细地描述Executor的内部组件，解释一些设计选择我们做的。2.1.1. 状态一个状态代表一个路径的执行快照。1 （a），每个节点中的Luca Borzacchiello，Emilio Coppa和Camil Demetrescu软件X 20（2022）1012193图二. Architecture of SENINJA.图3.第三章。 涉及CRC 32校验和的 符 号 计 算 的 基 准 测 试 的 实 验 结 果 [19]。树代表一个国家。在SENinja中，状态包含指令指针、内存内容、寄存器值、打开的文件和路径约束。符号执行中一个著名的问题是状态爆炸2。虽然SENinja不能解决这个问题，但它至少可以最大限度地减少跟踪不同的但在探索过程中产生了类似的状态。为此，我们设计了国家的每一个组成部分，写入时复制（CoW）行为，以便在分叉状态时减少资源消耗。符号执行中的另一个常见问题是符号存储器访问的处理[21，22]，即，当存储器地址取决于程序输入值时，对存储器操作效果的推理。SENINJA支持不同的内存模型来处理内存访问：完全是象征性的。通过考虑可以访问的每个存储单元来处理符号存储器访问[23]。虽然这是最慢的模式，但它也是最准确的。完全混凝土。这个模型将地址的表达式具体化为一个具体的值[17]。这是最快的模式，但也不太准确。部分象征性的。这个模型落在前面的方法的中间。它使用完全符号化的方法，但只有当符号地址可以假设的可能值的数量足够小时[24]，否则地址被具体化。当符号地址不受它可以跨越整个地址空间），访问被具体化到新分配的页面，并且将其作为基地址的任何其他符号地址在分配的页面内被准确地处理[25]。这是SENinja中的默认内存模型。2 例如，循环中的分支很容易导致状态爆炸，当循环条件是符号时，它可以生成指数数量的状态。为了评估符号内存模型和CoW策略的影响，我们考虑了一个涉及CRC 32校验和的符号计算的基准[26]，这是由最近的一篇论文[19]提出的。图中左侧的图表。3显示了不同的符号执行器的运行时间，当计算校验和的符号字节数增加（从1到1024字节）。基准测试的特点是通过几个符号访问，其结果是至关重要的计算输入时，处理应生成预期的CRC值。我们认为：(a)Klee [10]，一个基于源代码的符号执行器，（b）angr [8]，一个二进制符号框架，支持符号访问，（c）SENinja（完全具体），它使用完全具体的内存模型，（d）SENinja（部分符号），它使用部分符号内存模型。在这个基准测试中，我们没有考虑完全符号内存模型，因为内存访问被限制在几个内存页面内，从而产生与部分符号内存模型相同的行为。SENinja（完全具体）非常有效，但非常不准确：它无法（图表中的交叉标记）导出大多数校验和大小的输入。angr只针对较小的校验和大小（最多16个字节）进行缩放，因为它需要超过1小时（这是我们实验期间的超时）。Klee是非常高效的，它利用了从源代码中获得的知识（特别是基准测试访问的数组的大小SEN-inja（部分符号）可以正确地推理高达512字节的校验和计算，在几个校验和大小上比Klee快。最近提出的阵列优化[27]可以集成到SENinja中，以进一步提高其可扩展性。图的中间和右边的图表。图3显示了使用和不使用CoW策略时SENINJA的资源消耗（部分符号）。在这些实验中，我们禁用了求解器，以关注由于状态探索而导致的资源消耗，这是受CoW策略影响的。从运行时间和内存消耗方面可以清楚地看到CoW策略带来的好处。Luca Borzacchiello，Emilio Coppa和Camil Demetrescu软件X 20（2022）1012194[客户端]−见图4。 BinarY Ninja界面与SENinja插件。活动状态位于绿色地址（1）。延迟状态用红色（2）标记，显示一条注释，指示同一地址的状态数。可以使用小部件（3）和（4）查看活动状态的存储器和寄存器。符号缓冲区可以使用（5）查看和创建可通过右击菜单（6）访问命令可以使用Python控制台访问CLI（7）。2.1.2. 符号表达式SENINJA使用位向量理论[28]表示符号表达式，该理论模拟了固定大小位向量算术的语义。特别是，SENinja使用自定义的抽象树类来包装来自Z3 SMT求解器的位向量对象。它不直接使用Z3的AST，主要有两个原因：（a）可以更有效地执行具体计算，（b）SENINJA可以通过更新包装器类轻松地移植到其他SMT求解器。此外，SENinja丰富了表示具有范围间隔的表达式的AST，这提供了表达式在状态中可以假设例如，SENINJA COM-在给定表达式256 +ZeroExtend（α，32）的情况下，计算区间范围256、512，该表达式表示常量256与零扩展的8位输入值α的32位加法。间隔肛门-在存在符号存储器访问的情况下，解析是非常有价值的，因为它可以允许SENinja评估哪些存储器页面可以在执行期间被修改，而无需查询SMT解算器当前的实现还不支持步幅间隔，并且在回绕的情况下返回范围[0， 2n 1]，其中n是表达式中的位数2.1.3. 指令处理程序SENINJA是作为BinarY Ninja的LLIL表示的解释器构建的。由于它使用的是一种中间语言，因此它的大部分代码都是与架构无关的，并且可以以最小的努力添加对新架构的支持（只要BinarYNinja支持目标架构）。目前，SENINJA支持x86、x86_64和ARMv8。由于LLIL指令在内部表示为AST对象，SENinja使用访问者类来解析AST，为绝大多数LLIL节点实现处理程序。处理程序的工作是根据指令的语义修改当前状态，可能生成新的状态（例如，用于分支指令）。除了LLIL处理程序，SENINJA还定义了利用底层架构知识的自定义处理程序这种设计选择背后的两个主要原因：- BinarY Ninja的提升器不支持每个架构的每个指令（例如，cpuidx86_64指令不支持），因此SENINJA必须以ad-hoc方式处理它们。- 自定义处理程序可以帮助缓解状态爆炸。例如，x86指令setcc将被表示为LLIL中的分支，而使用if-then-else表达式对其进行建模而不分叉状态可能是有益的。2.1.4. 操作系统和功能模型为了处理来自动态库的系统调用和函数调用，SENINJA设计了描述外部代码对当前状态的影响的模型[8]。目前，SEN-inja为最常见的C库函数提供了模型（例如，memcmp，memset）和最常用的Linux系统调用。模型是用Python编写的，新模型可以通过几行代码添加[29]。然而，为了减少从头开始编写操作系统模型的需要，SENinja提供了对兼容性层的初步支持，允许它重用可用于著名符号执行器angr的模型[8]。最后，SENinja支持自定义钩子[30]。它们允许对外部代码的一小部分功能进行建模，这在几个逆向工程任务中已经足够了，并且可以用来克服某些模型的不足2.2. 工具功能图4示出了SENinja的界面的概览。我们现在回顾一下主要功能，重点介绍如何通过BinarY Ninja的UI直接访问它们。符号状态构造和初始化。符号执行可以在程序中的任何一点开始. SENINJA使用从Bi- narY Ninja获得的内存内容来存储状态。它还利用BinarY Ninja执行的值集分析 [31]来检测，例如，常数寄存器默认情况下，未知数据被标记为符号，但是用户可以选择其他策略（例如，零初始化）。类似于步进函数。在SENinja中，任何时候都只能激活一个状态。符号执行可以在当前活动状态下使用受调试器启发的命令执行。这些命令是：单步执行，继续直到地址，继续直到分支。因此，通过UI，用户可以Luca Borzacchiello，Emilio Coppa和Camil Demetrescu软件X 20（2022）1012195图五、F l a r e - O n 挑 战 的 代码片段[32]。更改当前活动状态，并使用前面的命令之一开始新的探索。由于符号探索可能需要很长时间，例如，到达特定地址时，用户可以通过设置超时（通过面板设置）来限制探索时间，或者使用右键单击菜单中的专用命令随时停止探索。在探测之后，SENinja可以在CFG中突出显示在探测期间状态已经执行了州合并。如果两个或多个状态正在执行相同的指令，用户可以决定将它们合并[33]。虽然状态合并可以减少内存消耗，但求解程序可能会在对从合并状态导出的公式进行推理时遇到困难，因为它们可以更复杂。合并算法受到基于源代码的符号执行器Klee [10]中实现的策略的启发。在合并两个状态之前，SENINJA检查它们的后继状态：如果它们不同，即，这两个状态将采取不同的方向，则中止合并操作。自动搜索器除了执行单个状态之外，SENINJA还设计了自动搜索器，可用于搜索程序的路径，以便找到到达某个程序点的输入。用户可以通过右键单击菜单将地址设置为搜索目标，在搜索过程中要避免的一组地址。然后，用户可以使用DFS或BFS算法开始搜索过程内存、寄存器和缓冲区视图。可以使用SENinja小部件查看当前活动状态的内存和寄存器（见图3和图4）。4）.这些小部件可以用于查看和修改具体数据、查看符号表达式、使用求解器计算表达式或注入新符号。在计算表达式时，用户最多可以生成k个解，其中k是用户定义的值。符号缓冲区可以使用专用的小部件创建和约束（参见图5）。 4）.命令行界面。可以使用命令行界面执行复杂的操作。BinarYNinja有一个嵌入式Python控制台，可用于调用SENinja的命令行API。例如，用户可以在输入上设置特定的约束，或者可以为库函数定义自定义钩子。关于命令行API的详细描述可以在项目wiki中找到3. 说明性示例：分析虚拟机混淆在本节中，我们将介绍一个案例研究，SENINJA用于混淆代码的逆向工程Luca Borzacchiello，Emilio Coppa和Camil Demetrescu软件X 20（2022）1012196见图6。 SENinja小部件：（1）处理符号缓冲区，（2）设置命令行参数，（3）和（4）获得符 号 缓 冲 区 的具体分配。混淆是产生人类难以理解的代码的行为。开发人员混淆代码是为了为了使逆向工程过程更加困难，例如，来保护许可证检查器或专有算法混淆在恶意软件编写者中也很普遍。虚拟机混淆是最常用和最有效的混淆技术之一[34]：它将代码转换为自定义字节码，然后用字节码和自定义虚拟机替换二进制中的原始代码，当使用自定义操作码处理程序解释生成的字节码时，自定义虚拟机在运行时能够再现原始代码的行为。作为混淆代码的示例，我们考虑来自反向竞争Flare-On 6 [35]的第11个挑战[32]。该程序是一个使用虚拟机模糊处理的64位PE以保护对用户提供的输入检查若干条件的功能。因此，这个函数可以被看作是一个许可证密钥检查器，我们使用SENinja来自动查找这个检查器接受的输入3.1. 初步分析我们首先使用BinarY Ninja手动分析二进制文件主函数可以在地址0x140001220处识别（见图11）。5）。此函数考虑两个输入字符串（作为命令行参数获得），其中第二个字符串的大小为32字节。然后它调用vm_loop：这个函数是虚拟机器调度器循环，即，获取字节码并调用适当的处理程序来执行模糊计算的例程。在运行模糊代码后，main调用函数final_checks，检查第一个字符串是否为FLARE2019并且验证混淆计算的输出，在成功的情况下执行0x14000169d处的代码，或者在失败的情况下执行0x14000178a处的代码。由于在此初步分析之后第一个输入是已知的，因此主要目标是找到第二个输入的值，而无需花费数小时手动反转混淆的计算。3.2. 查找有效输入在对二进制文件的结构有了大致的了解之后，我们可以使用SENinja来自动识别二进制文件输入能够满足检查。我们首先在main开始时创建一个初始状态（右键单击，开始符号执行），然后使用buffers小部件创建一个32字节的新符号缓冲区（图1中的步骤1）。6）。然后，我们使用SENinja工具栏中的Setup argv命令设置命令行参数（步骤2），将字符串FLARE2019设置为第一个参数，将我们刚刚创建的缓冲区设置为第二个参数。在 定 义 符 号 输 入 并 创 建 初 始 状 态 之 后 ， 我 们 将 地 址0x14000169d定义为代码中的目标点（右击，设置目标），我们希望在符号探索期间到达该目标点，并将地址0x14000178a定义为代码中的避免点（右击，设置避免最后，我们可以开始执行利用DFS文件夹（右键单击，运行DFS）。几秒钟后，SENINJA能够生成达到目标点的状态。使用buffers小部件（图3中的步骤3和4），6），我们可以获得通过检查的具体输入：cHCyrAHSXmEKpyqoCByGGuhFyCmy86Ee。4. 与其他工具的一些以前的作品[36，37]已经探索了将符号执行集成到图形化逆向工程工具中的解决方案。例如，Ponce [36]将动态符号执行引擎Triton [38]集成到商业反汇编器和调试器IDA Pro中。与SENinja的一个关键设计差异是Ponce不能静态分析代码，这是非标准架构的二进制文件或非可执行内存转储的常见另一个有趣的解决方案是IDAngr [37]，它结合了符号框架angr [8]和IDA Pro。 不幸的是，这个插件不再积极维护，与IDA Pro的UI的集成非常有限。AngrY Ghidra [39]和modalitY [40]是最近的两个项目，分别在Ghidra [4]和Radare2 [2]中公开了angr的功能。AngrY Ghidra被设计成获得一些勘探参数（例如，开始目标），但随后它使用固定的和预定义的脚本启动Angr，留下非常有限的交互机会。modalitY反而拥抱Radare 2的精神，Luca Borzacchiello，Emilio Coppa和Camil Demetrescu软件X 20（2022）1012197在其命令行界面中添加了几个新操作。当使用这两个插件的当前版本时，第3节中的几个步骤无法执行，迫使用户手动与angr交互或面临严重的路径爆炸。最后，SY mNav [41]设计了符号树的视觉表示。不幸的是，这个查看器是一个独立的组件，目前不能集成到调试器，如IDAPro或BinarY Ninja。5. 影响和结论SENINJA是BinarY Ninja的一个符号执行插件，Binar y Ninja是一个被网络安全社区广泛使用的商业反汇编程序。SENinja扩展了反汇编器的功能，使用户可以直接在BinarY Ninja中访问符号执行分析，从而可能简化逆向工程活动。此外，它被设计为可扩展的，允许用户通过添加几行Python代码来实现新功能。SENinja在GitHub上公开发布后，BinarY Ninja社区对它表现出了积极的兴趣：SENinja最近被正式纳入BinarY Ninja的社区插件库[42]此外，一位著名的安全专家也尝试过SENINJA，并在一篇博客文章中积极地提到了它[43]。我们希望，在未来几年内，SENINJA可以成为逆向工程师的参考工具之一。竞合利益作者声明，他们没有已知的竞争性财务利益或个人关系，可能会影响本文报告的工作附录A. 补充数据与本文相关的补充材料可以在https://doi.org/10.1016/j.softx.2022.101219上找到。引用[1] 六 角 射 线 IDA pro. 2020 年 ， https ： //www. 他 是 X-R 。 com/products/ida.[2020年9月15日在线访问]。[2] 雷达22020年，https：//rada. re. [2020年9月15日在线访问[3] 霍珀2020年，https：//www. hopepepeperapapp. com。[2020年9月15日[4] 国安局吉德拉2 0 1 6 ，https：//ghidra-sre. 或g/。[2020年7月11日[5] 矢量35。二进制忍者。2020年，https：//binary. ninja. [2020年9月[6] Lattner C，Adve V. LLVM：终身程序分析转换的编译框架&。In：Proc. int.symp.关于代码生成和优化：反馈导向和运行时优化。CGO 2004，2004，p.75比86[7] Nethercote N，Seward J. Valgrind：重量级动态二进制插装框架。第28届ACM SIGPLAN编程语言设计与实现会议论文集。PLDI 2007，2007，p. 八九比一百[8] Shoshitaishvili Y，Wang R，Salls C，Stephens N，Polino M，Dutcher A，等. 战争的艺术：二进制分析中的进攻技术。2016年IEEE安全与隐私研讨会论文集。SP 2016，2016，p. 138比57[9] Poeplau S，Francillon A. Symbolic execution with SymCC：不要解释，编译！第29届USENIX安全研讨会论文集。SEC2020，2020，p. 181比98[10]放大图片创作者：Cadar C，Dunbar D，Engler D. KLEE：为复杂系统程序自动生成高覆盖率测试。第八届USENIX操作系统设计与实现会议论文集。OSDI2008，2008，p. 209比24[11]放大图片作者：Chipounov V，Kuznetsov V，Candea G. S2E平台：设计、实施和应用。ACM传输计算系统（TOCS）2012;30（1）：2：1-49。[12]作者：J.J. E，J. C.重建C2服务器，用于远程访问特洛伊木马程序的符号执行。在：网络安全密码学和机器学习。CSCML 2019，2019，p.121比40[13]博尔扎基耶洛 L、 COPPA E， 德梅特雷斯库 C. 模糊： 混合 起毛concolic处决。 计算机&安全2021.[14]放大图片创作者：J. Symfusion：concolic执行的混合工具。第37届IEEE/ACM自动化软件工程国际会议论文集。ASE[15]作者：John L.Z3：一个高效的SMT求解器。在：Proceedings of第14届国际构造和分析工具和算法会议的系统。TACAS 2008/ETAPS2008，2008，p.337比40[16]作者：J. J.模糊符号表达式。于：第43届软件工程国际会议论文集。 ICSE'21，2021。[17]GodefroidP，Levin MY，Molnar DA。SAGE：白盒模糊安全试验.队列2012;10（1）：20：20-7.[18]DARPA。网络大挑战。2016，https：//www. darpa。mil/program/cyber-grand-challee。[2020年9月15日在线访问]。[19]SharmaV，Emamdoost N，Kim S，McCamant S.不hard：CRC的高效符号推理。在：2020二进制分析研究研讨会。NDSS BAR2020，2020.[20]BaldoniR，Coppa E，调查符号执行技术ACM Comput Surv 2018;51（3）：50：1[21]张晓刚，李晓刚. Memory Models inSymbolic Execution：Key Ideas and NewThoughts.软件测试验证Reliab2019;29（8）：e1722。[22]作者：J. J.处理内存密集型操作象征性的执行。第15届软件工程创新会议论文集。ISEC[23]杨伟华，李伟华.具有集合和复制操作的数组理论于：SMT 2012。第十届可满足性模理论国际研讨会。 SMT2012，vol. 20，2012，p.98比108[24]ChaSK，Avgerinos T，Rebert A，Brumley D.在二进制上释放混乱代码. In：Proc. 2012 IEEE symp.在sec。和隐私SP 2012，2012，p. 380 -94.[25]CaseldenD，Bazhanyuk A，Payer M，McCamant S，Song D.HI-CFG：Construc-二进制分析和应用攻击多态性。第18届欧洲计算机安全研究研讨会。ESORICS2013，2013，p. 164比81[26]博尔扎基耶洛湖 CRC示例。 2021年，https：//github. com/borzacchiello/seninja/wiki/Benchmarks.[27]Shuai Z，Chen Z，Zhang Y，Sun J，Wang J.基于类型和区间的数组约束求解。第30届ACM SIGSOFT软件测试与分析国际研讨会论文集。ISSTA 2021，2021，http://dx.doi.org/10.1145/3460319.3464826。[28] SMT-LIB。可满足性模理论库。2018年12月28日，http://smtlib.cs。uiowa.edu/网站。[29]博尔扎基耶洛湖在Seninja添加新模型。2020，https://github.com/borzacchiello/seninja/wiki/Extend#add-a-new-model.[30]博尔扎基耶洛湖在Seninja中定义自定义钩子2020年，https：//github。com/borzacchiello/seninja/wiki#hooks.[31]Balakrishnan G，Reps T. WYSINWYX：你所看到的并不是你所执行的。ACM跨计划Lang Syst 2010;32（6）.[32] FlareOn。月11挑战.2020年，https://www.fireeye.com/blog/threat-research/2019/09/2019-flare-on-challenge-solutions.html.[2020年9月15日在线访问[33]吴晓波，李晓波.高效的状态合并象征性的处决第33届ACM SIGPLAN编程语言设计与实现会议论文集。PLDI2012年，2012年，p. 193-204.[34]方红，吴勇，王S，黄勇。 多级二进制代码混淆使用改进的虚拟机。信息安全。ISC 2011，2011，p. 168比81[35] 火眼Flare-on. 2020，http://flare-on.com/。[2015年9月15日]ber 2020]。[36] Illera AG.庞塞2016年，https://github.com/illera88/Ponce。[2020年9月15日在线访问[37]菲 奥 拉 尔 迪 IDAngr. 2018 年 12 月 28 日 ， 中 国 科 学 院 出 版 社 。https://github.com/andreafioraldi/IDAngr [在线2020年9月15日[38]Saudel F，Salwan J. Triton：一个动态符号执行框架。In：Symp.关于信息和通信技术安全的报告。SSTIC 2015，2015，p.31比54[39]Nalen98. 安格里·吉德拉 2020年，https://github.com/Nalen98/AngryGhidra。[40]卡尼佩角 模态。 2019年，https://github.com/0xchase/modality。[41]Angelini M，Blasilli G，Borzacchiello L，Coppa E，D'Elia DC，Lenti S，等.SymNav：视觉辅助符号执行。在：第16届IEEE网络安全可视化研讨会论文集。VizSec 2019，2019，p. 1比11[42] 宁加湾社区插件2020年，https：//github。com/Vector35/comuni你-你。 [2020年9月15日在线访问]。[43] 汉 金 斯 自 动 化 字 符 串 去 混 淆 。 2020年 ， https ： //www. kryptooslogic.com/blog/2020/12/automated-string-de-gobfuscation/. [2021 年 7月30 日 在线访问]。