Linux中System V进程通信机制安全性形式化验证

摘要

基于Linux开发安全操作系统是提高计算机安全的重要途径,而形式化验证则是开发过程的重要和必要的环节.我们从Linux的各个子系统着手进行验证,逐步搭建起整个操作系统的验证模型.考虑到访问控制机制是实现操作系统安全性的关键,本文主要讨论使用SPIN模型检验器对IPC子系统中的System V进程通信机制进行形式化验证的过程与方法,查找安全漏洞并改进现有的机制,为开发工作提供理论上的保证.