Beosin 正式完成对 Linea 公链上最大的衍生品交易所 Tifo.trade 的形式化验证与安全专家审计

Beosin2023/10/27 07:30

作者:Beosin

近日，区块链安全领域领军企业 Beosin 正式完成了对 Linea 公链上最大的衍生品交易所 Tifo.trade 智能合约代码的严格审计。

Tifo.trade 是构建在 Linea 链上的 DeFi 项目，将于 9 月 7 日正式上线 Linea 主网。Tifo.trade 在完成智能合约开发，筹备主网上线前，委托 Beosin 对其智能合约代码进行严格的审计。本次 Beosin 的审计包括了 Tifo.trade 项目的稳定币质押、Tifo 代币质押、金库管理、DEX 等业务合约。

Beosin 审计包含形式化验证和安全专家的人工审计，以确保代码没有业务逻辑漏洞，符合预期运行流程和结果。在本次审计中，Beosin 安全专家发现了一个可能导致用户恶意提取额外资产的业务逻辑漏洞。Beosin 第一时间与 Tifo.trade 进行了沟通，随后 Tifo.trade 已修复该漏洞。

审计报告查阅：

https://beosin.com/audits/Tifo_202308171828.pdf

形式化验证的优势

形式化验证的过程：安全人员先使用规范语言编写程序需要满足的规范，然后将规范转换成证明，并用自动化验证引擎检验程序实现与规范的一致性。

对于智能合约的形式化验证，主要有以下三类技术：

1. 模型检测

我们知道，智能合约实际上看作是状态转化器。模型检测通过创建智能合约与其属性的数学表示来验证一个模型（即智能合约）是否满足给定的逻辑公式，如模型检测可以用于验证合约中访问控制，确认特定函数的调用权限。

2. 定理证明

定理证明是将智能合约以及规范转换成逻辑语句，通过验证这些语句的逻辑等价性确保智能合约与其规范是否完全相符。定理证明需要专业人员辅助，目前无法实现证明过程的完全自动化。

3. 符号执行

符合执行是通过符号值（可以理解成某一约束范围里的所有值）而非特定值去推理合约代码的执行轨迹和验证属性。符号执行会使用 SMT 求解器检查代码执行轨迹中需要符号值输入的节点是否存在满足的值，若无满足的值，则该路径存在错误。

由于自动化程度高，模型检测与符号执行在实际工程中的应用频度远超过定理证明，但模型检测与符号执行难以求解非线性约束和计算密集型库函数调用等问题。

Beosin 通过充分挖掘静态分析适用面广和动态分析精确程度高的优势，利用自主研发的高性能 Beosin VaaS 形式化验证工具对智能合约代码进行形式化验证。

Beosin VaaS，一款全球领先的“一键式”智能合约形式化验证平台。检测准确率高达 97% 以上，精确定位风险代码位置并给出修改建议，自动检测智能合约 80 余项的常规安全漏洞及功能逻辑缺陷。Beosin VaaS 可自动发现智能合约中存在的常规漏洞、业务逻辑错误等安全问题，并给出专家的修复意见。同时支持 evm，wasm 的所有公链的智能合约的上百种常规安全漏洞和业务逻辑缺陷检测，能精确定位风险代码位置，帮助开发者提高智能合约的安全能力。

在 Tifo.trade 的合约代码审计中，Tifo.trade 的各合约代码均通过了形式化验证。然而，形式化验证技术存在它的局限性：

例如，形式化验证对于复杂业务合约以及外部函数调用顺序的检验仍有可能存在路径遍历不完备的问题。这是因为复杂合约的验证或者外部函数调用顺序的组合可能导致“状态爆炸”问题，在限定时间内难以找到违反属性规范的可达状态路径。因此，这就需要 Beosin 安全专家的助力。

人 工审计，快速定位复杂业务逻辑漏洞

针对形式化验证技术存在的问题，需要辅以人工审计解决。安全专家的人工审计可以在理解项目业务逻辑的基础上快速定位复杂业务逻辑漏洞。在本次审计中，Beosin 安全专家发现了一个可能导致用户恶意提取额外资产的高危业务逻辑漏洞（Tifo.trade 已修复）。

以下是详细分析：

在 Tifo.trade 的 Staking 合约中可以将持有的 sTIFO 通过 unstake() 提取出本金，这个在提取之后 stakingAmountOf 会减少。由于 stakingAmountOf 为用户的总质押量记录，从这个函数单看的话，提取的本金量不会超过这个质押值。

在 TifoTreasury 合约中进行通过 incurDebt() 进行借贷，在 incurDebt() 中通过用户的 sTIFO 余额获取最大的可借贷数量即 maximumDebt 参数，用户最多可以借出与 sTIFO 持有余额等价值的 usd。在借贷之后用户会增加 debtorBalance 的值作为债务记录，下一次用户的可借贷量就为 maximumDebt 减去 debtorBalance( 即最大借贷量减去总债务量 )。这个函数单看也将无法借出的价值超过本金。

但是由于 unstake() 缺少用户的债务校验，在结合函数的调用顺序，就可以达到将一次的质押金额提取出最多两倍金额的效果。因为用户调用 incurDebt() 进行借贷后仍然持有 sTIFO，只是加了 debtorBalance 债务量，而这并不影响对 unstake() 的本金提取。也就是持有 sTIFO 的用户可以先调用 incurDebt() 借出等额的稳定币，然后再调用 unstake() 提取等额的资产，这样就提取了相当于原来 2 倍的资产。如下图所示：

由于两个函数位于不同的合约，且该业务逻辑漏洞是通过特定顺序的函数调用产生的，使用常规的自动化检测和形式化验证技术都很难发现。尽管该代码通过了开发团队和形式化验证，Beosin 的安全审计专家仍进行了高规格的审计，发现了此次的高危漏洞。

Beosin 建议，对于智能合约审计，应采用形式化验证对合约属性的不变性加以检测，同时结合人工审计检测复杂业务逻辑漏洞。

Beosin 作为一家全球领先的区块链安全公司，业务涵盖项目上线前的代码安全审计、项目运行时的安全风险监控、预警与阻断、虚拟货币被盗资产追回、安全合规 KYT/AML 等“一站式”区块链安全产品 + 服务，已审计智能合约和公链主网超 3000份，同时 Beosin 专注于 DEX 的安全审计，目前已审计包括 PancakeSwap、DoDo Finance、Impossible Finance、TerraSwap、SyncSwap、ArbSwap、BetDEX 等项目。欢迎点击公众号留言框，与我们联系。