蚂蚁集团开创性项目，CertiK为其提供先进形式化验证服务

　　近日,全球区块链和智能合约安全领域的先锋CertiK宣布,已完成了对蚂蚁集团可信原生技术团队开发的创新开放式跨平台可信执行环境(TEE)HyperEnclave的先进形式化验证。CertiK的形式化验证过程涉及应用机器检查证明来验证HyperEnclave代码的正确性和安全性,其中包括了最关键的组件部分:RustMonitor。CertiK应用了其独有的先进系统代码验证方法,开发了一个用于验证Rust代码的定制框架。

　　CertiK是区块链安全领域的先驱。通过将学术界的尖端创新技术延伸至业界,CertiK可帮助企业任务关键型软件及应用在足够安全和正确的环境下构建,从而保护Web3世界。凭借其在形式化验证方面的丰富经验和创新技术及应用,CertiK能够有效评估HyperEnclave的安全性。

　　蚂蚁集团的可信原生技术团队开发了开放跨平台软件可信执行环境HyperEnclave,旨在提高蚂蚁集团隐私保护计算工作负载的效率和兼容性。CertiK利用其独有的先进形式化验证技术,验证了HyperEnclave核心组件的安全性和技术正确性。

　　CertiK的联合创始人、其所独有的系统代码验证方法发明人顾荣辉教授表示:“CertiK为能参加该开创性项目感到自豪和荣幸,我们所完成的形式化验证工作印证了我们要不断发展技术和推动Web3领域安全不断进步的承诺。”

　　自今年6月以来,经历调整的Web3.0市场日益呈现回暖信号,行业内对于安全合规普遍给予了高度重视。行业宏观趋势将CertiK这样的头部安全审计公司推向舞台中心。综合此间媒体报道,CertiK今日刚刚宣布完成对XRPLedger上自动做市商(AMM)的审计;6月底宣布完成了对OKX用于支持BRC-20代币基础设施的安全审计;6月初,CertiK还因成功发现并报告了Sui的“仓鼠轮”新型安全威胁而被授予了50万漏洞赏金。CertiK期待在未来可进一步对行业其他机密计算组件进行审计、测试和形式化验证。