2014年4月7日，世界首次知道心臟滴血漏洞。OpenSSL中TLS/DTLS(傳輸層安全協議)心跳擴展實現上的一個小漏洞，卻能使攻擊者解開受脆弱OpenSSL軟件保護系統中的加密措施。在當時，這些加密措施占據了公網大約2/3的江山。攻擊者可以竊聽那些看起來加密了的通信，盜取隱私數據，冒充服務和用戶。
漏洞一見諸報道，OpenSSL便發布了針對心臟滴血的補丁。即便如此，1年半之后，仍有20多萬臺設備沒有打上補丁。
心臟滴血只是冰山一角
圍繞心臟滴血的所有關注(當然還有不必要的心理恐懼)，表明了小小編程失誤在當下互聯時代會造成多大的破壞。
計算機技術早期，漏洞不過意味著一點點的不便。那個時候，計算機間互不聯通，一個編程缺陷最多就是某個軟件時不時地故障一下。或許你需要不時重啟一下機器，但最多也就是如此了。
但互聯網世界中，一切都不一樣了。全球連接性讓黑客可以瞄準更多的用戶。考慮到人們銀行憑證和其他敏感數據的激增，在今天，一個漏洞不僅僅意味著不方便這么簡單。通常，編程漏洞就是安全漏洞，攻擊者可利用來盜取或披露成千上萬用戶的個人信息。這也就是為什么心臟滴血之類的漏洞會演變成大事件的原因所在。
但也別會錯意。我們的軟件也不是全部都被攻破了的。OpenSSL的大多數用例仍然運作良好。心臟滴血僅僅構成了少數黑客入侵場景之一，這些場景中，攻擊者可以操縱編程缺陷產生軟件功能上的非預期結果。
這就是編程的現實。漏洞司空見慣，因為要把自然語言能描述的想法，轉換成機器能理解的指令，可不是件容易的事兒。
除此之外，編程的目標，是使計算機程序能夠只實現一套既定的操作，不做多余的事。正派程序員都不會希望有人在自己的軟件里找到能讓他們竊聽加密通信或盜取個人信息的漏洞。因此，程序員有責任讓自己的代碼無懈可擊。
但知易行難。稍微學過一點編程的人都會告訴你，編程出錯簡直太容易了。要是有什么方法，能讓程序員確保自己的代碼只做應該做的事就好了……
事實證明，還真有這么一種資源。
代碼驗證好處多
形式化驗證是自70年代以來就在用的一種編程風格，通過確保程序符合每個用例，達到甚至超出程序應在某些可能用例情況下可用的最低要求。
程序員為達到這種包容性，往往將自己的代碼展開得像是數學證明，每條語句都延續前面語句的邏輯。程序員們寫下的，是描述程序行為的數學公式，并用某種形式的驗證程序檢查語句的正確性。
你正在寫下一個數學公式來描述程序的行為，并使用幾種驗證機制去校驗程序運行后所達到狀態的正確性。
想進行形式化驗證，程序員首先需要寫出形式化規約，或者對計算機程序應怎樣工作作出解釋說明。然后，用這一規約來驗證軟件是否到達既定目標。
這可不總是毫不費力的過程。在規約和驗證規約所需的語句之間，采用形式化驗證的程序，最終可能會比不采用驗證卻在大多數用例中工作良好的程序代碼長度的好幾倍。
幸運的是，碼農們現在可以用編程語言和證明輔助程序之類的工具來驗證自己的程序。事實上，正是幾十年前此類資源的缺乏，才導致了直到互聯網出現的現代，形式化驗證才真正可行。
普林斯頓大學計算機科學教授安德魯·阿佩爾將之闡述為：
科學技術的很多部分，僅僅是不夠成熟到能應用的階段，因此，1980年前后，計算機科學領域很多部分興趣漸失。
走向應用
安全研究人員一刻也等不及補回失去的時間了。例如，美國國防部高級研究計劃局(DARPA)設立的高可靠性網絡軍事系統(HACMS)計劃中，工程師們就著手制作黑不掉的休閑四軸飛行器。他們通過先將飛行器的代碼分區，再通過使用“高可靠的構件”重寫其軟件架構，做到了這一點。其中一個構件就包含了入侵者不能升級權限以訪問其他分區的驗證。
在其代號“小鳥”的實驗中，黑客組成的紅隊，收到了四軸飛行器攝像頭控制分區之一的訪問權。他們的任務，就是獲取該飛行器基本功能的控制權。但在努力6周之后，他們依然無法進入另一個代碼分區。
這一成果吸引了國防部研究人員的注意。HACMS項目經理，塔夫斯大學計算機科學教授卡斯靈·費舍爾說：
他們無論如何也突破不進去，破壞不了其運行。該結果讓DARPA矚目，紛紛驚訝捧臉：“上帝啊，我們可以在擔心的系統里實際使用這種技術了！”
發展前景
自“小鳥”開始，DARPA將形式化驗證應用到了其他技術，比如自動駕駛汽車和衛星。
他們還給自己設定了一些未來想達到的崇高目標。阿佩爾希望用1000萬美元打造完全經驗證的端到端系統，比如Web服務器。同時，在微軟，工程師們正在創建HTTPS的驗證版本，以及無人機之類設備的驗證規范。
京公網安備 11010502049343號