机器代码安全认证：浅嵌入与深嵌入

# 机器代码安全认证：浅嵌入与深嵌入 ## 1. 引言 Proof Carrying Code（PCC）是一种安全执行不可信代码的方案，它无需加密和可信第三方。代码生产者负责为程序添加注释并构建证明证书，以证明程序符合安全策略；代码消费者只需检查证书（机器可检查的证明）是否正确。 这个检查过程包含两个步骤： 1. 验证条件生成器（VCG）将带注释的程序转换为验证条件（VC），只有当程序在运行时安全时，该逻辑公式才可证明。 2. 证明检查器确保证书是 VC 的有效证明。 安全逻辑在 PCC 中具有多种用途： - 提供机器状态的形式化描述语言，用于编写注释或指定安全策略。 - 用于表达和证明验证条件。 对于某些安全策略，类型系统可充当安全逻辑，例如 Java 字节码验证。但对于更复杂的属性，如内存安全，类型系统可能需要与逻辑结合或扩展为类逻辑系统。 我们的方法使用一个小型通用的 VCG，并将其建模为 Isabelle/HOL 框架的一部分。该框架可实例化为各种机器语言、安全策略和安全逻辑。我们已对多种非平凡的安全策略进行了实例化，并验证了多个示例程序。本文聚焦于安全逻辑在 Isabelle/HOL 中的浅嵌入和深嵌入方式，并讨论它们的优缺点。 ## 2. 执行平台 ### 2.1 SAL 平台 我们使用的简单汇编语言（SAL）是 TAL 的简化版本。SAL 区分两种地址： - 位置（Locations）：用自然数表示，用于标识内存单元。 - 位置（Positions）：表示程序中的位置，记为 `(pn, offset)`，其中 `pn` 是过程名，`offset` 是过程内的相对位置。 ```plaintext types loc = nat, pname = nat, pos = pname × nat ``` SAL 包含算术、指针、跳转和过程相关的指令： ```plaintext datatype instr = SET loc nat | ADD loc loc | SUB loc loc | MOV loc loc | JMPL loc loc nat | JMPB nat | CALL loc pname | RET loc | HALT ``` 程序状态的形式为 `(pos, memory, env)`，其中： - `pos` 是程序计数器，指向下一条要执行的指令位置。 - `memory` 是将位置映射到类型化值的主内存，存储程序处理的所有数据。 - `env` 是环境，跟踪程序运行的有用信息，包含调用栈 `cs` 和历史记录 `hist`。 ```plaintext types state = pos × (loc → tval) × env datatype tval = ILLEGAL | NAT nat | POS pos ``` 程序是过程的列表，每个过程由名称和可能带注释的指令列表组成。 ### 2.2 程序语义 我们使用转换关系 `effS` 来形式化 SAL 指令的效果。例如，`ADD X Y` 指令更新 `X` 的值： ```plaintext ADD X Y updates X with (X + Y) if X = NAT x and Y = NAT y, and ILLEGAL otherwise. ``` 其他指令的语义类似，如 `SUB`、`SET`、`JMPL`、`JMPB`、`CALL`、`RET` 和 `MOV` 等。 ### 2.3 安全逻辑和策略 为了正式表示和证明程序的安全属性，我们使用安全逻辑。安全逻辑的基本组成部分包括逻辑连接词（如蕴含和合取）以及可证明性和有效性的判断。 我们假设公式语言足够表达程序的初始状态和安全状态。定义了两个函数： - `initF`：指定初始状态。 - `safeF`：生成局部安全公式。 这两个函数共同构成安全策略。一个程序是安全的，当且仅当从初始状态可达的所有状态都是安全的。 ### 2.4 验证条件生成 我们定义了一个通用的 VCG，将格式良好的程序转换为验证条件（VC）。VC 是一个大的合取式，包含一个初始合取项和每个代码位置的合取项。 VCG 的正确性依赖于一些基本假设： - `succsF` 函数必须近似程序的控制流图，可产生虚假后继，但不能遗漏或产生无效的分支条件。 - `wpF` 运算符必须与 SAL 的语义兼容，其产生的公式必须保证后继状态中的后置条件。 - 安全逻辑必须正确，即可证明的公式对于所有安全状态都有效。 - 逻辑连接词具有普通语义，且 `initF` 与初始程序计数器一致。 ## 3. 浅嵌入 ### 3.1 语法 在浅嵌入中，逻辑公式直接用定理证明器的逻辑编写，即 SAL 公式