科研之友
微信
新浪微博
Facebook
分享链接
摘要
针对智能合约对安全性方面的相关性质的极高要求,有必要改进已有的建模算法,提出将智能合约函数的函数体语句建模为DTMC的算法,并对生成的DTMC进行验证。通过为状态迁移添加概率,实现了对随机现象的关注。通过对调用函数的分类处理,精细化了对函数调用函数情况的处理。通过添加标识符,实现了对智能合约所有控制语句的支持。对常被用于判定函数是否可以被触发的require语句,提供了差异化的处理方式从而改善算法的处理能力。同时对智能合约应保障的部分性质进行规约以验证模型效果。实验结果表明,建模方法可以实现对智能合约所有控制结构语句建模的支持,能够实现对合约函数的建模并完成验证。
- 单位
