令黑客一籌莫展的程式設計方法

2014年4月7日，世界首次知道心髒滴血漏洞。openssl中tls/dtls(傳輸層安全協定)心跳擴充實作上的一個小漏洞，卻能使攻擊者解開受脆弱openssl軟體保護系統中的加密措施。在當時，這些加密措施占據了公網大約2/3的江山。攻擊者可以竊聽那些看起來加密了的通信，盜取隐私資料，冒充服務和使用者。

漏洞一見諸報道，openssl便釋出了針對心髒滴血的更新檔。即便如此，1年半之後，仍有20多萬台裝置沒有打上更新檔。

心髒滴血隻是冰山一角

圍繞心髒滴血的所有關注(當然還有不必要的心理恐懼)，表明了小小程式設計失誤在當下互聯時代會造成多大的破壞。

計算機技術早期，漏洞不過意味着一點點的不便。那個時候，計算機間互不聯通，一個程式設計缺陷最多就是某個軟體時不時地故障一下。或許你需要不時重新開機一下機器，但最多也就是如此了。

但網際網路世界中，一切都不一樣了。全球連接配接性讓黑客可以瞄準更多的使用者。考慮到人們銀行憑證和其他敏感資料的激增，在今天，一個漏洞不僅僅意味着不友善這麼簡單。通常，程式設計漏洞就是安全漏洞，攻擊者可利用來盜取或披露成千上萬使用者的個人資訊。這也就是為什麼心髒滴血之類的漏洞會演變成大事件的原因所在。

但也别會錯意。我們的軟體也不是全部都被攻破了的。openssl的大多數用例仍然運作良好。心髒滴血僅僅構成了少數黑客入侵場景之一，這些場景中，攻擊者可以操縱程式設計缺陷産生軟體功能上的非預期結果。

這就是程式設計的現實。漏洞司空見慣，因為要把自然語言能描述的想法，轉換成機器能了解的指令，可不是件容易的事兒。

除此之外，程式設計的目标，是使計算機程式能夠隻實作一套既定的操作，不做多餘的事。正派程式員都不會希望有人在自己的軟體裡找到能讓他們竊聽加密通信或盜取個人資訊的漏洞。是以，程式員有責任讓自己的代碼無懈可擊。

但知易行難。稍微學過一點程式設計的人都會告訴你，程式設計出錯簡直太容易了。要是有什麼方法，能讓程式員確定自己的代碼隻做應該做的事就好了……

事實證明，還真有這麼一種資源。

代碼驗證好處多

形式化驗證是自70年代以來就在用的一種程式設計風格，通過確定程式符合每個用例，達到甚至超出程式應在某些可能用例情況下可用的最低要求。

程式員為達到這種包容性，往往将自己的代碼展開得像是數學證明，每條語句都延續前面語句的邏輯。程式員們寫下的，是描述程式行為的數學公式，并用某種形式的驗證程式檢查語句的正确性。

你正在寫下一個數學公式來描述程式的行為，并使用幾種驗證機制去校驗程式運作後所達到狀态的正确性。

想進行形式化驗證，程式員首先需要寫出形式化規約，或者對計算機程式應怎樣工作作出解釋說明。然後，用這一規約來驗證軟體是否到達既定目标。

這可不總是毫不費力的過程。在規約和驗證規約所需的語句之間，采用形式化驗證的程式，最終可能會比不采用驗證卻在大多數用例中工作良好的程式代碼長度的好幾倍。

幸運的是，碼農們現在可以用程式設計語言和證明輔助程式之類的工具來驗證自己的程式。事實上，正是幾十年前此類資源的缺乏，才導緻了直到網際網路出現的現代，形式化驗證才真正可行。

普林斯頓大學計算機科學教授安德魯·阿佩爾将之闡述為：

科學技術的很多部分，僅僅是不夠成熟到能應用的階段，是以，1980年前後，計算機科學領域很多部分興趣漸失。

走向應用

安全研究人員一刻也等不及補回失去的時間了。例如，美國國防部進階研究計劃局(darpa)設立的高可靠性網絡軍事系統(hacms)計劃中，工程師們就着手制作黑不掉的休閑四軸飛行器。他們通過先将飛行器的代碼分區，再通過使用“高可靠的構件”重寫其軟體架構，做到了這一點。其中一個構件就包含了入侵者不能更新權限以通路其他分區的驗證。

在其代号“小鳥”的實驗中，黑客組成的紅隊，收到了四軸飛行器攝像頭控制分區之一的通路權。他們的任務，就是擷取該飛行器基本功能的控制權。但在努力6周之後，他們依然無法進入另一個代碼分區。

這一成果吸引了國防部研究人員的注意。hacms項目經理，塔夫斯大學計算機科學教授卡斯靈·費舍爾說：

他們無論如何也突破不進去，破壞不了其運作。該結果讓darpa矚目，紛紛驚訝捧臉：“上帝啊，我們可以在擔心的系統裡實際使用這種技術了！”

發展前景

自“小鳥”開始，darpa将形式化驗證應用到了其他技術，比如自動駕駛汽車和衛星。

他們還給自己設定了一些未來想達到的崇高目标。阿佩爾希望用1000萬美元打造完全經驗證的端到端系統，比如web伺服器。同時，在微軟，工程師們正在建立https的驗證版本，以及無人機之類裝置的驗證規範。

本文轉自d1net（轉載）