区块链研究实验室|形式验证如何帮助防止Gridlock错误( 五 )
综上所述 ， 对lock函数节码的符号执行可能揭示了这三种不良行为 ， 并且仔细检查它们可能发现其中一种可被DoS攻击利用 ， 从而在部署之前修复了Gridlock错误 。
吸取教训
EVM通常是不直观的 。
Gridlock错误源自对EVM设计中某些非显而易见部分的错误理解 。 如果不考虑EVM级别的智能合约 ， 就很容易错过这种EVM问题 ， 并且可能会再次引入类似的bug 。
形式验证可以提供帮助 。
如果不采用有原则的方法 ， 那么探索所有可能的行为（尤其是在EVM级别）并非易事 。 形式验证 ， 尤其是它的符号执行过程 ， 可以系统地探索给定智能合约的所有可能行为 ， 这比仅手工检查代码要严格得多 。
具体来说 ， 我们的KEVM验证程序使用的是EVM的确切规范（又称KEVM） ， 不会让您摆脱错误的假设 。 如上所示 ， 它甚至会发现执行路径非常不可能 ， 例如攻击者找到哈希的预映像并将其合同部署到下一个地址的情况 。
推荐阅读
- gta三部曲|梦幻西游：129级五开分析师，研究抓鬼任务最优化投入，不浪费一分钱
- 电子竞技|S12或迎来双败制？Riot全球电竞负责人发话：会去仔细研究！
- 世界弹射物语|皇室战争：职业选手研究的英雄卡组，要论机动性，黄金圣骑YYDS
- 新世界|游戏推出一个多月就在研究合服，《新世界》如今情况如何？
- fly|Fly让AG得重新研究对策，终结ES八连胜！留在S组只差AG这一步
- 弈星|职业赛场八连跪，弈星已经被研究透了？这英雄的强度到底如何？
- 原神|原神成为中国文化敲门砖，这群老外甚至因北斗研究起了国产导航
- 鲁班|王者荣耀：将王研究出鲁班发育秘诀，网友看后纷纷点赞！
- 青钢影|《地下城与勇士》：玩这个游戏，要花时间研究一下活动和成长路线
- 手机游戏|哈利波特手游：虎牙四个四深入研究，配置斯内普卡组，只为榜一