EN
2021.06.14-06.21
Part.1 Insight
Runtime Verification: 区块链安全审计行业的变革者
Runtime Verfication 是一家扎根区块链以及传统高科技行业代码安全审计的全球头部企业，开发了行业内最先进的“形式化验证”安全审计技术，并将大力运用这一技术提升智能合约系统的安全系数，重塑区块链金融基础设施的行业安全标准。
IOSG Ventures 非常荣幸成为 Runtime Verification 自 2010 年成立以来首次融资的领投者。 我们将积极参与 Runtime Verification 在区块链行业实现形式化验证技术的普遍应用，并将为团队在产品适应的市场能力、人才招募、市场推广和业务发展上提供深度支持。
本文我们将分享 Runtime Verification 开发的形式化验证技术在区块链安全领域的独特价值。
区块链为什么需要安全审计？
**
**
随着区块链各种应用的快速发展，链上资金的金额呈指数级增长。智能合约的安全变成了投资者和开发者的首要关注。据 AIthority 报道，仅在 2020 年就有 122 起区块链黑客攻击事件，直接造成了价值 38 亿美金的数字资产损失。
截至 2021 年 6 月，DeFi 智能合约的锁仓资产已超出 520 亿美元。如果出现重大漏洞，资产损失将不可避免，甚至项目会就此彻底失去用户的信任。 尽管目前大多数 DeFi 智能合约都经过了一定程度的审计，但各种安全事故仍然层出不穷，因此区块链需要一个更好的工具来保障其安全。
形式化验证技术是区块链审计的未来吗？
形式化验证是什么？相比于人工审计优势在哪？
形式化验证是一种革命性的安全审计方法，与传统的安全审计有着根本的不同。形式化验证首先会在公链最底层的虚拟机上建立一套数学模型，然后在字节码级别去检验智能合约代码。这种基于最底层级别进行的验证可以从智能合约所有可能的输入、初始状态出发，逐步推导出所有可能的结束状态，当中间推演过程出现卡壳时即可定位出漏洞的位置。 相比于人工审计，形式化验证技术基于严格的数学方法，推导出所有可能的系统状态，因此其安全性要高出普通的人工审计几个数量级。
不同形式化验证技术方案在安全分析覆盖的程度和自动化水平的取舍
资料来源：法国政府研究机构 Inria
Runtime Verification 的核心技术——编程语言的形式语义框架 K Framework
**
**
K 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, Consensys Diligence, Quantstamp 等）
目前，大部分区块链安全审计团队依旧使用传统的审计形式。而正如我们在前文所解释的，形式化验证能提供更强数量级的安全性。我们也看到了令人鼓舞的现象，一些安全审计公司已经开始尝试一些形式化验证的初级产品，例如 Manticore。 我们预计在未来几年，区块链代码的形式化验证和智能合约安全审计之间的交叉会越来越多。
结论
**
**
随着区块链市场尤其是去中心化的金融基础设施的爆发式发展，人们对链上资产的安全需求迫在眉睫。现有的安全审计服务将无法满足金融基础设施日益增长的安全需求。形式化验证是常用于军事、航空航天等对系统安全性要求非常高的领域的计算机安全技术，也非常适用于区块链底层协议和金融基础设施。 Runtime Verification 是学术和工业实践中形式化验证技术的领导者。IOSG Ventures 相信该团队将在区块链安全领域建立行业新标杆。
Part.2 投融资事件
安全审计机构 Runtime Verification 完成 530 万美元融资， IOSG Ventures 领投
*安全审计
安全审计机构 Runtime Verification 完成 530 万美元融资， IOSG Ventures 领投，Fenbushi Capital、Maven 11、Borderless Capital、cFund、Hypersphere、Elrond Research 和 Tezos Foundation 参投。募集的资金将用于加速工具的开发，旨在提高不同区块链和嵌入式系统的安全性、可靠性和正确性，以及推广「运行中验证」（Runtime Verification）的方式来审计虚拟机以及智能合约。
去中心化衍生品交易所 SynFutures 完成 1400 万美元 A 轮融资，Polychain 领投
*去中心化衍生品交易所
去中心化衍生品交易所 SynFutures 宣布完成 1400 万美元的 A 轮融资，由 Polychain Capital 领投，Framework Ventures、Pantera Capital、Bybit、Wintermute、CMS、Kronos 和 IOSG Ventures 参投。目前 Synfutures 合约已部署至以太坊主网及 Polygon，正通过官网邀请用户进行 closed alpha 测试，并计划于 7 月份正式对全用户开放。Polychain Capital 创始人兼首席执行官 Olaf Carlson-Wee 表示，「随着去中心化交易所占领更大的市场份额， 我们认为 SynFutures 有机会在去中心化衍生品市场占据优势。」
波卡生态跨链去中心化交易平台 Mangata 完成 140 万美元融资
*去中心化交易平台
波卡生态跨链去中心化交易平台 Mangata 完成 140 万美元融资，参投放包括 Polychain Capital、 IOSG Ventures 、Altonomy、CMS Holdings、TRGC，个人投资者包括天使投资人 Ricky Li 等。Mangata Finance 是为波卡上的交易者和流动性提供者创建的协议，作为基于波卡的 DEX 和平行链，其交易资产可以通过其自行开发的 POLKA-ETH 桥在两个生态系统之间完成迁移。Mangata 共识协议通过将订单随机排序处理，用户不需支付网络费，可防止抢跑交易。
加密金融服务商 Amber Group 以 10 亿美元估值完成 1 亿美元 B 轮融资
*加密金融
加密金融服务商 Amber Group 以 10 亿美元估值完成 1 亿美元 B 轮融资，投资方包括 Tiger Brokers、Tiger Global Management、Arena Holdings、Tru Arrow Partners、A&T; Capital、Sky9 Capital、DCM Ventures 和 Gobi Partners，A 轮融资参与机构 Pantera Capital、Coinbase Ventures 和 Blockchain.com 继续参与，本轮融资所得将用于全球扩张。
Amber Group 成立于 2017 年，总部位于香港，企业创始人均来自摩根、高盛、彭博社等华尔街顶尖投行，为全球 200 多家知名大型机构及零售客户提供全年 24 小时全天候服务，包含算法交易、电子做市、高频交易、场外交易、借贷、衍生品等产品。2020 年 2 月 Amber Group 完成 2800 万美元 A 轮融资，投资者包括 Pantera Capital、Paradigm、Polychain、Coinbase Ventures 和 Dragonfly Capital 等区块链投资机构，估值 1 亿美元，而此次 Amber Group B 轮融资最新估值为 10 亿美元，是 A 轮融资的十倍。
Bybit 发起的 BitDAO 完成 2.3 亿美元融资，Peter Thiel、Pantera 和 Dragonfly 领投 z
*DAO
去中心化自治组织 BitDAO 宣布完成 2.3 亿美元融资，Peter Thiel、Founders Fund、Pantera Capital 和 Dragonfly Capital 领投，Alan Howard、Jump Capital、Spartan Group、Fenbushi、Kain Warwick （Synthetix）、Peak Capital、NGC、LongHash Ventures 等参投，另外加密货币衍生品交易所 Bybit 已承诺将其期货合约交易量的 0.025% 收入贡献到 BitDAO 的财库中，按今年 1 月至 5 月的收入作为参考，预计每年将超过 10 亿美元，并将随着 Bybit 业务的增长和整体加密货币行业的成长而不断扩大。
去中心化衍生品交易所 dYdX 完成 6500 万美元 C 轮融资，Paradigm 领投
*DEX
去中心化衍生品交易所 dYdX 完成 6500 万美元 C 轮融资，由 Paradigm 领投，流动性供应方 QCP Capital、CMS Holdings、CMT Digital、Finlink Capital、Sixtant、Menai Financial Group、MGNR、Kronos Research 和投资机构 HashKey、Electric Capital、Delphi Digital 及合作伙伴 StarkWare 跟投，a16z、Polychain Capital、Three Arrows Capital、Wintermute 等往轮参投机构也参与了本轮融资，本轮融资资金将主要用于 1. 将协议去中心化；2. 迅速为永续合约添加新的资产和功能；3. 推出手机端应用；4. 与基础设施参与者合作，弥合中心化和去中心化金融之间的差距；5. 对亚洲等国际增长型市场进行战略投资；6. 继续聘用世界一流工程师、设计师和企业运营人员。
加密资产管理公司 Bitwise 完成 7000 万美元 B 轮融资，黑石集团、桥水基金高管参投
*加密资产管理公司
加密资产管理公司 Bitwise 以 5 亿美元估值完成 7000 万美元融资，Elad Gil、Electric Capital 领投，参投方包括 Third Point LLC、Willoughby Capital、Moore Strategic Ventures、Vetamer Capital、Coinbase Ventures、ParaFi Capital、Blockchain Coinvestors 等，个人投资者包括 D1 Ventures 合伙人 Daniel Sundheim、传奇对冲基金经理 Stanley Druckenmiller、黑石集团美洲房地产主管 Nadeem Meghji、桥水基金首席执行官 David McCormick、前美联储理事 Kevin Warsh、Facebook App 负责人 Fidji Simo、Google X CFO Helen Riley、前 Facebook 副总裁 Carolyn Everson 与 Julie Zhuo、Visa 董事会董事 Mary Cranston、前花旗银行负责人 Tracey Warson、Instagram 产品负责人 Ashley Yuki、Spotify 产品负责人 Howard Akumiah 等。本轮融资将用于新产品开发。
Part.3 行业脉搏
四川省发改委、能源局要求各市州清理关停虚拟货币挖矿项目
*政策
据多个微信群流传的照片显示，四川省发改委、能源局面向各州市人民政府、国网四川省电力企业、省能投集团、中央在川发电企业、省属国有发电企业，发布《关于清理关停虚拟货币「挖矿」项目的通知》，通知表示，将「打击比特币挖矿行为」。
StarkWare 推出的 ZK Rollup 扩容解决方案 StarkNet 测试版本已在以太坊测试网 Ropsten 上线
*扩容
零知识证明研发机构 StarkWare 研发的二层扩容解决方案 ZK Rollup「StarkNet」的测试版本已在以太坊测试网 Ropsten 上线。该测试版本没有白名单，允许任何开发人员编写和部署用于一般计算的 StarkNet 合约。用户可以通过向这些合约发送交易并检查其状态来与这些合约进行交互。StarkNet 的状态转换经过链下验证，然后在链上验证。团队表示，将在未来几周内完善 L1 与 L2 的交互、链上数据和可组合性。
以太坊存储项目 Swarm 结束公募， 并已正式上线 1.0 主网
*以太坊存储项目
以太坊 存储项目 Swarm 基金会宣布 Swarm 1.0 主网正式上线，并将于 6 月 21 日 21:00 开启 Swarm One 活动，该活动将对 Swarm 1.0 及未来发展进行演讲。另外，Swarm 于 CoinList 的公募现已结束，此前计划通过销售超 517 万枚 BZZ 代币来募集约 993 万美元。Swarm 将于 6 月 21 日分发除 CoinList 公募募集，CoinList 公募参与者将在 8 月 2 日前后获得代币。
马斯克母亲将发布 NFT，并于推文内提及麦子钱包
*NFT
伊隆·马斯克（Elon Musk）的母亲 Maye Musk 发推表示，将于今日和 6 月 24 日通过 BakerySwap 发行个人 NFT，并在推文中提及麦子钱包。麦子钱包表示，还将支持她的 NFT 拍卖和收藏。MATH 是围绕多链、跨链以及资产 Hub 为核心的区块链平台，旗下产品包括：麦子钱包、MathVault、MathDAppStore、MathStaking、MathCustody、MathNFT、MathChain、MathHub、MathDEX、MathID、MathPay 等。
去中心化内容发布平台 Mirror 为 NFT 新增限量发行工具 Editions
*去中心化内容发布平台
去中心化内容发布平台 Mirror 添加 Editions 为 NFT 新增限量发行工具 Editions。Mirror 认为，当前创作者的作品拍卖的最终结果仅能有一人竞拍成功，而且价格往往非常高，这并不利于普通投资者或者粉丝参与。Editions 实现以固定成本铸造多份 NFT，创作者可以将自己的作品复制多份进行限量发行从而降低门槛，同时首先出售的 NFT 价值更高也一定程度上保证了稀缺性，并且规避了铸造多份 NFT 产生的高手续费问题。
Part.4 IOSG 投后项目进展
