2018 ISC互联网安全大会于9月4日至6日在北京国家会议中心隆重举行，安比(SECBIT)实验室创始人郭宇受邀亮相区块链与安全技术论坛，并就“智能合约漏洞与防护”问题与现场嘉宾进行了深入探讨，全面展示了SECBIT 团队在智能合约语言和区块链安全领域攻防兼备的杰出实力。

在区块链应用领域，智能合约利用区块链点对点的技术特性，允许在没有第三方的情况下进行可信、可追踪的交易。“然而，一旦部署就无法修改的特性，为攻击者创造了机会。”郭宇表示。

郭宇指出，智能合约漏洞是区块链独有的风险点，目前阶段，智能合约安全隐患主要有三类：

1 智能合约代码中是否有常见的安全漏洞；2 智能合约是否可信；3 智能合约是否符合一定规范和流程。

以太坊创始人Vitalik曾说，智能合约安全的定义取决于合约的实现与意图之间的差异。郭宇博士对此深表认同，在他看来，形式化验证是保证智能合约没有问题的唯一办法，携带显式形式化证明的智能合约具有更高的可信度，任何人可以采用轻量级的证明检查工具来检验智能合约代码是否满足所证明的性质，比如发行总量不变、增发过程的权限合理等等。更重要的是，它能以一种去中心化的方式检验形式化验证的结果。从而从根本上杜绝合约的实现与意图之间的差异。

安比（SECBIT）实验室利用交互式定理证明工具 COQ 结合形式化规范，采用数理证明的方式，对多个智能合约的重要性质加以证明，如 Token 合约发行总量不变，DEX 合约中管理权限等，从根本上为智能合约提供更高级别的安全保证。目前，携带显式形式化证明的 Token 合约仓库（tokenlibs）已开源，并收录于 ConsenSys 的智能合约工具列表中。

仓库地址：https://github.com/sec-bit/tokenlibs-with-proofs

本文由安比（SECBIT）实验室提供，安比实验室致力于解决区块链全生态的安全问题，共建共识、可信、有序的区块链经济体。合作交流请联系 info@secbit.io。