利用數學工具寫出黑客無法攻陷的軟體
程序員是人類，但數學是不朽的。通過使編程更具數學性，計算機科學家希望消除可能被黑客利用、泄露數字機密並對現代社會造成普遍困擾的程序bug。
現在，隨著EverCrypt(一款數字加密工具)的發布，一組計算機科學家朝著宏偉目標邁出了重要的一步。研究人員能夠證明——證明畢達哥拉斯定理的那種證明——對於黑客用來攻陷以往程序的主要手段，最新的安全工具是完全無懈可擊的。「我們的意思是，我們通過數學方法證明，我們的代碼不會受到這種攻擊。」巴黎Inria的計算機科學家Karthik Bhargavan表示。
EverCrypt程序並非是按照常見的方式編寫。通常，程序員團隊先創建他們希望能夠滿足某些需求的軟體。完成後，他們會測試。如果它順順噹噹地完成了目標，並且不會出現預期外的行為，程序員就得出結論：該軟體能用了。
然而，bug通常只出現在極端的「邊界情況corner cases」下。近年來，許多最具破壞性的黑客工具都利用了極端情況。
相比之下，卡內基梅隆大學計算機科學家Bryan Parno和同事已經明確限定了他們程序的功能，然後證明了它的行為真的被局限在已知的範圍內，排除了在特殊情況下代碼可能以意想不到的方式偏離正軌的可能性。這種策略被稱為「形式驗證」。
因為完全定義複雜軟體系統(如網路瀏覽器)的功能幾乎是不可能的，所以研究人員轉而關注那些既重要又適合數學定義的程序。 EverCrypt是處理密碼或私人信息編碼和解碼的軟體庫。這些加密庫具有天生的數學性。它們涉及算術與素數和對規範幾何對象(如橢圓曲線)的操作。定義加密庫並不是一件容易的事。
EverCrypt的開發始於2016年，作為Project Everest的一部分，後者是由微軟研究院主持的項目。當時——現在仍然如此——加密庫是許多軟體應用程序中的一個軟肋。它們運行緩慢，拖累了所屬應用程序的整體性能，且充滿bug。
創建EverCrypt的主要挑戰是發明出一款一體化的開發平台，可以容納研究人員為經過驗證的加密庫添加的所有不同屬性。該平台既需要C++這樣的傳統編程語言的能力，又能如Isabelle和Coq這樣的證明輔助程序一樣提供邏輯語法和結構——數學家們已經使用了這兩款軟體很多年。當EverCrypt項目啟動時，還並沒有這樣的一體化平台，因此他們自己開發了一種——名為F *的編程語言。它把數學和編程放到了平等的地位。
「我們將這些事情統一到一個連貫的框架中，這樣就可以減少編寫程序和數學證明之間差異，」Bhargavan說，「你可以像軟體開發人員一樣寫代碼，但同時你也可以寫數學證明。」
他們證明，EverCrypt並沒有可供黑客利用的bug，如緩衝區溢出。實際上，可以證明它排除了對所有可能的極端情況的敏感性。他們還證明，EverCrypt每次都能獲得正確的數學加密結果——它從不執行錯誤的運算。
但EverCrypt最引人注目的承諾來自對完全不同方向上的安全弱點——當壞人通過觀察程序如何操作來推斷加密消息的內容時，就會出現的情況——的防護。
例如，有經驗的觀察者可能知道加密演算法為值賦予「0」時，程序的運行速度稍快，而在向值添加「1」時稍慢。通過測量演算法加密消息所花費的時間量，觀察者可以判斷出消息的二進位表示是否包含更多的0或1——並最終推斷出完整的消息。
「傳統加密演算法的原理本身，或者實現演算法的方式，正在泄露你的信息。」Bhargavan說。這種「旁道攻擊」是近年來幾次最臭名昭著的黑客事件的幕後推手，其中包括幸運13襲擊。研究人員證明，EverCrypt絕不會被利用以上述方式泄露信息。
雖然EverCrypt可以免疫許多攻擊類型，但它並不意味著絕對安全的軟體時代已然來臨。Protzenko指出，人們總是會想出未知的方式來利用程序漏洞，無法證明EverCrypt是永遠安全的。
此外，即使是經過驗證的加密庫也必須與許多其他軟體(如操作系統和許多常見的桌面應用程序)協同工作，這些軟體通常是未經驗證的，並且可能在可預見的未來也不會通過形式驗證。
由於未經驗證的協同應用可能會抵消加密庫的安全性，Project Everest希望使用儘可能多地使用經過驗證的軟體來配合EverCrypt。該計劃的首要目標是完成安全超文本傳輸協議(HTTPS)的全面驗證，該協議可保護大多數網路通信的安全。
本文譯自 quantamagazine，由譯者 majer 基於創作共用協議(BY-NC)發布。
TAG:煎蛋 |