标准当前状态不透明性与强当前状态不透明性的归约

Reduction Between Standards and Strong Current-State Opacity

不透明性是信息流安全中的一种重要属性,它表征了系统对入侵者保密的能力.在离散事件系统中,标准当前状态不透明性刻画的是入侵者无法根据当前的输出观测序列确定系统是否达到秘密状态.强当前状态不透明性刻画的是对每一个到达秘密状态的运行,存在一个观测等价的非秘密运行与之对应.显然,强当前状态不透明性比标准当前状态不透明性具有更强的隐秘性.针对标准当前状态不透明性与强当前状态不透明性之间的归约问题,提出一种新的转换方法,即在原系统基础上添加一些新的状态及相关跃迁,分别构造两个新的系统,证明了原系统是标准当前状态不透明的(强当前状态不透明的),当且仅当新系统是强当前状态不透明的(标准当前状态不透明的).

Opacity,as an important property in information-flow security,characterizes the ability of a system to keep some secret information from an intruder.In discrete-event systems,standard current-state opacity characterizes that an intruder cannot determine for sure whether a system has reached a secret state based on the current sequence of output observations.Strong current-state opacity describes that for each run of a system ending at secret state,there exists a non-secret run whose observation is the same as that of the previous run.Obviously,it has higher-level confidentiality than the standard currentstate opacity.For the reduction problem between standard and strong current-state opacity,a new conversion method is proposed in this article,that is,two new systems are constructed respectively based on the original system by adding some new states and related transitions.It is proved that the original system is standard current-state opacity(resp.,strong current-state opacity)if and only if the new system is strong current-state opacity(resp.,standard current-state opacity).