耶鲁大学计算机系教授邵中：CertiK 希望建立完全可信的智能合约以及区块链生态系统

耶鲁大学计算机系教授 &CertiK 联合创始人邵中在第五届区块链全球峰会分享《建立完全可信的智能合约以及区块链生态系统》。

非常荣幸今天来讲网络安全和区块链安全，刚才 Dr. Garvinwood 给了一个很好的 Trust 和 Truth 的阐述，他还说了 Trustworthy 好像跟 True 没什么差别。所以今天要讲讲 Trustworthy 怎么能把像黑箱一样的 Blockchain Ecosystem 变的和 True 一样。

今天的主题主要讲网络安全，网络安全和区块链安全的联系。大家都知道，现在 Blockchain Security 有非常严重的问题，当然不止是 Blockchain 的问题，Cyber Security 本身就有非常巨大的问题。最近的 Data，从 2019 年 Cybersecurity Market Worldwide Share 就有 167Billion dollars，到 2024 认为会有 300billion，这是 Cybersecurity。光在 2019 年上半年 The amount of cryptocurrency stolen 就将近有 4billion，所以 Blockchain Security 是个 major issue。

在讲 Blockchain Security 的时候，一般大家讨论的常见问题都是智能合约的问题，现在有很多给智能合约做审计的公司，大部分讨论的都是 Code Security Loophole，像 Untrustworthy Contracts、Integer Overflow、Unsafe Authorization，当然有很多是功能上的问题。如果 Smart Contract 里有功能上的 bug，那也会被认为是一个 major issue，所有这些 hacker 的 attack 也都是通过 explore 这些 venerability 来导致。

当然，Blockchain Security 其实有更大的问题，大家都知道 security，现在的 Computer system 基本上都有很多的 vnlnerabilities，只不过 hacker 没有攻击这些 computer system 的 motivation，没有被 strongly motivated。

而区块链系统不一样，因为里面存了很多跟 currency 有关的内容，所以整个区块链的 Stack 都可能 go wrong。从底下的 OS、Hypervisor、Storage System 里面都可能有 Bug，到上面的 Blockchain Consensus Protocol 的 Implementation、Smart Contract 本身、Programming Languages Compilers，甚至到上面的 Off-chain 和 Cross-chain 的跨链 Protocols 都有可能带来问题。

其实这些代码是很复杂的代码，不是一般意义上的 sequential code，有很多是 concurrent 和 distributed code。大家都知道 concurrent、distributed code 是很难写对的，所以很多这些 cross chain protocols 本身会带来 Accountability 的 issues。要是好几个 party 在上面做 trade，怎样才能知道一旦有问题究竟是哪个 party 带来的问题？尤其现在有很多是 heterogenes Blockchain，带来的问题更加严重。

大家都说到 Blockchain 不仅要快、performance，又要 Decentralized。一旦你要做跟 perfomance 相关的 optimization，就像 sharding、sophiscated consensus protocols，都会带来很多新的 challenge，带来的 challenge 很可能就把代码变的更糟糕。再往上还要隐私保护，pravacy enforcement，所有的这些就会带来一个问题，十天前美国 US Federal Reserve Chairman, Jerome Powell，说过这样一句话：“It’s one thing to be able to counterfeit paper currency, it’s anotherthing to hack into a cyber currency and create, with a computer, however much of it you want.”

所以 Security 对于区块链系统是至关重要的问题，只要 Blockchain System 能够被 hacker 攻击，只要有一线希望，hacker 一定会把它找出来，所以 security 成不成、能不能对这个问题处理，对将来 Blockchain ecosystem 起一个决定性的作用。

大家都知道我们平时讲形式化验证，or so called formal verification, is supposed to solve all the problem。我要给大家介绍一下——形式化验证，这个领域已经经历了将近 40 多年的演变，从 60 年代 Tony Hoare 发明 Hoare 逻辑，到接下去的那么多年一直进行了很多年的演变，有点像 machine learning，现在特别火的一个技术，但也过了很多热和严冬又变热。形式化验证也是这样的技术，从一开始成长到变成熟再变 cold。曾经在八十年代，有很多人用形式化验证验证了很多代码、证明 , 写的是数学证明，来证明为什么程序会满足它的一些 property，后来大家发现你即使说验证了也不见得能相信，因为所有人都可以说这个已经被验证了，写了证明在纸上或者用程序来验证了，怎么能相信它？所有人都说可以验证了，证明可能好几十页，有什么人会真正看证明来说证明是对的？

所以形式化验证演变过来有很多自己的问题，前十五年我们引入了 Certified Software 的概念，被形式化验证的软件不能你说了验证就算，你一定要给我一个 machine checkable proof，不能靠我的肉眼来看证明，因为我们没有耐心看这么长的证明，一定要 only if the programmer can prove （through formal machine-checkable proofs） It is free of bugs，这样我们才能相信这个代码的确满足了我们原来想要做的属性。有一段时间这个叫做 Proof-Carrying Code，卖给你代码或者给你做个区块链系统的时候还另外带了 machine-checkable proof，可以叫第三方来验证这个证明说代码不存在任何问题。

为什么有了这个可以 turn trust in to truth 呢？因为 proof，mathematical proof are uncontroversial mathematical truth。That’s what proof is。只要一个 software component is certified，its trustworthiness w.r.t. specification would last for eternity。这个意思就是说，一旦验证了就纯粹变成数字上的定理。本来里面隐藏了很多代码，你不知道它是做什么，只能靠 trust。但你如果有了这个证明，就把 black box 变成 verified black box，so you can fully trust it。

我们在耶鲁大学一直在经营的 CertiKOS Project 的目的就是如何能把形式化验证和 Certified Software 变得能够 scale up，能够用它来 build large systems。我们观察了人写程序的 pattern，平时写 program 的时候从来没有为了打算以后要写证明的，都是觉得我写了代码运转差不多，或者用肉眼看一下基本上差不多了就可以做 debug，可以 develop，但这样的情况在很复杂的区块链系统、分布式系统是不能一直 scale up 的，因为你肉眼能想象的将来看到的 Blockchain protocol 是非常复杂的 protocol，即使脑袋里想也不可能把它完全想清楚，所以必须要用数学证明保证每一个 case 都 cover。

我们发现如果你能把任何复杂系统拆分成很多种的 abstracion layers，就是一个个 black box，因为现实社会我们看宇宙中任何一个东西，它都是从非常简单的东西一步步 build 起来的，整个宇宙有 planet，planet 中有 planet earth，planet earth 我们有不同的 city，不同的 city 有政府、community 等等。每个东西我们都是把一堆小的东西搁在一起，然后 build 一个大的东西。我们认为 software 或者说 complex system 也是需要这么一步步 build，把中间所有的 interface 和 specification 都写出来，我们的这个 technology 叫 Deep Spec。用了这个 technology 把本来很复杂的操作系统 divde 成 65 个 layer，每一个 layer 非常容易被 certify，通过此就做到了世界上第一个 hacker 无法攻击的并发操作系统，这是我们团队几年前一直做的工作。

在做积累技术的时候根本没有想到这些技术会有新的应用，等到 blockchain application coming out 的时候，我们才意识到这是 killer app。This is perfect application。因为一旦有了 Blockchain System，别的系统 hacker 都不会去攻击了。Why we want to hack into your car？You don’t get any money out of it。所有人都会说区块链系统 is what hacker is paying attention to。

我们主要的目的是要拿形式化验证和计算机程序语言 30、40 年积累下来的形式化验证技术用在 Blockchain 的每一个方面，我们公司 focus on 很多方面，不仅要做 security Verification，还要用形式化验证技术 build CertiK Blockchain ，区块链系统是从底层到高层每一行代码都是被验证的，都会保证不会出错，工具可以用来帮助别的团队、别的公链、联盟链团队给他们有 end-to-end 的 security coverage。

公司成立于大概一年半之前，由我和我的博士学生顾荣辉博士，他现在是哥伦比亚大学的助理教授。我们公司的很多人员这次很有幸都在这里，像倪兆中博士就在这边，chief economist 闫开也在这边，在中国有个北京 office，有个团队，负责人陈波锦也在 audience 里面。

公司主要提供的技术除了 Verification-as-a-service，which is trying to improve smart contract security，我们和其他公司不太一样的是我们有 machine Checkable Proof Objects，别的人会说我已经验证了智能合约的安全性，但是你怎么知道它真的是验证了呢？我们有一个证明可以让你 check，通过它可以 replay reasoning。另外还有很多其它，像 layer-based technology、Smart Labels、Pluggable Proof Engine、Certified Dapp Libraries、AutoScan ability，把这些技术用在 Smart Contract 上。

整个 business scope 基本上是 follow security auditing 的 standard steps，也做一些 Penetration Testing 和 Platform Customization，这些在公司的 website 上有介绍，欢迎你们可以去看一看。

公司长远的目的是要建造 CertiK Chain，What do we believe？我们认为 Blockchain 最重要的特点是，out of everything，security is the most important and the most fundamental point that upholds everything else。虽然现在大部分的区块链课题都 focus on performance 和 Decentralization，但 performance 做的越多总是要 worry，把这个东西加快了，用了这个 protocol，有没有可能区块链马上就不安全了？就因为昨天做了代码上的小修改，是不是明天银行货币就有可能被人偷走？这是一个非常关键的问题。如果没有 Security 的支持，没有能够 maintain 的 certified machine checkable proof，那你是不可能有那样的 confidence，要让它用到实用背景中还是比较困难的。

所以 what do we vision？We believe we can build this kind of fully trustworthy blockchain ecosystem。我们会来做 end-to-end certified systems software stack。

今天演讲的好几个团队，包括 Polkadot、Blockstack、Cosmos 等，希望能够把我们的技术用到那样系统里。

What do we offer？给 developers 可以 offer open fully trustworthy development environment。end users 是 certifited secure infrastructure。community 会让大家有一个 peace of mind，你知道用的 Dapp 是不会被人 hacked 的。

具体的技术上，我们把做 Certified OS 的技术完全运用到了 build Blockchain 的 ecosystem 里。所以我们底下用了 CertiKOS 来 bootstrap Linux，用来 bootstrap Blockchain Consensus implementation，包括 Contract Execution Environment。具体的 architecture，从 CertiKOS boot Linux，在上面 run Certik Chain 的 full nodes 和 validators，再在上面跑 Certified VM。我们还有一个 smart contract language 叫 DeepSEA，会帮助你写 Smart Contract，又能从中生成代码，连带 machine checkable proof 一起，所以你能保证你写的 Smart Contract 不存在 implementation related bugs。

用两分钟的时间给大家看一下 CertiKOS 的演进过程，究竟怎么能把非常复杂的系统一步步用形式化验证的方式搭起来。这是我们团队现在做的，让 Certified OS 能够用在各种各样的 Heterogeneous platform 上。

传统意义上，造一个操作系统，在 X86、ARM、RISCV 等平台上跑起来就可以了，但现在大部分的平台基本都是要用 SOC，Heterogeneous SOC。像有些在汽车上跑的都是 SOC。在 distributed Heterogeneous blockchain platform 上，很可能是在 Amazon EC2 或阿里云上面的 node。如何让 CertiKOS 在这些上面都可以跑起来？The starting point, 我们把通用组件按照 architecture abstraction 和 platform abstraction 来 build generic OS kernel，这种做法一般讲中间有个 machine，要保证 code 在 machine 上跑的时候满足一定的特点。但事实上在具体的情况下，没有哪个机器底下只有一个 machine，往往有很多 device controllers，代码会在不同的 machine 上跑，到了 Heterogeneous setting，很可能代码会在不同的 machine 上跑，而且 CPU 会去 multiplex 不同的 device driver，不同的 code。

怎么验证这样的代码？怎么让 system scale up？需要把 shared resources，像 CPU、Memory 等，分到不同的 machine 上，再 isolate component，抽象机器，把中间的 component 并起来。这有点像我刚刚说的 Certified Abstraction Layer 的概念，世界再复杂也能把它分成几百层的 abstraction，在每一层建立一个 new black box 来验证，只需要在其底下做验证，每验证一小部分就可以把 implementation details encapsulated 起来。通过这样的方式，用一个 general interface 就可以验证各种各样复杂的系统，包括 distributed systems。这是我们验证操作系统的方法。

再讲一下团队目前 focus on 的 technology。一个是 CertiKOS，能够 bootstrap system for distributed blockchain ecosystem。另外一个是 DeepSEA，smart contract language。另外还有 Chain Analysis 和 Monitoring，它和我们的操作系统是有关联的。