C*: 统一编程与验证的C语言

# C语言编程与验证的统一
**来源**：https://arxiv.org/html/2504.02246  
**DOI**：XXXXXXX.XXXXXXX (https://doi.org/XXXXXXX.XXXXXXX)  
**会议**：请确保输入您权限确认邮件中的正确会议标题；2018年6月3日–5日；纽约州伍德斯托克  
**ISBN**：978-1-4503-XXXX-X/18/06  

**作者**：  
庄嘉毅 (Jiayi Zhuang)  
单位：北京大学，中国北京  
陈厚金 (Houjin Chen)  
单位：北京大学，中国北京  
樊金凯 (Jinkai Fan)  
单位：北京大学，中国北京  
徐文博 (Wenbo Xu)  
单位：北京大学，中国北京  
王志毅 (Zhiyi Wang)  
单位：北京大学，中国北京  
王迪 (Di Wang)  
单位：北京大学，中国北京  
曹钦翔 (Qinxiang Cao)  
单位：上海交通大学，中国上海  
熊英飞 (Yingfei Xiong)  
单位：北京大学，中国北京  
赵海燕 (Haiyan Zhao)  
单位：北京大学，中国北京  
胡振江 (Zhenjiang Hu)  
单位：北京大学，中国北京  

**收到日期**：2009年6月5日  

#### 摘要  
鉴于系统软件的安全关键性和底层特性，确保其正确功能是形式化验证研究和应用的首要关注点。尽管验证工具已取得进展，但传统程序员很少参与其自身代码的验证，导致已验证软件的开发和维护成本更高。程序员参与验证实践的一个主要障碍是编程与验证实践在环境和范式上的脱节，这限制了可访问性和实时验证。我们引入了 C⋆（C-star），一种用于C编程的证明集成语言设计。C⋆ 扩展了C语言，赋予其验证能力，由符号执行引擎和LCF风格的证明内核提供支持。它通过允许程序员在实现代码旁嵌入证明代码块，支持对当前证明状态的交互式更新，从而实现实时验证。其富有表现力且可扩展的证明支持允许用户构建可复用的逻辑定义、定理和可编程证明自动化库。至关重要的是，C⋆ 使用C作为通用语言，统一了实现和证明代码的开发。我们实现了C⋆ 的原型，并在一组具有代表性的小型C程序和一个具有挑战性的实际案例（pKVM伙伴分配器的 `attach` 函数）上进行了评估。结果表明，C⋆ 支持验证广泛的C语言编程惯用法，并能有效处理现实场景中的复杂推理任务。  

#### 关键词  
软件验证、实时验证、C编程、LCF风格定理证明、分离逻辑、符号执行  

## 1. 引言  

### 背景  
系统软件构成了现代计算的基础设施，为所有更高级别的应用程序提供底层基础。鉴于其关键作用，近年来系统软件组件的形式化验证取得了显著进展（Leinenbach and Santen, 2009；Tao et al., 2021；Li et al., 2021；Klein et al., 2014；Xu et al., 2016；Gu et al., 2016；Amani et al., 2016；Chen et al., 2015；Leroy, 2009；Kumar et al., 2014；Protzenko et al., 2020；Ramananandro et al., 2019）。在本文中，我们专注于用C编程语言实现的软件的验证。C语言因其可预测的性能、对系统资源的精细控制以及大量已用其编写的关键代码而被广泛使用。C程序的验证框架和工具链已取得重大进展（Greenaway et al., 2014；Zhou et al., 2024；Mansky and Du, 2024；Leroy, 2009；Appel, 2011；Sammler et al., 2021；Pulte et al., 2023；Jacobs et al., 2011；Gruetter et al., 2024；Kirchner et al., 2015；Cohen et al., 2009；Protzenko et al., 2017）。在形式化验证软件组件和验证工具开发方面的巨大进展，已经证明了大规模验证的可行性，并使我们更接近所有关键软件都应经过验证的愿景（Hoare et al., 2009）。尽管取得了这些成功，形式化验证软件项目仍然成本高昂，因为它们需要具有深厚专业知识的专业团队，并且通常需要数人年才能完成（Leroy, 2009；Klein et al., 2014）。为了更广泛地采用验证实践，必须降低已验证软件的开发和维护成本。高成本的一个重要来源是**程序员参与的缺乏**，他们承担了大部分实现工作，却很少参与其自身代码的验证。  

### 现有方法  
程序员参与不足的一个原因是，C程序的验证通常需要一个外部环境，例如 Coq 等交互式定理证明器，这要求程序员学习与C编程体验截然不同的证明范式。此类别中的示例包括 AutoCorres（Greenaway et al., 2012）、VST（Appel, 2011）及其最近在 Iris 中的变体（Mansky and Du, 2024），以及 Live Verification 框架（Gruetter et al., 2024）。前三者将现有C程序翻译成元逻辑中的某种逻辑表示（单子浅层嵌入或深层嵌入），然后要求程序员在底层的定理证明器中围绕这些表示进行证明。Live Verification 框架选择了另一种方法，即在证明过程中懒惰地、增量地组合程序，依赖于 Coq 中特定的元变量存在机制来表示部分构造的程序。  

为了鼓励更多程序员参与，其他C验证工具提供了编程与验证的语言级集成，使验证过程对程序员更易于访问。主要有两类：（i）**基于断言的验证器**，如 Frama-C（Kirchner et al., 2015）和 VST-A（Zhou et al., 2024）；以及（ii）**基于高级类型的验证器**，如 RefinedC（Sammler et al., 2021）和 CN（Pulte et al., 2023）。这些工具允许程序员在规格说明之外，为C程序添加中间断言（例如，循环不变式）或高级类型（例如，所有权类型和精炼类型）以指导验证过程。这些工具通常是**（半）自动化的**，这意味着它们使用断言或类型检查器，借助程序员提供的注释来自动验证程序是否符合规格说明。然而，当自动化能力不足时，程序员又需要切换到外部定理证明环境来完成验证（例如，在 Coq 中（Zhou et al., 2024；Sammler et al., 2021；Pulte et al., 2023））。为了缓解这个问题，VeriFast（Jacobs et al., 2011）——一个用于C程序的基于断言的自动化验证器——提供了有限的证明支持，允许程序员使用一组固定的证明命令注释程序，并编写幽灵引理函数来执行某些形式的归纳推理。然而，VeriFast 缺乏程序员和证明专家协作验证底层系统软件所需的证明支持的表达力和可扩展性。  

### 我们的目标  
如上所述，目前缺乏适合传统系统程序员的令人满意的验证工具。在本文中，我们的目标是设计并实现一个新的C验证工具，满足以下两个标准：  
- •它应提供编程与验证的**语言级集成**；并且  
- •它应在C的编程范式内提供**全面的证明能力**。  

为了进一步增强C验证工具的可用性，我们考虑另一个标准：  
- •它应支持**实时验证**，即该工具应能在每个程序点提供程序状态的静态摘要，并允许程序员在证明过程中检查每个中间证明状态。  

### 我们的方法  
在本文中，我们提出了 C⋆，一种证明集成语言，在C语言中嵌入了成熟的验证和证明能力。我们下面重点介绍 C⋆ 的三个关键设计。  
- •我们采用了基于断言的设计，允许程序员使用**分离逻辑**断言注释程序，并结合**前向符号执行**，它抽象了具体语义的复杂性，并在处理程序片段后维护符号程序状态的静态摘要。  
- •我们将C编程语言与**高阶逻辑**的**LCF风格证明支持**集成，为编程形式化证明和转换符号状态提供了全面且可扩展的接口，便于使用C语言的全部能力开发高级推理抽象——作为**证明支持库**。  
- •凭借前两个设计，C⋆ 已准备好支持实时验证：前向符号执行在每个程序点提供符号程序状态的摘要，而LCF风格的证明支持允许程序员使用熟悉的C编程构造来检查和操作证明状态。  

我们实现了 C⋆ 的原型，并在一组C程序上进行了评估，以展示 C⋆ 在开发已验证程序方面的实用性。具体来说，我们的评估表明 C⋆（i）支持系统编程惯用法和C语言特性的很大子集，（ii）为高级所有权和功能推理提供了足够的表达力，并且（iii）能够验证现实的C程序。  

### 贡献  
在本文中，我们做出以下贡献：  
- •我们提出了一种证明集成语言设计，将规格说明和证明代码嵌入C程序中，在C的编程范式内提供全面的推理能力，从而使程序员能够参与形式化验证实践。  
- •我们通过扩展C语言并整合两个成熟的组件：一个符号执行引擎和一个LCF风格的证明内核，将两者接口连接以创建一个轻量级但强大的验证工作流，从而实现了我们的设计作为 C⋆ 工具链。  
- •我们使用文献中的一组基准程序和一个真实的案例研究评估了我们的 C⋆ 实现，以表明借助 C⋆ 的标准证明支持库，它在开发已验证C程序方面是有效的。  

## 2. C⋆ 导览  

在本节中，我们将为读者展示在 C⋆ 中开发一个已验证C程序的导览。我们以图中所示的 `clear` 函数作为运行示例，其期望功能是从基地址 `to` 开始重置 `len` 个连续字节。`clear` 的实现代码包括第3、6、8、10、17、19、20、22和24行；其他行是验证特定的代码。在实现代码中，程序员在第8行声明了一个局部变量 `i`，然后是一个从第10行到第22行的循环，每次循环迭代将基地址 `to` 起第 `i` 个字节设置为零，并将 `i` 递增1，直到 `i` 达到函数参数 `len`。我们以引导读者遵循 C⋆ 工作流进行增量开发的方式解释验证特定的代码。我们的解释将遵循第1节（https://arxiv.org/html/2504.02246#S1）中提到的三个标准：第2.1节（https://arxiv.org/html/2504.02246#S2.SS1）关于编程与验证的语言级集成，例如用户如何为 `clear` 编写规格说明和断言；第2.2节（https://arxiv.org/html/2504.02246#S2.SS2）关于通过C编程实现的全面证明能力，例如用户如何证明 `clear` 的实现符合其规格说明；以及第2.3节（https://arxiv.org/html/2504.02246#S2.SS3）关于实时程序验证，例如 C⋆ 在增量开发过程中如何辅助用户。  

```c
1 #include "cstarlib.h"
2 #include "clear.h"
3 void clear(void* to, int len)
4 [[require('fact(len >= 0) ** undef_array_at(to, Tchar, len)')]]
5 [[ensure('array_at(to, Tchar, replicate(len, 0))')]]
6 {
7   «term params='data_at(&"to", Tptr, to) ** data_at(&"len", Tint, len)';»
8   int i = 0;
9   «»
10   while (i < len) {
11     «pre='array_at(to + i, Tchar, replicate(len - i, 0))'»
12     ((byte*)(to))[i] = 0;
13     «post='array_at(to, Tchar, replicate(i, 0) * replicate(len - i, 0))'»
14     i++;
15   }
16 }
```  

#### 语言级集成：编写规格说明  
C⋆ 的一个基本设计是**语言级集成**，允许程序员直接在C源代码中编写规格说明。在C⋆ 中，我们使用 `[[require]]` 和 `[[ensure]]` 属性来指定函数的前置条件和后置条件。在示例中，`[[require('fact(len >= 0) ** undef_array_at(to, Tchar, len)')]]`（第4行）指定 `clear` 函数的前置条件是：一个事实 `fact(len >= 0)` 表示 `len` 是非负的，以及一个谓词 `undef_array_at(to, Tchar, len)` 表示从 `to` 开始的长度为 `len` 的连续字节的内存块，其中 `Tchar` 是C类型 `char` 的逻辑级表示。使用分离合取 `**` 组合这两个谓词，形成了预期的精确前置条件表述。  
- •C⋆ 使用 `[[ensure]]` 表示后置条件。在第5行，谓词 `array_at(to, Tchar, replicate(len, 0))` 表示一个长度为 `len` 的连续零的内存块，其中逻辑项 `replicate(len, 0)` 创建了一个包含 `len` 个零的列表。这再次精确地对应了我们之前讨论的预期后置条件。  

表 1. C⋆ 中使用的某些分离逻辑谓词的具体表示法。  

读者可能已经注意到前置条件和后置条件中 **引号** `‘...‘` 的使用。引号机制允许用户使用传统的具体语法构造分离逻辑谓词和其他逻辑级项，这类似于现有的基于断言的C验证器。但正如我们将在第2.2节（https://arxiv.org/html/2504.02246#S2.SS2）中所示，这些项在 C⋆ 中是 **一等公民** 值：除了直接用引号书写外，它们还可以从表达式计算得出，存储在变量中，作为参数传递，并使用C编程语言的全部能力进行操作。这是 C⋆ 与传统基于断言的C验证器的一个关键区别。  

编写前置条件和后置条件远未完成验证，因为通常难以找到一个算法来自动验证函数体是否“转换”前置条件到后置条件。与许多现有的C验证器类似，C⋆ 采用基于断言的设计来启用 **声明式** 风格的验证。