有研究人員于4月2日在GitHub上發布了一個號稱能防黑客的加密代碼工具,名為“EverCrypt”。從字面意思看,這個名字取得一點都不客氣——“永遠加密”。
負責該項目的計算機科學家Karthik Bhargavan在《Quanta Magazine》撰文稱,通過將計算機代碼視為數學證明,該庫被證實對大多數黑客攻擊都是無懈可擊的。
Evercrypt據稱是一個“軟件庫”,涉及簡單的算術,包括幾何和素數。
通常情況下,程序員團隊創建的軟件是來滿足他們所希望達成的某些目標。完成后,他們會測試代碼;如果軟件能在沒有帶來不良后果的情況下完成了目標,程序員就可以得出結論,認為該軟件可以完成它的目標。
編碼錯誤通常情況下只是出現在極端的“臨界情況”中,是由一些“不太可能發生的事”構成的完美風暴帶來的重大漏洞。近年來最具破壞性的黑客攻擊之中,許多例子都和這種極端情況有關。
然而,EverCrypt沒有采用大多數代碼的編寫方式。負責EverCrypt的卡內基梅隆大學計算機科學家Bryan Parno說:“你可以減少代碼在數學公式中的行為方式的問題,然后你可以檢查公式是否成立。如果確實如此,你知道你的代碼有這個屬性。”
EverCrypt的工作始于2016年,是由微軟研究院領導的Project Everest的一部分。EverCrypt是采用F*語言編寫、驗證的,F*是一個由微軟研究院開發的基于F?的依賴類型函數式程序語言。