Certora 通过形式化验证技术确保智能合约安全

我们如何确保 Web3 应用程序更加安全？Web3 开发者可以做些什么来更容易地检查他们的代码？在 Certora，我们使用一种称为 形式验证 的技术来保护智能合约，并且我们发现，在开发智能合约时，某些最佳实践可以更容易地对代码进行形式验证，从而使其更安全。

形式验证是一种证明程序行为符合规范的技术。它基于数学逻辑。形式验证可用于智能合约中，以证明不存在某些类型的安全漏洞。这对于去中心化金融应用程序非常重要，在这些应用程序中，大量的资金处于风险之中，恶意攻击者可以利用安全漏洞造成严重的经济损失。我们开发了 Certora Prover，它是一个开源的形式验证工具，旨在保障智能合约在 Stellar、Solana 和 Ethereum 等区块链上的安全性。

我们对 Soroban 和 Solana 进行 Rust 智能合约 形式化验证的经验帮助我们识别了哪些因素使 Rust 智能合约易于或难以验证。这篇博文分享了从我们的观察中提炼出的五个最佳实践，以帮助 Web3 开发者编写不仅安全和可读，而且 可验证 的 Rust 智能合约。

以下是五个最佳实践的简短摘要。

1. 保持代码模块化：将大型函数分解为更小的组件。
2. 使用编译器的完备性检查：在模式匹配时要小心使用通配符。
3. 偏好简单的数据结构：尽可能使用简单的、扁平的数据结构，而不是具有哈希行为的数据结构。
4. 更少的状态与陷阱值：设计使非法状态不可能出现的数据类型。
5. 将核心逻辑与副作用分离：将纯逻辑与副作用操作和事件隔离。

请继续阅读，查看说明这些实践的具体示例！

1. 保持代码模块化

众所周知，模块化是一种良好的软件工程实践，因为它可以使代码更具可读性，并使通用组件可重用。事实证明，模块化代码也更容易验证！将过于庞大的函数拆分为更小的函数，使验证工具可以独立地推理每个部分。这不仅提高了可读性，还简化了规范并使其可重用。

糟糕的例子：

pub fn process_user_ops(
  env: &Env,
  protocol: &mut Protocol,
  user: &Address,
  op: UserOp
) -> bool {
    let mut state = UserState::load(env, user);
    let mut check_needed = false;

    match op.kind {
        OpType::Deposit => {
            let vault = protocol.get_vault(&op.asset);
            state.balance += op.amount;
            protocol.transfer_from_user(env, user, &vault, op.amount);
        }
        OpType::Withdraw => {
            let vault = protocol.get_vault(&op.asset);
            if state.balance >= op.amount {
                state.balance -= op.amount;
                protocol.transfer_to_user(env, user, &vault, op.amount);
            }
        }
        OpType::Borrow => {
            let market = protocol.get_market(&op.asset);
            state.debt += op.amount;
            protocol.transfer_to_user(env, user, &market, op.amount);
            check_needed = true;
        }
        OpType::Repay => {
            let market = protocol.get_market(&op.asset);
            let payment = op.amount.min(state.debt);
            state.debt -= payment;
            protocol.transfer_from_user(env, user, &market, payment);
        }
    }

    state.save(env, user);
    check_needed
}

这里，一个单一的类似调度器的方法具有处理每种用户操作类型的所有逻辑。这使得为每个操作单独编写不变量和其他属性变得困难。

好的例子：

pub fn process_user_ops(
  env: &Env,
  protocol: &mut Protocol,
  user: &Address,
  op: UserOp
) -> bool {
    let mut user_state = UserState::load(env, user);
    let mut check_needed = false;

    match op.kind {
        OpType::Deposit => {
            handle_deposit(env, protocol, user, &mut user_state, &op);
        }
        OpType::Withdraw => {
            handle_withdraw(env, protocol, user, &mut user_state, &op);
        }
        OpType::Borrow => {
            handle_borrow(env, protocol, user, &mut user_state, &op);
            check_needed = true;
        }
        OpType::Repay => {
            handle_repay(env, protocol, user, &mut user_state, &op);
        }
    }

    user_state.save(env, user);
    check_needed
}

fn handle_deposit(
    env: &Env,
    protocol: &mut Protocol,
    user: &Address,
    state: &mut UserState,
    op: &UserOp,
) {
    let vault = protocol.get_vault(&op.asset);
    state.balance += op.amount;
    protocol.transfer_from_user(env, user, &vault, op.amount);
}

...

在这个例子中，每个操作都有一个单独的处理程序，因此可以更容易地指定和验证。

2. 尽可能依赖编译器的完备性检查

让我们再次参考上面的用户操作场景，并考虑以下具有 4 个变体的 OpType 枚举，以及一个检查操作是否增加用户资金的函数：

pub enum OpType {
    Deposit,
    Withdraw,
    Borrow,
    Repay
}

pub fn increases_user_funds(env: &Env, op: UserOp) -> bool {
    match op.kind {
        OpType::Withdraw => true,
        OpType::Borrow => true,
        _ => false
    }
}

这段代码依赖于通配符（_）来指示只有 Withdraw 和 Borrow 可以增加资金，并且在所有其他情况下，它必须返回 false。但是，如果稍后更改枚举以添加另一个变体（例如，Redeem），它也会增加用户的资金，会发生什么情况？

这种编写代码的方式存在风险，开发者很容易忘记更改 increases_user_funds 以处理新情况。现在假设开发者有一个属性来检查 increases_user_funds 是否对于 Redeem 情况返回 true。在这种情况下，该属性将失败，开发者最终将花费额外的时间来调试失败的原因，最终修复代码。

通过以一种要求依赖 Rust 编译器完备性检查的方式编写代码，可以避免所有这些情况，该检查可以防止代码在不处理所有场景的情况下进行编译：

pub fn increases_user_funds(env: &Env, op: UserOp) -> bool {
    match op.kind {
        OpType::Withdraw | OpType::Borrow => true,
        OpType::Deposit | OpType::Repay => false,
    }
}

现在，当添加一个新变体时，开发者将被迫仔细考虑并以正确的方式处理它。

3. 尽可能使用更简单的数据结构

在求助于像 HashSet 或 BTreeMap 这样的复杂数据结构之前，请仔细考虑。工作负载真的需要它吗？它们很诱人，但推理堆分配的数据结构和哈希函数很难。如果可能，最好使用更简单的线性结构。

为了展示一个具体的例子，考虑一个函数，该函数通过查看少量现有地址来检查给定的Address是否唯一。在这种情况下，线性扫描addrs就足够了，并且在实践中对于多达几十个元素来说足够快，并且比具有哈希行为的代码更容易验证。

fn is_unique (addrs: &Vec<Address>, addr: &Address) -> bool {
    !addrs.contains(addr)
} // 当 addrs 是一个小的集合时，值得使用 Vec 而不是哈希数据结构

即使在集合很大但不需要太多插入时，最好使用按键排序的关联映射。当然，有些工作负载中，哈希数据结构效率更高，但智能合约通常寿命很短，并且在小型数据集上运行。在这些设置中，简单的关联列表（平面映射）表现更好，并且也更容易验证。

4. 通过构造来最小化具有陷阱值的状态

有时，我们最终会得到“扁平”的用户定义数据类型，这些数据类型具有太多的字段，这些字段可以容纳“陷阱值”（例如，None）。这些可能很难跟踪，尤其是在一个字段具有“陷阱值”时，该值会影响其他字段可能或可能不允许具有“陷阱值”的情况。这要求开发者仔细考虑所有组合，并确保程序不会处于某种可选字段错误地保留为 None 或允许为 Some(...) 的状态。

糟糕的例子：

pub struct LoanPosition {
    pub user: Address,
    pub collateral_amount: Option<u64>,
    pub borrowed_amount: Option<u64>,
    pub liquidation_price: Option<u64>,
    pub interest_accrued: Option<u64>,
    pub closed_at: Option<Time>,
    pub status: LoanStatus,
}

pub enum LoanStatus {
    Open,
    InLiquidation,
    Closed,
}

在这里，字段 collateral_amount、borrowed_amount 和 interest_accrued 对于 Closed 贷款没有意义。类似地，closed_at 仅对 Closed 贷款有意义。这种系统设计允许非法状态，其中状态可以为 Closed，但 borrowed_amount 为 Some(num)，这是不应该允许的。

下面展示了另一种设计系统的方法：

好的例子：

pub struct LoanPosition {
    pub user: Address,
    pub state: LoanState,
}

pub enum LoanState {
    Open {
        collateral_amount: u64,
        borrowed_amount: u64,
        interest_accrued: u64,
        liquidation_price: u64,
    },
    InLiquidation {
        collateral_amount: u64,
        borrowed_amount: u64,
    },
    Closed {
        closed_at: Time
    }
}

现在，Open 贷款必须具有 borrowed_amount 字段，并且 Closed 贷款只能具有 closed_at 字段。这种方法使代码更容易验证，因为规范需要担心的非法状态更少。

但是，开发者应该注意，价值表示的选择与序列化和反序列化的简易性之间存在权衡。最后，使用像 AnyBitPattern 或 Pod（来自 bytemuck crate）这样的标记特征也可能影响设计决策。

5. 将纯逻辑与副作用和错误处理分离

将协议的核心逻辑与错误处理代码、副作用代码（例如，存储 I/O）和事件发射混合在一起的代码对推理和验证提出了挑战。分离纯计算允许验证工具专注于逻辑行为，而无需跟踪复杂的控制流。

这允许单独验证纯函数，具有相对更多的可重用属性，而可以针对副作用相关的属性和 panic 安全性验证效果部分。

糟糕的例子：

pub fn borrow(env: &Env, protocol: &mut Protocol, user: &Address, amount: u64) {
    let mut account = Account::load(env, user);
    let market = protocol.get_market();
    let new_debt = account.debt + amount;

    if new_debt > market.max_borrow {
        panic_with_error!(env, Error::LimitExceeded);
    }

    account.debt = new_debt;
    protocol.transfer_to_user(env, user, &market.token, amount);
    env.events().publish(("borrow", user.clone()), amount);
    account.save(env, user);
}

此函数混合了几种不同类型的任务：加载状态、计算债务、错误处理、转移金额的副作用操作和事件发射。

好的例子：

pub fn borrow(env: &Env, protocol: &mut Protocol, user: &Address, amount: u64) {
    let mut account = Account::load(env, user);
    let market = protocol.get_market();

    match compute_borrow(account.debt, amount, market.max_borrow) {
        Ok(new_debt) => {
            account.debt = new_debt;
            protocol.transfer_to_user(env, user, &market.token, amount);
            env.events().publish(("borrow", user.clone()), amount);
            account.save(env, user);
        }
        Err(e) => panic_with_error!(env, e),
    }
}

fn compute_borrow(current_debt: u64, amount: u64, max: u64) -> Result<u64, Error> {
    let new_debt = current_debt + amount;
    if new_debt > max {
        Err(Error::LimitExceeded)
    } else {
        Ok(new_debt)
    }
}

在这个版本中，纯逻辑被分离到它自己的函数中，使得编写检查逻辑本身的属性变得更容易。包装函数 borrow 负责调用 compute_borrow 并处理影响 I/O 操作异常。

这也可以推广并应用于合约级别。例如，拥有一个具有核心协议逻辑的最小合约，以及一个具有对协议的核心功能来说不重要的辅助逻辑的“包装”合约（例如，接口、授权等），可以很容易地隔离验证关键组件。

验证友好的代码也是开发者友好的代码

编写考虑到验证的智能合约不仅可以使代码更安全，还可以使代码更易于理解、测试和维护。编写正式规范的行为也有助于软件设计和文档编写。它可以成为揭示规范不一致和低效实现的一个有用工具。

这里的建议不仅使代码更容易验证，而且更适合测试和模糊测试。例如，将核心逻辑与副作用组件分离，可以更轻松地使用基于属性的测试等技术，专注于检查主要逻辑是否正确，而无需担心额外的基础架构（例如，启动虚拟机）来测试整个程序。清晰定义的接口通过避免不相关的输入并专注于仅生成有意义的输入，使模糊测试等技术更加有效。

虽然我们在此提供的列表肯定不是详尽无遗的，但我们希望这些简单的最佳实践可以帮助开发者提高智能合约的长期质量和可靠性。

参考

• Stellar 基金会关于安全最佳实践的文档：https://developers.stellar.org/docs/build/security-docs
• JaneStreet 的 Yaron Minsky 的精彩视频，其中启发了这里的一些想法：https://www.youtube.com/watch?v=-J8YyfrSwTk
• OpenZeppelin 关于安全 Solidity 开发的博客：https://www.openzeppelin.com/readiness-guide#code-clarity

致谢

感谢 Arie Gurfinkel 和 Alexander Bakst 对内容提供的宝贵反馈！

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