近期,Web3安全巨头CertiK与蚂蚁集团旗下的蚂蚁密算联合发布了最新研究工作,对下一代开源通用操作系统——星绽(Asterinas)——的核心组件进行了形式化验证。星绽与Linux兼容,可无缝运行Linux应用,但完全从头使用Rust语言开发。此项工作展示了对Rust操作系统形式化验证的重要进展,推动其安全性迈向“数学证明级”标准,并为提升下一代通用操作系统的安全性提供了新的思路。

星绽是由蚂蚁密算、中关村实验室、北京大学、南方科技大学等机构共同发起的开源操作系统,专注于安全可信的底层技术。星绽的目标是打造一个安全、可靠、高效的通用操作系统,为各种应用场景提供强大的支持。

形式化验证通过数学方法严格验证系统正确性,是构建高可信软件的“黄金标准”。作为Web3及系统安全领域“先进形式化验证”的倡导者和领先者,CertiK致力于验证具体代码而非局限于抽象模型、揭示代码独有的性质而非局限于常见性质、进行任意复杂的机械化推理而非局限于仅凭人力所能进行的简单推理、面向大规模生产环境而非局限于学术研究用途。

此次合作中,Asterinas社区和CertiK的先进形式化验证团队共同致力于验证星绽的核心组件——页面管理模块的安全性和正确性。在已完成的工作中,CertiK不仅成功应用其特有的分层抽象模块化验证框架,而且做到了对Rust源代码的直接验证,显著提升了验证效率和开发可维护性。