徐令予博客
考槃在澗，碩人之寬。獨寐寤言，永矢弗諼。考槃在阿，碩人之薖。獨寐寤歌，永矢弗過。考槃在陸，碩人之軸。獨寐寤宿，永矢弗告。
攻不破、摧不垮、百毒不侵的電腦是怎樣練成的？
5月12日早上醒來，全球人終於明白互聯網上不全是音樂和鮮花。一個名為“想哭”的勒索病毒襲擊了全球上百個國家和地區使用微軟操作係統的電腦，原來網上的江湖波譎雲詭、危機四伏。
怎樣打造攻不破、摧不垮、百毒不侵的電腦，怎樣才能還太平於網民，科學家們為了網絡維穩真是操碎了心。
2015年的夏天，一群黑客企圖控製一架名為“小鳥”（LITTLE BIRD H-6U）的軍用無人直升機，這是亞利桑那州的波音工廠為美軍特種作戰任務研製的。當時為黑客作了這樣的安排：他們開始操作時已經可以訪問無人機的電腦係統的一部分，他們隻需入侵“小鳥”的機上飛行控製電腦，無人機就是他們的了。
一開始，黑客團隊可以像侵入家庭Wi-Fi一樣輕鬆地接管直升機，易如囊中探物。但在隨後的幾個月中，國防高級研究計劃局（DARPA）的工程師們開發並實施了一種新型的安全機製，一種百毒不侵的軟件係統。“小鳥”的計算機係統的關鍵部分是現有技術完全無法入侵的，其代碼的正確可靠能像數學一樣被證明。盡管把無人機的計算機網絡完全開放，黑客團隊一直無法掌握“小鳥”的控製係統，他們經過連續六周的攻擊而不能越雷池於一步，黑客以徹底失敗而告終。
 |  |
壓製黑客的技術是一種稱為軟件編程的形式化方法[1]。過去對傳統計算機代碼的評估主要是檢查它是否在各種情況下都能正常工作，而形式化軟件驗證如同數學證明：程序中每個語句的前後都遵循嚴格的邏輯關係，整個程序測試的確定性就像數學家證明定理一樣。
大多數傳統計算機的程序是如何工作的呢？設想為無人駕駛車編寫一個計算機程序。在操作層麵上，可以定義汽車在行程中各種必須的操作行為，它們可以是左轉、右轉、製動或加速。而程序則是按照適當順序排列的基本操作的匯編，以確保讓車子到達雜貨店而不是機場。
長期以來對此類程序的評估和驗收的傳統方法是進行簡單的測試。把各種起始和目標的位置輸入程序，檢查在程序控製下的無人駕駛車輛是否正確到達預定目標。這種測試方法在大多數情況下可以滿足我們的要求。但是這種測試法不能保證軟件將百分之百地正常工作，因為各種輸入和輸出的組合無窮無盡，現實環境中總會有罕見的情況發生，總會有不能預測到的“角落”，從而導致程序出錯。
在程序的運行中，這些出錯和故障當然要不得，但更大的危害可能引起計算機內存緩衝區溢出，為黑客攻擊係統提供了跳板，軟件中的任何一個缺陷都可能就是係統安全的漏洞。
再舉一個例子，考慮對一串數字排序的程序。程序員對排序程序的定義可能會寫成這樣：
對於列表中的每個元素j，確保元素j≤j+1
然而，這種定義——確保列表中的每個元素小於或等於其後麵的元素——隱含了一個錯誤：程序員假定輸出總是輸入的一種置換。也就是說，對於輸入列表[9,2,5]，期望程序將輸出[2,5,9]以滿足排序定義。但是列表[2,5,7]也同樣滿足定義，它也是一個排序列表，但它不是我們希望得到的排序列表。嚴格地說，除了排序還必須確保輸出與輸入的元素集合完全一致，這在以往的程序設計中常常被忽視。
換句話說，將一個程序應該做些什麽的想法轉化為一個正式的規範，同時又要排除可能產生的各種不正確的解釋，這常常是十分困難的。上麵的例子隻是一個簡單的排序程序。現在想象一下比排序更抽象的程序，比如保護密碼，這在數學上又是什麽意思？ 它可能涉及對密碼保護進行數學描述，或者對加密算法的安全性作出定義。
使用形式邏輯規則來指導程序設計起源於上世紀七十年代。艾茲格·迪科斯徹(Edsger Dijkstra)首先提出了創建無錯代碼的想法。他在1976年完成的“編程規則”這部著作為程序驗證打下了基礎，他也因此獲得了圖靈獎。
七十年代末，我在上海交大三係讀碩，我的兩位同門師兄的選題就是“程序設計自動化驗證”，可見當時中國高校對世界科技動向還是挺敏感的。那個年月碩士生課題不少是“高大上”的，但大多嚴重脫離實際，對課題項目也缺少長期的規劃和投入，我估計也難有實質性的收獲。
將正確性證明納入計算機程序編製一直沒有得到廣泛的應用，計算機科學的發展畢竟不能單純依靠願望。長年以來，使用形式邏輯規則來指定程序的功能，如果不是不可能也至少是不實際的。包含形式驗證信息的程序長度可能是傳統程序的五倍。這種編程的額外負擔可以通過專用的編程語言和輔助程序減輕一些，但那些輔助軟件工具在上世紀七八十年代並不存在。
即使輔助工具有所改進，推廣程序驗證的更大障礙是：沒有人確定是否有必要。雖然一些專家一再強調編碼小錯誤會導致災難性的後果，但是吃瓜群眾看到的是計算機程序大多數情況下工作正常。當然，有時候會丟失數據或藍屏死機，但是天又塌不下來，讓文秘重新輸入數據或者偶爾重新啟動計算機又有什麽大不了。
但是互聯網改變了一切，如同航空旅行的普及導致傳染病的飛速傳播，當計算機都互相聯接在一起，一台計算機的編碼錯誤可能會被黑客利用，導致成千上萬計算機被非法入侵控製，甚至使網絡局部癱瘓。至少2017年5月12日全球網民嚐到了苦頭。
當研究人員開始了解互聯網對計算機安全的威脅時，程序驗證技術終於有了用武之地。首先，研究人員在基於形式化方法的編程技術上取得了巨大進步：改進了支持形式化方法的Coq和Isabelle等驗證輔助程序;開發新的邏輯係統(dependent-type theories)，為計算機對代碼的推理提供了全新的框架;並且改進了所謂的“操作語義”——本質上是一種具有確切詞匯的語言，可以更明確地表達程序究竟應該做什麽。
美國的高保證網絡軍事係統(HACMS)項目顯示了如何通過計算機係統分區隔離以保證總體的安全。該項目的第一個目標是創造一個無法入侵的娛樂級四軸飛行器。運行該飛行器的商品化軟件是整體單一化的，這意味著如果攻擊者突破一點，他就可以控製整個軟件。在接下來的兩年中，HACMS團隊將四軸飛行器任務控製計算機中的代碼分區隔離。
該團隊還重新製定了軟件架構，使用了被HACMS項目經理凱瑟琳·費舍爾稱之為“高保證構建塊”，這是一種讓程序員證明其代碼正確無誤的工具。其中一個經過驗證的構建塊可以保證在某個分區內具有訪問權限的操作者無法升級越界進入其他分區。
在四軸飛行器取得經驗之後，研究人員在“小鳥”軍用無人直升機上安裝了這個分區隔離軟件。在測試中，他們提供了黑客團隊進入無人直升機的某一分區，例如攝相機控製分區，但並不是核心功能分區。在無情的數學公式麵前，黑客被死死地卡住在一個分區中不得亂說亂動。“他們以機器檢查的方式證明，黑客不能脫離分區，這毫不奇怪，他們就是不能。”凱瑟琳·費舍爾說：“這與定理是一致的，試驗也證明了這一點。”
為了幫助非專業人員了解分區隔離技術的基本原理，讓我們回顧一下上世紀中國絕密軍工廠的管理，這類軍工廠不僅門衛森嚴，而且內部分成密級不同的獨立車間，人員不得互相來往。每個產品又必經多個車間加工生產。一個間諜（黑客）進入工廠並混進某個車間已經非常不易，他下足工夫取得車間主任的信任或許獲得某種特權，但他最多隻能在一個車間中活動，他對整個產品的認識和控製是十分有限的，因為任何試圖跨越車間界限的行為會被嚴格的限製，而且其真實身份會立刻受到特別調查。計算機係統的分區隔離技術與絕密軍工廠的管理方式有著某種程度的類同。
近年來計算機硬件性能的飛速進步也為計算機係統的分區隔離技術提供了物質基礎，今日強大的中央處理器能力和海量的內存空間完全可以支持係統的分區運行管理。
在“小鳥”無人直升機測試之後的一年，DARPA正努力將HACMS項目的工具和技術應用於其他軍事技術領域，如衛星和無人自動駕駛車隊。
為了捍衛互聯網的安全，形式化方法的研究人員正在推動更加雄心勃勃的計劃。DeepSpec合作項目力圖將過去十年中已經成功通過形式化驗證的許多小型模塊進行組合，以構建一個經過完全形式化驗證的端點到端點的係統，如Web服務器。
在微軟的研究部門，軟件工程師正在進行兩項雄心勃勃的形式化驗證項目。第一個名為珠穆朗瑪峰，這是創建一個經過形式化驗證的HTTPS版本，新的協議可以有效地保護被稱之為“互聯網的阿喀琉斯之踵”的網絡瀏覽器。第二個是為複雜的網絡物理係統（如無人機）製定形式化驗證規範，這裏的挑戰可能更為嚴峻。無人機飛行涉及到機器學習，以及在連續的環境數據流中進行概率判定，如何對不確定性進行推理並製定形式化規範是極大的挑戰。但在過去的十年中，軟件工程的形式化方法已經有了長足的進步，從事該項研究的科學家們對未來持有謹慎樂觀的態度。
高保證網絡軍事係統（HACMS）項目主管 凱瑟琳·費舍爾 
[1]形式化方法(Formal Method)是基於嚴密的、數學上的形式機製的計算機係統研究方法，該知識體係中有6個主要領域，分別為:
① 基礎(Foundations);
② 形式化規格(Formal specification paradigms);
③ 正確性驗證及演算(Correctness, verification and calculation);
④ 形式化語義(Formal semantics);
⑤ 可執行規範支持(Support for executable specification);
⑥ 其他(Other Topics)。
本文首發於觀察者網 2017年5月22日
