基于模型检测的区块链众筹合约形式化验证方法

摘要文本

本发明公开了一种基于模型检测的区块链众筹合约形式化验证方法，涉及众筹类区块链智能合约安全技术领域，解决了众筹合约应用场景缺少专用的安全解决方案的技术问题。本发明包括：对获取的智能合约代码进行漏洞分析，对存在漏洞的智能合约代码进行优化；对优化的智能合约代码或不存在漏洞的智能合约代码进行模块分化，对分化的模块进行形式化建模，得到智能合约代码模型；声明智能合约满足的性质规约，性质规约包括可达性、有界性和安全性；根据性质规约，通过智能合约代码模型对智能合约进行形式化验证。本发明快速、有效实现众筹合约上链前的漏洞排查，为众筹合约的形式检查提供了专业的解决方案。