Runtime Verification

Runtime Verification简介

Runtime Verification 旨在使用 runtime verification 技术，提升软件系统的安全性、可靠性和正确性。其团队由这一领域的先驱与领导者组成。

运行时验证 runtime verification 是一种动态软件分析方法，可在程序执行时对其进行分析、观察执行结果，并使用这些结果查找错误。

运行时验证 runtime verification 比传统的形式分析技术更轻量级，也不意味着取代传统的基于单元的、功能和集成测试，甚至是轻量级的静态分析工具。

【动态 | 多抵押Dai安全审计结果公布】Runtime Verification、Trail of Bits、PeckShield、Certora四家公司已经完成了对多抵押Dai的安全审计。审计成功发现了系统里的一些漏洞，包括高严重性和重大严重性的问题。Maker开发团队已经评估和解决这些漏洞，并且将继续与审计公司一起，确保多抵押Dai发布前完全解决潜在威胁。 接下来，Maker开发团队将专注于以下方面：1.多抵押Dai的阶段性部署；2.即时访问模块的可升级性，包括直接对Dai信贷系统进行有限制更改的组件，无需通过DS-Chief的全体一致授权；3.紧急关停模块和重新部署的测试运行。

【动态 | 以太坊2.0存款合约字节码完成形式化验证】以太坊基金会宣布ETH 2.0存款合约（deposit contract）字节码的审计和形式化验证（formal verification）已经由技术团队Runtime Verification完成。以太坊基金会表示，这是一个重要的里程碑，使得项目更接近ETH 2.0主网的第0阶段（Phase 0），但以太坊基金会依旧希望其他专业人士或者社区可以对于形式化验证提供更多反馈，可以在代码库提交相关问题。除此之外，以太坊基金会表示虽然ETH 2.0 的第2阶段核心原则已经被定义清楚，但其具体设计还是相对开放的，Quilt（ConsenSys 的研究团队）和eWASM （以太坊基金会的研究团队）在最近一年里已经花了非常多的精力研究，而新成立的TXRX （ConsenSys 的研究团队）会将一部分精力投入到第2阶段的研发中，最初的重点将会放在更好地了解跨分片交易的复杂性，以及研究和原型化将ETH 1.0集成到ETH 2.0的方法。（链闻）}

【动态 | 以太坊2.0抵押合约已准备就绪】金色财经报道，ETH 2.0的抵押合约 (deposit contract) 已通过最后一道障碍，进行了名为“Runtime Verification”的端到端的正式验证。这意味着抵押合约现在可以执行了，尚不清楚它将首先在测试网上启动还是直接在主网上启动。此前，ETH 2.0协调员Danny Ryan在上个月表示，Runtime Verificaton将在一个月内发布其完整的正式验证、分析和报告。一旦发布，我们就可以部署合约。

【Cardano创始人：IOHK与安全审计公司Runtime Verification签署了一份七位数的合同】Cardano创始人、IOHK首席执行官Charles Hoskinson在最新的AMA上透露，IOHK已与安全审计公司Runtime Verification签署了一份七位数的合同。此外，Charles还表示将在10月29日的月度产品更新中发布关于Goguen的路线图。（Crypto News Flash）}

【公告 | Algorand官方：Runtime Verification正式验证Algorand区块链永不分叉】Algorand官方博客发文称：为了更好地保证Algorand协议，并使未来的协议设计和验证更容易，Algorand选择通过机器验证来增强数学上的理论证明。为此，Algorand聘请了具有深入验证能力的专业公司通过运行环境验证来验证Algorand共识协议的正确性。我们很高兴地报告了这项工作的一个重要里程碑：使用Coq定理证明，团队已经开发了一个精确的协议数学模型，并正式验证了其安全保证（区块链从不分叉）。在今年早些时候，Algorand用Runtime Verification（运行时验证）来验证其共识协议。Algorand宣布已经完成该工作的第一部分，即协议建模和证明其安全定理。具体来说，我们使用了一个证明助手（Coq）来系统地确定协议在数学上保证不会分叉的假设。

标签：Runtime Verification

官方信息

• 

  Facebook

• 

  Twitter

• 

  微博

• 

  YouTube