Aave的代码库经过了形式化验证，区块链领域的一个趋势是，人们会认为安全特性是圣杯。用户可能会尝试根据这些特性的存在与否，对各种合约的安全性进行排序。

这是危险的，它会导致错误的安全感。

Aave形式化验证报告列出了 LendingPool 视图函数（例如，它们没有副作用）以及池操作（例如，操作成功后返回true且不还原）的属性。

然而，如果逻辑合约遭到破坏，则该属性可能会被破坏。那如何才能对此进行验证？虽然无法访问定理证明或所使用的设置，但很可能证明proof没有考虑可升级性，或者prover不支持复杂的合约交互。

这在代码验证中是很常见的。你可以通过对整体行为的假设来证明目标组件中的行为，但是在多合约设置中证明属性是具有挑战性和耗时的，因此必须进行权衡。

形式化验证技术很棒，但是用户必须意识到它们覆盖范围很小，并且可能会错过攻击媒介。另一方面，自动化工具和人工审查可帮助开发人员以较少的资源来提升代码库的安全性。

了解每种解决方案的优点和局限性，对开发人员和用户而言都至关重要。

Aave做出了积极反应，并在发现问题后迅速修复了该漏洞。危机避免了，但最近遭受黑客攻击的其他受害者却没有那么幸运。

本帖 steem 首发

形式化验证合约并不是防弹的

最近新帖

1. defi保险引入流动性
2. 百倍爆发的Aave
3. 瑞波defi的Spark
4. 中国在 CBDC 以及未来货币赛道领跑
5. uGAS喂价和质押
6. 资产跨链先行者ChainX
7. Bancor开启流动性挖矿
8. Alpha Homora新增Uniswap ETH / DPI带杠杆流动性资金池
9. AC下一个目标
10. KingSwap的高收益流动性平台
11. Fireblocks DeFi的功能
12. 建立数字信任
13. Inclusive Pool 的新玩法中有何机遇
14. 稳定币挖矿成了一种需求很大的市场
15. DeFi下半场
16. 为加密爱好者准备的ETF加密产品
17. CrescoFin将与DODO进行上币计划
18. DeFi协议共同点
19. DeFi堆栈中的原子价值层
20. defi源起MakerDao
21. 闪电贷是部署资金的桥梁
22. DEFI逐步替代传统金融
23. DeFi真实锁仓量突破120亿美元
24. DeFi新星Harvest的兴起
25. DeFi+CeFi结合
26. 黑客的狂欢
27. 以太坊2.0将提升DeFi
28. DeFi高危下的无风险保险方案
29. 闪电贷与预言机防篡改
30. NGK DeFi项目Baccarat
31. 各国推动数字货币
32. 流动性挖矿基本宣告终结
33. 配置以太坊算力资产的价值和意义
34. L2哪家方案胜出
35. 速度增长的DeFi合规性
36. 马云的金融
37. 解锁DeFi挖矿新姿势
38. 基于真实需求的新DeFi项目:Stoploss,Overlay,Unipeer,Crescendo
39. DeFi意味着什么
40. ourDeFi去中心化借贷
41. 其他公链的逆袭
42. Tokenview DeFi数据查