针对代币智能合约的安全问题,提岀一种基于代币智能合约整数溢岀漏洞的形式化建模与验证方法。分析现有 The dao和BEC等漏洞攻击事件,定义代币智能合约的安全属性,通过引入全局变量和数值比较等约束条件对代币智能合约的建模语言进行扩展,使其支持智能合约各类语句的形式化表示。借鉴数学归纳法的思想,优化 Smart verif模型验证过程,避免状态空间的无限遍历。实验结果表明,该方法能成功找岀代币智能合约的整数溢出漏洞,并且具有较强的通用性。
声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉
全部0条评论
快来发表一下你的评论吧 !