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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社