Kamino Lending 安全审计

Certora
发布于 2025-03-26 16:41
阅读 151

Kamino Lending (KLend) is a lending protocol on Solana that emphasizes security through a partnership with Certora for rigorous code audits and formal verification。

### **Kamino Lending及其对安全的承诺**

[Kamino Lending](https://github.com/Kamino-Finance/klend) (KLend) 是一个基于Solana的前沿借贷协议，旨在提供高效的去中心化借贷解决方案。KLend专为速度和可扩展性而构建，让用户提交抵押品并借贷流动性，同时确保公平和透明的汇率。

作为其持续致力于安全的一部分，[Kamino Finance](https://app.kamino.finance/) 与Certora合作，进行严格的代码审计，包括对协议中关键不变性的[形式验证](https://learnblockchain.cn/article/13811)，使用[Certora Prover](https://learnblockchain.cn/article/13811)。

我们的[分析](https://www.certora.com/reports/kamino-lending-security-report)揭示了汇率计算中的一个精度损失问题。一个微妙而重要的舍入错误使得某人能够兑换的抵押品超过他们最初存入的量——这是一个边缘案例，虽然今天不可利用，但未来可能成为风险。感谢Kamino的主动做法，他们迅速解决了这个问题，巩固了他们在DeFi安全领域的领导地位。

让我们仔细看看：

### Kamino Lending中的精度损失错误

[Kamino的借贷协议](https://github.com/Kamino-Finance/klend) 确定抵押品份额与流动性之间的汇率，以系统中每个流动性代币的份额价值为基准：

![](https://img.learnblockchain.cn/2025/04/05/30588294_image.png)

汇率采用68位整数和60位分数部分的固定点表示法Fraction，这是Rust内置固定点库[Fixed](https://docs.rs/fixed/latest/fixed/)的一个封装。

这是关键逻辑：

```rust
/// 返回当前的抵押品汇率。
fn exchange_rate(&self, total_liquidity: Fraction) -> LendingResult<CollateralExchangeRate> {
    let rate = if self.mint_total_supply == 0 || total_liquidity == Fraction::ZERO {
        INITIAL_COLLATERAL_RATE
    } else {
        Fraction::from(self.mint_total_supply) / total_liquidity
    };
    Ok(CollateralExchangeRate(rate))
}
```

**除法舍入：** 尽管这种方法在大多数情况下有效，但除法引入了舍入问题，因为**Fraction**类型使用60位用于小数部分：任何值必须舍入到最接近的`2^-60`的倍数。然而，确切的数学商可能有超过60位的精度。在这种情况下，仅保留前60位，其余部分被丢弃，导致存储值稍低。

**后续操作中的误差放大：** 由于汇率在存储为**Fraction**时向下舍入，使用该利率的任何后续计算——例如通过执行除法将抵押品转换为流动性——都可能放大小的精度损失。用稍微过低的数字进行除法会产生稍微过高的商。

**对兑换抵押品的影响：** 汇率向下舍入意味着除法操作可能产生稍大的输出。这在用户赎回抵押品时变得问题重重。协议通过另一算法，确定赎回资产的流动性，将要提取的份额数量除以汇率：

```rust
impl CollateralExchangeRate {
    /// 将储备抵押品转换为流动性
    pub fn fraction_collateral_to_liquidity(&self, collateral_amount: Fraction) -> Fraction {
        collateral_amount / self.rate
    }
}
```

由于汇率向下舍入，在除法操作中使用它可能导致流动性金额上舍入。这可能允许用户提取略高于预期的流动性。

### 我们如何在形式验证的帮助下发现边缘案例？

形式验证的魔力在于其能够探索每个参数的所有可能值，确保即使是最稀有的边缘情况也能被发现。使用[符号执行](https://en.wikipedia.org/wiki/Symbolic_execution)，Certora Prover系统地评估了两个偿付能力不变性：已发行股份的数量始终必须小于或等于基础资产的数量，并且没有用户操作应降低单个股份的价值。

符号执行确保每个潜在的输入组合，包括那些远超出“正常”范畴的组合，都得到了分析。证明者发现这些不变性在某些极端条件下可能会被破坏。

#### **验证归纳不变性**

为了证明不变性是归纳的，我们需要证明它对于可能修改相关金额的每个用户操作都是成立的。在此情况下，必要的值存储在协议的**储备**对象中，因此任何接受**储备**作为参数的操作都需要验证。

使用结构归纳法，我们：

1. **证明基本情况：** 在初始化储备之后，不变性立即成立。
2. **验证步骤情况：** 假设不变性在一个非确定性但固定的状态下成立，我们执行一个操作并确认不变性保持完整。每个操作都导致一个这样的步骤情况。

揭示错误的规则聚焦于兑换抵押品的操作。

**储备偿付能力：** 以下规则假设系统中流动性数量必须大于或等于在调用赎回函数前铸造的抵押品份额数，通过一个非确定性的份额数量`collateral_amount`进行赎回。它检查在赎回操作后该属性是否仍然有效。以下是该规则的要点：

```rust
#[rule]
pub fn reserve_solvency_redeem_reserve_collateral(){
		// 非确定性但固定状态
    let reserve: &mut Reserve = nondet_reserve!();

// 加载前状态
    let liquidity_pre = reserve.liquidity.total_supply();
    let collateral_pre = reserve.collateral.mint_total_supply;

// 假设前状态成立
    cvt_assume!(liquidity_pre >= collateral_pre);

// 检查所有非回退路径的操作
    let collateral_amount = nondet();
    let add_amount_to_withdrawal_caps: bool = nondet();
    lending_operations::redeem_reserve_collateral(
        reserve,
        collateral_amount,
        clock,
        add_amount_to_withdrawal_caps
    ).unwrap();

// 加载后状态
    let liquidity_post = reserve.liquidity.total_supply();
    let collateral_post = reserve.collateral.mint_total_supply;

// 检查存储的流动性 >= 抵押品铸造供应
    cvt_assert!(liquidity_post >= collateral_post);
}
```

Certora Prover发现，在特定条件下，涉及大数字的情况下，偿付能力不变性可能会失败，这是由于在赎回抵押品过程中引入的舍入误差。通过系统地测试操作与偿付能力规则，Prover暴露了这一微妙问题，展示了形式验证的精确度和全面性。

**股份价值演变：** 显示关键路径的第二条规则涉及假设在时间推移中股份价值的发展性质。无论执行哪种用户操作，股份的价值只能增加。具体而言，这意味着必须满足以下条件：

![](https://img.learnblockchain.cn/2025/04/05/80389025_image.png)

我们可以以下面（简化的）方式检查这种行为：

```rust
#[rule]
pub fn share_value_redeem_reserve_collateral(){
		// 非确定性但固定状态
    let reserve: &mut Reserve = nondet_reserve!();

// 加载前状态
    let liquidity_pre = reserve.liquidity.total_supply();
    let collateral_pre = reserve.collateral.mint_total_supply;

// 加载后状态
    let liquidity_post = reserve.liquidity.total_supply();
    let collateral_post = reserve.collateral.mint_total_supply;

// 检查 liquidity_pre/collateral_pre ≤ liquidity_post/collateral_post
    cvt_assert!(liquidity_pre*collateral_post <= liquidity_post*collateral_pre);
}
```

Certora Prover展示了另一个赎回的反例，允许用户降低股份价格。一旦被标记，人工审计团队分析了被标记的代码路径，确认了错误并将其与现实世界的影响进行了上下文化。

### 了解Solana上的误差阈值和可利用性风险

需要注意的是，尽管舍入错误在流动性计算中引入了轻微的向上偏差，但今天在Solana上并不可利用。在计算过程中，汇率向下舍入，引入的舍入错误非常小（每次操作最多`2^-60`）。当将大量抵押品数量除以此汇率时，产生的流动性值可能上舍入。具体而言，像超过`2^59`的抵押品数量这样的极大数字，可能使绝对误差在金融计算中变得显著。

为了把这一点放在上下文中，Solana生态系统中供应量最大的代币之一是BONK。在撰写本文时，BONK Token的供应量为：

```rust
Supply: 88854036064747.15849. (使用63位存储此值)
Price: $0.00001076
Market Value: $956M
```

要触发舍入错误，我们需要存入大于`2^59`的数量，并且必须有一个具有正确特征的汇率。如果我们模拟一下，则可以得到：

```rust
起始状态：
Reserve: total liquidity:   1000000
Reserve: collateral supply: 999999
exchange_rate: 0.999998999999999999

存款：
deposit   2000000000000000000 liquidity
exchange_rate: 0.1000000000000000000
received  1999997999999999999 collateral

赎回：
redeem    1999997999999999999 collateral
received  2000000000000000001 liquidity

结束状态：
Reserve: total liquidity:   999999
Reserve: collateral supply: 999999
```

这表明通过利用这个舍入错误，获得1个BONK的lamport是可能的，而攻击者需要价值**$216m**的`2e12`个BONK代币才能进行攻击。这是目前最大单一BONK持有账户持有量的三倍左右。这些数字表明，这个舍入问题在此时几乎不具可利用性，尤其是考虑到执行此类攻击的交易成本。

不过，**识别这个边缘案例突显了前瞻性安全实践的重要性**。尽管这远远超出了当前Solana代币的供应，未来仍然存在潜在的问题。在理论上，这种行为允许用户通过赎回超过他们最初提供的抵押品而进行利用，这就是免费的钱💸

虽然目前生态系统使得利用这个漏洞在现在可行，但揭示这一点强调了将形式验证与手动审计相结合的必要性。它展示了符号工具揭示微妙的边缘性漏洞的能力，单靠手动工作可能会遗漏。

### Kamino借贷团队是如何修复汇率计算中的精度损失问题的？

尽管在发现时这个错误并不可利用——因为目前没有Solana代币的总供应量足以触发它——Kamino立即采取行动，增强其协议对未来风险的防范。

他们实现了业界标准的**Mul-Div模式**，以确保精确且安全的汇率计算。更新的公式遵循以下通用结构：

```rust
collateral_amount * total_liquidity / total_collateral_supply
```

通过向下舍入此计算的结果，该修复[保证](https://prover.certora.com/output/696612/3b2a3cf46a84404193fd4d0b11230f74/?anonymousKey=723d59c10c84cd7f12a25b9f93f442d08fc84db1)用户在赎回时无法提取超过预期的流动性。

### 结论

这个案例体现了为什么**结合形式验证和手动代码审计是DeFi安全的黄金标准**。手动审计擅长于评估逻辑和寻找创意漏洞，而形式验证深入探讨数学保证和边缘情况。形式验证确保协议能够抵御未来变化，无论是来自拥有较大供应的新代币，还是区块链动态的不可预见变化。

项目通过及早捕捉这些错误建立信任和韧性，表明他们对安全性和可靠性的承诺。Kamino Finance对该问题的积极响应突显了他们对DeFi安全的承诺。他们选择修补这个不可利用的错误，而不是忽视它，从而确保他们的协议在Solana生态系统发展时仍然强大。

在[Certora](https://www.certora.com/)中，我们以帮助像Kamino这样的团队识别和减少安全风险为荣，以防它们成为问题。通过利用形式验证，我们能够检测到即使是最微妙的漏洞，帮助DeFi协议保持最高的安全标准。

想要通过Certora确保你的协议安全吗？ [今天联系我们](https://www.certora.com/signup?plan=audit)!

>- 原文链接： [certora.com/blog/securin...](https://www.certora.com/blog/securing-kamino-lending)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

Kamino Lending及其对安全的承诺

Kamino Lending (KLend) 是一个基于Solana的前沿借贷协议，旨在提供高效的去中心化借贷解决方案。KLend专为速度和可扩展性而构建，让用户提交抵押品并借贷流动性，同时确保公平和透明的汇率。

作为其持续致力于安全的一部分，Kamino Finance 与Certora合作，进行严格的代码审计，包括对协议中关键不变性的形式验证，使用Certora Prover。

我们的分析揭示了汇率计算中的一个精度损失问题。一个微妙而重要的舍入错误使得某人能够兑换的抵押品超过他们最初存入的量——这是一个边缘案例，虽然今天不可利用，但未来可能成为风险。感谢Kamino的主动做法，他们迅速解决了这个问题，巩固了他们在DeFi安全领域的领导地位。

让我们仔细看看：

Kamino Lending中的精度损失错误

Kamino的借贷协议确定抵押品份额与流动性之间的汇率，以系统中每个流动性代币的份额价值为基准：

汇率采用68位整数和60位分数部分的固定点表示法Fraction，这是Rust内置固定点库Fixed的一个封装。

这是关键逻辑：

/// 返回当前的抵押品汇率。
fn exchange_rate(&self, total_liquidity: Fraction) -> LendingResult&lt;CollateralExchangeRate> {
    let rate = if self.mint_total_supply == 0 || total_liquidity == Fraction::ZERO {
        INITIAL_COLLATERAL_RATE
    } else {
        Fraction::from(self.mint_total_supply) / total_liquidity
    };
    Ok(CollateralExchangeRate(rate))
}

除法舍入： 尽管这种方法在大多数情况下有效，但除法引入了舍入问题，因为Fraction类型使用60位用于小数部分：任何值必须舍入到最接近的2^-60的倍数。然而，确切的数学商可能有超过60位的精度。在这种情况下，仅保留前60位，其余部分被丢弃，导致存储值稍低。

后续操作中的误差放大： 由于汇率在存储为Fraction时向下舍入，使用该利率的任何后续计算——例如通过执行除法将抵押品转换为流动性——都可能放大小的精度损失。用稍微过低的数字进行除法会产生稍微过高的商。

对兑换抵押品的影响： 汇率向下舍入意味着除法操作可能产生稍大的输出。这在用户赎回抵押品时变得问题重重。协议通过另一算法，确定赎回资产的流动性，将要提取的份额数量除以汇率：

impl CollateralExchangeRate {
    /// 将储备抵押品转换为流动性
    pub fn fraction_collateral_to_liquidity(&self, collateral_amount: Fraction) -> Fraction {
        collateral_amount / self.rate
    }
}

由于汇率向下舍入，在除法操作中使用它可能导致流动性金额上舍入。这可能允许用户提取略高于预期的流动性。

我们如何在形式验证的帮助下发现边缘案例？

形式验证的魔力在于其能够探索每个参数的所有可能值，确保即使是最稀有的边缘情况也能被发现。使用符号执行，Certora Prover系统地评估了两个偿付能力不变性：已发行股份的数量始终必须小于或等于基础资产的数量，并且没有用户操作应降低单个股份的价值。

符号执行确保每个潜在的输入组合，包括那些远超出“正常”范畴的组合，都得到了分析。证明者发现这些不变性在某些极端条件下可能会被破坏。

验证归纳不变性

为了证明不变性是归纳的，我们需要证明它对于可能修改相关金额的每个用户操作都是成立的。在此情况下，必要的值存储在协议的储备对象中，因此任何接受储备作为参数的操作都需要验证。

使用结构归纳法，我们：

证明基本情况： 在初始化储备之后，不变性立即成立。
验证步骤情况： 假设不变性在一个非确定性但固定的状态下成立，我们执行一个操作并确认不变性保持完整。每个操作都导致一个这样的步骤情况。

揭示错误的规则聚焦于兑换抵押品的操作。

储备偿付能力： 以下规则假设系统中流动性数量必须大于或等于在调用赎回函数前铸造的抵押品份额数，通过一个非确定性的份额数量collateral_amount进行赎回。它检查在赎回操作后该属性是否仍然有效。以下是该规则的要点：

#[rule]
pub fn reserve_solvency_redeem_reserve_collateral(){
        // 非确定性但固定状态
    let reserve: &mut Reserve = nondet_reserve!();

    // 加载前状态
    let liquidity_pre = reserve.liquidity.total_supply();
    let collateral_pre = reserve.collateral.mint_total_supply;

    // 假设前状态成立
    cvt_assume!(liquidity_pre >= collateral_pre);

        // 检查所有非回退路径的操作
    let collateral_amount = nondet();
    let add_amount_to_withdrawal_caps: bool = nondet();
    lending_operations::redeem_reserve_collateral(
        reserve,
        collateral_amount,
        clock,
        add_amount_to_withdrawal_caps
    ).unwrap();

    // 加载后状态
    let liquidity_post = reserve.liquidity.total_supply();
    let collateral_post = reserve.collateral.mint_total_supply;

    // 检查存储的流动性 >= 抵押品铸造供应
    cvt_assert!(liquidity_post >= collateral_post);
}

股份价值演变： 显示关键路径的第二条规则涉及假设在时间推移中股份价值的发展性质。无论执行哪种用户操作，股份的价值只能增加。具体而言，这意味着必须满足以下条件：

我们可以以下面（简化的）方式检查这种行为：

#[rule]
pub fn share_value_redeem_reserve_collateral(){
        // 非确定性但固定状态
    let reserve: &mut Reserve = nondet_reserve!();

    // 加载前状态
    let liquidity_pre = reserve.liquidity.total_supply();
    let collateral_pre = reserve.collateral.mint_total_supply;

        // 检查所有非回退路径的操作
    let collateral_amount = nondet();
    let add_amount_to_withdrawal_caps: bool = nondet();
    lending_operations::redeem_reserve_collateral(
        reserve,
        collateral_amount,
        clock,
        add_amount_to_withdrawal_caps
    ).unwrap();

    // 加载后状态
    let liquidity_post = reserve.liquidity.total_supply();
    let collateral_post = reserve.collateral.mint_total_supply;

    // 检查 liquidity_pre/collateral_pre ≤ liquidity_post/collateral_post
    cvt_assert!(liquidity_pre*collateral_post &lt;= liquidity_post*collateral_pre);
}

了解Solana上的误差阈值和可利用性风险

需要注意的是，尽管舍入错误在流动性计算中引入了轻微的向上偏差，但今天在Solana上并不可利用。在计算过程中，汇率向下舍入，引入的舍入错误非常小（每次操作最多2^-60）。当将大量抵押品数量除以此汇率时，产生的流动性值可能上舍入。具体而言，像超过2^59的抵押品数量这样的极大数字，可能使绝对误差在金融计算中变得显著。

为了把这一点放在上下文中，Solana生态系统中供应量最大的代币之一是BONK。在撰写本文时，BONK Token的供应量为：

Supply: 88854036064747.15849. (使用63位存储此值)
Price: $0.00001076
Market Value: $956M

要触发舍入错误，我们需要存入大于2^59的数量，并且必须有一个具有正确特征的汇率。如果我们模拟一下，则可以得到：

起始状态：
Reserve: total liquidity:   1000000
Reserve: collateral supply: 999999
exchange_rate: 0.999998999999999999

存款：
deposit   2000000000000000000 liquidity
exchange_rate: 0.1000000000000000000
received  1999997999999999999 collateral

赎回：
redeem    1999997999999999999 collateral
received  2000000000000000001 liquidity

结束状态：
Reserve: total liquidity:   999999
Reserve: collateral supply: 999999

这表明通过利用这个舍入错误，获得1个BONK的lamport是可能的，而攻击者需要价值$216m的2e12个BONK代币才能进行攻击。这是目前最大单一BONK持有账户持有量的三倍左右。这些数字表明，这个舍入问题在此时几乎不具可利用性，尤其是考虑到执行此类攻击的交易成本。

不过，识别这个边缘案例突显了前瞻性安全实践的重要性。尽管这远远超出了当前Solana代币的供应，未来仍然存在潜在的问题。在理论上，这种行为允许用户通过赎回超过他们最初提供的抵押品而进行利用，这就是免费的钱💸

Kamino借贷团队是如何修复汇率计算中的精度损失问题的？

尽管在发现时这个错误并不可利用——因为目前没有Solana代币的总供应量足以触发它——Kamino立即采取行动，增强其协议对未来风险的防范。

他们实现了业界标准的Mul-Div模式，以确保精确且安全的汇率计算。更新的公式遵循以下通用结构：

collateral_amount * total_liquidity / total_collateral_supply

通过向下舍入此计算的结果，该修复保证用户在赎回时无法提取超过预期的流动性。

结论

这个案例体现了为什么结合形式验证和手动代码审计是DeFi安全的黄金标准。手动审计擅长于评估逻辑和寻找创意漏洞，而形式验证深入探讨数学保证和边缘情况。形式验证确保协议能够抵御未来变化，无论是来自拥有较大供应的新代币，还是区块链动态的不可预见变化。

在Certora中，我们以帮助像Kamino这样的团队识别和减少安全风险为荣，以防它们成为问题。通过利用形式验证，我们能够检测到即使是最微妙的漏洞，帮助DeFi协议保持最高的安全标准。

想要通过Certora确保你的协议安全吗？今天联系我们!

原文链接： certora.com/blog/securin...

登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

翻译
学分: 9
标签: Kamino Lending Solana 安全性代码审计精准度损失正式验证

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。