近日，2023级博士生杨叶倩为第一作者、戴鸿君教授为通讯作者的论文《RISC-V SBI固件安全启动过程的形式化验证》被中国科学院主管的权威学术期刊《计算机研究与发展》正式接收并录用，拟安排在2026年第63卷正式发表。《计算机研究与发展》创刊于1959年，是国内计算机领域历史最为悠久、学术水平最高的核心期刊之一，也是中国计算机学会（CCF）推荐的A类期刊。

 论文聚焦于RISC-V体系结构下SBI（Supervisor Binary Interface）固件的安全启动问题。与x86和ARM平台相比，RISC-V SBI固件在规范性和可靠性方面具有优势，但现有版本仍存在启动正确性缺乏验证、物理内存保护（PMP）地址访问漏洞等安全隐患。针对这一问题，论文提出了定理证明驱动的闭环形式化验证框架，并研发了首个经形式化验证的SBI固件——SeSBI。在技术实现上，论文结合Dafny与Isabelle/HOL，采用分层验证策略完成对固件启动过程的形式化建模与验证。为进一步提升验证效率，提出了RISC-V硬件模拟策略，以统一方式建模固件与硬件交互过程，有效降低了验证开销。最终，成功完成了SeSBI固件启动过程的功能正确性验证。结果表明，SeSBI不仅以更简洁的代码实现了SBI标准接口，还在可靠性方面达到新高度，为RISC-V生态系统提供了首个经形式化验证的可信SBI固件实现。

 该研究工作首次在国内权威期刊系统性地提出并实现了SBI固件的形式化验证，为未来RISC-V开源生态的可信计算提供了重要基础。未来，将进一步拓展验证范围至更多高级属性，并优化验证工具以提升验证效率，为安全可靠的RISC-V生态体系建设贡献力量。