CertiK has successfully completed the formal verification of HyperEnclave, an innovative open and cross-platform Trusted Execution Environment (TEE) from Ant Group’s Trust Native Technology team.
This marks the first time in the industry that such “an in-depth formal verification process has been completed for a TEE.”
Ant Group’s Trust Native Technology team “developed HyperEnclave as an open and cross-platform TEE to increase the efficiency and compatibility of its privacy-preserving computing workload.”
CertiK, using its exclusive world-class advanced formal verification technologies, “successfully verified the security and technical correctness of HyperEnclave’s core components.”
CertiK’s formal verification process “involved applying machine-checked proofs to validate the correctness and security of HyperEnclave’s code, including its most critical component: RustMonitor.” CertiK applied its exclusive advanced systems code verification approach and developed “a customized framework for verifying Rust code.”
With extensive experience in formal verification and a number of innovative applications of the process, the CertiK team was able “to accurately evaluate the security of HyperEnclave.”
Prof. Ronghui Gu, co-founder of CertiK and inventor of the exclusive approach to systems code verification, said:
“CertiK is proud to work on this ground-breaking project. Our work on this formal verification is a testament to our commitment to pushing the boundaries of security in the ever-evolving tech and Web3 landscapes.”
CertiK says it looks forward to further auditing, testing, and formal verification of other confidential computing building blocks.”
In another update, it was noted that the Conti Group, a notorious ransomware gang that is now defunct, was speculated by many in the threat intelligence community to be a continuation of successful elements from the also defunct Ryuk ransomware gang.
This speculation was based “on the significant overlap observed in both groups’ code and operations.”
An analysis of Conti’s operating structure and fund movements “using Bitcoin has revealed another potential area of overlap between the two groups.”
Wallets attributed to Conti were found “to be active outside of Conti’s known operational timeframes, and these periods of activity significantly coincide with the operational timeline of Ryuk.”
This report examines the overlap “between the operations of the Conti and Ryuk groups, providing a deeper understanding of their activities and potential interactions.”
A detailed investigation into Ryuk’s activities will “follow this report to further identify any possible interactions between the two groups.”
