探索软件中的“怪异机器”：从漏洞利用到可证明安全

为什么“怪异机器”重要

攻击者寻找“怪异机器”来击败现代漏洞利用缓解措施。“怪异机器”是部分图灵完备的代码片段，它们固有地存在于函数和函数组周围的“松散契约”中。松散契约是指一段代码不仅实现了预期的程序功能，而且以一种程序状态变化超出应有范围的方式实现（即程序状态的前置条件集合比必要的大）。我们希望有“紧密契约”以获得更好的安全性，程序仅在确切预期的前置条件下改变状态，不会出现“怪异”或非预期的状态变化。

“怪异机器”是一段代码片段，会以程序员未预期的方式处理有效或无效输入。

不幸的是，松散契约存在于大多数软件中，是链表遍历、文件解析、小型单一用途函数以及复杂系统中出现的任何其他功能的副产品。现代攻击者利用这些非预期的计算，构建绕过漏洞利用缓解措施和安全检查的“怪异机器”。让我们看一个“怪异机器”的例子。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12


struct ListItem
{
    ListItem* TrySetItem(ListItem* new_item)
    {
        if (!m_next)
            m_next = new_item;

        return m_next;
    }

    struct ListItem *m_next = nullptr;
};

函数 ListItem::TrySetItem 看起来有以下前置条件：

必须传入 this 和 item，两者都是指针
this 和 item 必须是已分配和构造的 ListItem 实例

然而，一旦生成机器码，前置条件实际上是：

this 参数必须是指向至少 8 字节已分配内存的指针
必须传入第二个参数（item），但它可以是任何类型

这是一个松散契约的例子，这是我们编写代码方式的固有特性。攻击者如果覆盖了 m_next 指针，可以利用此函数检查任意地址的内存是否已设置：如果是，攻击者可能泄露内存；如果不是，攻击者可能设置内存。

漏洞用于改变程序执行或数据状态。此后的执行要么是怪异状态，要么是在非预期数据上操作的状态。

收紧契约

一种松散契约是“执行”契约，即程序中有效间接分支的可能地址集合。

1995 年的 Windows NT 是松散执行契约的一个例子，所有标记为“读取”的内存也隐含“执行”。这包括程序中的所有数据——不仅仅是代码。2003 年，微软在 Windows XP SP2 中引入不可执行数据（NX，DEP）时收紧了执行契约。微软在 2006 年 Windows Vista 中引入地址空间布局随机化（ASLR）时进一步改进了契约，该技术随机化可执行代码的位置。2016 年，Windows 8.1/10 引入了控制流防护（CFG），验证间接分支的前向边缘指向一组已批准的函数。

在下图中，很明显，有效的间接目标所剩无几。这种紧密的“执行”契约使得漏洞利用更加困难，对“怪异机器”的需求更大，显著增加了“怪异机器”的价值。如果我们能进一步收紧程序契约，将使“怪异机器”更难识别。

执行契约定义了程序的可执行区域（黄色）。随着契约的收紧，这些区域多年来已经减少。

“怪异”是什么样子

识别“怪异机器”是一个难题。当我们甚至不知道契约是什么时，如何识别松散契约？自动识别这些“怪异机器”将使我们能够正确分类漏洞是否实际上可利用，以及在缺乏“怪异机器”的情况下是否不可利用。

一种以编程方式描述“怪异机器”的方法是通过 Hoare 三元组。Hoare 三元组描述了一段代码的执行如何改变计算状态：进入新状态所需的前置条件以及描述如何离开状态的后置条件。当我们识别“怪异机器”时，可以通过移除它们或约束前置条件恰好符合状态预期来自动收紧此类契约。这将使我们更接近创建可证明安全的程序。

重新审视我们的例子，我们可以添加 dynamic_cast 来强制执行契约前置条件。如果我们分析代码片段作为 Hoare 三元组，我们会注意到函数执行的前置条件是松散的，因此任何地址都可以传递给函数。此外，后置条件不存在，因此一旦执行，函数将设置或返回内存，无论程序状态如何。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18


struct ListItem
{
    ListItem* TrySetItem(ListItem* new_item)
    {
        if (!dynamic_cast<ListItem*>(this) ||
            !dynamic_cast<ListItem*>(new_item)) {
                // 此路径不应被允许
                abort();
        }

        if (!m_next)
            m_next = new_item;

        return m_next;
    }

    struct ListItem *m_next = nullptr;
};

dynamic_cast 是运行时守卫，检查以验证函数是否在预期的指针上操作。这个新函数在漏洞利用中显然不如以前有用。

具有不精确定义前置条件的 Hoare 三元组允许发生“怪异”状态变化。通过改进输入检查来收紧这些前置条件将使这些状态无法实现。

那么我们如何找到它们？

在通往解决方案的道路上存在许多难题。首先是规模。我们不关心简单的测试用例，我们关心的是今天部署给数十亿人的真实代码：浏览器、操作系统、邮件客户端、消息应用程序。自动识别这些平台上的“怪异机器”是一个重大挑战。

给定一组可能的执行路径及其对象创建和访问模式，我们必须识别具有特定和可控副作用的程序切片。这些切片本身必须是图灵完备的。这些“图灵 thunk”的行为在正常执行路径位置之外或不同数据状态下可能不同。为了扩展我们的分析，我们可以将问题分解为子组件。

从识别图灵 thunk 开始，分析它们的副作用，并确定它们的可达性。我们可以使用数据流分析和形状分析来识别这些“图灵 thunk”并测量它们的副作用。将测量这些已识别“怪异机器”的副作用，以确定这些候选“怪异机器”如何组合。对全局状态的改变可能改变后续“怪异机器”的执行。数据流提供基于受控输入可转换的路径。形状分析有助于重建堆对象、布局和对象之间的交互。这有助于确定生成执行路径到“怪异机器”所需的输入约束，以及执行“怪异机器”之前和之后的堆状态。

一旦识别出候选，可以根据特定功能和副作用进行优先级排序。我们可以使用符号执行和混合执行来验证这些候选，并使用机器学习按行为、执行约束和副作用对候选进行分组，以便后续查询更容易。

漏洞利用的未来

最终，“怪异机器”是漏洞利用的基本工具。随着程序变得更加复杂和缓解措施的堆积，“怪异机器”的重要性只会增加。在现实世界程序中找到这些图灵片段并枚举它们的属性将有助于下一代漏洞利用和安全。

一旦我们能够自动识别“怪异机器”，我们将有能力移除这些怪异状态，并确定程序的可利用程度。我们可能还能够证明特定漏洞不可利用。

解决方案的一部分是改进术语，需要成熟。解决方案的另一部分是进一步研究问题空间。虽然对该主题有兴趣，但我希望 DARPA 未来投资这一领域。

识别和分类“怪异机器”的工具和系统尚不存在。我们还有很多工作要做，但构建块已经存在。有了它们，我们将更接近解决明天的问题。

如果您想了解更多关于这一研究领域的信息，我建议您从以下出版物开始：

Weird machines, exploitability, and provable unexploitability
Exploit Programming: From Buffer Overflows to “Weird Machines” and Theory of Computation
Exploitation as Code Reuse: On the Need of Formalization
The Weird Machines in Proof-Carrying Code