號稱「不會被黑」的加密工具Evercrypt發布

IT之家4月8日消息 有研究人員於4月2日在GitHub上發布了一個號稱能防黑客的加密代碼工具，名為「EverCrypt」。從字面意思看，這個名字取得一點都不客氣——「永遠加密」。

負責該項目的計算機科學家Karthik Bhargavan在《Quanta Magazine》撰文稱，通過將計算機代碼視為數學證明，該庫被證實對大多數黑客攻擊都是無懈可擊的。

Evercrypt據稱是一個「軟體庫」，涉及簡單的算術，包括幾何和素數。

通常情況下，程序員團隊創建的軟體是來滿足他們所希望達成的某些目標。完成後，他們會測試代碼；如果軟體能在沒有帶來不良後果的情況下完成目標，程序員就能得出結論——軟體可以照預想那樣工作。

軟體的編碼錯誤則通常是出現在極端的「臨界情況」中，是由一些「不太可能發生的事」構成的完美風暴帶來的重大漏洞。近年來最具破壞性的黑客攻擊之中，許多例子都和這種極端情況有關。

與此相反，EverCrypt沒有遵循大多數代碼的編寫方式。參與EverCrypt的卡內基梅隆大學計算機科學家Bryan Parno說：「你可以減少代碼在數學公式中的行為方式的問題，然後你可以檢查公式是否成立。如果確實如此，你知道你的代碼有這個屬性。」

EverCrypt的工作始於2016年，是由微軟研究院領導的Project Everest的一部分。EverCrypt是採用F*語言編寫、驗證的，F*是一個由微軟研究院開發的基於F?的依賴類型函數式程序語言。

IT之家讀者若對此感興趣，可以點此鏈接前往相關GitHub頁面了解。

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！