形式化验证WebAssembly - Soroban案例研究

WebAssembly（或称Wasm）最近在如Arbitrum、Stellar和Polkadot等区块链中得到了显著应用。例如，在Stellar区块链中，用户在Soroban平台上编写智能合约。这些程序用Rust编写并编译为Wasm，部署在Stellar区块链的隔离虚拟机中。

智能合约旨在实现涉及数百万美元的金融交易。这些程序中的漏洞通常会导致严重后果。理所当然，形式验证在这一领域发挥着至关重要的作用。

在这篇博客中，我们介绍了Certora最近在形式验证Wasm字节码方面的努力。

什么是Wasm？

Wasm是一种低级二进制指令格式，旨在实现安全和快速的执行，主要应用于Web环境，但在无服务器计算和物联网等非浏览器环境中也日益受到广泛使用。它作为更高级语言如C、C++和Rust的编译目标，并与JavaScript互操作，使其易于集成到现有的Web应用程序中。Wasm是“平台无关的”，这意味着相同的二进制文件可以在任何设备或操作系统上运行，只要环境支持Wasm（例如，大多数现代Web浏览器都支持）。

Wasm在一个安全的沙盒环境中执行，确保恶意或错误代码不会影响主机系统。当将Wasm编译为本地代码时，Wasm编译器（和解释器）会插入检查，以确保Wasm程序在自己的沙盒内存区域内运行[1]。

由于上述特点，Wasm在DeFi领域的使用越来越广泛。

众所周知，智能合约中的漏洞可能会被利用，从而造成巨大的财务损失。形式验证可以帮助提高智能合约的安全性。在过去十年中，对智能合约高层次功能正确性的验证因此成为一个备受关注的主题，促生了许多依赖于交互式验证（例如，Runtime Verification）、自动验证（例如，Certora Prover和Halmos）和符号执行（例如，Hevm）等技术的工具。还有许多针对智能合约的模糊测试和错误发现工具，其中有数个在关于智能合约威胁缓解的最新调查中进行了涵盖。

随着Wasm在区块链中的使用日益增加，确保Wasm程序的正确性尤为重要。形式验证技术使我们能够实现这一目标。

形式化验证（ Formal Verification）简介

“程序测试可以用来显示存在错误，但决不可以用来证明不存在错误！”

― Edsger W. Dijkstra

形式验证和模糊测试之间的主要区别在于，前者可以生成证明，表明程序对于所有输入满足规范，而后者只能在一组具体值上进行检查，通常无法涵盖所有输入。

在这篇博客中，我们将专注于使用满足性模理论（SMT）求解器的自动形式验证。这些工具接受两个输入：一个待验证的程序和程序必须满足的属性。

这些属性通常使用前置条件和后置条件来书写。非正式地说，它们说明如果在程序“S”执行之前前置条件“P”为真，那么在“S”执行之后后置条件“Q”必须成立，前提是“S”的执行终止。这种推理风格可以归因于传奇计算机科学家Tony Hoare。

接下来，程序和属性被编译以生成验证条件（或VC）[9]。构造时，VC是一个有效的数学公式，当且仅当程序对于该属性是正确的，即它始终满足该属性。如果VC是无效的，这意味着程序对某些输入违反了该属性，即存在错误。

在使用SMT求解器进行验证时，检查VC的有效性通常通过对其进行否定来简化为一个可满足性问题。一个可满足公式的例子是x * 3 + y = 0：此公式对于x = 0, y = 0成立。一个不可满足公式的例子是(x XOR y) AND (x == y)，因为x XOR y和x == y不能同时为真。

在形式验证的上下文中，如果否定的VC是不可满足的（UNSAT），则意味着原始VC是有效的。这一UNSAT结果表明程序是正确的，并且在所有输入下均按照属性所述的行为。如果是可满足的（SAT），则说明存在某个输入使得程序违反该属性。

让我们看一个例子以使这一过程更加具体。考虑下面来自Soroban智能合约的简化Rust函数，该函数在两个账户之间转移某个amount（从from到to）。这里，spend_balance读取from的当前余额，并通过从中减去amount来更新它。receive_balance同样通过将amount加到它上来更新to的余额。check_nonnegative确保amount >= 0。

pub fn transfer(e: &Env, from: Address, to: Address, amount: u64) {
    check_nonnegative(amount);
    spend_balance(e, from.clone(), amount);
    receive_balance(e, to.clone(), amount);
}

我们希望transfer满足哪些属性？

首先，在transfer执行完成后，from的余额应比调用transfer之前少amount，而to的余额应比调用transfer之前多amount。

另一个属性是transfer只能影响from和to的余额。与这两个地址不同的任何地址都不应该受到transfer的影响。这些是高层次功能正确性的属性示例。

在基于SMT的自动形式验证工具中，用户在规范语言中书写这些属性，然后工具按上面描述的方式检查程序是否符合规范。

在过去六年中，Certora一直在开发用于检查以太坊和Solana区块链上运行的智能合约的此类属性的工具。在以太坊的例子中，Certora以低级字节码为目标，即运行在以太坊虚拟机（EVM字节码）上的字节码，而对于Solana，则以低级Solana二进制格式（SBF）为目标。Certora提供了用于书写属性的规范语言。在以太坊的情况下，用户用Solidity编写代码，用CVL（Certora Verification Language）编写规范，CVL的设计使其与Solidity相似。在Solana的情况下，Certora提供了一个轻量级Rust库，允许用户用Rust书写任务。然后，Certora证明器检查低级字节码是否满足属性。

Rust生成的Wasm的形式验证

形式验证的学术研究社区已经深入研究了Wasm，这导致了从Wasm到本地代码的经过验证的编译器[2]、检查内存隔离的工具[3]和在生成本地代码时验证指令选择的工具[4]、机械化的Wasm语义[8]以及开发内存安全扩展到Wasm的研究[5]。

最近，我们在Certora开发了Sunbeam，这是一种新工具，用于验证Rust智能合约的高层次功能正确性。Sunbeam允许用户用嵌入在Rust中的轻量级规范语言书写正确性属性，然后验证智能合约是否满足属性。关键的是，Sunbeam并不检查Rust源代码的正确性；它首先将Rust编译为Wasm字节码，然后验证生成的Wasm是否满足属性。通过这种方式，Sunbeam验证实际部署在区块链上的代码，而不需要信任Rust编译器。

图1显示了Sunbeam的详细工作流程。Sunbeam使用Rust编译器从源代码和用户编写的规范生成Wasm。然后，它将Wasm编译为Certora的中间表示，称为TAC，这是一种三地址寄存器机。一旦生成TAC，Sunbeam执行语义保持重写以简化TAC。最终，TAC被编译为逻辑公式，以供SMT求解器求解（如前一节所述）。最后，验证结果以交互式Web报告的形式与用户分享。

图1. Certora Sunbeam的工作流程。它将智能合约及其用Rust编写的规范作为输入，(2) 将二者编译以生成Wasm，(3) 将Wasm转换为Certora的内部中间表示TAC，(4) 在TAC上执行语义保持变换以简化代码，(5) 将代码和规范转换为VC，(6) 使用现成的SMT求解器检查VC的有效性，通过将其简化为可满足性问题，最后 (7) 在报告中显示验证结果。

目前，Sunbeam的目标是Soroban智能合约，这些合约以Wasm字节码的形式部署在Stellar区块链上。Soroban的设计使这些程序特别适合形式验证——合约的环境分为_来宾_和主机，许多复杂功能转移给主机，从而使合约代码变得简单且较小。因此，这些程序的验证可以归结为验证合约代码本身的正确性，前提是主机环境的实现是正确的。

回到我们之前看到的transfer方法，让我们试着为之前列出的某些属性写下代码。我们声明的第一个属性可以这样用Sunbeam编写：

#[rule]
fn transfer_is_correct(e: Env, to: Address, from: Address, amount: i64) {
    cvt::require!(to != from, "地址不同");
    // 读取`from`在转账前的余额
    let balance_from_before = Token::balance(&e, from.clone());
    // 读取`to`在转账前的余额
    let balance_to_before = Token::balance(&e, to.clone());
    // 执行转账
    Token::transfer(&e, from.clone(), to.clone(), amount);
    // 读取`from`在转账后的余额
    let balance_from_after = Token::balance(&e, from.clone());
    // 读取`to`在转账后的余额
    let balance_to_after = Token::balance(&e, to.clone());
    cvt::assert!(balance_to_after == balance_to_before + amount);
    cvt::assert!(balance_from_after == balance_from_before - amount);
}

关于transfer仅对from和to的影响的第二个属性可以这样表述：

#[rule]
fn effect_on_other(e: Env, amount: i64, from: Address, to: Address, other: Address) {
    cvt::require!(to != other && from != other, "地址均不同");
    // 在转账前读取余额
    let balance_other_before = Token::balance(&e, other.clone());
    // 执行转账
    Token::transfer(&e, from.clone(), to.clone(), amount);
    // 在转账后读取余额
    let balance_other_after = Token::balance(&e, other.clone());
    cvt::assert!(balance_other_after == balance_other_before);
}

这里，cvt::require!和cvt::assert!是两个宏，Sunbeam将其解读为前置条件和后置条件。#[rule]属性将规则添加到Wasm二进制中的专用部分，并防止Rust编译器对其进行混淆或移除。

然后，Sunbeam使用Rust编译器从上述代码生成Wasm，并使用SMT求解器验证属性，如上述所述。关于如何运行Sunbeam以验证上述代码的确切细节，请访问我们的教程，该教程将在Meridian 2024上发布：https://github.com/Certora/meridian2024-workshop。

验证低级Wasm的挑战

验证低级Wasm字节码的优势在于，它使我们不需要信任Rust编译器。编译器，和其他软件一样，容易出现错误，这已通过如CSmith[6]和RustSmith[7]等工具得以证明。去年，Vyper编译器中的一个错误导致从Vyper智能合约生成EVM字节码的过程出现了严重的安全漏洞，导致Curve协议损失了数百万美元。最近，Certora及其合作者在LLVM中发现了一个优化中的错误，该错误可能被利用从Aave在ZKsync上的实例中提取资金。因此，能够验证最终部署和执行的代码是有益的。

另一方面，在Wasm层面验证属性也带来了一些挑战。

Wasm提供的数据类型非常有限（32位和64位有符号整数与我们目前的使用案例相关）。因此，具有复杂数据类型的Rust程序在编译为Wasm时看起来会非常不同。举个简单的例子，如果一个Rust程序在有符号128位（i128）值上执行某些计算，则编译后的Wasm将使用两个i64（64位有符号整数）表示i128类型。如果结果也是i128，它将作为代表高位和低位的两个i64存储。即使使用像wabt这样的工具，能够让用户看到Wasm二进制文件的文本表示，从Wasm代码中查看哪个Rust代码对应于它可能也并不明显。

在区块链环境中使用像Wasm这样的低级语言会有更深远的影响。一方面，如果对应用户编写的智能合约的字节码过大和复杂，将会产生额外的Gas费用，这是不希望的。另外，智能合约开发者能够使用类似映射、字符串和结构自定义数据类型在其程序中也是非常重要的，这不可避免地使字节码变得复杂。

Soroban平台通过将合约环境分为客体和主机，处理这两种相互矛盾的需求。主机环境实现了广泛的功能，允许将复杂数据类型创建为不可变的“主机对象”，这些对象只能通过对象Handle（表示为整数）让客体环境访问。这些函数简单地在与用户编写的智能合约对应的Wasm模块中“导入”和使用，从而显著减少智能合约的字节码大小。客体和主机之间的通信通过“Soroban值类型”进行，这涉及到将对象包装和解包为这些值。

所有这些意味着，尽管Wasm是Soroban使用的二进制格式，但在底层实际上有一个与Soroban平台对应的完整领域特定语言，实质上嵌入在Wasm中。像Sunbeam这样的针对Wasm的验证工具，因此必须能够推理关于Wasm语义以及嵌入语言的语义，在这种情况下是“Soroban语言”。，如果简单地将Wasm程序编码为验证条件而不考虑Soroban环境功能的语义，将注定会失败。同时，将整个Soroban环境实现包含在要验证的代码中是不可扩展的。Sunbeam通过在Certora的中间表示TAC中忠实地建模和实现Soroban主机功能来解决这一挑战（见图1）。每当智能合约调用这些函数时，Sunbeam便在TAC中用其对Soroban环境的模型替换这些函数。

验证完成后，Sunbeam向用户显示一份报告，总结验证结果，如图2所示。结果要么是“已验证”，要么是“已违反”。由于形式验证在一般情况下是一个不可判定的问题，因此，在某些情况下，Sunbeam可能无法验证属性并将返回“超时”或“未知”。当验证查询对SMT求解器来说太复杂时，会发生这种情况。该报告是交互式的，显示调用跟踪信息，并总结有关验证任务复杂性的主要指标。

图2. Sunbeam生成的输出：显示一份验证报告，表明Sunbeam检查了哪些属性及其状态（已验证、已违反等）。

结论

总之，我们介绍了Sunbeam，一种新的形式验证工具，专门针对Wasm；具体来说，它检查Rust中为Soroban智能合约编写的高层次功能正确性属性是否被编译的Wasm所满足。为此，它提供了一种轻量级的Rust规范语言。

我们正在积极改进Sunbeam。我们最近使用Sunbeam验证了Reflector预言机协议的几个属性，特别是订阅和DAO合约。Sunbeam的早期版本快捷用户试用，并可以通过此处注册获得： https://www.certora.com/。我们的研讨会内容，展示了如何使用Sunbeam，可以在此处访问：https://github.com/Certora/meridian2024-workshop。由于Sunbeam仍在开发中，我们鼓励用户与我们联系并提供反馈。我们期待收到你的消息！

展望未来

从长远来看，我们渴望扩展Sunbeam，以验证不仅从Soroban程序生成的Wasm，还包括来自智能合约和区块链以外的领域的Wasm。由于Wasm的内存隔离、安全性和接近本地性能，它已在许多领域得到应用并持续获得人气。我们期待了解Wasm的其他用例，并探索如何利用Sunbeam对这些领域的Wasm程序进行形式验证。敬请关注更多更新及未来的博客文章！

感谢

我们感谢所有为此项目做出贡献的人。Sunbeam的成果源于一个出色团队的协作，其中包括Alexander Bakst、Eric Eilebrecht、Johannes Späth、Rahav Yairi、Sameer Arora、Ondrej Kurák、Netanel Rubin-Blaier、Gadi Auerbach、Anastasia Fedotov、Jaroslav Bendik、Alexander Nutz、Arie Gurfinkel和Chandrakana Nandi。

参考文献

[1] E. Johnson 等，"WaVe：一种可验证安全的WebAssembly沙箱运行时，" 2023 IEEE Symposium on Security and Privacy (SP)，美国加利福尼亚州旧金山，2023年。

[2] Jay Bosamiya, Wen Shih Lim和Bryan Parno，“使用WebAssembly的可证明安全的多语言软件沙箱”，USENIX Security 22，美国马萨诸塞州波士顿，2022年。

[3] Evan Johnson, David Thien, Yousef Alhessi, Shravan Narayan, Fraser Brown, Sorin Lerner, Tyler McMullen, Stefan Savage, Deian Stefan，“Довер´яй, но провер´яй：原生编译Wasm的SFI安全性，”网络和分布式系统安全（NDSS）研讨会，2021年。

[4] Alexa VanHattum, Monica Pardeshi, Chris Fallin, Adrian Sampson和Fraser Brown. 2024. 轻量级、模块化验证用于WebAssembly到本地指令选择。在第29届ACM国际会议关于程序设计语言和操作系统的支持的会议记录中。

[5] Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena和Deian Stefan. 2023. “MSWasm：有效执行不安全代码的内存安全执行，”Proc. ACM Program. Lang. 7, POPL，第15号文章（2023年1月）。

[6] Xuejun Yang, Yang Chen, Eric Eide和John Regehr. 2011. 查找和理解C编译器中的错误。SIGPLAN Not. 46, 6（2011年6月），283-294. https://doi.org/10.1145/1993316.1993532

[7] Mayank Sharma, Pingshi Yu和Alastair F. Donaldson. 2023. RustSmith：Rust的随机差异编译器测试。在第32届ACM SIGSOFT国际软件测试与分析研讨会（ISSTA 2023）上。与计算机协会，纽约，NY，美国，1483-1486. https://doi.org/10.1145/3597926.3604919

[8] Conrad Watt，“机械化和演化WebAssembly的形式语义：网络的新低级语言”，https://www.isa-afp.org/entries/WebAssembly.html

[9] Mike Barnett和K. Rustan M. Leino. 2005. 无结构程序的最弱前置条件。SIGSOFT软件工程笔记31, 1（2006年1月），82-87. https://doi.org/10.1145/1108768.1108813

• 原文链接： certora.com/blog/formall...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～