警惕无处不在的"分歧表示"：编译器优化导致的代码语义分裂

当心！分歧表示无处不在！ - Trail of Bits博客

Trail of Bits最近发布了一篇关于特定版本SQLite中存在符号整数溢出漏洞的博客文章，该漏洞可实现任意代码执行并导致拒绝服务。在针对该漏洞开发概念验证利用程序时，我们注意到编译器对某个重要整数变量的表示在程序不同部分存在语义差异。这些差异导致变量溢出时产生不一致的解释，我们称之为"分歧表示"。

简单示例

以下是一个现实代码模式的简单示例，可能产生分歧表示：

int index_of(char *buf, char target) {
    int i;
    for (i=0; buf[i] != target; i++) {}
    return i;
}

index_of函数接收字符数组作为输入，循环遍历数组并递增i，直到找到第一个目标字符，然后返回该目标字符的索引。

如果目标字符出现在缓冲区的第一个INT_MAX字节内，函数将表现良好定义的行为。但如果函数扫描数组的前INT_MAX字节后仍未找到目标字符，i将递增超过int类型可表示的最大正值，即发生未定义行为。

分歧表示如何出现？

编译器可以对程序应用优化以提高性能。当编译器应用的程序优化导致单个源变量在输出程序中以不同语义表示时，就会出现分歧表示。

我们观察到的分歧表示实例都源于未定义行为（特别是符号整数溢出）。虽然程序员不应该编写具有未定义行为的程序，但我们主张即使在未定义行为的情况下，程序也应对相同值保持一致性解释。

发现分歧表示！

我们在尝试为CVE-2022-35737（我们在SQLite中发现的漏洞）开发概念验证利用时发现了第一个分歧表示。我们注意到概念验证利用在使用libsqlite3.so的调试版本（无优化编译）和优化发布版本时表现不同。

通过反汇编两个版本的库并分析漏洞附近代码，我们发现编译代码的差异源于源代码，特别是sqlite3_str_vappendf函数：

806 int i, j, k, n, isnull;
    ...
824 k = precision;
825 for(i=n=0; k!=0 && (ch=escarg[i])!=0; i++, k--){
826   if( ch==q )  n++;
827   if( flag_altform2 && (ch&0xc0)==0xc0 ){
828     while( (escarg[i+1]&0xc0)==0x80 ){ i++; }
829   }
830 }

在优化版本中，源代码变量i在循环中被表示为32位有符号整数，但在内部循环扫描Unicode字符时被表示为64位无符号整数。

寻找更多分歧表示

在流行代码库中发现分歧表示后，我们尝试了两种方法来识别其他潜在的分歧表示，并在SQLite和libxml2中找到了更多示例。

自底向上（编译二进制）搜索

我们编写了一个Binary Ninja脚本，模拟分歧表示的编译模式，并利用Binary Ninja的中级中间语言（MLIL）静态单赋值（SSA）形式提供的抽象。该脚本在SQLite和libxml2中发现了额外的潜在分歧表示。

自顶向下（源代码）搜索

我们使用CodeQL创建源代码查询，识别符合以下条件的源代码：

• 变量在循环外声明
• 变量在循环体内递增
• 变量用于在循环体内访问内存
• 变量在循环后再次使用

CodeQL在libxml2中发现了20个可能产生分歧表示的代码模式，其中两个（在xmlBuildURI中）也被Binary Ninja识别。

预防编译程序中的分歧表示

预防分歧表示的最佳方法是避免在程序中包含未定义行为。程序员应该使用不会溢出的数据类型来计数或访问数组（例如使用size_t或uintptr_t而不是int），并避免C程序员中常见的不幸实践：将错误条件与int函数的负返回值绑定。

结论

我们无法对与分歧表示相关的风险做出全面评估。有些基本上不可达的分歧表示可以被视为未定义行为的好奇心，而其他可能更具后果性，将原本良性的整数溢出转变为可利用漏洞，就像我们的SQLite漏洞案例一样。

感谢我的导师Peter Goodman，在我于Trail of Bits暑期实习期间，在追求漏洞和奇怪编译器行为方面提供的专家指导。