Vitalik对它竖起大拇指

9月10日的万向区块链大会上，以太坊创始人Vitalik 了解完成都链安科技的智能合约形式化验证VaaS平台后竖起了大拇指，同时表达了合作的意愿，感谢成都链安科技为以太坊生态安全所做出的贡献。

成都链安科技的掌舵人是杨霞女士，学霸杨霞老师，从本科到博士，一路“保送”。博士毕业后留校任教，在电子科技大学信息与软件工程学院担任副教授。创立链安之前她曾三次创业，都是围绕安全，势要把安全的牢底坐穿。

第四次创业的起因源于区块链史上一个知名的漏洞——The DAO事件。2016年The DAO安全事件爆发后，她尝试用形式化验证解决区块链智能合约的安全问题，并意识到区块链安全存在的痛点和需求，于是立马转向区块链安全领域。2018年3月获得分布式资本的股权投资，创办了成都链安科技。

经过短短的半年时间，成都链安科技已经和国内外30多家知名公链、联盟链、交易所等达成了合作。目前，成都链安主攻智能合约的形式化验证，同时提供智能合约的安全开发服务，审计开发一条龙服务。

今年5月，成都链安科技发布了智能合约形式化验证平台VaaS 1.0，成为全球第一个同时支持EOS和ETH的智能合约形式化验证平台。近期，还将发布VaaS 2.0版本。

以下内容来自哔哔News与杨霞的对话整理。

01

链安是我第四次创业

很多人以为链安是我第三次创业，其实认真算起来，应该是第四次创业。最早一次创业是在我读博士期间，2008年。

每次创业，我选择的方向都很准，比如我从很早期就开始研究安卓系统的安全。但每次创业都踩了不少坑，要么在最后产品化的时候才发现合作伙伴没选对，要么过于专注技术，不懂得市场，推广不利。

这次创业，我总结了之前的经验教训，准备得更加充分。而且合伙人郭文生教授在形式化验证区域积淀也很深，我们是形式化验证的两个门派，此前我们也多次合作，志同道合。

进入区块链行业后，我真正体会到链圈一天人间一年，也成长了很多。我至今仍旧无法理解，为什么那么多项目一定要发币？为什么大家对币的关注度比对技术的关注度还高？别人都不相信我不炒币。

 02

智能合约的形式化验证

目前以太坊之上智能合约漏洞分为10大类27个小类。由智能合约安全问题导致的损失已经达到14亿美元。

我相信，未来随着落地应用越来越多，智能合约的数量肯定会爆发性增长。未来面向行业领域特定需求的智能合约，业务逻辑会更加复杂，而且会逐步形成标准化开发流程。

同时智能合约很可能会以电子合同的形式出现，逐步取代原来的纸质合同，更加结合实际应用的需要，为实业服务。

因此目前链安主攻智能合约安全审计和开发。

我们采用形式化验证的方式对智能合约的安全性和功能正确性进行高度自动化的形式化验证，减少人工参与提高验证效率。

通过对已发现的安全漏洞建立安全属性模型，然后VaaS工具再自动证明这些安全问题是否存在。整个证明过程由严格的数学推导完成，相比人工以及其他安全扫描工具更加严谨、准确。

形式化验证是根据某些规范、属性使用数学的方法，证明“其”（软件系统、硬件系统）的正确性。它是系统性的过程，使用数学推理来验证系统的设计意图是否符合用户期待的功能需求，同时保证安全。

目前针对智能合约的安全验证主要分为两派。一派是形式化验证，一派是白帽社区的渗透测试。

形式化验证和渗透测试的区别是测试不能穷举，只能测出某些已知Bug，但未知的Bug却显示不出来。

形式化验证可以通过数学推理的方式满足功能正确性，同时保证一定不存在指定属性的安全问题、或者一定存在指定安全属性的问题。

举一个我们合作过的真实案例，在之前的一次合作中，有个项目方事先找了一个安全公司做了代码安全审计，审计结果为通过。为保万无一失，项目方再次找到我们进行第二次审计。

我们在Vaas形式化验证平台上对该合约进行审计时，发现了一个重大安全漏洞，通过我们进一步人工复核，发现该漏洞的确存在。之后和项目方沟通，为其重构了整个合约。 

03

我们要做全生态区块链产品

在链安起步时，我们用传统的人工建模方式，发现人工建模代价太大，人工参与对人员的素质要求很高，形式化人才又很紧缺，不适合工业化。

后来，我们开始往自动化方向发展，降低人工成本的同时减少人为误判，提高形式化验证的准确度，让合约审计变得更严谨更准确。

目前，我们已开发完成了“一键式”安全验证平台VaaS。

它的操作非常简单，只需把公链的合约代码导入VaaS自动验证工具，点开始审计按钮，工具就会开始审查智能合约的漏洞，并且精确到代码的哪一行存在常规安全隐患。因此VaaS被成为“一键式”智能合约形式化验证平台。对于复杂的功能逻辑的正确性验证，则需要部分人工的参与。

VaaS的安全检测准确度高达95%以上，相比市场上大多半自动化的形式化验证产品，我们可以说做到了高度自动化。

不同公链的虚拟机和代码语言都不一样，不同的语言需要采用不同的验证方法。我们针对不同公链项目定制开发VaaS验证工具，这对公链的生态安全是一大帮助。

近期，我们会开放VaaS 2.0版本的部分功能给大家免费试用，也是对我们工具的一次展示。如果在试用过程中发现存在安全漏洞的合约，欢迎反馈给我们，我们会给与奖励。通过新发现的安全问题，不断丰富我们的形式化验证库。

除了不断提高形式化验证的自动化程度，链安未来的产品规划是做全生态的区块链安全产品。不仅仅是面向智能合约的安全，未来，我们将会瞄准更多的区块链安全场景和需求，做更多新的产品。