Foresight News reported, according to NetEase News, Web3 security company CertiK and Ant Group's Ant Quantum Computing have jointly released their latest research work, conducting formal verification on the core components of the next-generation open-source general-purpose operating system "Asterinas". Asterinas is developed based on Rust and is compatible with Linux applications. This work demonstrates important progress in the formal verification of Rust-based operating systems, pushing its security towards a "mathematical proof-level" standard, and providing new ideas for enhancing the security of the next-generation general-purpose operating systems.
Previously, CertiK has successfully completed the formal verification of Ant Quantum Computing's TEE platform HyperEnclave.
