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

• 作者: 刘芳 吴丹 戴葵 王志英
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 形式化验证 访问控制 IPC SPIN System V
• 年，卷（期）: 2002,（2）
• 所属期刊栏目: 网络与信息安全
• 页码范围: 13-17
• 页数: 5页
• 分类号: TP316.08
• 字数: 3488字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2002.02.003

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘芳	国防科技大学计算机学院	34	380	11.0	18.0
2	王志英	国防科技大学计算机学院	108	680	15.0	21.0
3	戴葵	国防科技大学计算机学院	63	410	12.0	18.0
4	吴丹	国防科技大学计算机学院	8	47	3.0	6.0