編者按：一直以來，我們都理所當(dāng)然地認(rèn)為程序就像高墻，無法不透風(fēng)，自然也無法躲過黑客無孔不入的攻擊。而這篇首發(fā)于quantamagazine 的文章卻要顛覆我們的認(rèn)知了：采用形式驗(yàn)證(formal verification)編寫的軟件，代碼就像“數(shù)學(xué)證明一樣可靠”。那么，它是如何實(shí)現(xiàn)的？又能帶給我們?cè)鯓拥捏@喜呢？本文由雷鋒網(wǎng)獨(dú)家編譯，未經(jīng)授權(quán)不得轉(zhuǎn)載。

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

在這一項(xiàng)目開始時(shí)，作為紅方的黑客團(tuán)隊(duì)可以像破解家用 Wi-Fi 網(wǎng)絡(luò)一樣，輕易地控制這架直升機(jī)。但在接下來的幾個(gè)月里，美國國防部高級(jí)研究計(jì)劃局的工程師們部署了一種新的安全機(jī)制：一個(gè)無法被攻占的軟件系統(tǒng)。

“小鳥”無人軍事直升機(jī)計(jì)算機(jī)系統(tǒng)的關(guān)鍵部分靠現(xiàn)有技術(shù)無法攻破，它的代碼就像數(shù)學(xué)證明一樣可靠。即便給予了黑客團(tuán)隊(duì)六周時(shí)間和更多直升機(jī)計(jì)算機(jī)系統(tǒng)的訪問權(quán)限，他們還是不能攻破“小鳥”無人軍事直升機(jī)計(jì)算機(jī)系統(tǒng)的防御。

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

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

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

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

隨著越來越多的關(guān)鍵社會(huì)職能轉(zhuǎn)移到網(wǎng)上，研究人員們對(duì)形式軟件驗(yàn)證技術(shù)的興趣也越來越濃厚。在以前，計(jì)算機(jī)還只是局限于家里和辦公室，程序漏洞最多也就是讓使用者感到不便。但現(xiàn)在，程序漏洞可能會(huì)導(dǎo)致巨大危害，任何具備相關(guān)知識(shí)的人都能利用同一漏洞自由地進(jìn)出某個(gè)計(jì)算機(jī)系統(tǒng)。

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

完美程序的夢(mèng)想

高可靠性軍事網(wǎng)絡(luò)系統(tǒng)(HACMS)項(xiàng)目發(fā)起人、美國塔夫斯大學(xué)計(jì)算機(jī)科學(xué)教授 Kathleen Fisher

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

計(jì)算機(jī)科學(xué)并沒有采用這一視角，因?yàn)榇撕蠛芏嗄昀?，要?shí)現(xiàn)這一視角看起來非常不切實(shí)際，即用形式邏輯規(guī)則來明確程序的功能。

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

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

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

實(shí)際的形式規(guī)范要比自動(dòng)駕駛?cè)グ儇浬痰昙?xì)致得多。比如編寫一個(gè)確認(rèn)收到文件，并按收到時(shí)間對(duì)文件進(jìn)行排序的程序，形式規(guī)范需要規(guī)定計(jì)數(shù)器永遠(yuǎn)只能增長（好讓后面接收的文件序號(hào)總比前面收到的文件高），以及程序永遠(yuǎn)也不會(huì)泄露給文件簽名的密鑰。

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

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

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

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

（對(duì)于列表中的每一項(xiàng) j，確保 j ≤ j+1）

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

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

基于代碼塊的安全

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

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

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

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

十年前，形式方法的研究者們（我是其中錯(cuò)得最厲害的一個(gè)）預(yù)測(cè)，計(jì)算機(jī)世界會(huì)擁抱并感激形式化帶來的每一點(diǎn)協(xié)助……結(jié)果是，全世界并沒有碰到我們一開始打算解決的那種問題。

后來出現(xiàn)了互聯(lián)網(wǎng)。互聯(lián)網(wǎng)之于編程錯(cuò)誤就像是飛機(jī)之于傳染?。寒?dāng)所有電腦都連接在一起時(shí)，不方便但可以忍受的軟件漏洞會(huì)導(dǎo)致一系列安全問題。

Andrew Appel 說道：“有一點(diǎn)我們當(dāng)時(shí)沒有特別明白，那就是互聯(lián)網(wǎng)上有一些軟件面向所有黑客開放，如果這種軟件里有一個(gè)漏洞，它就會(huì)成為安全威脅?！?/p>

在微軟研究院開發(fā)形式驗(yàn)證版 HTTPS 協(xié)議的計(jì)算機(jī)科學(xué)家 Jeannette Wing

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

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

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

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

高可靠性軍事網(wǎng)絡(luò)系統(tǒng)項(xiàng)目證明，通過明確定義計(jì)算機(jī)系統(tǒng)中的一小部分，就能極大地提高安全性。這個(gè)項(xiàng)目的最初目標(biāo)是打造一架無法被黑的娛樂四旋翼無人機(jī)。但無人機(jī)運(yùn)行的軟件非常龐大，黑客攻破一部分，就能獲得整個(gè)系統(tǒng)的控制權(quán)。于是在接下來的兩年里，高可靠性軍事網(wǎng)絡(luò)系統(tǒng)團(tuán)隊(duì)將無人機(jī)的任務(wù)控制計(jì)算機(jī)程序代碼分成了很多塊。

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

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

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

驗(yàn)證互聯(lián)網(wǎng)

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

隨著安全風(fēng)險(xiǎn)的日益增加，形式方法研究人員們正推動(dòng)更具野心的計(jì)劃。Andrew Appel 領(lǐng)導(dǎo)的 DeepSpec 正試圖建立一個(gè)經(jīng)過完全驗(yàn)證的端到端系統(tǒng)（就像網(wǎng)絡(luò)服務(wù)器一樣）。如果這一計(jì)劃成功，就能將過去十年中許多更小規(guī)模的驗(yàn)證成果組合到一起，比如經(jīng)過完全驗(yàn)證的操作系統(tǒng)內(nèi)核。Andrew Appel 說道：“DeepSpec 現(xiàn)在專注在做但還沒有做到的事情是，如何將這些組件用規(guī)范接口連接起來?！?/p>

在微軟研究院中，軟件工程師們已經(jīng)在進(jìn)行兩個(gè)雄心勃勃的形式驗(yàn)證項(xiàng)目。第一個(gè)項(xiàng)目名為 Everest，旨在打造經(jīng)過形式驗(yàn)證的 HTTPS 協(xié)議。

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

via quantamagazine

推薦閱讀：

尤金·卡巴斯基：網(wǎng)絡(luò)安全已陷“黑暗時(shí)代”，我們?cè)撊绾螒?yīng)對(duì)？

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

雷峰網(wǎng)原創(chuàng)文章，未經(jīng)授權(quán)禁止轉(zhuǎn)載。詳情見轉(zhuǎn)載須知。