安比（SECBIT）受邀2018网络安全生态峰会 热议智能合约安全问题

8月21-22日，由中国互联网协会、阿里巴巴、蚂蚁金服、阿里云主办的“2018网络安全生态峰会”在北京举行。本届峰会的主题为“共建网络防线，共治安全环境，共享安全生态”。吸引了众多政府主管部门、国内、国际安全行业顶尖专家、学者，高端技术人才的关注和参与。安比（SECBIT）实验室创始人郭宇受邀出席本届峰会，就智能合约安全与形式化验证问题同与会嘉宾进行了深入交流。

网络安全生态峰会(原阿里安全峰会)是国内创办最早、规模最大、嘉宾阵容最强大、安全行业最权威的国际大型安全盛会之一，本次大会主要探讨前沿安全趋势、全球化数据保护、AI与内容治理、金融安全与黑灰产治理、互联网＋知识产权保护、云安全、区块链安全等社会关注领域。

当前，区块链行业的技术创新正在经历一个明显加速的过程，区块链技术的应用将带来新的商业规则和新的业态，帮助企业重塑形态，改进社会结构。以区块链技术的应用——智能合约为例，使用智能合约来执行合同将会提高商业交易效率，增加信任和确定性。据悉，英国法律委员会正在将智能合约的使用写入英国法律。智能合约的发展前景由此可见一斑。

安比（SECBIT）创始人郭宇就智能合约安全发表演讲

然而，智能合约的安全问题并不鲜见。安比（SECBIT）实验室发现，以太坊上ERC20 Token 智能合约中，带有整数溢出漏洞的合约共有 630 个，超过 2,000 个 Token 的转账功能存在缺陷。“智能合约问题频出，严重影响了区块链应用的发展。”SECBIT创始人郭宇博士对智能合约的安全现状深表忧虑。郭宇指出，目前阶段，智能合约安全问题主要有三类：第一是合约安全漏洞遭受黑客攻击，造成资金损失；第二是Token 合约管理者拥有超级特权，权力中心化，随意增发 Token，丧失可信度；第三是ERC20 Token智能合约标准混乱，转账功能存在缺陷。
为解决智能合约安全问题，安比（SECBIT）实验室将形式化验证应用于智能合约安全领域，首次完成了完整的ERC20形式化证明，并以开源的方式发布。携带显式形式化证明的智能合约具有更高的可信度，任何人可以采用轻量级的证明检查工具来检验智能合约代码是否满足所证明的性质，比如发行总量不变、增发过程的权限合理等等。

安比（SECBIT）创始人郭宇在2018网络安全生态峰会

“智能合约的安全性不能建立在对某个权威的依赖基础上，也不能建立在不开源的软件工具上，是否能以去中心化的方式去验证其正确性是智能合约安全的关键。”在郭宇看来，形式化验证是保证智能合约没有问题的唯一办法，更重要的是，它能以一种去中心化的方式检验形式化验证的结果。从而从根本上杜绝合约的实现与意图之间的差异。
安比（SECBIT）实验室专注于区块链与智能合约安全问题，全方位监控智能合约安全漏洞、提供专业合约安全审计服务，在智能合约安全技术上开展全方位深入研究，致力于参与共建共识、可信、有序的区块链经济体。

安比（SECBIT）实验室专注于区块链与智能合约安全问题，全方位监控智能合约安全漏洞、提供专业合约安全审计服务，在智能合约安全技术上开展全方位深入研究，致力于参与共建共识、可信、有序的区块链经济体。

安比（SECBIT）实验室创始人郭宇，中国科学技术大学博士、耶鲁大学访问学者、曾任中科大副教授。专注于形式化证明与系统软件研究领域十余年，具有丰富的金融安全产品研发经验，是国内早期关注并研究比特币与区块链技术的科研人员之一。研究专长：区块链技术、形式化验证、程序语言理论、操作系统内核、计算机病毒。

安比（SECBIT）实验室

info@secbit.io