形式化验证合约并不是防弹的
Aave的代码库经过了形式化验证,区块链领域的一个趋势是,人们会认为安全特性是圣杯。用户可能会尝试根据这些特性的存在与否,对各种合约的安全性进行排序。
这是危险的,它会导致错误的安全感。
Aave形式化验证报告列出了 LendingPool 视图函数(例如,它们没有副作用)以及池操作(例如,操作成功后返回true且不还原)的属性。
然而,如果逻辑合约遭到破坏,则该属性可能会被破坏。那如何才能对此进行验证?虽然无法访问定理证明或所使用的设置,但很可能证明proof没有考虑可升级性,或者prover不支持复杂的合约交互。
这在代码验证中是很常见的。你可以通过对整体行为的假设来证明目标组件中的行为,但是在多合约设置中证明属性是具有挑战性和耗时的,因此必须进行权衡。
形式化验证技术很棒,但是用户必须意识到它们覆盖范围很小,并且可能会错过攻击媒介。另一方面,自动化工具和人工审查可帮助开发人员以较少的资源来提升代码库的安全性。
了解每种解决方案的优点和局限性,对开发人员和用户而言都至关重要。
Aave做出了积极反应,并在发现问题后迅速修复了该漏洞。危机避免了,但最近遭受黑客攻击的其他受害者却没有那么幸运。
本帖 steem 首发
最近新帖
- defi保险引入流动性
- 百倍爆发的Aave
- 瑞波defi的Spark
- 中国在 CBDC 以及未来货币赛道领跑
- uGAS喂价和质押
- 资产跨链先行者ChainX
- Bancor开启流动性挖矿
- Alpha Homora新增Uniswap ETH / DPI带杠杆流动性资金池
- AC下一个目标
- KingSwap的高收益流动性平台
- Fireblocks DeFi的功能
- 建立数字信任
- Inclusive Pool 的新玩法中有何机遇
- 稳定币挖矿成了一种需求很大的市场
- DeFi下半场
- 为加密爱好者准备的ETF加密产品
- CrescoFin将与DODO进行上币计划
- DeFi协议共同点
- DeFi堆栈中的原子价值层
- defi源起MakerDao
- 闪电贷是部署资金的桥梁
- DEFI逐步替代传统金融
- DeFi真实锁仓量突破120亿美元
- DeFi新星Harvest的兴起
- DeFi+CeFi结合
- 黑客的狂欢
- 以太坊2.0将提升DeFi
- DeFi高危下的无风险保险方案
- 闪电贷与预言机防篡改
- NGK DeFi项目Baccarat
- 各国推动数字货币
- 流动性挖矿基本宣告终结
- 配置以太坊算力资产的价值和意义
- L2哪家方案胜出
- 速度增长的DeFi合规性
- 马云的金融
- 解锁DeFi挖矿新姿势
- 基于真实需求的新DeFi项目:Stoploss,Overlay,Unipeer,Crescendo
- DeFi意味着什么
- ourDeFi去中心化借贷
- 其他公链的逆袭
- Tokenview DeFi数据查
#chinese #hnt #zzan #upfundme #actnearn #spt #lifestyle #steemleo #marlians #dblog #neoxian #aaa #palnet #liv #iv #creativecoin #mediaofficials #lassecash #cn
本帖中 , @hnt 作为受益人获得奖励 : 7.682 $ + 0.0 STEEM + 47.724 SP = 89.933 STEEM = 16.368 $ , 因此 @hnt 保留 5%(4.497 STEEM) 作为费用 , 并且支付本帖作者 85.436 STEEM . 谢谢使用 @hnt 的流动性服务 !
详细说明 ...