三分钟读懂区块链安全审计机构 Runtime Verification 形式化验证方案

原文标题：《IOSG Weekly Brief #81 | 为什么我们领投 Runtime Verification》撰文：IOSG Ventures

Runtime Verfication 是一家扎根区块链以及传统高科技行业代码安全审计的全球头部企业，开发了行业内最先进的「形式化验证」安全审计技术，并将大力运用这一技术提升智能合约系统的安全系数，重塑区块链金融基础设施的行业安全标准。

IOSG Ventures 非常荣幸成为 Runtime Verification 自 2010 年成立以来首次融资的领投者。我们将积极参与 Runtime Verification 在区块链行业实现形式化验证技术的普遍应用，并将为团队在产品适应的市场能力、人才招募、市场推广和业务发展上提供深度支持。

本文我们将分享 Runtime Verification 开发的形式化验证技术在区块链安全领域的独特价值。

区块链为什么需要安全审计？

随着区块链各种应用的快速发展，链上资金的金额呈指数级增长。智能合约的安全变成了投资者和开发者的首要关注。据 AIthority 报道，仅在 2020 年就有 122 起区块链黑客攻击事件，直接造成了价值 38 亿美金的数字资产损失。

截至 2021 年 6 月，DeFi 智能合约的锁仓资产已超出 520 亿美元。如果出现重大漏洞，资产损失将不可避免，甚至项目会就此彻底失去用户的信任。尽管目前大多数 DeFi 智能合约都经过了一定程度的审计，但各种安全事故仍然层出不穷，因此区块链需要一个更好的工具来保障其安全。

形式化验证技术是区块链审计的未来吗？形式化验证是什么？相比于人工审计优势在哪？

形式化验证是一种革命性的安全审计方法，与传统的安全审计有着根本的不同。形式化验证首先会在公链最底层的虚拟机上建立一套数学模型，然后在字节码级别去检验智能合约代码。这种基于最底层级别进行的验证可以从智能合约所有可能的输入、初始状态出发，逐步推导出所有可能的结束状态，当中间推演过程出现卡壳时即可定位出漏洞的位置。相比于人工审计，形式化验证技术基于严格的数学方法，推导出所有可能的系统状态，因此其安全性要高出普通的人工审计几个数量级。

不同形式化验证技术方案在安全分析覆盖的程度和自动化水平的取舍

资料来源：法国政府研究机构 Inria

Runtime Verification 的核心技术——编程语言的形式语义框架 K FrameworkK Framework 的诞生背景

自然语言具有比较大的容忍度，允许从不同角度诠释甚至容忍一定程度上的误解，而编程语言需要开发者告诉电脑准确的指令。如果没有严格的定义来传达每段程序的意图 , 则无法保证高可靠性和高安全性的计算系统。

「形式化语义（formal semantics）」 就是计算机程序语言的语义作严格定义。

根据《编程语言的形式化语义（Formal Semantics of Programming Language)》 的定义，形式语义学是属于计算机领域中的学科，它是以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义，使语义形式化。简单来说，形式语义学就是要寻找能让开发者的开发意图（即「语义」）和实现（即编程语言的「语法」）精确相符的语言框架。

什么是编程语言里的语法（Syntax）和语义（Semantics）？

资料来源 : Newbedev

由于计算机的形式语义学需要基于大量的数学证明，具有高度复杂性，因此大多数计算机语言的早期设计者并没有足够的精力和能力来为开发语言定义正式的语义，他们往往会使用特制的解释程序、编译器或其他的手动工具，但这样的后果就是会带来大量的漏洞。

伊利诺伊大学香槟分校（UIUC）计算机科学教授、Runtime Verification 的创始人 Grigore Rosu 在他早期在 NASA 实验室工作时，就开始为大多数计算机语言开发一套通用形式语义框架。他认为如果没有对编程语言的语义正式定义，就无法定义和判断程序是否正确运行。

什么是 K Framework？

K 是一个可执行的语义框架，可通过配置、计算和规则来定义编程语言、calculi 以及各种表达式分析工具。简单来说它是一套计算机程序的语言框架，能让你用一种直观和模块化的方法去定义和执行形式语义，用户能够用它来验证各种编程语言（比如 Solidity），或者可以基于这套框架重新设计自定义的编程语言。当然这一切的前提是在这套严谨的形式化框架下，编程的安全性将大大提高。

资料来源 : Runtime Verification

Runtime Verification 正在成为区块链安全审计的行业标准

早在 2016 年，Runtime Verification 就密切关注区块链行业，而那时候引起他们注意的是以太坊的 DAO 攻击事件。

在区块链行业安全审计尤其是底层基础设施领域，真正奠定 Runtime Verification 领先地位的是他们与以太坊基金会在 Ethereum 2.0 开发的安全审计上的深入合作（开发了一个模拟和验证 Ethereum 2.0 信标链协议的形式化框架，并成功验证了 Gasper 协议）以及与 IOHK （Cardano 开发公司）在 KEVM 和 IELE 的合作（Cardano 的两个测试环境：KEVM&IELE;）。

Runtime Verification 的区块链客户（部分名单）

Runtime Verification 相对其他解决方案的优势

Runtime Verification 结合了领先的学术研究能力和其广泛的行业实践经验，这一点在美国国家航空航天局、丰田以及头部区块链项目中得已验证。

一方面，在安全级别上，Runtime Verification 的「动态验证」比市场上许多其他竞品的「静态验证」具有更高的安全级别。与其他团队直接验证源代码相比，Runtime Verification 在 EVM 等虚拟机上使用 K Framework 形式化建模，直接验证字节码。同时，可以在实际运行环境下对程序进行验证，进一步保证了编译器的安全。Runtime Verification 和以太坊 2.0 信标链协议 Gasper 、Cardano、Algorand 等在基础设施上的深度安全审计合作就可以证明这一点。

另一方面，Runtime Verification 的 K-Framework 在工具用户友好性和自动化方面比其他竞品采用的 Coq 更有竞争力。用户可以自由选择或定义任何语言来编程与验证。

然而，行业共同努力才能推动科学的创新边界，形式化验证也将受益于其他强大团队的努力竞争，例如 Certora、CertiK 和 hevm。特别是在区块链领域的开放和社区驱动的精神下，我们相信顶尖团队之间的合作将加速形式化验证的应用。

Runtime Verification VS. 智能合约审计团队（Trail of Bits,ConsensysDiligence,Quantstamp等）

目前，大部分区块链安全审计团队依旧使用传统的审计形式。而正如我们在前文所解释的，形式化验证能提供更强数量级的安全性。我们也看到了令人鼓舞的现象，一些安全审计公司已经开始尝试一些形式化验证的初级产品，例如 Manticore。我们预计在未来几年，区块链代码的形式化验证和智能合约安全审计之间的交叉会越来越多。

结论

随着区块链市场尤其是去中心化的金融基础设施的爆发式发展，人们对链上资产的安全需求迫在眉睫。现有的安全审计服务将无法满足金融基础设施日益增长的安全需求。形式化验证是常用于军事、航空航天等对系统安全性要求非常高的领域的计算机安全技术，也非常适用于区块链底层协议和金融基础设施。Runtime Verification 是学术和工业实践中形式化验证技术的领导者。IOSG Ventures 相信该团队将在区块链安全领域建立行业新标杆。