CertiK攜手螞蟻密算：為星綻操作系統打造「數學證明級」安全

，據網易新聞消息，Web3安全巨頭CertiK與螞蟻集團旗下的螞蟻密算聯合發布了最新研究工作，對下一代開源通用操作系統——星綻(Asterinas)——的核心組件進行了形式化驗證。星綻基於Rust開發，兼容Linux應用。此項工作展示了對Rust操作系統形式化驗證的重要進展，推動其安全性邁向「數學證明級」標准，並為提升下一代通用操作系統的安全性提供了新的思路。此前，CertiK已成功為螞蟻密算的TEE平台HyperEnclave完成形式化驗證。