一种高度自动化的智能合约形式化验证系统及方法

基本信息

申请号 CN201810790872.0 申请日 -
公开(公告)号 CN108985073B 公开(公告)日 2020-05-22
申请公布号 CN108985073B 申请公布日 2020-05-22
分类号 G06F21/57;G06Q40/04 分类 计算;推算;计数;
发明人 杨霞 申请(专利权)人 成都链安科技有限公司
代理机构 成都四合天行知识产权代理有限公司 代理人 成都链安科技有限公司
地址 610000 四川省成都市成华区二环路东二段508号7层714号房
法律状态 -

摘要

摘要 本发明公开了一种高度自动化的智能合约形式化验证系统及方法,包括:步骤001:将智能合约功能需求描述文档转换为使用非自然语言描述的智能合约功能需求规范文档,智能合约功能需求规范文档内容包括目标合约功能规范描述和安全属性描述;步骤002:建立形式化验证规则模型库。步骤003:通过自动化建模工具对合约源代码和/或字节码进行自动化建模;步骤004:对步骤003生成的抽象语法树解析,为代码中常量、变量分配内存地址;步骤005:形式化证明。本发明适应于多种的高级编程语言编写的程序代码,也适应多种形式化语言,同时提供源代码建模和字节码建模两种自动化建模方式,能够针对用户的不同建模需求进行建模,进一步提高验证效率。