編者按：一直以來，我們都理所當然地認為程序就像高墻，無法不透風，自然也無法躲過黑客無孔不入的攻擊。而這篇首發(fā)于quantamagazine 的文章卻要顛覆我們的認知了：采用形式驗證(formal verification)編寫的軟件，代碼就像“數學證明一樣可靠”。那么，它是如何實現的？又能帶給我們怎樣的驚喜呢？本文由雷鋒網獨家編譯，未經授權不得轉載。

2015 年夏天，一個黑客團隊在美國亞利桑那州嘗試控制波音的“小鳥”（Little Bird）無人軍事直升機。這隊黑客的優(yōu)勢在于：他們一開始就能訪問這架無人軍事直升機計算機系統的一部分。從這里出發(fā)，他們需要做的就是黑進“小鳥”的機載飛行控制計算機，進而控制整架直升機。

在這一項目開始時，作為紅方的黑客團隊可以像破解家用 Wi-Fi 網絡一樣，輕易地控制這架直升機。但在接下來的幾個月里，美國國防部高級研究計劃局的工程師們部署了一種新的安全機制：一個無法被攻占的軟件系統。

“小鳥”無人軍事直升機計算機系統的關鍵部分靠現有技術無法攻破，它的代碼就像數學證明一樣可靠。即便給予了黑客團隊六周時間和更多直升機計算機系統的訪問權限，他們還是不能攻破“小鳥”無人軍事直升機計算機系統的防御。

高可靠性軍事網絡系統(HACMS)項目發(fā)起人、美國塔夫斯大學計算機科學教授 Kathleen Fisher 表示：“黑客們無法以任何方式擴大控制并干擾機器運行。這一結果讓美國國防部高級研究計劃局非常高興，他們說現在終于能用這一技術來保護核心計算機系統了?！?/p>

這一讓黑客們束手無策的技術是名為形式驗證(formal verification)的軟件編程風格。和大多數計算機代碼不同，采用形式驗證風格編寫的軟件讀起來就像是數學證明：每一個聲明在邏輯上都承接上一個聲明。一個這樣的程序可以像證明數學定理一樣，無論如何測試都一定會得到正確的結果。

微軟研究院研究形式驗證和安全的研究員 Bryan Parno 表示：“你寫下的就是一個描述程序行為的數學公式，再利用一些證明檢查器來檢查聲明的正確性?！?/p>

早在計算機科學誕生之初，創(chuàng)造形式驗證風格軟件的想法就已出現。很長一段時間以來，嘗試創(chuàng)造形式驗證風格軟件的企圖都徒勞無功，但在過去十年間，“形式方法”方面的進展讓開發(fā)形式驗證風格軟件變得越來越靠譜。如今，學術界、美國軍方和微軟、亞馬遜等科技公司正攜手探索形式軟件驗證技術。

隨著越來越多的關鍵社會職能轉移到網上，研究人員們對形式軟件驗證技術的興趣也越來越濃厚。在以前，計算機還只是局限于家里和辦公室，程序漏洞最多也就是讓使用者感到不便。但現在，程序漏洞可能會導致巨大危害，任何具備相關知識的人都能利用同一漏洞自由地進出某個計算機系統。

程序驗證領域領導者之一的普林斯頓大學計算機科學教授 Andrew Appel 表示：“在上世紀，如果程序有漏洞，頂多也就是體驗糟糕或者程序崩潰。但進入 21 世紀，漏洞可能成為黑客控制程序并竊取數據的通道。漏洞也從糟糕但可以忍受變成了致命威脅，這就嚴重多了?！?/p>

完美程序的夢想

高可靠性軍事網絡系統(HACMS)項目發(fā)起人、美國塔夫斯大學計算機科學教授 Kathleen Fisher

1973 年 10 月，Edsger Dijkstra 產生了一個編寫零錯誤代碼的想法。當時他正在參加一次會議，在下榻的酒店里，Edsger Dijkstra 熬到深夜來讓編程變得更數學化。他在后來回憶道：“這個想法讓我很興奮，于是我凌晨兩點半爬起來，寫了一個多小時?！边@一材料后來擴充成了《編程的修煉》(A Discipline of Programming)一書，并于 1976 年出版。這本書加上 Tony Hoare 的工作，建立了將正確性證明融入計算機程序編寫過程中的視角。

計算機科學并沒有采用這一視角，因為此后很多年里，要實現這一視角看起來非常不切實際，即用形式邏輯規(guī)則來明確程序的功能。

形式規(guī)范要定義一個計算機程序要做什么事，而形式驗證則用來確定無疑地證明程序代碼完美地符合了規(guī)范。打個比方，比如你要給無人駕駛汽車編寫一個把你送到百貨商店的計算機程序，你需要定義讓汽車實現這一目的的動作：汽車可以左轉或右轉、剎車或加速、啟動或停車。最終，你的程序就是為了實現這一目的而對基本操作進行的合理組合，要求是把你送到百貨商店而不是機場。

檢查程序是否工作正常的傳統方式是跑測試。程序員們會給程序大量輸入（或單元測試），以確保它符合設計要求。如果你的程序是給無人駕駛汽車規(guī)劃路徑的算法，你也許會用多個不同的位置點來測試它。這一基于測試的方法能得到運行正確的軟件，但只是在大多數時候針對大多數應用而言。不過，單元測試并不能確保軟件永遠運行正確，因為沒有辦法用所有可能的輸入來測試程序。即便程序能通過每一個測試，也不能排除它在一些極端情況下運行不正常，進而形成漏洞。在實際的程序中，這種漏洞也許會簡單到只是一個緩沖溢出錯誤，即程序拷貝多了一丁點數據，并覆蓋了某一小塊計算機內存。這個看起來無害的錯誤很難徹底根除，是黑客們攻入計算機系統的捷徑。

Bryan Parno 說道：“只要程序中有一個缺陷，就能成為安全弱點。很難測試所有可能輸入的所有路徑?！?/p>

實際的形式規(guī)范要比自動駕駛去百貨商店細致得多。比如編寫一個確認收到文件，并按收到時間對文件進行排序的程序，形式規(guī)范需要規(guī)定計數器永遠只能增長（好讓后面接收的文件序號總比前面收到的文件高），以及程序永遠也不會泄露給文件簽名的密鑰。

這么說著容易，真正要用形式語言來編寫一個計算機能應用的規(guī)范卻很難，更何況還是要在整個軟件編寫過程中都這么做。

Bryan Parno 表示：“寫出機器能識別的形式規(guī)范或目標非?？简炛巧?。站在高處說‘不要泄露密碼’很容易，真正要把它用數學定義的形式寫出來卻需要很多思考?！?/p>

再比如，給列表或數字排序的程序，程序員可能會這么給它寫形式規(guī)范：

For every item j in a list, ensure that the element j ≤ j+1

（對于列表中的每一項 j，確保 j ≤ j+1）

然而這個形式規(guī)范卻有一個漏洞：這個程序員默認輸出會是輸入的排序結果，即假設列表為 [7, 3, 5]，這個程序應該返回 [3, 5, 7]，這樣就滿足了定義。但列表 [1, 2] 也滿足定義，因為“這是一個排序好了的列表，只不過可能不是我們希望的那種排序好了的列表?！?/p>

換言之，要把你想要讓程序做的事，用排除了所有可能不正確解釋的形式規(guī)范表示出來很難。上面的例子還只是一個簡單的排序程序，想象一個更抽象的例子，比如保護密碼。Bryan Parno 說道：“這在數學上是什么意思？定義它也許要寫出保護密碼的數學描述。安全的加密算法又是什么意思呢？這也是我們一直在研究中一直在思考并取得進展的問題，但要正確應用必須非常小心。”

基于代碼塊的安全

編寫這種程序需要同時編寫形式規(guī)范以及幫助編程軟件推導代碼所必須的額外注釋， 因此其長度達到了傳統程序的五倍。

用合適的工具可以在一定程度上減輕這一負擔，比如專門的編程語言和輔助證明程序。但這些東西在上世紀 70 年代時還不存在。同時擔任形式驗證計算機系統開發(fā)團體 DeepSpec 首席研究員的 Andrew Appel 表示：“當時的很多技術都不成熟，因此到 80 年代，很多人就對它失去了興趣?！?/p>

即便工具得到了改進，形式驗證計算機程序還有另一個問題要解決：沒人確定是否有必要用它。雖然形式方法愛好者們總是在說小的程序錯誤最后會變成災難性漏洞，但大家看到的卻是計算機程序工作得相當好。

的確，這些計算機程序有時候會崩潰，但和巨細無遺地一條條用形式邏輯系統的語言來編寫程序相比，丟失未保存的數據或時不時重啟機器貌似也可以接受。有時候，連形式規(guī)范最早期的領導者也會懷疑其是否有用。在上世紀 90 年代，霍爾邏輯(Hoare logic，首批推導計算機程序正確性的形式系統之一)的發(fā)明者 Hoare 就承認，也許形式規(guī)范是一個不存在的問題的勞動密集性解決方案。他在 1995 年寫道：

十年前，形式方法的研究者們（我是其中錯得最厲害的一個）預測，計算機世界會擁抱并感激形式化帶來的每一點協助……結果是，全世界并沒有碰到我們一開始打算解決的那種問題。

后來出現了互聯網。互聯網之于編程錯誤就像是飛機之于傳染?。寒斔须娔X都連接在一起時，不方便但可以忍受的軟件漏洞會導致一系列安全問題。

Andrew Appel 說道：“有一點我們當時沒有特別明白，那就是互聯網上有一些軟件面向所有黑客開放，如果這種軟件里有一個漏洞，它就會成為安全威脅?！?/p>

在微軟研究院開發(fā)形式驗證版 HTTPS 協議的計算機科學家 Jeannette Wing

在研究人員們開始明白互聯網給計算機安全帶來的致命威脅后，程序驗證就開始煥發(fā)第二春了。研究人員們這一次在加強形式方法的技術上取得了很大進展：改進了支持形式方法的輔助證明程序 Coq 和 Isabelle；開發(fā)了新的邏輯系統，為計算機提供推導代碼的框架；發(fā)展改進了運算語義學(operational semantics)，即可以用正確的詞語來表達程序應該做什么事了。

微軟研究院企業(yè)副總裁 Jeannette Wing 表示道：“所有自然語言都具有歧義性。而在形式規(guī)范中，你會寫出基于數學的精確規(guī)范，以解釋你想要程序做什么?！?/p>

另外，形式方法的研究人員們也修改了自己的目標。在上世紀七、八十年代，他們想要打造完整的經過形式驗證的計算機系統，從芯片到計算機程序?，F在，大多數形式方法研究人員都專注于驗證更小但更脆弱或系統關鍵的組成部分，比如操作系統或加密協議。

Jeannette Wing 說道：“我們不再宣稱要證明整個系統都正確，每一個比特都百分百可靠，連芯片層面也如此。做出這樣的宣言很可笑。對于我們能以及不能做什么，我們現在有了更清楚的認識?！?/p>

高可靠性軍事網絡系統項目證明，通過明確定義計算機系統中的一小部分，就能極大地提高安全性。這個項目的最初目標是打造一架無法被黑的娛樂四旋翼無人機。但無人機運行的軟件非常龐大，黑客攻破一部分，就能獲得整個系統的控制權。于是在接下來的兩年里，高可靠性軍事網絡系統團隊將無人機的任務控制計算機程序代碼分成了很多塊。

他們還用“高可靠性構建模塊”重寫了軟件架構，這些模塊可以讓程序員們證明自己代碼的可靠性。其中一個經過了形式驗證的模塊可以確保，即便用戶取得了一個代碼塊的控制權，他也不能提升自己的權限來進入其他代碼塊。

隨后，高可靠性軍事網絡系統團隊將這一區(qū)塊化的軟件安裝到了“小鳥”無人軍事直升機上。在和紅方黑客團隊的較量中，他們先讓黑客們可以訪問某一次要功能如攝像頭的代碼，但黑客們肯定會被困住，因為這經過了數學證明。Kathleen Fisher 說道：“我們用機器從數學上證明了紅方肯定無法突破這一代碼塊，因此他們無法突破也就很順理成章了。結果與定理一致，也很好確認?！?/p>

在“小鳥”無人軍事直升機上測試后，美國國防部高級研究計劃局就開始將這些工具和技術應用到其他軍事技術上，比如衛(wèi)星和無人駕駛載重卡車。新的項目和過去十年中形式驗證傳播的方式保持一致：每一個成功的項目都能加強下一個項目。Kathleen Fisher 表示道：“人們再也沒有借口說這么做太難了?！?/p>

驗證互聯網

安全和可靠性是驅動形式方法的兩大目標。每過一天，提高這兩大目標的需要就會變得越發(fā)明顯。在 2014 年，一個本可以被形式規(guī)范捕捉到的小編程錯誤導致了“心臟失血”漏洞，甚至可能讓互聯網癱瘓。一年以后，兩個白帽子黑客證明了我們對聯網汽車的最大恐懼：他們成功地控制了別人的大切諾基。

隨著安全風險的日益增加，形式方法研究人員們正推動更具野心的計劃。Andrew Appel 領導的 DeepSpec 正試圖建立一個經過完全驗證的端到端系統（就像網絡服務器一樣）。如果這一計劃成功，就能將過去十年中許多更小規(guī)模的驗證成果組合到一起，比如經過完全驗證的操作系統內核。Andrew Appel 說道：“DeepSpec 現在專注在做但還沒有做到的事情是，如何將這些組件用規(guī)范接口連接起來。”

在微軟研究院中，軟件工程師們已經在進行兩個雄心勃勃的形式驗證項目。第一個項目名為 Everest，旨在打造經過形式驗證的 HTTPS 協議。

第二個項目則是希望能為無人機這樣的復雜物聯網系統開發(fā)出經過驗證的規(guī)范。這個項目面臨的挑戰(zhàn)非常大。要知道傳統軟件按離散、確定的步驟執(zhí)行，無人機軟件會根據連續(xù)的環(huán)境數據流，運用機器學習來計算概率并進行決策。要把這種不確定性形式規(guī)范化會需要很多思考。不過形式方法在過去十年中取得了很多進展，Jeannette Wing 對此表示樂觀，認為形式方法研究人員們會找到解決辦法。

via quantamagazine

推薦閱讀：

尤金·卡巴斯基：網絡安全已陷“黑暗時代”，我們該如何應對？

Chrome發(fā)布重要安全更新，將抵御量子計算機發(fā)起的黑客攻擊

雷峰網原創(chuàng)文章，未經授權禁止轉載。詳情見轉載須知。