攻不破、摧不垮、毒不侵的電腦怎樣煉成？

文 觀察者網專欄作者 徐令予

加州大學洛杉磯分校物理系研究員

5月12日早上醒來，全球人終於明白互聯網上不全是音樂和鮮花。一個名為「想哭」的勒索病毒襲擊了全球上百個國家和地區使用微軟操作系統的電腦，原來網上的江湖波譎雲詭、危機四伏。

怎樣打造攻不破、摧不垮、毒不侵的電腦，怎樣才能還太平與網民，科學家們為了網路維穩真是操碎了心。

2015年的夏天，一群黑客企圖控制一架名為「小鳥」（LITTLE BIRD H-6U）的軍用無人直升機，那是在亞利桑那州的波音工廠為美軍特種作戰任務研製的裝備。當時黑客作了這樣的安排：他們開始操作時已經可以訪問無人機電腦系統的一部分。從那裡開始，他們只需入侵「小鳥」的機上飛行控制電腦，無人機就是他們的了。

LITTLE BIRD H-6U 軍用無人直升機

當項目開始時，黑客團隊可以像侵入家庭Wi-Fi一樣輕鬆地接管直升機，易如囊中探物。但在隨後的幾個月中，美國國防高級研究計劃局（DARPA）的工程師們開發並實施了一種新型的安全機制，一種百毒不侵的軟體系統。

「小鳥」的計算機系統的關鍵部分是現有技術完全無法入侵的，其代碼的正確可靠能像數學一樣被證明。儘管把無人機的計算機網路完全開放，黑客團隊一直無法掌握「小鳥」的控制系統，他們經過連續六周的攻擊而不能越雷池於一步，黑客以徹底失敗而告終。

「黑客無法以任何方式突破系統和破壞正常的飛行。」塔夫茨大學計算機科學教授和高保證網路軍事系統（HACMS）項目的主管凱瑟琳·費舍爾指出，「這個結果使所有的DARPA人員信服，我們實際上可以在我們關心的系統中使用這種技術。」

壓制黑客的技術是一種稱為軟體編程的形式化方法[1]。過去對傳統計算機代碼的評估主要是檢查它是否在各種情況下都能正常工作，而形式化軟體驗證如同數學證明：程序中每個語句的前後都遵循嚴格的邏輯關係，整個程序測試的確定性就像數學家證明定理一樣。

大多數傳統計算機的程序是如何工作的呢？設想為無人駕駛車編寫一個計算機程序。在操作層面上，你可以定義汽車在行程中各種必須的操作行為，它們可以是左轉、右轉、制動或加速。而程序則是按照適當順序排列的基本操作的彙編，以確保讓你到達雜貨店而不是機場。

長期以來，對此類程序的評估和驗收的傳統方法是進行簡單的測試。把各種起始點和目標的位置輸入程序，檢查在程序控制下的無人駕駛車輛是否正確到達預定目標。這種測試方法在大多數情況下可以滿足我們的要求。

但是這種測試法不能保證軟體將百分之百地正常工作，因為各種輸入和輸出的組合無窮無盡，現實環境中總會有罕見的情況發生，總會有不能預測到的「角落」，從而導致程序出錯。

在程序的運行中，這些出錯和故障當然要不得，但更大的危害是可能引起計算機內存緩衝區溢出，為黑客攻擊系統提供了跳板，軟體中的任何一個缺陷都可能就是系統安全的漏洞。

再舉一個例子，考慮對一串數字排序的程序。程序員對排序程序的定義可能會寫成這樣：

對於列表中的每個元素j，確保元素j≤j+1

然而，這種定義——確保列表中的每個元素小於或等於其後面的元素——隱含了一個錯誤：程序員假定輸出總是輸入的一種置換。也就是說，對於輸入列表[7,3,5]，她期望程序將輸出[3,5,7]以滿足排序定義。然而，列表[2,5,7]也同樣滿足定義，它是一個排序列表，但它不是我們希望的排序列表。嚴格地說，除了排序還必須確保輸出與輸入的元素集合完全一致，這在以往的程序設計中常常被忽視。

換句話說，將一個程序應該做些什麼的想法轉化為一個正式的規範，同時又要排除對此可能產生的各種不正確的解釋，這常常是十分困難的。上面的例子只是一個簡單的排序程序。現在想像一下比排序更抽象的程序，比如保護密碼，這在數學上又是什麼意思？ 它可能涉及為保護密碼進行數學描述，或者對加密演算法的安全性作出定義。這些問題提岀並不太難，但找到正確簡單的方案卻十分不易。

使用形式邏輯規則來指導程序設計起源於上世紀七十年代。1973年10月，艾茲格·迪科斯徹(Edsger Dijkstra)提出了創建無錯代碼的想法。在會議期間他住在酒店，半夜三更產生了讓編程更加數學化的靈感。他在後來回憶道：「我的大腦在燃燒，凌晨2:30離開了我的床，伏案書寫了一個多小時。」這些材料成為了他於1976年完成的「編程規則」這部著作的基礎，他因此獲得了圖靈獎——計算機科學的最高榮譽。

但是將正確性證明納入計算機程序編製一直沒有得到廣泛的應用，計算機科學的發展畢竟不能單純依靠願望。主要是因為長年以來，使用形式邏輯規則來指定程序的功能，即便並非不可能，似乎也是不實際的。包含形式驗證信息的程序可能是相同的傳統程序的五倍長度。這種編程的額外負擔可以通過專用的編程語言和輔助程序減輕一些，但那些旨在幫助軟體工程師的工具在上世紀七八十年代並不存在。

即使輔助工具有所改進，推廣程序驗證的更大障礙是：沒有人確定是否有必要。雖然一些專家一再強調編碼小錯誤會導致災難性的後果，但是吃瓜群眾看到的是計算機程序大多數情況下工作正常。當然，有時候會丟失數據或藍屏死機，但是天又塌不下來，讓文秘重新輸入數據或者偶爾重新啟動計算機又有什麼大不了。

到了在20世紀90年代，程序驗證的鼻祖也開始懷疑它的用處了。圖靈獎得主Tony Hoare——「霍爾邏輯」的創始人——也承認軟體編程的形式化方法可能既勞民傷財又無的放矢。

他在1995年寫道：十年前，形式化方法的研究人員（而我是其中最為錯誤的一位）預測，軟體業界將會懷著感激之情擁抱形式化方法帶來的成果，而事實證明：我們企圖要解決的問題實質上對世界並沒有產生多大的影響。

但是互聯網改變了一切，如同航空旅行的普及導致傳染病的飛速傳播，當計算機都互相聯接在一起，一台計算機的編碼錯誤可能會被黑客利用，導致成千上萬計算機被非法入侵控制，甚至使網路局部癱瘓。至少2017年5月12日全世界嘗到了苦頭。

當研究人員開始了解互聯網對計算機安全的威脅時，程序驗證技術終於有了用武之地。首先，研究人員在基於形式化方法的編程技術上取得了巨大進步：改進了支持形式化方法的Coq和Isabelle等驗證輔助程序；開發新的邏輯系統(called dependent-type theories)，為計算機對代碼的推理提供了全新的框架；並且改進了所謂的「操作語義」——本質上是一種具有確切辭彙用以表達程序究竟應該做什麼的語言。

今日，形式化方法的研究人員的目標也變得更為現實。在20世紀70年代和80年代初期，這些研究人員試圖創建可以驗證的計算機系統，一個從硬體電路到軟體程序的完整系統。如今大多數研究人員側重於驗證系統中較小但特別脆弱或關鍵的部分，如操作系統和加密協議。

「我們並不聲稱我們將證明整個系統是正確的，每一點都百分之百的可靠，從上至下直到電子電路的水平。」微軟研究院的計算機科學家Jeannette Wing指出：「這些做法是荒謬的。我們更清楚我們能做什麼，不能做什麼。」

HACMS項目顯示了如何通過計算機系統分區隔離以達到總體的安全保證。該項目的第一個目標是創造一個無法入侵的娛樂級四軸飛行器。運行該飛行器的商業軟體是一個整體，這意味著如果攻擊者突破一點，他就可以控制整個軟體。在接下來的兩年中，HACMS團隊將四軸飛行器的任務控制計算機中的代碼分區隔離。

該團隊還重新制定了軟體架構，使用了被HACMS項目經理凱瑟琳·費舍爾稱之為「高保證構建塊」的技術，這是一種讓程序員證明其代碼正確無誤的工具。其中一個經過驗證的構建塊可以保證在某個分區內具有訪問許可權的操作者無法升級越界進入其他分區。

高保證網路軍事系統（HACMS）項目主管 凱瑟琳·費舍爾

在四軸飛行器取得經驗之後，HACMS程序員在「小鳥」軍用無人直升機上安裝了這個分區隔離軟體。在測試中，他們提供了黑客團隊進入無人直升機的某一分區，例如攝相機控制分區，但並不是核心功能分區。在無情的數學公式面前，黑客被死死地卡住在一個分區中無法亂說亂動。「他們以機器檢查的方式證明，黑客不能脫離分區，這毫不奇怪，他們就是不能。」凱瑟琳·費舍爾說：「這與定理是一致的，試驗也證明了這一點。」

為了幫助非專業人員了解分區隔離技術的基本原理，讓我們回顧一下上世紀中國絕密軍工廠的管理，這類軍工廠不僅門衛森嚴，而且內部分成密級不同的獨立車間，人員不得互相來往。每個產品又必經多個車間加工生產。

一個間諜（黑客）進入工廠並混進某個車間已經非常不易，他下足工夫取得車間主任的信任或許能獲得某種特權，但他最多只能在一個車間中活動，他對整個產品的認識和控制是十分有限的，因為任何試圖跨越車間界限的行為會被嚴格的限制，而且其真實身份會立刻受到特別調查。計算機系統的分區隔離技術與絕密軍工廠的管理方式有著某種程度的類同。

近年來，計算機硬體性能的飛速進步也為計算機系統的分區隔離技術提供了物質基礎，今日強大的中央處理器能力和海量的內存空間完全可以支持系統的分區運行管理。

在「小鳥」無人直升機測試之後的一年，DARPA正努力將HACMS項目的工具和技術應用於其他軍事技術領域，如衛星和無人自動駕駛車隊。

為了捍衛互聯網的安全，形式化方法的研究人員正在推動更加雄心勃勃的計劃。DeepSpec合作項目力圖將過去十年中已經成功通過形式化驗證的許多小型模塊進行組合，以構建一個經過完全形式化驗證的端到端系統，如Web伺服器。

在微軟的研究部門，軟體工程師正在進行兩項雄心勃勃的形式化驗證項目。第一個名為珠穆朗瑪峰，這是創建一個經過形式化驗證的HTTPS版本，新的協議可以有效地保護被稱之為「互聯網的阿喀琉斯之踵」的網路瀏覽器。

第二個是為複雜的網路物理系統（如無人機）制定形式化驗證規範，這裡的挑戰可能更為嚴峻。無人機飛行涉及到機器學習，以及在連續的環境數據流中進行概率決定，如何對不確定性進行推理並制定形式化規範是極大的挑戰。但在過去的十年中，軟體工程的形式化方法已經有了長足的進步，從事該項研究的科學家們對未來持有謹慎樂觀的態度。

[1]形式化方法(Formal Method)是基於嚴密的、數學上的形式機制的計算機系統研究方法，該知識體系中有6個主要領域，分別為:

基礎(Foundations);

形式化規格(Formal specification paradigms);

正確性驗證及演算(Correctness, verification and calculation);

形式化語義(Formal semantics);

可執行規範支持(Support for executable specification);

其他(Other Topics)。

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！