CAJ | 학술논문

动态调整安全级是目前提高强制访问控制模型可用性的主要途径,它大致包括两类方法.其中,安全级范围方法对主体权限最小化的支持不够,而污点传播方法存在已知隐蔽通道.提出了保护操作系统保密性和完整性的广义污点传播模型(generalized taint propagation model,简称GTPM),它继承了污点传播在最小权限方面的特点,拓展了污点传播语义,以试图关闭已知隐蔽通道,引入了主体的降密和去污能力以应对污点积累；还利用通信顺序进程(CSP)语言描述了模型的规格,以明确基于GTPM的操作系统的信息流控制行为的形式化语义；基于CSP的进程等价验证模型定义了可降密无干扰,并借助FDR工具证明形式化构建的抽象GTPM系统具有可降密无干扰安全性质.最后,通过一个示例分析了模型的可用性提升.
동태조정안전급시목전제고강제방문공제모형가용성적주요도경,타대치포괄량류방법.기중,안전급범위방법대주체권한최소화적지지불구,이오점전파방법존재이지은폐통도.제출료보호조작계통보밀성화완정성적엄의오점전파모형(generalized taint propagation model,간칭GTPM),타계승료오점전파재최소권한방면적특점,탁전료오점전파어의,이시도관폐이지은폐통도,인입료주체적강밀화거오능력이응대오점적루；환이용통신순서진정(CSP)어언묘술료모형적규격,이명학기우GTPM적조작계통적신식류공제행위적형식화어의；기우CSP적진정등개험증모형정의료가강밀무간우,병차조FDR공구증명형식화구건적추상GTPM계통구유가강밀무간우안전성질.최후,통과일개시례분석료모형적가용성제승.