近期,Web3安全巨头CertiK与蚂蚁集团旗下的蚂蚁密算联合发布了最新研究工作,对下一代开源通用操作系统——星绽(Asterinas)——的核心组件进行了形式化验证。星绽与Linux兼容,可无缝运行Linux应用,但完全从头使用Rust语言开发。此项工作展示了对Rust操作系统形式化验证的重要进展,推动其安全性迈向“数学证明级”标准,并为提升下一代通用操作系统的安全性提供了新的思路。
星绽是由蚂蚁密算、中关村实验室、北京大学、南方科技大学等机构共同发起的开源操作系统,专注于安全可信的底层技术。星绽的目标是打造一个安全、可靠、高效的通用操作系统,为各种应用场景提供强大的支持。
形式化验证通过数学方法严格验证系统正确性,是构建高可信软件的“黄金标准”。作为Web3及系统安全领域“先进形式化验证”的倡导者和领先者,CertiK致力于验证具体代码而非局限于抽象模型、揭示代码独有的性质而非局限于常见性质、进行任意复杂的机械化推理而非局限于仅凭人力所能进行的简单推理、面向大规模生产环境而非局限于学术研究用途。
此次合作中,Asterinas社区和CertiK的先进形式化验证团队共同致力于验证星绽的核心组件——页面管理模块的安全性和正确性。在已完成的工作中,CertiK不仅成功应用其特有的分层抽象模块化验证框架,而且做到了对Rust源代码的直接验证,显著提升了验证效率和开发可维护性。
星绽的OS框架提供了一组安全的抽象,但因需操作底层硬件,包含非内存安全Rust代码(unsafe Rust code),Rust语言本身无法保证其安全性。例如,物理内存页面及页表管理的安全性,严重依赖于页表游标的细粒度互锁,以及页面引用计数的正确性。验证的结果提高了对内核安全性的信心:基于游标的页表遍历和对页面指针的引用计数,均被证明是正确的。关于验证工作的细节详见技术博客。
此前CertiK已为蚂蚁密算的开放式跨平台可信执行环境(TEE)平台HyperEnclave完成了形式化验证,确保其核心组件在安全性和技术正确性方面达到了严格的标准。该合作帮助HyperEnclave在全球范围内赢得了技术信任。
通过此次验证工作,CertiK在区块链安全与系统软件安全之间的桥梁作用将越发凸显,展现出更加广阔的发展前景。
