CertiK已完成对蚂蚁集团HyperEnclave先进形式化验证

CertiK宣布已经完成了对蚂蚁集团创新开放式跨平台可信执行环境（TEE）HyperEnclave的先进形式化验证。

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

CertiK的形式化验证过程涉及应用机器检查证明来验证HyperEnclave代码的正确性和安全性，其中包括了最关键的组件部分：RustMonitor。CertiK应用了其独有的先进系统代码验证方法，开发了一个用于验证Rust代码的定制框架。

凭借其在形式化验证方面的丰富经验和创新技术及应用，CertiK能够有效评估HyperEnclave的安全性。 

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

CertiK期待在未来可进一步对行业其他机密计算组件进行审计、测试和形式化验证。