Sophia Drossopoulou：如何在开放世界中验证可信代码

过去十年，我和合作者研究了在开放世界中，封装应当提供什么保证。问题源于对对象能力、膜和所有权类型的讨论：这些机制可以保护状态，但我们首先必须说明希望它们保证什么性质。

在开放系统中，可信的内部对象会与行为未知的外部对象互动。外部代码可能诚实也可能恶意，可能回调内部代码，也可能持有其他对象的引用。当可信代码调用不可信对象时，我们需要推理它对内部状态可能产生的影响。

有两种互补的保证。封装和对象不变量可以使某些影响永远不会发生；另一些影响则可能只有在外部对象拥有特定能力时才能发生。控制对该能力的访问，就可以控制谁能造成这一影响。

假设一家商店有一个账户，取款需要一把密钥。买家是外部对象，但商店将账户交给买家以便付款。买家能偷走钱吗？如果取款需要密钥、买家无法访问密钥、商店也不泄露密钥，那么答案是否定的。

不同的账户实现说明，为什么必须考虑整个模块的行为。安全版本只允许在初始化时设置密钥；另一个版本要求持有旧密钥才能更换。危险版本允许任何人替换密钥，然后转账。两个分别可用的调用组合起来，就产生了有害效果。

历史上的多重签名钱包事件展示了类似的涌现行为：初始化与后续操作可能以意想不到的方式组合。我们希望有一种规格语言区分安全与不安全的模块，并有一套推理系统证明模块是否满足规格。

对商店而言，目标是证明：在调用外部付款方法后，只要所需保护条件成立，余额可以增加，但不能减少。我们还希望有工具验证这些性质，而不只是依赖非形式化推论。

第二个问题涉及中介。内部服务可能处于多个外部对象之间，却不知道哪些对象诚实。服务应当提供有用行为，同时限制诚实参与者面临的风险，并在规格中清楚说明剩余风险。

希望表达的核心保证是：除非造成影响的对象能够访问某个能力，否则该影响不会发生。在账户例子中，余额减少是影响，密钥是能力。我们探索过时序逻辑、自定义规格构造和不变量等表达方式。

可以用会被某种影响破坏的断言来描述该影响。例如，将余额降到某个阈值以下，会使“余额至少为该阈值”的断言失效。为了推理访问，还需要精确定义外部对象无法获得某个能力是什么意思。

当从当前顶层栈帧可达的相关外部对象没有直接指向某个对象，并且该对象没有作为参数传给外部接收者时，我们称它受到保护。可达性上下文很重要：堆中其他位置一个无关的外部对象，本身不会让这一定义失效。

我们还定义相对于特定对象的保护。直观地说，从该对象通向受保护能力的路径必须经过不会泄露能力的可信对象。这类似支配关系：可信对象位于外部来源与能力之间。

另一个关键要素是有作用域的不变量。与常见的循环或对象不变量一样，它不必在每个中间步骤都成立。只要它在相关起点成立，在特定调用作用域中执行处于外部状态时，这一性质就必须再次成立。

当前栈帧弹出时，作用域结束。在该范围内可以发生任意内部和外部调用，但不变量必须在定义所覆盖的外部状态再次成立。这与声称它在整个执行历史中永远成立不同。

对账户来说，我们可以说明受保护的密钥在该作用域内保持受保护，且密钥受保护时余额不会减少。方法级规格进一步说明：如果调用前密钥相对于买家受保护，调用后余额至少等于原来的值。

这些规格描述可观察的影响，而不要求某种特定的 API 表示方式。余额和密钥可以用不同方式表示，包括 ghost fields 或数据库。目标是捕捉跨调用产生的涌现行为，而不仅是单个方法的局部结果。

为了证明此类规格，我们基于现有的 Hoare 逻辑，而不是从头开始。我们将普通的前置条件与后置条件三元组扩展为四元组，额外描述执行期间的中间外部状态必须满足什么。

证明系统需要关于保护和封装的规则。要建立有作用域的不变量，相关断言必须涉及封装在模块内的状态，公共方法也必须在调用过程中保持它。推理还需要将断言调整到调用方或被调用方的视角。

一旦模块的有作用域不变量得到证明，就可以用它推理外部调用。在商店例子中，这有助于得出结论：调用买家的付款方法不能减少受保护账户的余额。研究团队检查了一些例子，并给出了手写的可靠性证明。

团队还有一个映射到 Dafny 的原型。技术挑战在于，保护断言涉及可达性，而其影响范围并不像许多现有验证工具所预期的那样固定。该工具仍是研究原型，不是完成的通用解决方案。

对于中介问题，考虑买家与卖家之间的托管服务。买家提供钱，卖家提供货物，但双方互不信任。理想服务应在双方都有足够资源时完成交换，否则让各方持有的资源保持不变。

双方提供外部钱包对象。理想规格会说明，成功的交换转移约定的钱和货物，同时不影响其他钱包；失败则让它们保持不变。难点在于，中介不能假定每个提供的钱包都诚实。

一个简单的托管实现会创建临时钱包，要求买家转入钱、卖家转入货物，然后完成交换。如果第二次转账失败，就尝试将钱退回。只有在对象报告的结果可信时，这种做法才有效。

不诚实的买家钱包可能谎称自己已经转账。托管服务随后可能继续交付货物，尽管钱从未到账。这个反例表明，面对任意外部对象时，原始代码不满足期望的规格。

提出的应对方法是更强的协议，以及“诚实钱包”的概念。诚实钱包会创建诚实钱包，并可以通过成功转账提供另一个钱包是否可信的信息。转账失败可能意味着余额不足，也可能意味着对方不诚实，因此规格必须区分这些情况。

交换之前，额外的交互会在相关钱包之间建立信任关系。得到的规格描述参与者全部诚实、诚实与不诚实对象混合，以及全部不诚实并可能串通时分别能得出什么结论。它还说明哪些未暴露的对象保持不受影响。

这些规格是行为性的、假设性的：诚实与否通过多次调用可能发生的行为来定义，而不是简单检查类或存储字段。当定义同时以正向和负向方式引用诚实时，就会出现问题，使循环定义不可靠。

团队的解决方法是分层。一个规格可以正向引用同层规格，但只能负向引用较低层的规格。在这个例子中，钱包与托管性质处于不同层级，从而避免有问题的负向自引用。

用于中介验证的工具仍在设计中，计划映射到 Dafny。团队希望增加机械化程度、支持更丰富的语言，并引入超过两个视角，因为真实系统可能有多个互不信任的利益相关方。

另一个重点是框架问题：反复说明每个无关对象都不受影响很繁琐。如果能更好地描述哪些状态不会变化，规格的编写和使用就会更容易。

更广泛的启示是区分内部和外部对象、提供某种封装，并询问某种影响必须具备什么能力。当关注的是多次调用产生的行为时，传统的前置和后置条件可能不够方便。

我们还应推理良好、恶意及混合场景，包括一个对象最终是否能够触及另一个对象。保护只是提出的一种定义，并非唯一可能的设计。无论通过逻辑还是测试，规格和验证都有助于明确这些假设。