形式化验证：让智能合约更安全(2)

智能合约采用全生命周期的形式化验证，在设计和开发过程都可用形式化验证，代码的形式化验证在统一的环境可以采用源码和编译后的字节码进行双管齐下的验证，源代码进行转换验证，编译后的字节码进行反编译验证低级别性能，两个验证方法利用等价证明保证功能、运行上的一致。如以太坊可用在F*环境下进行验证，反编译字节验证gas总量上限。

【本文是51CTO专栏作者“”李少鹏“”的原创文章，转载请通过安全牛（微信公众号id:gooann-sectv）获取授权】

戳这里，看该作者更多好文

【编辑推荐】

1. 一文深入了解：分布式系统中的缓存架构
2. 量子技术威胁加密基础 区块链或成救星
3. 海星、蜘蛛与区块链
4. 区块链技术能否解决「疫苗之痛」？
5. 收藏 | 第一次有人把“分布式事务”讲的这么简单明了

（编辑：ASP站长网）