耶魯大學計算機系教授 &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,它和我們的操作系統是有關聯的。