J4 ›› 2002, Vol. 24 ›› Issue (2): 13-17.
• 论文 • 上一篇 下一篇
吴丹 刘芳 等
出版日期:
发布日期:
Online:
Published:
摘要：
基于Linux开发安全操作系统是提高计算机安全的重要途径，而形式化验证则是开发过程的重要和必要的环节，我们从Linux的各个子系统着手进行验证，逐步搭建起整个操作系统的验证模型。考虑到访问控制机制是实现操作系统安全性的关键，本文主要讨论使用SPIN模型检验器对IPC子系统中的SystemV进程通信机制进行形式化验证的过程与方法法。查找安全漏洞并改进现有的机制，为开发工程提供理论上的保证。
关键词: Linux SystemV 进程通信机制 安全性 形式化验证 操作系统 计算机网络
吴丹 刘芳 等. Linux中SystemV进程通信机制安全性形式化验证[J]. J4, 2002, 24(2): 13-17.
0 / / 推荐
导出引用管理器 EndNote|Ris|BibTeX
链接本文: http://joces.nudt.edu.cn/CN/
http://joces.nudt.edu.cn/CN/Y2002/V24/I2/13
