编程语言语义与内存安全

# 编程语言语义与内存安全 原文来源：https://burakemir.ch/post/formal-semantics/ 编程语言语义与内存安全 2026年8月21日 --- 你是否曾思考过，编程语言*究竟*是什么？ 人们常说，编程语言只是我们用来指令计算机执行任务的工具。我实在不喜欢这种比喻。那么请告诉我，这个工具是如何工作的？ 在大学里，我们可能学到一门语言由其**语法**和**语义**定义，以及用数学精确性来表述这些定义的方法。语法有语法规范，但语义呢？ ### 为何重要？ 内存安全，除此之外还能是什么！过去几年我一直在从事内存安全相关工作。作为Rust团队负责人，我协助推动了Google采用Rust语言；我代表Google参与内存安全标准讨论。我接触过对该话题持有各种观点的专业人士。我还参与了Carbon编程语言的设计讨论并为其实现贡献了一份微薄之力，尽管不确定这是否重要。目前我正处于职业过渡期，因此难得可以不用担心“非雇主观点”的免责声明。 对我而言，内存安全是编程语言领域的话题。我热爱编程语言！这是一个充满行话和惯例的狂野研究领域，大多数人难以企及。希望本文能稍作弥补。 内存安全本应是让编程语言研究大放异彩的契机！可惜，广泛的非技术因素让基于事实的讨论变得困难。 - 成人谈论安全时，通常指网络安全。防范攻击是主要关切和驱动力，仅靠惯例、测试、缓解措施远远不够。 - 安全问题基于风险权衡，因此常涉及经济学论证。 - 世界正被遗留代码淹没。 投资安全充满不确定性，即便变革势在必行。我们无需完全取代C和C++即可显著提升安全性，但这需要付出时间和资源代价。当争夺有限资源时，不仅有诚实者为艰难决策争论，也有推动私利者。 我认为学术界的编程语言研究者很像数学家，他们希冀自己的工作能被实践应用，期待有资金和影响力的人发现并善用其成果。 因此我也将如此！以下内容是邀请你回归编程*科学*的探索。如果你希望编译器和库正确且安全地工作，*必须有人*基于原则展开论证。 ### 深入形式语义 当你写下`x = y + 1`，我们如何形式化地定义其含义？实际上有三种主要视角：**操作语义**、**指称语义**和**公理语义**。 这些术语听起来学术而吓人，但作为开发者，你已直觉理解其概念——只是你知道它们的不同名称：*解释器*、*编译器*和*断言*。这些语言视角各有其用。 为解析这些概念，让我们创建一个微型玩具语言。它包含算术运算、不可变变量（`let`）和可变变量（`var`）。 以下是玩具语言的代码片段： ``` var x = 0; let y = 5 in x = y + 1 ``` *`x`是初始值为0的可变变量，`y`是绑定为5的不可变变量。最后我们更新`x`的值。* 现在，我们通过形式语义的三重透镜来审视这段代码。 --- ### 1. 操作语义：“解释器”视角 **核心问题：***我们如何逐步执行这段代码？* 操作语义通过描述程序在抽象机器上的执行过程来定义其含义。它更关注“如何运行”，而非“数学本质”。 如果你曾编写过解释器，你就在提供操作语义。虽然它可能不适合排版印刷于文章或书籍中，但一个程序确实能体现数学精确性定义的规则。研究者常使用一组逻辑规则（通常称为结构操作语义）来重写形式符号串。但本质上： 我们跟踪一个**状态**（可变变量到值的映射）和一个**环境**（不可变`let`绑定到值的映射）。 1. **初始状态：**`\{ x: 0 \}`, **环境：**`\{\}` 2. 评估`let y = 5`。将`y`加入环境。**状态：**`\{ x: 0 \}`, **环境：**`\{ y: 5 \}` 3. 评估`x = y + 1`。在环境中查找`y`（值为5），加1，并在状态中更新`x`。**状态：**`\{ x: 6 \}`, **环境：**`\{ y: 5 \}` **开发者为何关心：**操作语义是定义语言规范最常用的方式。我们期望代码执行时行为清晰明确。当ECMAScript规范描述JavaScript执行规则时，就采用了操作语义的形式。它回答：“这行代码执行时会发生什么？” --- ### 2. 指称语义：“编译器”视角 **核心问题：***请（用数学精确性）告诉我这段代码表示什么对象？* 指称语义采取不同路径——它不定义程序*如何*运行，而是将程序映射到其数学本质（即“指称”）。在形式语义中，这是一种数学概念，语义本质上是数学化的编译过程。 关键并非数学本身，而是翻译目标必须是我们已理解且无需进一步定义的对象。同时我们需要能判断两个翻译对象是否“相同”。 回到我们的小语言。我们不逐步执行代码，而是将每行代码翻译为数学函数： - `var x = 0`翻译为接收输入状态、返回`x=0`新状态的函数。 - `let y = 5`翻译为接收环境、返回`y=5`新环境的函数。 - `x = y + 1`翻译为接收状态和环境、查找`y`、加1并更新`x`的函数。 在指称语义中，整个程序就是这些数学函数的组合。 若用$S$表示状态、$E$表示环境，程序可表示为单一数学函数$P$： $$P(S, E) = S' \text{ 其中 } S'(x) = E(y) + 1$$ 注意我们从未讨论“逐步执行”，而是说：“该程序是将输入状态映射到输出状态的函数。”数学函数及其组合蕴含着神奇力量。 编译器的类比比表面更深：若将Rust语法规范和编译器交给只懂机器码和目标平台的人，他们能从中理解任意Rust程序的含义。当然，前提是编译器正确。因此仅靠编译器远远不够，我们需要其他语义定义来判断编译器是否正确。 **开发者为何关心：**指称语义便于数学化证明程序性质。若要证明两段代码执行完全相同，只需证明其翻译结果（如数学函数）相同。这也是Haskell等纯函数式语言的基础，其中我们将程序视为数学函数。 --- ### 3. 公理语义：“断言”视角 **核心问题：***代码执行前后，什么命题为真？* 公理语义完全忽略程序*如何*运行或表示何种数学函数，而是通过程序对逻辑命题的影响来定义其含义。 如果你曾编写单元测试或使用`assert`语句，你就在实践公理语义。 我们使用**霍尔三元组**，写作`\{P\} C \{Q\}`，意为：*若前置条件P在代码C执行前成立，则后置条件Q在执行后成立。* 审视我们的代码片段： ``` var x = 0; let y = 5 in x = y + 1 ``` 我们可以基于公理断言什么？ 1. 断言前置条件：`\{ True \}`（无需任何前提条件）。 2. 执行代码。 3. 断言后置条件：`\{ x == 6 \}` 因此霍尔三元组为：`\{ True \} var x = 0; let y = 5 in x = y+1 \{ x == 6 \}` 但如何*不执行代码*就确知后置条件为真？我们使用逻辑公理。例如赋值公理（`x = E`）指出：若要*执行后*使`\{ x == 6 \}`成立，则*执行前*`E == 6`必须成立（将`x`替换为`E`）。 **开发者为何关心：**公理语义是形式化验证和程序证明的基础。当欧洲航天局为飞船编写软件时，他们不仅进行测试，更用公理语义数学证明某些后置条件（如“舱门开启时推进器不会点火”）由代码保证。现代静态分析器和证明辅助工具（如Coq或Dafny）都重度依赖此视角。 --- ### 插曲：该用哪种透镜？ 你无需只选其一！每种语义模型提供不同工具解决不同问题： - **操作语义：**“如何执行？”联想*解释器*。适合语言设计者编写参考实现。 - **指称语义：**“数学意义是什么？”联想*数学编译器*。适合证明代码等价性。 - **公理语义：**“能证明什么为真？”联想*断言*。适合验证安全性和正确性。 形式语义不必是希腊字母的恐怖领域。通过将视角从“执行代码”转向“解释、翻译和证明”，你能更深刻理解日常工具的本质。 --- ### 未定义行为与内存安全的深渊 我想更进一步，将此与编译器及内存安全现实世界联系起来。 如果你编写C或C++，必然熟悉那个令人恐惧的术语——**未定义行为**。 内存安全问题（如缓冲区溢出、释放后使用、空指针解引用）都属于未定义行为。但在形式语义中，未定义行为究竟意味着什么？为何一位教授曾告诉我，C语言规范可理解为公理语义，尽管未定义行为感觉像操作语义的漏洞？ 原来，操作语义与公理语义是从同一硬币的两面观察未定义行为。 #### 操作视角：缺失的规则 从**操作语义**角度，编程语言由一组转换规则定义（如“若状态为X，则转移到Y”）。 未定义行为顾名思义：**规范中的空白。**这是平淡的声明“我们既不愿也无法预测接下来会发生什么”。规范空白与留待实现决定（“实现定义”）截然不同。 假设我们的玩具语言支持指针运算，我们编写访问数组的规则：“*若索引`i`在数组边界内，则返回对应值*”。 但若`i`越界呢？我们根本没写这条规则。在操作语义中，若程序进入无规则适用的状态，抽象机器就会“卡住”。规范未说明后续行为——程序可能崩溃、读取垃圾数据，甚至格式化硬盘。操作上这是黑洞。 #### 公理视角：虚空吞噬逻辑 那么，**公理语义**如何介入？那位教授很可能是通过霍尔逻辑（断言）视角审视C标准。 在公理语义中，我们定义语句如何影响前置/后置条件。对于正常语句，可写：`\{ x == 5 \} x = x + 1 \{ x == 6 \}` 但具有未定义行为的语句（如空指针解引用）如何公理化？ 在公理语义中，未定义行为由一条可怕但数学优雅的原则处理：**若安全执行的前置条件不满足，程序可执行任意操作。** 假设C标准公理为：“*解引用指针`p`时，`p`不能为null*”。 若我们编写*可能*解引用空指针的代码，则该代码块的前置条件被违反。在形式逻辑中，若从假前提出发，可证明任意结论为真（爆炸原理）。 因此未定义行为的霍尔三元组变为：`\{ False \} C \{ Anything \}` *（若前置条件为假，任意后置条件均为真）*。 #### 解决矛盾：编译器的后门 那么如何解决这矛盾？未定义行为究竟是缺失的操作规则，还是公理逻辑爆炸？ **二者兼有，这正是编译器行为如此的原因。** 现代C/C++编译器（如GCC和Clang）不仅解释代码，还依赖C标准的**公理语义**进行优化。 因为标准规定越界访问是未定义行为，编译器从公理角度假设你永远不会这样做。 经典案例： ``` int table[10]; for (int i = 0; i <= 10; i++) { table[i] = 0; } ``` 操作上，当`i`达到10时无规则适用。但编译器不会停止，它会审视公理。 编译器可能推理： 1. 访问`table[10]`是未定义行为。 2. 程序员不会编写含未定义行为的代码（因其违反语言前置条件）。 3. 因此`i`永远无法达到10。 4. 因此条件`i <= 10`恒真。 5. 因此这是无限循环！ 编译器可自由将其优化为硬编码无限循环，完全移除边界检查。公理空白允许编译器假设不可能之事。 注意这并非唯一可能行为。在Mac上，`clang`默认启用“-fstack-protector”，程序会在返回前终止。若禁用该选项，它将运行并可能写入非法内存。一切皆有可能！ 我们或许会想：“编译器告知此处存在未定义行为并报错，岂不是更好？”编译器作者是否“武器化”了未定义行为？在C语言早期，平台和实现众多，统一行为可能不现实。此例中我们易懂，但静态检查代码（无需运行）非常困难——无论是规范还是实现。C/C++标准作者选择了捷径，因此规范实际上允许“任意”行为。 基础也已变化。并发使一切更复杂。自2000年代中期，CPU采用多核架构和并发机制。多线程比这更早，但通过时间片实现。多核CPU中线程真正并行执行。此后理解程序执行需要规范描述并行线程。C/C++内存模型（二者不同）在语言规范发布*数十年*后才制定。 #### 内存安全的启示 这正是内存安全问题如此深刻的缘由。不仅是有缺陷的代码可能崩溃——若规范规定某操作导致崩溃（程序终止），这实际上很好处理。