主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
杨智,殷丽华,段洣毅,吴金宇,金舒原,郭莉.基于广义污点传播模型的操作系统访问控制.软件学报,2012,23(6):1602-1619
基于广义污点传播模型的操作系统访问控制
Generalized Taint Propagation Model for Access Control in Operation Systems
投稿时间:2010-10-18  修订日期:2011-04-28
DOI:10.3724/SP.J.1001.2012.04083
中文关键词:  污点传播  隐蔽通道  通信顺序进程  无干扰  最小权限  信息流控制  操作系统
英文关键词:taint propagation  covert channel  CSP  noninterference  least privilege  information flow control  operating system
基金项目:国家自然科学基金(61070186); 国家高技术研究发展计划(863)(2009AA01Z438); 国家重点基础研究发展计划(973)(2007CB311100, 2011CB311801)
作者单位E-mail
杨智 中国科学院 计算技术研究所,北京 100190
解放军信息工程大学,河南 郑州 450004
中国科学院 研究生院,北京 100049
信息内容安全技术国家工程实验室,北京 100190 
zynoah@163.com 
殷丽华 中国科学院 计算技术研究所,北京 100190
信息内容安全技术国家工程实验室,北京 100190 
 
段洣毅 中国科学院 计算技术研究所,北京 100190  
吴金宇 中国科学院 计算技术研究所,北京 100190
信息内容安全技术国家工程实验室,北京 100190 
 
金舒原 中国科学院 计算技术研究所,北京 100190
信息内容安全技术国家工程实验室,北京 100190 
 
郭莉 中国科学院 计算技术研究所,北京 100190
信息内容安全技术国家工程实验室,北京 100190 
 
摘要点击次数: 3043
全文下载次数: 2837
中文摘要:
      动态调整安全级是目前提高强制访问控制模型可用性的主要途径,它大致包括两类方法.其中,安全级范围方法对主体权限最小化的支持不够,而污点传播方法存在已知隐蔽通道.提出了保护操作系统保密性和完整性的广义污点传播模型(generalized taint propagation model,简称GTPM),它继承了污点传播在最小权限方面的特点,拓展了污点传播语义,以试图关闭已知隐蔽通道,引入了主体的降密和去污能力以应对污点积累;还利用通信顺序进程(CSP)语言描述了模型的规格,以明确基于GTPM 的操作系统的信息流控制行为的形式化语义;基于CSP 的进程等价验证模型定义了可降密无干扰,并借助FDR工具证明形式化构建的抽象GTPM系统具有可降密无干扰安全性质.最后,通过一个示例分析了模型的可用性提升.
英文摘要:
      Dynamically adjusting the security label of each subject is a main approach to improving the availability of MAC models. It includes the method of security label range and the method of taint propagation. The former lacks the support for a less proviledge subject, and the latter has a known covert channels. In this paper, a model called generalized taint propagation model (GTPM) is proposed to protect the confidentiality and integrity of operating systems. It inherits the least privilege characteristic of taint propagation model (TPM), expands the semantics of TPM to close the known covert channels, and introduces declassification and decontamination capacities of subjects to avoid accumulating contamination. The paper also introduces its specification using communicating sequential processes (CSP) language to clear the formal semantics of a GTPM operating system's behaviors of information flow control; Moreover, the study noninterference with declassification in CSP verification model of process equivalence, and proves that abstract GTPM system have the security property of noninterference with declassification in virtue of FDR tool. Finally, this paper uses an example to demonstrate its improvement of availability.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利