Site updated: 2024-04-09 15:15:18

2024/02/27/Symbion初探/index.html

@@ -13,7 +13,7 @@
 
 
 
-    <script type="application/ld+json">{"@context":"http://schema.org","@type":"BlogPosting","author":{"@type":"Person","name":"一瓢清浅","sameAs":["#about","https://github.com/"],"image":"photo.jpg"},"articleBody":"\n\n一、原理  原始论文：SYMBION: Interleaving Symbolic with Concrete Execution\n官方博客：symbion: fusing concrete and symbolic execution\n1. 背景  符号执行可以用来获取走到指定程序区块的可行输入，但是符号执行在实际应用中面临很多挑战：\n\n路径爆炸问题：符号执行从程序入口开始探索，当程序中出现分支和循环时，会导致路径状态呈指数增长。\n\n环境交互问题：当程序与系统或三方库进行交互时，由于缺失源码或交互复杂等原因，会阻碍符号执行的状态更新。\n\n\n2. 方案Symbion 通过具体执行环境与符号执行环境的同步与切换，实现具体值和符号值交替执行。通过这种交替执行机制，减少符号执行探索的路径状态，并解决程序对外部环境的依赖问题。\n图中演示了具体执行环境与符号执行环境相互切换的过程：\n\n\n目标是对从 PoI 到TP的路径进行符号推理，CSP节点是程序入口。从 CSP 到PoI要经过复杂的运算和交互，这导致直接从 CSP 开始符号推理，将无法向后演进到PoI。\n使用 Symbion 时，首先将具体值输入给 CSP，在具体执行后到达PoI。然后在PoI 切换到符号执行环境，算出到达 TP 所需的变量取值。再将算出来的结果同步给具体执行环境，在 PoI 恢复具体执行，即可到达TP。\n3. 实现Symbion 的架构设计如下：\n\n\nSymbion 在 Angr 的基础上，增加了如下组件：\n\nConcrete Target：定义了与具体执行环境交互的方法，通过实现这些方法可以让 Symbion 支持特定的交互环境。例如 Symbion 实现的GDBConcreteTarget，它通过 gdbsever 控制远程目标程序的交互。\n\nread_memory(address, nbytes)：从具体进程内存中 address 开始读取 nbytes 字节。\nwrite_memory(address, value)：在具体进程内存中 address 处写入value。\nread_register(register)：返回具体进程中指定 register 的内容。\nwrite_register(register, value)：在具体进程的 register 中写入value。\nset_breakpoint(address)：在具体进程中的 address 处设置断点。\nremove_breakpoint(address)：移除之前在 address 处设置的断点。\nrun()：恢复具体进程的执行。\n\n\nSimEngineConcrete：利用 Concrete Target 的方法执行以下步骤，实现 Symbolic 环境到 Concrete 环境的切换。\n\n用用户提供的值修改具体进程的内存。\n用用户提供的值修改具体进程的寄存器。\n通过断点来设置新的PoI。\n恢复程序的具体执行，直到到达新的PoI，并将控制权交还给 Angr。\n\n\nConcrete SimPlugin：当具体执行到达 PoI，这个插件实现Concrete 环境到 Symbolic 环境的切换，它将具体状态导入 Angr 来创建SimState。\n\n将 SimState 的内存后端重定向到具体进程的内存，即在符号执行过程中，SimState的内存读取都是从具体进程中来操作。\n\n将具体进程中的寄存器值复制到 SimState 中。\n\n将具体进程的内存映射与 Angr 在启动期间加载的内存映射同步。\n\n\n\nSYMBION Exploration Technique：提供用户使用 Symbion 的 API ，通过这些 API ，用户指定 PoI 的地址，在具体执行到达 PoI 后，Symbion 切换为符号执行。\n\n\n简而言之，在 Symbion 的工作流程中，各组件的作用为：\n\n用户通过 SYMBION Exploration Technique 指定PoI。\n\n程序经过具体执行到达到 PoI 后暂停， Concrete SimPlugin 根据具体执行环境来创建一个SimState。\n\nAngr 通过符号执行，计算到达下一个 PoI 的可行解。\n\nSimEngineConcrete 用 Angr 算出来的结果修改具体进程中的变量，恢复具体执行直到下一个PoI。\n\n\n二、示例Symbion 官方示例：test_concrete_not_packed_elf64\n示例使用的二进制：not_packed_elf64\n二进制没有给源码，通过 IDA 逆向源码，并用 AI 改写，得到 C 源码如下，源码中取 dest 变量中的一串数值做判断，不同的分支触发不同的print。\n\n\n在 Symbion 的示例代码中，首先通过具体执行到达 BINARY_DECISION_ADDRESS，然后用符号执行探索从BINARY_DECISION_ADDRESS 到DROP_STAGE2_V2的路径。\n\n\n在符号执行求解成功后，再将求解结果传递给具体执行环境，并启动具体执行，即可到达DROP_STAGE2_V2：\n\n\n结合 CFG 和源码可以看到，符号执行的起点 BINARY_DECISION_ADDRESS 对应源码图右侧 55 行，符号执行的终点 DROP_STAGE2_V2 对应源码图右侧 77 行。通过 Symbion，实现了对二进制按指定路径的进行分析的目的。\n\n\nSymbion 的示例代码中，涉及到很多内存地址操作，需要结合 IDA 的反编译源码来看：\n\n\n\nline 2：启动具体执行，到 BINARY_DECISION_ADDRESS 停下，即 IDA 反编译源码第 67 行代码\n\nline 3：从具体执行环境的获取寄存器中的栈指针sp，指向栈顶（即栈开始的位置）\n\nline 4：从栈顶 sp 开始读取 20 个字节的内存，这块内存包括反编译源码中的变量 i 和v5\n\nline 5：判断是否为符号变量，此时为具体执行环境，所以不是符号变量\n\nline 7：定义符号变量，变量名为arg0，大小为 32 字节\n\nline 8：用 symbolic_buffer_memory 指向具体执行环境中 rbp-0xc0 的内存地址，它对应 IDA 反编译源码中的数组 s 的起始地址。\n\nline 10：从 symbolic_buffer_memory 开始加载 36 个字节的内存\n\nline 11：判断是否为符号变量，此时为具体执行环境，所以不是符号变量\n\nline 12：将 angr0 存储到symbolic_buffer_memory，将符号变量与具体执行环境的内存地址关联起来\n\nline 15：从 symbolic_buffer_memory 开始加载 36 个字节的内存\n\nline 16：判断是否为符号变量，因为 把 angr0 保存到这块内存，所以是符号变量\n\nline 19：符号执行状态初始化\n\nline 37：启动符号执行\n\n\n可以看到，Symbion 在切换具体执行环境和符号执行环境时，是通过内存地址把变量的具体值和符号值对应起来。需要结合 IDA 反编译的源码中给出的变量地址和内存大小，人工设置符号执行中所需要的符号变量，难以实现自动化。","dateCreated":"2024-02-27T16:33:24+08:00","dateModified":"2024-04-09T15:00:01+08:00","datePublished":"2024-02-27T16:33:24+08:00","description":"Symbion 是 Angr 的一款插件，可以实现具体执行与符号执行交替运行","headline":"交替符号执行工具——Symbion 初探","image":[],"mainEntityOfPage":{"@type":"WebPage","@id":"https://jiliguluss.github.io/2024/02/27/Symbion%E5%88%9D%E6%8E%A2/"},"publisher":{"@type":"Organization","name":"一瓢清浅","sameAs":["#about","https://github.com/"],"image":"photo.jpg","logo":{"@type":"ImageObject","url":"photo.jpg"}},"url":"https://jiliguluss.github.io/2024/02/27/Symbion%E5%88%9D%E6%8E%A2/","keywords":"安全, Angr, 符号执行"}</script>
+    <script type="application/ld+json">{"@context":"http://schema.org","@type":"BlogPosting","author":{"@type":"Person","name":"一瓢清浅","sameAs":["#about","https://github.com/"],"image":"photo.jpg"},"articleBody":"\n\n一、原理介绍  原始论文：SYMBION: Interleaving Symbolic with Concrete Execution\n官方博客：symbion: fusing concrete and symbolic execution\n1. 背景  符号执行可以用来获取走到指定程序区块的可行输入，但是符号执行在实际应用中面临很多挑战：\n\n路径爆炸问题：符号执行从程序入口开始探索，当程序中出现分支和循环时，会导致路径状态呈指数增长。\n\n环境交互问题：当程序与系统或三方库进行交互时，由于缺失源码或交互复杂等原因，会阻碍符号执行的状态更新。\n\n\n2. 方案Symbion 通过具体执行环境与符号执行环境的同步与切换，实现具体值和符号值交替执行。通过这种交替执行机制，减少符号执行探索的路径状态，并解决程序对外部环境的依赖问题。\n图中演示了具体执行环境与符号执行环境相互切换的过程：\n\n\n目标是对从 PoI 到TP的路径进行符号推理，CSP节点是程序入口。从 CSP 到PoI要经过复杂的运算和交互，这导致直接从 CSP 开始符号推理，将无法向后演进到PoI。\n使用 Symbion 时，首先将具体值输入给 CSP，在具体执行后到达PoI。然后在PoI 切换到符号执行环境，算出到达 TP 所需的变量取值。再将算出来的结果同步给具体执行环境，在 PoI 恢复具体执行，即可到达TP。\n3. 实现Symbion 的架构设计如下：\n\n\nSymbion 在 Angr 的基础上，增加了如下组件：\n\nConcrete Target：定义了与具体执行环境交互的方法，通过实现这些方法可以让 Symbion 支持特定的交互环境。例如 Symbion 实现的GDBConcreteTarget，它通过 gdbsever 控制远程目标程序的交互。\n\nread_memory(address, nbytes)：从具体进程内存中 address 开始读取 nbytes 字节。\nwrite_memory(address, value)：在具体进程内存中 address 处写入value。\nread_register(register)：返回具体进程中指定 register 的内容。\nwrite_register(register, value)：在具体进程的 register 中写入value。\nset_breakpoint(address)：在具体进程中的 address 处设置断点。\nremove_breakpoint(address)：移除之前在 address 处设置的断点。\nrun()：恢复具体进程的执行。\n\n\nSimEngineConcrete：利用 Concrete Target 的方法执行以下步骤，实现 Symbolic 环境到 Concrete 环境的切换。\n\n用用户提供的值修改具体进程的内存。\n用用户提供的值修改具体进程的寄存器。\n通过断点来设置新的PoI。\n恢复程序的具体执行，直到到达新的PoI，并将控制权交还给 Angr。\n\n\nConcrete SimPlugin：当具体执行到达 PoI，这个插件实现Concrete 环境到 Symbolic 环境的切换，它将具体状态导入 Angr 来创建SimState。\n\n将 SimState 的内存后端重定向到具体进程的内存，即在符号执行过程中，SimState的内存读取都是从具体进程中来操作。\n\n将具体进程中的寄存器值复制到 SimState 中。\n\n将具体进程的内存映射与 Angr 在启动期间加载的内存映射同步。\n\n\n\nSYMBION Exploration Technique：提供用户使用 Symbion 的 API ，通过这些 API ，用户指定 PoI 的地址，在具体执行到达 PoI 后，Symbion 切换为符号执行。\n\n\n简而言之，在 Symbion 的工作流程中，各组件的作用为：\n\n用户通过 SYMBION Exploration Technique 指定PoI。\n\n程序经过具体执行到达到 PoI 后暂停， Concrete SimPlugin 根据具体执行环境来创建一个SimState。\n\nAngr 通过符号执行，计算到达下一个 PoI 的可行解。\n\nSimEngineConcrete 用 Angr 算出来的结果修改具体进程中的变量，恢复具体执行直到下一个PoI。\n\n\n二、示例分析Symbion 官方示例：test_concrete_not_packed_elf64\n示例使用的二进制：not_packed_elf64\n二进制没有给源码，通过 IDA 逆向源码，并用 AI 改写，得到 C 源码如下，源码中取 dest 变量中的一串数值做判断，不同的分支触发不同的print。\n\n\n在 Symbion 的示例代码中，首先通过具体执行到达 BINARY_DECISION_ADDRESS，然后用符号执行探索从BINARY_DECISION_ADDRESS 到DROP_STAGE2_V2的路径。\n\n\n在符号执行求解成功后，再将求解结果传递给具体执行环境，并启动具体执行，即可到达DROP_STAGE2_V2：\n\n\n结合 CFG 和源码可以看到，符号执行的起点 BINARY_DECISION_ADDRESS 对应源码图右侧 55 行，符号执行的终点 DROP_STAGE2_V2 对应源码图右侧 77 行。通过 Symbion，实现了对二进制按指定路径的进行分析的目的。\n\n\nSymbion 的示例代码中，涉及到很多内存地址操作，需要结合 IDA 的反编译源码来看：\n\n\n\nline 2：启动具体执行，到 BINARY_DECISION_ADDRESS 停下，即 IDA 反编译源码第 67 行代码\n\nline 3：从具体执行环境的获取寄存器中的栈指针sp，指向栈顶（即栈开始的位置）\n\nline 4：从栈顶 sp 开始读取 20 个字节的内存，这块内存包括反编译源码中的变量 i 和v5\n\nline 5：判断是否为符号变量，此时为具体执行环境，所以不是符号变量\n\nline 7：定义符号变量，变量名为arg0，大小为 32 字节\n\nline 8：用 symbolic_buffer_memory 指向具体执行环境中 rbp-0xc0 的内存地址，它对应 IDA 反编译源码中的数组 s 的起始地址。\n\nline 10：从 symbolic_buffer_memory 开始加载 36 个字节的内存\n\nline 11：判断是否为符号变量，此时为具体执行环境，所以不是符号变量\n\nline 12：将 angr0 存储到symbolic_buffer_memory，将符号变量与具体执行环境的内存地址关联起来\n\nline 15：从 symbolic_buffer_memory 开始加载 36 个字节的内存\n\nline 16：判断是否为符号变量，因为 把 angr0 保存到这块内存，所以是符号变量\n\nline 19：符号执行状态初始化\n\nline 37：启动符号执行\n\n\n可以看到，Symbion 在切换具体执行环境和符号执行环境时，是通过内存地址把变量的具体值和符号值对应起来。需要结合 IDA 反编译的源码中给出的变量地址和内存大小，人工设置符号执行中所需要的符号变量，难以实现自动化。","dateCreated":"2024-02-27T16:33:24+08:00","dateModified":"2024-04-09T15:14:40+08:00","datePublished":"2024-02-27T16:33:24+08:00","description":"Symbion 是 Angr 的一款插件，可以实现具体执行与符号执行交替运行","headline":"交替符号执行工具——Symbion 初探","image":[],"mainEntityOfPage":{"@type":"WebPage","@id":"https://jiliguluss.github.io/2024/02/27/Symbion%E5%88%9D%E6%8E%A2/"},"publisher":{"@type":"Organization","name":"一瓢清浅","sameAs":["#about","https://github.com/"],"image":"photo.jpg","logo":{"@type":"ImageObject","url":"photo.jpg"}},"url":"https://jiliguluss.github.io/2024/02/27/Symbion%E5%88%9D%E6%8E%A2/","keywords":"Angr, 安全, 符号执行"}</script>
     <meta name="description" content="Symbion 是 Angr 的一款插件，可以实现具体执行与符号执行交替运行">
 <meta property="og:type" content="blog">
 <meta property="og:title" content="交替符号执行工具——Symbion 初探">
@@ -29,10 +29,10 @@
 <meta property="og:image" content="https://jiliguluss.github.io/2024/02/27/Symbion%E5%88%9D%E6%8E%A2/not_packed_elf64%E6%8C%87%E5%AE%9A%E8%B7%AF%E5%BE%84.png">
 <meta property="og:image" content="https://jiliguluss.github.io/2024/02/27/Symbion%E5%88%9D%E6%8E%A2/not_packed_elf64%E7%A4%BA%E4%BE%8B%E4%BB%A3%E7%A0%81%E5%88%86%E6%9E%90.png">
 <meta property="article:published_time" content="2024-02-27T08:33:24.000Z">
-<meta property="article:modified_time" content="2024-04-09T07:00:01.486Z">
+<meta property="article:modified_time" content="2024-04-09T07:14:40.547Z">
 <meta property="article:author" content="一瓢清浅">
-<meta property="article:tag" content="安全">
 <meta property="article:tag" content="Angr">
+<meta property="article:tag" content="安全">
 <meta property="article:tag" content="符号执行">
 <meta name="twitter:card" content="summary">
 <meta name="twitter:image" content="https://jiliguluss.github.io/2024/02/27/Symbion%E5%88%9D%E6%8E%A2/symbion%E4%B8%8A%E4%B8%8B%E6%96%87%E5%88%87%E6%8D%A2.png">
@@ -280,7 +280,7 @@ <h1 class="post-title">
         <div class="main-content-wrap">
             <!--excerpt-->
 
-<h2 id="一、原理"><a href="# 一、原理" class="headerlink" title="一、原理"></a>一、原理 </h2><p> 原始论文：<a target="_blank" rel="noopener" href="https://seclab.cs.ucsb.edu/files/publications/gritti2020_symbion.pdf">SYMBION: Interleaving Symbolic with Concrete Execution</a></p>
+<h2 id="一、原理介绍"><a href="# 一、原理介绍" class="headerlink" title="一、原理介绍"></a>一、原理介绍 </h2><p> 原始论文：<a target="_blank" rel="noopener" href="https://seclab.cs.ucsb.edu/files/publications/gritti2020_symbion.pdf">SYMBION: Interleaving Symbolic with Concrete Execution</a></p>
 <p>官方博客：<a target="_blank" rel="noopener" href="https://angr.io/blog/angr_symbion/">symbion: fusing concrete and symbolic execution</a></p>
 <h3 id="1- 背景"><a href="#1- 背景" class="headerlink" title="1. 背景"></a>1. 背景 </h3><p> 符号执行可以用来获取走到指定程序区块的可行输入，但是符号执行在实际应用中面临很多挑战：</p>
 <ol>
@@ -343,7 +343,7 @@ <h3 id="3- 实现"><a href="#3- 实现" class="headerlink" title="3. 实现"></a
 <li><p>SimEngineConcrete 用 Angr 算出来的结果修改具体进程中的变量，恢复具体执行直到下一个<code>PoI</code>。</p>
 </li>
 </ol>
-<h2 id="二、示例"><a href="# 二、示例" class="headerlink" title="二、示例"></a>二、示例</h2><p>Symbion 官方示例：<a target="_blank" rel="noopener" href="https://github.com/angr/angr-targets/blob/master/tests/test_concrete_not_packed_elf64.py">test_concrete_not_packed_elf64</a></p>
+<h2 id="二、示例分析"><a href="# 二、示例分析" class="headerlink" title="二、示例分析"></a>二、示例分析</h2><p>Symbion 官方示例：<a target="_blank" rel="noopener" href="https://github.com/angr/angr-targets/blob/master/tests/test_concrete_not_packed_elf64.py">test_concrete_not_packed_elf64</a></p>
 <p>示例使用的二进制：<a target="_blank" rel="noopener" href="https://github.com/angr/binaries/blob/master/tests/x86_64/not_packed_elf64">not_packed_elf64</a></p>
 <p>二进制没有给源码，通过 IDA 逆向源码，并用 AI 改写，得到 C 源码如下，源码中取 <code>dest</code> 变量中的一串数值做判断，不同的分支触发不同的<code>print</code>。</p>
 <img src="/2024/02/27/Symbion%E5%88%9D%E6%8E%A2/%E4%BA%8C%E8%BF%9B%E5%88%B6%E9%80%86%E5%90%91%E6%BA%90%E7%A0%81.png" class="">