高效的空间内存安全

将整个程序迁移至受检指针可带来空间内存安全（spatial memory safety）的优势，即指针不得越界访问缓冲区。Checked C编译器（基于clang扩展实现）会在受检指针解引用（加载/存储）时插入运行时检查，确保：

  1. 指针非NULL

  2. 对于arr或ntarr类型，解引用操作位于声明的边界范围内

例如代码if (n>0) a[n-1] = ...中，写入地址为𝛼 = a + sizeof(int)×(n-1)。若a的边界为count(u)，编译器会插入检查以确保解引用前满足a ≤ 𝛼 < a + sizeof(int)×u。检查失败将抛出异常。

LLVM通常能优化消除这些插入的检查。假设上述代码被外层条件包裹，如if (n<u) if (n>0) a[n-1] =...，此时由于外层条件n<u已确保解引用在边界内，插入的检查可被移除。程序员还可使用动态边界转换dynamic_bounds_cast<T>(e, b)辅助优化——该代码将e转换为T类型，并动态检查e为NULL或给定边界b是e当前边界的子范围。这种转换实质上是向编译器静态声明一个可通过动态验证的事实，特别适用于将循环内的检查外提（hoist）。

实际性能表现优异：根据小型基准测试集[Tarditi et al. 2018]的实验数据，平均运行时开销仅为X%（具体数据未在原文显示，此处保留原文引用格式）。

1 void baz(int *q,

2 int *c, int len) {

3 for (int i = 0; i

4 q[i] += *c;

5 }

6 }

7

8 extern void recordptr(void *x);

9

10 static int *g = 0;

11

12 void foo(int *p, int n) {

13

14

15 int m = 0;

16 recordptr(p);

17 g = p;

18 baz(p,&m,n);

19

20 }

21

22 void bar(int z) {

23 int *r =

24 malloc(sizeof(int)*z);

25 foo(r,z);

26 baz(r,g,z);

27 }

(a) Original C code

void baz(array_ptr q: count(len),

ptr c, int len) checked {

for (int i = 0; i

q[i] += *c;

}

}

extern void recordptr(void *x);

static int *g = 0;

void foo(int *p: itype(array_ptr)

count(n),

int n) {

int m = 0;

recordptr(p);

g = p;

baz(assume_bounds_cast>

(p, count(n)),&m,n);

}

void bar(int z) {

array_ptr r: count(z) =

malloc(sizeof(int)*z);

foo(r,z);

baz(r,assume_bounds_cast>(g),z);

}

(b) After initial conversion with marked root causes ()

void baz(array_ptr q: count(len),

ptr c, int len) checked {

for (int i = 0; i

q[i] += *c;

}

}

itype_for_any(T) extern void

recordptr(void *x : itype(array_ptr));

static ptr g = 0;

void foo(array_ptr p: count(n),

int n) checked {

int m = 0;

recordptr(p);

g = p;

baz(p,&m,n);

}

void bar(int z) checked {

array_ptr r: count(z) =

malloc(sizeof(int)*z);

foo(r,z);

baz(r,g,z);

}

(c) Complete conversion by 3C after manually fixing root causes.

向后兼容性讨论

Checked C的设计灵感源自Deputy [Condit et al. 2007; Zhou et al. 2006]和Cyclone [Jim et al. 2002]等安全C方言，其创新点在于支持渐进式迁移。通过与传统C语言保持向后兼容，Checked C允许逐步替换现有程序中的指针类型。例如以下代码是合法的Checked C：

空间内存安全检查仅针对受检指针类型（如上述代码中的p）插入。

对于未完全迁移的程序，空间安全性保证是局部的。程序员可将代码区域（整个文件、单个函数或代码块）标记为受检区域（通常通过_Checked注解实现）。这些区域必须仅使用受检指针类型并遵守其他限制（如禁用变参函数）。Ruef等人[2019]与Li等人[2022]已在其形式化模型中证明：若运行时发生安全违规，问题根源必定来自非受检代码的执行。因此，当整个程序处于受检区域时可确保空间安全；对于部分迁移的程序，受检区域执行比例越高，可利用漏洞的风险越低。

2.4 互操作类型（itypes）与可信转换

Checked C提供互操作类型（itypes）以便为传统C函数标注预期的受检类型。例如标准库函数strlen的Checked C版本声明为：

该类型表明：传统代码可传入char*，而Checked C调用方应传入nt_array_ptr<char>。

互操作类型也可用于函数定义。当函数定义位于受检区域时，其参数按受检类型进行类型检查；否则按传统类型检查。编译器会确保itypes的自洽性（例如char *p : itype(ptr<int>)会被拒绝）。

互操作类型的语义支持渐进式迁移：

  1. 若需迁移模块A（调用模块B的未迁移函数foo），可为foo添加itype注解

  2. 迁移后的模块A会将foo调用视为受检类型

  3. 后续迁移模块B时，将foo函数体置于受检区域后，其参数自动按受检类型处理

  4. 当所有调用方完成迁移后，可将itype替换为完整受检类型

对于非受检区域的函数，其itype标注是可信假设——若函数实现不符合标注的受检类型语义，仍可能导致空间安全违规。例如，若将C函数foo标注为void foo(int *x: itype(array_ptr<int> count(8)))，但其实际需要长度为10的数组，受检区域的调用方可能传入过短数组而不会触发警告。这种情况与安全语言的FFI（外部函数接口）机制面临的问题本质相同——安全代码的正确性依赖于外部代码的准确注解。

在非受检区域中，程序员可使用assume_bounds_cast<T>(e, b)将e转换为类型T并指定边界b。该操作在编译时行为与动态边界转换相同，但不执行运行时检查，可能引发不健全性。受检区域内函数的itype可视为对非受检调用方参数隐式应用的assume_bounds_cast。

<

通过3C工具迁移C至Checked C

我们的目标是将传统C程序迁移至Checked C。虽然全自动化转换是理想方案，但实际中我们采用迭代式半自动化方法。

3.1 迁移 = 注解 + 重构

迁移工作包含两类变更：
注解：保持代码逻辑不变，仅将传统C类型替换为受检类型，添加边界注解和类型转换，标记（非）受检区域。例如下图表1的(a)(c)部分：(a)为原始C代码，(c)为经3C工具转换后人工修复根本问题的最终版本。

重构：修改代码结构以满足Checked C的要求。例如：

（注：原文Listing 1的示例代码未完整呈现，此处保留其结构化引用格式；实际翻译时应补全示例代码的完整内容）

性能表现

基准测试显示平均运行时开销仅为8.6%（极端案例49.3%），而FreeBSD的UDP/IP协议栈移植后甚至实现零开销[Duan et al. 2020]。Ruef等人[2019]和Li等人[2022]的形式化模型证明：完全迁移的Checked C程序具有空间安全性——程序要么无限运行，要么返回终值，要么因NULL/越界异常终止，永远不会因误将整数作为受检指针解引用而卡死。对于部分迁移的程序，安全性保障与受检区域的代码覆盖率成正比。

int resize_buf(char **buf, unsigned *sz) {

unsigned news = round_up(*sz, 64);

char *newbuf = NULL;

newbuf = realloc(buf, news);

*buf = newbuf;

*sz = news;

return newbuf != NULL;

}

(a) Original code

int resize_buf(ptr: count(*sz)> buf,

ptr sz) {

unsigned news = round_up(buf->sz, 64);

array_ptr newbuf: count(news) = NULL;

... // as above

}

(b) Invalid Annotations

typedef struct {

array_ptr buf: count(sz);

unsigned sz;

} SIZEBUF;

int resize_buf(ptr buf) checked {

unsigned news = round_up(buf->sz, 64);

array_ptr newbuf: count(news) = NULL;

newbuf = realloc(buf->buf, news);

buf->buf = newbuf;

buf->sz = news;

return newbuf != NULL;

}

// Refactor callers of resize_buf ...

(c) Refactored and Annotated Checked C

代码清单2：通过重构与注解实现迁移

（前文所述）前者是原始C代码，后者是最终完成的Checked C转换版本。注意转换后的函数baz：其代码逻辑未变，但参数类型已改为受检类型，且函数体被标记为_Checked区域。

虽然仅靠注解可能满足部分需求，但通常需要先重构代码才能通过Checked C的校验。以代码清单2(a)为例：buf是指向数组的指针，其（原始及更新后的）大小存储在*sz中。尝试将其注解为清单2(b)的形式会被Checked C拒绝，因为边界注解不允许用于嵌套指针（此处*buf即为数组指针）。因此必须进行重构。实践中（如第6.6节所述），稳健的做法是将缓冲区与其长度封装为结构体并调整调用方，如清单2(c)所示。

完全自动化转换虽理想但难以实现。以清单2为例，自动化重构需准确推断*buf与长度*sz的关联，将其抽象为结构体并修改所有调用方——这可能引发"多米诺效应"式的连锁重构，任何失误都会导致代码混乱或转换失败（这也是C语言重构工具稀少的原因之一）。

3.2 迁移方法论

鉴于全自动转换不现实，我们设计了需要人工介入的迁移流程（图1示意整体过程），分为两个阶段：

第一阶段：

  1. 运行3C工具：自动将指针转换为受检类型并添加边界注解

  2. 分析未转换指针的根因：3C会按影响程度排序输出根因列表

  3. 通过重构修复根因：可能是局部调整或系统性修改，可能需手动添加Checked C注解
    每次修复后重新运行3C，迭代推进转换进度。所有修改后的代码均可正常编译测试。

例如对清单1(a)运行3C会生成1(b)，可见指针g（第10行）和p（第12行）未被转换（后者因itype保留为传统类型）。3C指出根因是recordptr(p)调用——该调用将p转为void*可能导致不安全操作，随后p被赋给g。

Checked C 使用