2014年4月7日，世界首次知道心臟滴血漏洞。OpenSSL中TLS/DTLS(傳輸層安全協(xié)議)心跳擴(kuò)展實(shí)現(xiàn)上的一個(gè)小漏洞，卻能使攻擊者解開受脆弱OpenSSL軟件保護(hù)系統(tǒng)中的加密措施。在當(dāng)時(shí)，這些加密措施占據(jù)了公網(wǎng)大約2/3的江山。攻擊者可以竊聽那些看起來(lái)加密了的通信，盜取隱私數(shù)據(jù)，冒充服務(wù)和用戶。

漏洞一見諸報(bào)道，OpenSSL便發(fā)布了針對(duì)心臟滴血的補(bǔ)丁。即便如此，1年半之后，仍有20多萬(wàn)臺(tái)設(shè)備沒有打上補(bǔ)丁。

心臟滴血只是冰山一角

圍繞心臟滴血的所有關(guān)注(當(dāng)然還有不必要的心理恐懼)，表明了小小編程失誤在當(dāng)下互聯(lián)時(shí)代會(huì)造成多大的破壞。

計(jì)算機(jī)技術(shù)早期，漏洞不過意味著一點(diǎn)點(diǎn)的不便。那個(gè)時(shí)候，計(jì)算機(jī)間互不聯(lián)通，一個(gè)編程缺陷最多就是某個(gè)軟件時(shí)不時(shí)地故障一下?；蛟S你需要不時(shí)重啟一下機(jī)器，但最多也就是如此了。

但互聯(lián)網(wǎng)世界中，一切都不一樣了。全球連接性讓黑客可以瞄準(zhǔn)更多的用戶?？紤]到人們銀行憑證和其他敏感數(shù)據(jù)的激增，在今天，一個(gè)漏洞不僅僅意味著不方便這么簡(jiǎn)單。通常，編程漏洞就是安全漏洞，攻擊者可利用來(lái)盜取或披露成千上萬(wàn)用戶的個(gè)人信息。這也就是為什么心臟滴血之類的漏洞會(huì)演變成大事件的原因所在。

但也別會(huì)錯(cuò)意。我們的軟件也不是全部都被攻破了的。OpenSSL的大多數(shù)用例仍然運(yùn)作良好。心臟滴血僅僅構(gòu)成了少數(shù)黑客入侵場(chǎng)景之一，這些場(chǎng)景中，攻擊者可以操縱編程缺陷產(chǎn)生軟件功能上的非預(yù)期結(jié)果。

這就是編程的現(xiàn)實(shí)。漏洞司空見慣，因?yàn)橐炎匀徽Z(yǔ)言能描述的想法，轉(zhuǎn)換成機(jī)器能理解的指令，可不是件容易的事兒。

除此之外，編程的目標(biāo)，是使計(jì)算機(jī)程序能夠只實(shí)現(xiàn)一套既定的操作，不做多余的事。正派程序員都不會(huì)希望有人在自己的軟件里找到能讓他們竊聽加密通信或盜取個(gè)人信息的漏洞。因此，程序員有責(zé)任讓自己的代碼無(wú)懈可擊。

但知易行難。稍微學(xué)過一點(diǎn)編程的人都會(huì)告訴你，編程出錯(cuò)簡(jiǎn)直太容易了。要是有什么方法，能讓程序員確保自己的代碼只做應(yīng)該做的事就好了……

事實(shí)證明，還真有這么一種資源。

代碼驗(yàn)證好處多

形式化驗(yàn)證是自70年代以來(lái)就在用的一種編程風(fēng)格，通過確保程序符合每個(gè)用例，達(dá)到甚至超出程序應(yīng)在某些可能用例情況下可用的最低要求。

程序員為達(dá)到這種包容性，往往將自己的代碼展開得像是數(shù)學(xué)證明，每條語(yǔ)句都延續(xù)前面語(yǔ)句的邏輯。程序員們寫下的，是描述程序行為的數(shù)學(xué)公式，并用某種形式的驗(yàn)證程序檢查語(yǔ)句的正確性。

你正在寫下一個(gè)數(shù)學(xué)公式來(lái)描述程序的行為，并使用幾種驗(yàn)證機(jī)制去校驗(yàn)程序運(yùn)行后所達(dá)到狀態(tài)的正確性。

想進(jìn)行形式化驗(yàn)證，程序員首先需要寫出形式化規(guī)約，或者對(duì)計(jì)算機(jī)程序應(yīng)怎樣工作作出解釋說(shuō)明。然后，用這一規(guī)約來(lái)驗(yàn)證軟件是否到達(dá)既定目標(biāo)。

這可不總是毫不費(fèi)力的過程。在規(guī)約和驗(yàn)證規(guī)約所需的語(yǔ)句之間，采用形式化驗(yàn)證的程序，最終可能會(huì)比不采用驗(yàn)證卻在大多數(shù)用例中工作良好的程序代碼長(zhǎng)度的好幾倍。

幸運(yùn)的是，碼農(nóng)們現(xiàn)在可以用編程語(yǔ)言和證明輔助程序之類的工具來(lái)驗(yàn)證自己的程序。事實(shí)上，正是幾十年前此類資源的缺乏，才導(dǎo)致了直到互聯(lián)網(wǎng)出現(xiàn)的現(xiàn)代，形式化驗(yàn)證才真正可行。

普林斯頓大學(xué)計(jì)算機(jī)科學(xué)教授安德魯·阿佩爾將之闡述為：

科學(xué)技術(shù)的很多部分，僅僅是不夠成熟到能應(yīng)用的階段，因此，1980年前后，計(jì)算機(jī)科學(xué)領(lǐng)域很多部分興趣漸失。

走向應(yīng)用

安全研究人員一刻也等不及補(bǔ)回失去的時(shí)間了。例如，美國(guó)國(guó)防部高級(jí)研究計(jì)劃局(DARPA)設(shè)立的高可靠性網(wǎng)絡(luò)軍事系統(tǒng)(HACMS)計(jì)劃中，工程師們就著手制作黑不掉的休閑四軸飛行器。他們通過先將飛行器的代碼分區(qū)，再通過使用“高可靠的構(gòu)件”重寫其軟件架構(gòu)，做到了這一點(diǎn)。其中一個(gè)構(gòu)件就包含了入侵者不能升級(jí)權(quán)限以訪問其他分區(qū)的驗(yàn)證。

在其代號(hào)“小鳥”的實(shí)驗(yàn)中，黑客組成的紅隊(duì)，收到了四軸飛行器攝像頭控制分區(qū)之一的訪問權(quán)。他們的任務(wù)，就是獲取該飛行器基本功能的控制權(quán)。但在努力6周之后，他們依然無(wú)法進(jìn)入另一個(gè)代碼分區(qū)。

這一成果吸引了國(guó)防部研究人員的注意。HACMS項(xiàng)目經(jīng)理，塔夫斯大學(xué)計(jì)算機(jī)科學(xué)教授卡斯靈·費(fèi)舍爾說(shuō)：

他們無(wú)論如何也突破不進(jìn)去，破壞不了其運(yùn)行。該結(jié)果讓DARPA矚目，紛紛驚訝捧臉：“上帝啊，我們可以在擔(dān)心的系統(tǒng)里實(shí)際使用這種技術(shù)了！”

發(fā)展前景

自“小鳥”開始，DARPA將形式化驗(yàn)證應(yīng)用到了其他技術(shù)，比如自動(dòng)駕駛汽車和衛(wèi)星。

他們還給自己設(shè)定了一些未來(lái)想達(dá)到的崇高目標(biāo)。阿佩爾希望用1000萬(wàn)美元打造完全經(jīng)驗(yàn)證的端到端系統(tǒng)，比如Web服務(wù)器。同時(shí)，在微軟，工程師們正在創(chuàng)建HTTPS的驗(yàn)證版本，以及無(wú)人機(jī)之類設(shè)備的驗(yàn)證規(guī)范。