全球首个EOS安全管家：区块链形式化验证平台VaaS

编辑：铅笔盒

近年来，随着The DAO、Parity钱包、Coincheck等一系列区块链平台安全事件的频繁爆发，区块链平台特别是智能合约的安全问题成为这项新技术向前发展的障碍。针对这一安全性问题，国内外研究学者一致认为，严格的形式化验证方法能够有效地提高区块链生态系统的安全性。

为此，兼具中国“985工程”与“双一流”称号的电子科技大学信息与软件工程学院杨霞副教授带领一支区块链形式化验证团队，经过近2年的研究和努力，研制出了一套高度自动化的区块链形式化验证平台VaaS（Verification as a Service）。该团队由20多名具有海外知名高校（如耶鲁、UCLA）留学经历的副教授、博士、硕士组成，具有多年的形式化验证经验。自2013年起，杨霞副教授所带领的团队也已经为航天、国防等领域的安全关键软件提供了专业的形式化验证服务。

VaaS形式化验证平台，采用了多种形式化验证方法，具有验证效率高、自动化程度高、人工参与度低、易于使用、支持多个合约开发语言、可支持大容量区块链底层平台的形式化验证等优点。VaaS提供了针对智能合约的形式化验证工具，极大提高了智能合约的安全性与可靠性。产品通过对合约代码进行严格的安全验证，杜绝逻辑漏洞，确保合约安全，在满足实际应用效率需求的同时，达到有效控制漏洞风险的目的。目前，VaaS平台已支持主流区块链平台（如以太坊等）智能合约的形式化验证，并且已与国内10多家区块链行业的知名企业建立了合作关系。

近期，VaaS将重点专注于EOS区块链平台的形式化验证工作，为EOS提供全面的形式化验证服务，包括EOS智能合约的形式化验证，EOS平台底层软件的形式化建模和验证。未来，VaaS平台将逐步支持其它主流区块链平台的形式化验证工作，将为更多的区块链平台提供形式化验证服务。

目前，杨霞副教授的团队已经得到分布式资本的投资，并成立了成都链安科技有限公司。链安科技因此成为中国首个专门从事区块链安全的团队，也是分布式资本资助的唯一一个致力于区块链平台安全的公司。成都链安科技现正与LongHash、Cybex共同建立服务于EOS生态系统的形式化验证社区，为EOS的安全运行保驾护航！

小科普——你知道什么是形式化验证方法吗？

所谓形式化验证方法，即指在计算机科学领域，特别是软件工程和硬件工程中，一种特殊的基于数学的技术，用于规范、开发和验证软件和硬件系统，以提高系统的安全性、可靠性和鲁棒性。形式化方法可以形容为建立在相当广泛的理论计算机科学基础上的应用，特别是逻辑演算，形式语言、自动机理论、离散事件动态系统和程序的语义，还包括类型系统和代数数据类型等理论。一般这类研究主要应用于昂贵的航空、航天、军事器材的操作系统、危险的医疗设备的程序之中。