%0 Journal Article
%T 基于广义污点传播模型的操作系统访问控制
%A 杨智？
%A 殷丽华？
%A 段洣毅？
%A 吴金宇？
%A 金舒原？
%A 郭莉？
%J 软件学报
%P 1602-1619
%D 2012
%R 10.3724/SP.J.1001.2012.04083
%X 动态调整安全级是目前提高强制访问控制模型可用性的主要途径,它大致包括两类方法.其中,安全级范围方法对主体权限最小化的支持不够,而污点传播方法存在已知隐蔽通道.提出了保护操作系统保密性和完整性的广义污点传播模型(generalizedtaintpropagationmodel,简称gtpm),它继承了污点传播在最小权限方面的特点,拓展了污点传播语义,以试图关闭已知隐蔽通道,引入了主体的降密和去污能力以应对污点积累;还利用通信顺序进程(csp)语言描述了模型的规格,以明确基于gtpm的操作系统的信息流控制行为的形式化语义;基于csp的进程等价验证模型定义了可降密无干扰,并借助fdr工具证明形式化构建的抽象gtpm系统具有可降密无干扰安全性质.最后,通过一个示例分析了模型的可用性提升.
%K 污点传播
%K 隐蔽通道
%K 通信顺序进程
%K 无干扰
%K 最小权限
%K 信息流控制
%K 操作系统
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4083&flag=1