RuntimeVerification：为以太坊等动态分析审计的形式化验证项目

Runtime Verification Inc 是一家初创公司，使用执行期验证技术对公链虚拟机和智能合约进行安全性审计，通过使用自己研发的动态分析验证技术致力于提高和区块链领域的软件系统的安全性，可靠性和正确性。

目前区块链安全审计领域多为静态分析（只对源代码内部逻辑进行审计），而动态分析（使用代码编译后执行时产生的数据进行审计）能够涵盖的安全漏洞比静态分析要广得多。Runtime Verification 拥有世界顶尖的形式化验证团队， 能够对编译后的二进制代码直接进行验证。相比对源代码进行形式化验证，可以发现由于编译器的问题而发生的一些很难找到的 bug。

优点：

团队有世界顶级的动态分析技术

在区块链领域之外也拥有丰富的成功经验

与许多顶级公链平台已建立合作关系

缺点：

媒体曝光少，知名度仍较低

团队不重视交易所、钱包方向业务的拓展

缺乏动态分析验证技术和其它审计方式表现的横向比较

行业（9/10）

区块链安全一直是行业关心的热点之一。交易所盗币、公链合约 bug 盗币、钱包 bug 盗币等都在行业内频繁发生，共造成数十亿美元的损失。目前交易所上币都要求有优质的安全审计报告，也间接促成了区块链安全行业的蓬勃发展。

与 Runtime Verification 有直接竞争关系的是耶鲁大学 Shao Zhong 教授创办的 Certik。两者都使用了形式化验证的技术对区块链项目进行代码审计。两者最大的不同点是， Runtime Verification 可以对虚拟机直接进行建模， 进而进行动态分析，而 Certik 的形式化验证仍然限于对源代码的静态分析。因此，Runtime Verification 的技术门槛更高一些， 审计的结果也更有说服力。从市场定位来看，Runtime Verification 的客户为各大公链， 而 Certik 更多为上层的生态项目服务，也体现了这一点。

模式（8/10）

在涉及区块链领域之前，runtime verification 就为汽车，飞机，航天器等系统提供先进的安全验证服务。从 2009 年开始，成为 NASA 的安全供应商， 陆续拿到了 3 笔政府合同。其它非区块链领域的客户包括 NSF，DARPA，丰田，波音等。

在区块链领域，Runtime Verification 目前主要为资金和技术雄厚的公链和 Defi 协议提供服务，目前的客户包括 IOHK(Cardano 的开发公司)、以太坊、Algorand、Web3 基金会、Elrond、Casper Labs、Gnosis、MakerDAO 等。

在商业推广上，Runtime Verification 似乎并不热衷于参加各种区块链大会，而是主要通过技术社区向外渗透。根据官方 ppt 中描述的伙伴佣金机制，成功推荐一名客户可获得 5% 佣金， 独立完成一个销售可以获得 15% 佣金。

技术 （8.5/10）

目前，针对区块链行业， Runtime Verification 提供以下业务的解决方案 : 智能合约审计、共识机制、虚拟机、代币等。

在智能合约审计领域， Runtime verification 验证技术依赖于程序执行不应违反某些属性的原理。Runtime verification 可以自动检查通用属性，不需要开发输入，并且可以检查开发人员用形式化方式表达的任何定制属性。

相比与 Certik 等直接对源代码进行形式化验证， Runtime Verification 通过对 EVM 等虚拟机进行 K-形式化标记，因此可以直接对编译后的二进制码进行验证，相比传统的形式化验证手段，进一步保证了编译器的安全性。Runtime Verification 开发了三大工具， 分别称为 RV-Match， RV-Predict 和 RV-Monitor。RV-Match 是一个基于语义的纠错器及动态类型检查器。RV-Predict 是一个动态数据竞争的检测器，不会出现假警报且最全面地找到可能的所有数据竞争。RV-Monitor 是一个执行期的监测工具，可以检测和施行所有保证执行期安全的性质。通过这三大工具， 可以较全面地覆盖到执行期出现的许多 bug。

在共识机制领域，Runtimeverification 将协议的 Safety 和 Liveness 两个性质总结成数学模型，并且明确列举出满足这些性质需要的假定条件。如此一来，开发者可以对在其上构造的系统的性质有更准确的期待。

在虚拟机领域， Runtime verification 与 IOHK 合作开发了 IELE 虚拟机，是以太坊虚拟机的一次重要进化。它证明了以太坊虚拟机通过 K-形式化标记后，可以自动生成一个「足够快」的虚拟机。

在代币领域，Runtime verification 开发了 ERC-20 和 ERC-777 代币标准的 K-形式化标记版本，是行业中第一个可以允许形式化验证的代币标准。

Runtime verification 的 github 非常活跃，有 55 个 repo， 且都为业务相关 最近有更新的 repo 包括以太坊信标链的属性， MakerDAO 多资产抵押 (MCD) 的属性， Casper 协议的属性、之前审计过的智能合约、波卡 WASM 虚拟机的审计等等， repo 中 commit 数量最多的是 IELE 虚拟机语义标记的 repo，共 1279 次。考虑到代码贡献者只有 10 个人，这样高的开发活跃度是区块链项目中非常罕见的。

尽管理论上动态验证的结果应当更全面，目前尚没有看到将其跟静态验证的横向比较， 因此这项技术在实际应用中的表现，以及性价比， 尚不能很好地被衡量。

社区生态（6/10）

Runtime Verification 的 Twitter 有 1172 个粉丝， 社区管理员在 reddit 上的以太坊版面较为活跃。近期团队仅参加过 Devcon 活动，以及一些小型学术会议， 没有在别的大型币圈活动上曝光过。因此， Runtime Verification 相比 Certik 的知名度要低得多。

Runtime Verification 主要的宣传渠道是通过与项目方合作的官宣。然而， 他们的官宣在国内外媒体都很少看到，说明团队在宣发方面并不重视。

此外，Runtime Verification 似乎并不热衷于中心化交易所、钱包方面的业务，这一点与 Certik 有很大的不同。由于目前这方面的业务仍然是更好的盈利点， Runtime Verification 的盈利前景可能因此而受负面影响。

团队（8/10）

网站上在团队一共列了 36 人， 包括 2 名管理层， 3 名顾问， 23 名研究工程人员和 8 名合作者。

CEO 是执行期验证概念的提出者，UIUC 教授 Grigore Rosu。他于 2000/2001 发表的几篇论文，奠定了执行期验证领域的理论基础， 并于 2016 年被 ACM 协会自动化工程分会评为最佳论文。

COO Patrick MacKay 曾创办并任职于 Capital One 银行在 UIUC 的研究中心， 以及曾任职于 004 GmbH，一家德国电商。

项目的顾问包括 UIUC 的科创中心主任 Jed Taylor， UIUC 计算机教授 Darko Marinov， 以及康奈尔计算机博士 Philip Daian。

总的来看，团队非常的学术范， 缺乏懂得币圈商业运营方面的成员，这是项目的一个短板。

融资

项目没有公布融资信息。

总结（8/10）

Runtime Verification 拥有较顶级的动态形式化验证技术， 在进入区块链领域之前就拥有丰富的军工、汽车等领域的业务经验， 可以提供智能合约审计、共识机制、虚拟机、代币等多项区块链相关的审计服务。目前客户已经囊括了几大重量级的公链以及 Defi 协议， 有良好的业务前景， github 上的开发活动也非常活跃。

然而， 由于团队对宣发和参会不是很重视， 导致品牌曝光率较低，社区也规模很小以硬核开发者为主， 并且团队似乎对服务交易所和钱包获得更丰厚的利润并不感兴趣。动态形式化验证技术相比传统审计方式，也没有能证明其实际表现优越性的案例。综合来看，该项目以技术见长，短板在于商务拓展和品牌建设。

如果您喜欢这篇报告，请支持我们的研究BTC 地址 ：

162Cnh4gLGxvfBzpGoJ6JYZBbYHncJeDaN

ETH 地址 :

0x9206D3D4ddd6a40f1Cadd19f25cB55E7A85de475

—-

编译者/作者：Evaluape

玩币族申明：玩币族作为开放的资讯翻译/分享平台，所提供的所有资讯仅代表作者个人观点，与玩币族平台立场无关，且不构成任何投资理财建议。文章版权归原作者所有。