哔哔News采访杨霞」: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版本的部分功能给大家免费试用,也是对我们工具的一次展示。如果在试用过程中发现存在安全漏洞的合约,欢迎反馈给我们,我们会给与奖励。通过新发现的安全问题,不断丰富我们的形式化验证库。


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


哔哔News采访原文请点击阅读原文查看!




成都链安科技官方发表正式声明:


近期,有XX链安科技与成都链安科技重名,且Logo及宣传语相似。成都链安科技是一家由分布式资本股权投资的专门从事区块链安全的公司,与其他XX链安科技无任何关联。请大家认准成都链安科技唯一指定商标品牌,谨防上当受骗,一切消息以官网及官方公众号为准。


成都链安科技官方公众号名称:链安科技

成都链安科技官方网址:

www.lianantech.com

——成都链安科技官方




关于链安科技


成都链安科技有限公司,专注区块链安全领域,总部位于成都。由电子科技大学杨霞和郭文生两位教授共同创建,团队核心成员由近40名来自海外知名高校和实验室留学经历的教授、博士后、博士及阿里、华为等知名企业精英组成。其核心技术为形式化验证,该团队使用此技术为航天、军事等领域提供多年的形式化验证服务,是国内唯一一家将此技术应用到区块链安全领域的公司。


成都链安科技获得了分布式资本等著名投资机构的股权投资,已与Huobi、OKEX、KuCoin、LBank、CoinBene、CoinMex、CoinTiger、ONT、Scry、Qtum、QuarkChain、IoTeX、比原链、布比区块链、云象区块链等30多家区块链公司签订战略合作协议。在国家工信部发布的《2018中国区块链产业白皮书》中公司榜上有名,公司已经入选Etherscan智能合约安全审计推荐名单,且荣获“OKEx 最佳安全审计合作伙伴奖”。



成都链安科技

作为Huobi、OKEX、LBank、CoinBene等

著名交易所指定的合约审计公司。 

入选Etherscan智能合约安全审计名单。

欢迎联系链安,进行智能合约安全审计。

 ·

电话:028-83262585

网站:www.lianantech.com

邮箱:[email protected]


官网:

https://www.lianantech.com


GitHub网址:

https://github.com/Lianantech/VCA


Facebook网址

https://www.facebook.com/LianAnTechChengdu/


twitter网址:

https://twitter.com/LianAnTech_com


Telegram中文群:

https://t.me/LiananTech_cn


Telegram英文群:

https://t.me/LiananTech_en


微博:

https://weibo.com/u/6566884467


CSDN博客:

https://blog.csdn.net/CDLianan