Iosg：为什么我们要领导运行时验证？

iosgventures认为，运行时验证技术在学术界和工业实践中处于领先地位，将在区块链安全领域树立新的标杆。

原标题：iosg每周简报为什么我们要领导运行时验证

运行时验证是根植于区块链和传统高科技行业代码安全审计的全球领先企业。开发了业界***的“形式验证”安全审计技术，并将大力运用该技术提高智能合约系统的安全系数，重塑区块链金融基础设施的行业安全标准。

Iosg ventures有幸成为自2010年成立以来**运行时验证融资的领军投资者，我们将积极参与运行时验证在区块链行业的普遍应用，并在市场能力、人才**等方面为团队提供深度支持，市场营销和业务发展。

在本文中，我们将分享由运行时验证开发的形式化验证技术在区块链安全领域的独特价值。

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

随着各种区块链应用的快速发展，区块链上的资金量呈指数级增长。智能合约的安全性已成为投资者和开发者关注的首要问题。据aithority统计，仅在2020年，就有122起区块链黑客攻击，直接造成价值38亿美元的数字资产损失。

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

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

形式化验证是一种革命性的安全审计方法，它与传统的安全审计有着本质的区别。形式化验证首先在公链底层的虚拟机上建立数学模，然后在字节码级对智能合约代码进行验证。这种基于**层的验证可以从智能合约的所有可能输入和初始状态开始，逐步推导出所有可能的最终状态。当中间推导过程卡住时，可以定位漏洞的位置。与手工审计相比，形式化验证技术基于严格的数学方法导出所有可能的系统状态，其安全性比普通手工审计高出几个数量级。

A660202选择了安全分析覆盖率和自动化程度不同的形式化验证技术方案

来源：INRIA，法国政府研究所

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

自然语言具有相对较大的容忍度，允许从不同角度进行解释，甚至在一定程度上容忍误解，而编程语言则要求开发人员向计算机说出准确的指令。如果没有严格的定义来传达每个程序的意图，就无法保证计算系统的高可靠性和高安全性。

形式语义是对计算机编程语言语义的严格定义。

根据“程序设计语言形式语义学”的定义，形式语义学是计算机领域的一门学科。它以数学为工具，用符号和公式精确地定义和解释计算机程序设计语言的语义，从而将语义形式化。简言之，形式语义学就是要找到一个能够使开发人员的开发意图（语义）和实现（语法）完全匹配的语言框架。

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

来源：newbedev

由于基于大量数学证明的计算机形式语义的复杂性，大多数早期的计算机语言设计者没有足够的精力和能力为开发语言定义形式语义。他们经常使用特殊的解释程序、编译器或其他手工工具，但这种结果会带来很多漏洞。

伊利诺伊大学计算机科学教授Grigore rosu（UIUC）和运行时验证的创始人，在NASA实验室工作时，开始为大多数计算机语言开发一个通用的正式语义框架。他认为，如果编程语言没有正式的语义定义，就不可能定义和判断程序是否正确运行。

什么是 K Framework？

K是一个可执行的语义框架，它可以通过配置、计算和规则来定义编程语言、计算和各种表达式分析工具。简而言之，它是一个计算机程序的语言框架，允许您以直观和模块化的方式定义和执行形式语义。用户可以使用它来验证各种编程语言（如SOLid），或者基于这个框架重新设计自己的编程语言。当然，这一切的前提是在这种严格的形式框架下，编程的安全性将得到极大的提高。

来源：运行时验证

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

早在2016年，运行时验证就密切关注区块链行业，当时吸引他们关注的是以太坊的Dao攻击。

在区块链行业的安全审计领域，特别是底层基础设施领域，运行时间验证的真正领先地位在于他们与ETHunm 2开发的安全审计中的ETHunm基金会的深度合作（他们已经开发了一个正式的框架来模拟和验证ETHum 2信标链协议，我们已经成功地验证了Gasper协议以及与iohk（Cardano开发公司）在kevm和iele（Cardano的两个测试环境：kevmamp；雅乐）；耶尔；）

运行时验证区块链客户（部分列表）

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

运行时验证结合了领先的学术研究能力和广泛的行业经验，这已经在NASA、丰田和head区块链项目中得到了证明。

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

另一方面，运行时验证的k框架在工具用户友好性和自动化方面比其他竞争产品更具竞争力。用户可以自由选择或定义任何语言进行编程和验证。

然而，行业的共同努力可以提升科学的创新边界，正式验证也将受益于certora、certik和hevm等其他强大团队的努力和竞争。特别是在区块链开放和社区驱动的精神下，我们相信**团队之间的合作将加速正式验证的应用。

运行时验证与智能合约审计团队（跟踪bits、consensys、diligence、quantstamp等）

目前，大部分区块链安全审计团队仍采用传统的审计形式。正如我们前面解释的，正式验证可以提供更强大的安全级别。我们也看到了令人鼓舞的现象。一些安全审计公司已经开始尝试一些初级产品的正式验证，如Manticore。我们预计，未来几年，区块链代码的形式化验证与智能合约的安全审计将有越来越多的交叉点。

结论

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