Author: Evan Johnson, Maxwell Bland, YiFei Zhou, Joshua Mason, Stephen Checkoway, Stefan Savage, Kirill Levchenko
Source: USENIX Security 2021
Paper: pdf
假设：为了使固件成功启动，仅模拟固件预期的行为就足够了，并且可以自动推断出这种行为。
Jetset，使用符号执行来推断固件期望来自目标设备的行为。Jetset可以用C语言为硬件外设生成设备模型，允许分析人员在模拟器中启动固件。
Jetset成功应用在了代表三种不同架构、三种不同应用领域(power grid, avionics, and consumer electronics)和五种不同操作系统的固件中。
嵌入式系统难以在模拟器中运行，因为需要同特定的片内（on-chip）和片外（off-chip）外设进行交互，如I/O接口（GPIO）、传感器、通信接口。由于外围设备种类繁多，且没有关于硬件的具体文档，没办法为所有的硬件建模，导致无法模拟所有硬件行为。
然而，在许多情况下，测试人员关心的代码并不是与外围设备交互的代码。虽然不能完全忽略外设，但所有设备的正确行为可能不是必需的（但硬件初始化必须成功，系统才能成功启动）。例如，对目标如何响应网络流量感兴趣的测试人员可能不需要执行环境精确地模拟系统 GPIO 端口或其他通信接口。
Jetset使用符号执行来生成外设取值，使程序运行到特定的代码位置。如在评估中，目标是到达代码跳转到用户空间的地址。关键见解：与外围设备交互的固件代码隐式编码了设备必须如何运行才能启动系统。Jetset使用符号执行引擎Angr来推断硬件设备需要返回的值。使用有指导的符号执行来减少路径爆炸，使用禁忌搜索（Tabu Search）的变体来选择路径，同时选择到达目标最近的距离。
Jetset的输入是一个固件镜像、固件入口地址、固件运行想要达到的目标地址、内存架构（RAM地址和memory-mapped I/O地址）。Jetset只需要模拟器支持CPU架构，不需要任何硬件相关的知识。
Evaluate中使用了13个示例程序：波音737飞行器通信管理组件（基于AMD 486）、运行在Raspberry Pi 2（基于ARM）中的Linux、运行在BeagleBoard-xM（基于ARM）上的第一阶段的bootloader、SEL-751 Feeder Protection Relay (Motorola ColdFire-based system)、9个P2IM中使用的评估程序。这些程序拥有三种架构、五种不同操作系统。对于每个目标，Jetset 会推断固件完成其启动序列所需的外设的行为。接下来，Jetset生成适用于QEMU的 C代码。
Jetset 操作有两个阶段：外设推断和外设合成。在外设推断阶段，Jetset使用符号执行来推断设备的预期行为。然后，在外设合成阶段，推断阶段的输出用于创建在模拟器中适配的代码。
Jetset使用符号执行来推断运行到特定代码点，外设寄存器需要返回的值是什么。
Jetset在仿真环境中运行固件。运行过程中，所有从MMIO地址空间读取的值都是不同的符号值，从同一地址读取两次也是不同的符号值。通过符号执行可以探索到固件的所有路径。当执行路径到达目标地址时，Jetset停止执行，推导出从设备寄存器读取值时产生的一组约束。
外设推导阶段的目标是找到一条路径可以运行到目标地址。但是符号执行会遇到路径爆炸问题，因此，Jetset使用引导符号执行来优先探索最有希望的路径。具体来说，Jetset使用目标程序的控制流图(CFG)来计算每个基本块与目标的距离，距离为基本块和包含目标地址的块之间的CFG边数。在一个分支，Jetset选择探索与目标距离较小的基本块。搜索路径在到达目标、触发系统重置或进入无限循环时终止。为了检测无限循环，Jetset在CFG级别检查一组简单的无限循环模式（4.4节）。
逆向工程无法恢复完整的CFG，因为有间接跳转（如函数指针）。首先探索到间接跳转的所有路径，然后解决跳转，然后生成更多CFG（5.1.3节）。
Jetset在过程间CFG上计算调用上下文敏感距离函数以指导其搜索，这个距离是指令级别的距离。调用上下文相关的距离函数是一种仅包含遵循有效调用链的路径的函数，即从返回的所有调用都返回到正确的位置。定义此距离函数是为了确保固件向前推进，并引导Jetset搜索最有效的启动顺序路径。
在推断阶段，Jetset周期性地注入中断。Jetset利用了这样一个事实，即精心设计的系统对中断的确切时间不敏感，并且编写ISR以优雅地处理虚假中断。Jetset在符号执行期间周期性地注入中断，以便在每个执行路径期间周期性地执行每个ISR。如果主执行线程恰好在等待 ISR 更新变量，Jetset最终将执行该ISR，并且线程可以继续进行。
当达到目标地址后，Jetset可以生成一个中断模型。
外设推断阶段的结果是一组对从固件启动所需的外设读取的值的约束。然后，Jetset使用Z3来查找满足这些约束的实例，从而生成一组具体值，这些值可以在执行期间响应外设读取。This al- lows Jetset to construct a light-weight, concrete device model, rendering peripheral inference a one-time cost per device.
每一个MMIO地址都有一个单独的跟踪，当Jetset达到一个跟踪队列的末尾时，返回跟踪队列的最后一个值。Jetset可以达到特定的地址，但是难以进行特定地址之后复杂的交互。
同推断阶段生成中断方法相同。
固件过于复杂难以分析所有的路径。本文的关注点在于达到一个安全相关的点。本文使用禁忌搜索来选择路径。禁忌搜索被用于搜索复杂的非线性搜索空间。Jetset使用禁忌搜索，因为它允许对特定于域的信息进行编码，以改善路径优先级（Jetset使用基于固件控制流图的距离函数）和回溯（Jetset使用专门的回溯规则来避免错误处理逻辑）。
禁忌搜索是由距离函数引导的深度优先搜索的变体：它保持在同一路径上，在每个决策点选择最近的选项，直到遇到终止条件。禁忌搜索编码了一个禁忌列表，该列表充当已知不良状态的阻止列表，充当 Jetset 将来可能回溯到的状态的过滤器。特别是，Jetset 不会将状态回溯到它已经访问过的位置。禁忌搜索还可以对回溯策略和终止条件等细节进行编码。
距离表现为两条指令之间指令的个数。从调用链从下到上，计算函数内的局部距离。函数调用相当于将函数展开，然后计算两个指令的距离。指令距离的查询输入为（pc，callstack）对。
Jetset的距离函数只是真实距离的一个近似值——它代表的是控制流图上的图距离，而不是到达目标需要执行的块数。使用 CFG 距离作为启发式方法是一种强大的指导执行技术，但它只是一种启发式方法——在某些情况下，更长的路径才是正确的路径。因此，Jetset 需要平衡它符合距离启发式的频率，以及它探索不遵循启发式的选择的频率。为此，Jetset 使用确定性方法在探索新选择和利用启发式之间取得平衡。它使用交替阈值 n——每 n 次 Jetset 访问一个位置，Jetset 都会选择一个次优决策。在实践中，发现交替阈值为3具有最佳性能。
Jetset 的搜索算法可能会将它引导到程序中的某个点，在该点到达目标变得不可行，它需要终止当前路径并回溯到先前的状态。 有两种不同的情况会发生这种情况。 Jetset 回溯的第一种情况是发生系统重置时； 系统重置不太可能以正确的启动顺序发生，系统重置时回溯允许 Jetset 避免启动循环。 Jetset 回溯的第二种情况是 Jetset 进入可静态检测的无限循环。
静态可检测的无限循环是这样一种情况，即使其中的所有路径都是可满足的，仍然没有出口。这些静态可检测的无限循环可以在控制流图上有效地检测到；例如，无法转义无条件分支到自身的单个基本块。Jetset 用断点标记所有这样的点，并在达到断点时回溯。
当Jetset 回溯时，它会回溯到最接近目标的最后一个未采用的符号分支。如果多个分支决策同样接近目标，则选择最近的一个。决策是以上下文敏感的方式识别的，因此如果在一个调用上下文下选择了特定决策而不是另一个，则 Jetset 仍可能在第二个调用上下文下回溯到该决策。
1、本文介绍的方法本质上来说相当于首先仿真固件找到一条从入口点到特定地址点的路径，该阶段外设输入为符号值，然后约束求解外设输入。然后再将求解到的外设值赋给外设寄存器，使其使用具体值运行到特定点。该方法只适用于系统初始化部分代码，不适用与复杂的用户逻辑。
2、面对复杂程序，如果将程序切片，及在一定范围内（如n个执行到的基本块）应用此方法是否可行。
3、此方法只能使程序延最短路径运行至特定的代码点，且只能运行初始化阶段代码。个人认为主要贡献在于使用了禁忌搜索在查找最短路径。