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

深潮 TechFlow 消息，据官方微信公众号消息，全球区块链和智能合约安全公司CertiK已经完成对蚂蚁集团创新开放式跨平台可信执行环境（TEE）HyperEnclave的先进形式化验证。

据悉，蚂蚁集团开放跨平台软件可信执行环境HyperEnclave由其可信原生技术团队开发，旨在提高蚂蚁集团隐私保护计算工作负载的效率和兼容性。

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