2019.12.13康跃馨在软件技术大会做《区块链合约的自动形式化验证实践》演讲

区块链合约的自动形式化验证实践

本次报告主要介绍了智能合约的现状、带来的问题、解决方案和形式化方法，用自动形式化验证来保证合约安全性。区块链节点需要具备：加密、通信、共识、合约这⼏部分功能，以太坊或其他很多实现都是将所有部分编译打包在⼀个可执⾏程序。这⼏部分最容易出问题的是合约层，主要思路是先解决最容易出安全问题的那部分。智能合约的⼤部分逻辑较为标准化，相对较容易⽤形式化验证的⽅式进⾏查验，由于区块链开发⼈员的稀缺，远远⽆法赶上智能合约数量的增⻓，⼈⼯审计智能合约是成本⾮常⾼昂的，因此机器辅助验证是必要的。