一种改进的无干扰模型分析和验证方法

Improved Analysis and Verification Approach for Noninterference Model

安全模型是网络空间安全研究的基础和起点.以机密性为例,历史上研究人员率先提出了BLP(Bell-LaPudula)模型,BLP从思想上精确把握了机密性“不上读,不下写”的本质,但在设计上存在不足,这导致BLP自身存在隐通道等缺陷.为此,研究人员基于信息流提出了无干扰的思想.无干扰通过研究“攻击者在系统内信息流动的过程中,能否通过观察系统所到达的不同状态之间的差异以非法获取机密信息”,来分析系统的安全性.目前,无干扰模型已成为事实上机密性领域的基础模型.当前无干扰分析主流(甚至唯一)的方法是Rushby所提出的视图分区(view-partition)方法.但是,视图分区方法的3条规则难以转化为可机械计算的递归形式,且缺少直观的数学解释,这使得无干扰模型的属性验证和实践应用长久以来一直难以取得进展.近年来,随着无干扰模型在可信计算、云计算和机密计算等新型计算领域获得广泛应用,上述问题进一步凸显.针对无干扰模型的分析和验证问题,提出了一种称为伙伴状态机(buddy state machines)的无干扰分析改进方法.该方法通过分析真实(real)和理想(ideal)两个状态机在同步运行过程中的状态等价关系,实现对无干扰属性的分析和验证.基于伙伴状态机,建立了一种新的无干扰模型形式分析框架;给出了可靠和完备的无干扰成立条件;提出了O(|S|^(2))时间复杂度的无干扰属性验证算法,为无干扰模型的分析、验证和应用提供了一种可参考的改进方法.

The security model serves as the cornerstone and starting point of cybersecurity research.Taking confidentiality as an example,researchers historically introduced the Bell-LaPadula(BLP)model,which precisely captured the essence of confidentiality as″no read up,no write down″.However,design flaws in BLP led to inherent defects such as covert channels.Consequently,researchers introduced the concept of noninterference based on information flow.Noninterference scrutinizes the security of a system by examining whether an attacker can illicitly obtain confidential information by discerning differences between various states reached by the system during information flow within the system.Presently,the noninterference model has solidified its position as the fundamental model in the realm of confidentiality.The prevailing(and often sole)method for noninterference analysis is currently Rushby′s View-Partition approach.Nonetheless,the three rules of the View-Partition method prove challenging to transform into computable recursive forms and lack a clear mathematical interpretation.This complexity has impeded progress in verifying properties and practical applications of the noninterference model for an extended period.In recent years,with the widespread adoption of the noninterference model in emerging computing domains such as trusted computing,cloud computing,and confidential computing,the aforementioned challenges have been further accentuated.To address the analysis and verification challenges of the noninterference model,a novel noninterference analysis method known as″Buddy State Machines″has been proposed.This method enables the analysis and verification of noninterference properties by assessing the state equivalence relationship between two state machines,i.e.,real and ideal ones,during synchronous operation.Building upon″Buddy State Machines″,a new framework for formally analyzing noninterference models has been established.It provides reliable and comprehensive conditions for noninterference and introduces a O(|S|^(2))time-complexity verification algorithm for noninterference properties.This innovative approach offers a valuable reference point for analyzing,verifying,and applying noninterference models.