基于DTE策略的安全域隔离Z形式模型

被引：5

作者：

卿斯汉 ^{[1
]}

李丽萍 ^{[1
]}

何建波 ^{[1
]}

沈晴霓 ^{[2
]}

机构：

[1] 中国科学院软件研究所

[2] 北京大学软件与微电子学院

来源：

计算机研究与发展 | 2007年 / 11期

基金：

北京市自然科学基金;

关键词：

安全域隔离; 信息流; DTE; 可信管道; 形式化;

D O I：

暂无

中图分类号：

TP393.08 [];

学科分类号：

0839 ; 1402 ;

摘要：

基于DTE策略的安全域隔离技术是构造可信系统的基本技术之一.但现有DTE实现系统存在安全目标不明确、缺乏对系统及其安全性质的形式定义和分析的缺点,导致系统安全性难以得到保证.定义了一个基于DTE策略的安全域隔离模型,采用Z语言形式定义了系统状态、基于信息流分析的不变量和安全状态,并借助Z/EVES工具给出验证系统安全的形式分析方法.解决了DTE系统的形式化建模问题,为安全域隔离技术的实现和验证奠定了基础.

引用

页码：1881 / 1888

页数：8

共 6 条

[1]

商务安全策略及其形式分析研究[D]. 温红子.中国科学院研究生院（软件研究所）. 2005

[2] Verifying information flow goals in Security-Enhanced Linux [J].

Guttman, Joshua ;

Herzog, Amy ;

Ramsdell, John ;

Skorupka, Clement .

JOURNAL OF COMPUTER SECURITY, 2005, 13 (01) :115-134

[3] TRUSTED SYSTEM CONCEPTS [J].

ABRAMS, MD ;

JOYCE, MV .

COMPUTERS & SECURITY, 1995, 14 (01) :45-56

[4]

Design and verification of secure systems[J] . J. M. Rushby.ACM SIGOPS Operating Systems Review . 1981 (5)

[5]

Specification,Refinement,and Proof .2 J Woodcock,J Davies,Z Using. . 1996

[6]

A practical Alternative to Hierarchical Integrity Policies .2 W E Boebert,R Y Kain. TheNational Computer Security Conf . 1985

← 1 →