近日,全球區塊鏈和智能合約安全領域的先鋒CertiK宣布,已完成了對螞蟻集團可信原生技術團隊開發的創新開放式跨平臺可信執行環境(TEE)HyperEnclave的先進形式化驗證。

　　CertiK是區塊鏈安全領域的先驅。通過將學術界的尖端創新技術延伸至業界,CertiK可幫助企業任務關鍵型軟件及應用在足夠安全和正確的環境下構建,從而保護Web3世界。憑借其在形式化驗證方面的豐富經驗和創新技術及應用,CertiK能夠有效評估HyperEnclave的安全性。

　　螞蟻集團的可信原生技術團隊開發了開放跨平臺軟件可信執行環境HyperEnclave,旨在提高螞蟻集團隱私保護計算工作負載的效率和兼容性。CertiK利用其獨有的先進形式化驗證技術,驗證了HyperEnclave核心組件的安全性和技術正確性。

　　CertiK的聯合創始人、其所獨有的系統代碼驗證方法發明人顧榮輝教授表示:“CertiK為能參加該開創性項目感到自豪和榮幸,我們所完成的形式化驗證工作印證了我們要不斷發展技術和推動Web3領域安全不斷進步的承諾。”

　　CertiK的形式化驗證過程涉及應用機器檢查證明來驗證HyperEnclave代碼的正確性和安全性,其中包括了最關鍵的組件部分:RustMonitor。CertiK應用了其獨有的先進系統代碼驗證方法,開發了一個用于驗證Rust代碼的定制框架。

　　自今年6月以來,經歷調整的Web3.0市場日益呈現回暖信號,行業內對于安全合規普遍給予了高度重視。行業宏觀趨勢將CertiK這樣的頭部安全審計公司推向舞臺中心。綜合此間媒體報道,CertiK今日剛剛宣布完成對XRPLedger上自動做市商(AMM)的審計;6月底宣布完成了對OKX用于支持BRC-20代幣基礎設施的安全審計;6月初,CertiK還因成功發現并報告了Sui的“倉鼠輪”新型安全威脅而被授予了50萬漏洞賞金。