CertiK携手蚂蚁密算：为星绽操作系统打造“数学证明级”安全

星绽基于Rust开发，兼容Linux应用。此项工作展示了对Rust操作系统形式化验证的重要进展，推动其安全性迈向“数学证明级”标准，并为提升下一代通用操作系统的安全性提供了新的思路。

区小号 3月14日消息，，据网易新闻消息，Web3安全巨头CertiK与蚂蚁集团旗下的蚂蚁密算联合发布了最新研究工作，对下一代开源通用操作系统——星绽(Asterinas)——的核心组件进行了形式化验证。星绽基于Rust开发，兼容Linux应用。此项工作展示了对Rust操作系统形式化验证的重要进展，推动其安全性迈向“数学证明级”标准，并为提升下一代通用操作系统的安全性提供了新的思路。此前，CertiK已成功为蚂蚁密算的TEE平台HyperEnclave完成形式化验证。