使用形式化验证来保障软件的安全性，是一个经久不衰的课 题。操作系统是基础软件栈的底座，同时也具有非常高的复杂性，利用 形式化验证技术来提升操作系统的安全性和可靠性在实践中有很重要的意义。华为操作系统内核实验室在操作系统内核形式化验证方面有着多年的投入和积累，我们将分享 在形式化验证实践过程中所遇到的挑战以及我们的相应对策与思考，希望与大家交流共勉。
[操作系统, 形式化验证]
李屹
