离散事件系统是由离散事件按照一定的运行规则相互作用而导致状态演化的一类动态系统,在军事国防、交通控制、计算机集成制造系统、电子通讯网络、机器人技术等领域都有成功应用[1-5]。近年来,离散事件系统的不透明性(opacity)研究引起了国内外众多学者的广泛关注。离散事件系统的不透明性在数字签名、信息认证、数据加密等信息安全机制中有着重要应用[6-9]。
文献[10-12]研究系统的不透明性验证,并提出了多种不同类型的不透明性。文献[10]使用监督控制的方法确保系统不透明性。文献[13]中K步不透明性首先被提出。K步不透明性用来验证入侵者能否确定系统在特定时刻之后的K个状态是否存在秘密状态。文献[14]提出,当K趋于无穷时,K步不透明度变为无穷步不透明度。文献[14]提出了一种改进的方法,使用了一种称为双向观测器的结构。文献[15]在随机离散事件系统中研究无穷步不透明性和K步不透明性,并提出随机无穷步不透明性和随机K步不透明性。
本文继续文献[14-15]的工作,将文献[14]提出的双向观测器引入至随机离散事件系统,提出一种基于双向观测器的随机无穷步不透明性和随机K步不透明性验证方法。首先对随机无穷步不透明性和随机K步不透明性进行形式化定义。然后运用文献[15]中的方法,构造
经典离散事件系统表示为式(1)的不确定自动机[1]
$ G=\left({X},{\varSigma },{\delta },{{X}}_{0}\right) $ | (1) |
式中:
而随机离散事件系统[2]是在经典离散事件系统的基础上附加一个概率结构,通常用一个随机有穷自动机
给定状态集
$ {\rm{UR}}\left({q}\right) =\left\{{x}\in {X}:\exists {{x}}'\in {q},\exists {s}\in {{\varSigma }}_{{{\rm{uo}}}}^{{*}},{{{\rm{s}}}}\text{.}{{{\rm{t}}}}\text{.}{\delta }\left({{x}}',{s}\right) ={x}\right\}$ | (2) |
用
$ {\rm{Next}}\left({q},{\sigma }\right) =\left\{\begin{array}{c}x\in X:\exists {{x}}'\in q,\\ \exists s\in {{\varSigma }}_{{{\rm{uo}}}}^{{*}},{{{\rm{s}}}}{.}{{{\rm{t}}}}{.}\delta \left({{x}}',{s}\right) =x\end{array}\right\} $ | (3) |
假设
$ {\widehat{{X}}}_{{G}}({\alpha })=\left\{\begin{array}{c}x\in X:\exists s\in L\left({G}\right) ,\exists {{x}}'\in q,\\ P\left({s}\right) =\alpha ,x=\delta \left({{x}}',{s}\right) \end{array}\right\}$ | (4) |
当执行
$ {\widehat{{X}}}_{{G}}({\beta }|{\alpha })=\left\{\begin{array}{c}x\in X:\exists st\in L\left({G}\right) ,\exists {{x}}'\in q,\\ P\left({s}\right) =\beta ,P\left({s}{t}\right) =\alpha ,x=\delta \left({{x}}',{s}\right) \end{array}\right\} $ | (5) |
直观上,
给定
$ \varTheta \left({\alpha }\right) =\left\{\begin{array}{c}\left({x},{{x}}'\right) \in X\times X:\exists s\in {{\varSigma }}^{{*}},\\ P\left({s}\right) =\alpha ,{{x}}'=\delta \left({x},{s}\right) \end{array}\right\}$ | (6) |
给定
$ {\overline{{r}}}_{1}\circ {\overline{{r}}}_{2}=\left\{\begin{array}{c}\left({{x}}_{1},{{x}}_{3}\right) \in X\times X:\exists {{x}}_{2}\in X,\\ \left({{x}}_{1},{{x}}_{2}\right) \in {\overline{{r}}}_{1},\left({{x}}_{2},{{x}}_{3}\right) \in {\overline{{r}}}_{2}\end{array}\right\} $ | (7) |
给定
$ \odot \left({r}\right) =\left\{\left({x},{{x}}'\right) \in {r}\times {X}:\exists {s}\in {{\varSigma }}_{{{\rm{uo}}}}^{{*}},{\delta }\left({x},{s}\right) ={{x}}'\right\} $ | (8) |
在实际应用中违反无穷步(或K步)不透明性的概率极其微小则可以忽略不计。定量评价无穷步(或K步)不透明性,还需考虑系统转移的概率。因此提出随机无穷步(或K步)不透明性定义。
定义1 给定一个随机离散事件系统
$ {{L}}_{{{\rm{IF}}}}^{{P}}=\{{s}\in {{L}}_{{{\rm{IF}}}}:\forall {t} < {s},{t}\notin {{L}}_{{{\rm{IF}}}}\} $ |
如果
直观上,
定义2 给定一个随机离散事件系统
$ {{L}}_{{{{KS}}}}^{{P}}=\{{s}\in {{L}}_{{{{KS}}}}:\forall {t} < {s},{t}\notin {{L}}_{{{{KS}}}}\} $ |
如果
直观上,
基于双向观测器
定理1 给定一个随机离散事件系统
$ {{L}}_{{{\rm{IFS}}}}=\{{s}\in {L}\left({G}\right) :\exists {t}\in {L}\left({{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})\right) , $ |
$ {P}\left({s}\right) ={{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\left({t}\right) \right) }_{{R}},{{f}}_{{{\rm{tw}}}}\left({{q}}_{{{\rm{tw}}},0},{t}\right) =\left({{q}}_{1},{{q}}_{2}\right) , $ |
$ {{{q}}_{1}\cap {{q}}_{2}\ne {\phi }\wedge {q}}_{1}\cap {{q}}_{2}\subseteq {{X}}_{{s}}\} $ |
随机离散事件系统
证明 (充分性)设
$ \begin{split} {\widehat{{X}}}_{\left|{{\tau }}_{1}\left({t}\right) \right|}({{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\left({t}\right) \right) }_{{R}})=&{{f}}_{{{\rm{obs}}}}({{x}}_{0},{{\tau }}_{1}\left({t}\right) )\cap {{f}}_{{{\rm{obs}}},{R}}({X},{{\tau }}_{2}\left({t}\right) )=\\ &{{q}}_{1}\cap {{q}}_{2}\subseteq {{X}}_{{s}} ^{[14]}。\end{split} $ |
(必要性)设
$ {{f}}_{{{\rm{tw}}}}\left({{q}}_{{{\rm{tw}}},0},{t}\right) =\left({{f}}_{{{\rm{obs}}}}({{x}}_{0},{{\tau }}_{1}\left({t}\right) ),{{f}}_{{{\rm{obs}}},{R}}({X},{{\tau }}_{2}\left({t}\right) )\right) $ |
从而
通过
$ {{L}}_{{{\rm{IFS}}}}=\{{s}\in {{L}}_{{{\rm{IF}}}}:\exists {\alpha }\le {p}\left({s}\right) {{\rm{s}}}.{{\rm{t}}}.{\widehat{{X}}}_{{G}}({\alpha }|{p}\left({s}\right) )\subseteq {{X}}_{{s}}\} $ |
对于任何
$ {{l}}_{1}({\rho })=\left\{{x}\in {X}:{\exists {x}}'\in {X}{{\rm{s}}}.{{\rm{t}}}.\left({x},{{x}}'\right) \in {\rho }\right\} $ | (9) |
作为
$ {{l}}_{1}({R})=\left\{{{l}}_{1}({\rho })\in {2}^{{X}}:{\rho }\in {{R}}\right\} $ | (10) |
确定是否
$ {{L}}_{{{\rm{IF}}}}^{{P}}=\{{s}\in {{L}}_{{{\rm{IFS}}}}:[{f}({{q}}_{0},{s}) \in {{Q}}_{{{\rm{IF}}}}]\wedge [\forall {t} < {s}:{f}({{q}}_{0},{s}) \notin {{Q}}_{{{\rm{IF}}}}\left]\right\} $ |
计算
${{p}}_{{M}}\left({{q}}'|{q}\right) =\left\{ {\begin{array}{*{20}{l}}\displaystyle\sum\nolimits _{{\sigma }\in {\varSigma }:{f}\left({q},{\sigma }\right) ={{q}}'}{p}\left({\sigma }|{x}\right) ,&q\notin {{Q}}_{{{\rm{IF}}}}\\ 1,&q\in {{Q}}_{{{\rm{IF}}}}\\ 0,&其他\end{array}} \right. $ | (11) |
$ P\left({q}\right) =\left\{ {\begin{array}{*{20}{l}}\displaystyle\sum\limits _{{{q}}'\in \overline{{Q}}}{{p}}_{{M}}\left({{q}}'|{q}\right) \mathbb{P}\left({{q}}'\right) ,& q\notin {{Q}}_{{{\rm{IF}}}}\\ 1,& q\in {{Q}}_{{{\rm{IF}}}}\end{array}} \right.$ | (12) |
定理2[15] 给定一个随机离散事件系统
基于双向观测器
定理3 给定一个随机离散事件系统
$ {{L}}_{{{{KSS}}}}=\{{s}\in {L}\left({G}\right) :\exists {t}\in {L}\left({{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})\right) $ |
$ {{\rm{s}}}.{{\rm{t}}}.{P}\left({s}\right) ={{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\left({t}\right) \right) }_{{R}},{{f}}_{{{\rm{tw}}}}\left({{q}}_{{{\rm{tw}}},0},{t}\right) =\left({{q}}_{1},{{q}}_{2}\right) $ |
$ {|{\tau }}_{2}\left({t}\right) |\le {K},{{q}}_{1}\cap {{q}}_{2}\ne {\phi }\wedge {{q}}_{1}\cap {{q}}_{2}\subseteq {{X}}_{{s}}\} $ |
如果随机离散事件系统
证明 (充分性)设
$ {s}\in {L}\left({G}\right) ,\exists {t}\in {L}\left({{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})\right) :$ |
$ {P}\left({s}\right) ={{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\right({t}\left) \right) }_{{R}},{|{\tau }}_{2}\left({t}\right) |\le {K} $ |
另有
$ {{q}}_{1}\cap {{q}}_{2}={\widehat{{X}}}_{\left|{{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\right({t}\left) \right) }_{{R}}\right|-\left|{\left({{\tau }}_{2}\right({t}\left) \right) }_{{R}}\right|}({{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\left({t}\right) \right) }_{{R}})\subseteq {{X}}_{{s}} $ |
则
(必要性)设
$ {{q}}_{1}\cap {{q}}_{2}={{f}}_{{{\rm{obs}}}}({{x}}_{0},{{s}}_{1})\cap {{f}}_{{{\rm{obs}}},{R}}({X},{\left({{s}}_{2}\right) }_{{R}}) ={\widehat{{X}}}_{\left|{{s}}_{1}{{s}}_{2}\right|-\left|{{s}}_{2}\right|}({{s}}_{1}{{s}}_{2})\subseteq {{X}}_{{s}} $ |
且
记
$ {{L}}_{{{{KSS}}}}=\{{s}\in {{L}}_{{{{KS}}}}:\exists {\alpha }\le {p}\left({s}\right) $ |
$ {{\rm{s}}}.{{\rm{t}}}.\left|{p}\left({s}\right) /{\alpha }\right|\le {K}{ },{\widehat{{X}}}_{{G}}({\alpha }|{p}\left({s}\right) )\subseteq {{X}}_{{s}}\} $ |
为了确定是否
$ \begin{split} {{Q}}_{{{{KS}}}}=&\left\{\right({x},{r},{{\rho }}_{1},\cdots,{{\rho }}_{{K}}) \in {{Q}}_{{K}}:[{{\rm{UR}}}\left({x}\right) \subseteq {{X}}_{{s}}]\vee \\ &[\exists {i}=1,\cdots ,{K}:{\phi }\ne {{l}}_{1}\left({{\rho }}_{{i}}\right) \subseteq {{X}}_{{s}}\left]\right\} 。\end{split} $ |
记:
$ {{L}}_{{{{KS}}}}^{{P}} = \left\{{s} \in {{L}}_{{{{KSS}}}}:\left[{{f}}_{{K}}\left({{q}}_{0},{s}\right) \in {{Q}}_{{{{KS}}}}\right] \wedge \left[\forall {t} < {s}:{{f}}_{{K}}\left({{q}}_{0},{s}\right) \notin {{Q}}_{{{{KS}}}}\right]\right\} $ |
计算
${{p}}_{{{M}}_{{K}}}\left({{q}}'|{q}\right) =\left\{ {\begin{array}{*{20}{l}}\displaystyle\sum\limits _{{\sigma }\in {\varSigma }:{{f}}_{{K}}\left({q},{\sigma }\right) ={{q}}'}{p}\left({\sigma }|{x}\right) ,&{q}\notin {{Q}}_{{{{KS}}}}\\ 1,&q={{q}}'\in {{Q}}_{{{{KS}}}}\\ 0,&其他\end{array}} \right.$ | (13) |
定理4[15] 给定一个随机离散事件系统
在给定阈值
算法1 输入:
输出:系统
系统
系统
系统
步骤:(1) 求得
(2) 求
(3) 求
(4) 分别构建
(5) 计算
(6) 如果
如果
如果
如果
算法复杂度分析:对于随机无穷步不透明性的验证,首先构造验证器
例1 在访问服务器时,用户权限存在两种:超级用户权限和普通用户权限。用户在登入服务器后,首先要获取相应的权限。拥有超级用户权限或者普通账户权限的账号都可以访问服务器。服务器的账户系统非常严格,普通用户在做系统级别的更改时会受到用户权限的限制。用户登录服务器默认拥有普通用户权限。拥有超级用户权限的用户可以以普通用户的身份访问服务器,还可以执行普通用户无法进行的系统操作。同时,拥有超级用户权限的用户还可以授权其他用户为超级用户。超级用户权限为系统最高权限,不受安全系统限制。为防止入侵者获得超级用户权限,将“超级用户权限登入”看作是一个秘密状态。对于一个已设计的服务器系统,能否通过比较随机离散事件系统具有随机K步不透明性的阈值
给定事件a为用户获取访问系统权限,事件b为超级用户权限转换成普通用户权限,事件c为访问系统。考虑如图1(a)所示用户访问服务器系统,其中状态1表示未登录用户,状态2表示用户以普通用户权限登入,状态3表示用户以超级用户权限登入,状态4为用户访问服务器系统。其中状态3被表示为秘密状态。当入侵者在入侵系统后可以确定用户是以超级用户权限登入(秘密状态)时,表明系统不具备随机
![]() |
图 1 系统
|
步骤1:求
![]() |
图 2 |
步骤2:求得
步骤3:求
![]() |
图 3 一个随机
|
步骤4:构建
步骤5:计算
$ \left\{ \begin{array}{l} {\boldsymbol{P}}\left({{M}}_{1}\right) =0.9 {\boldsymbol{P}}\left({{M}}_{2}\right) +0.1 {\boldsymbol{P}}\left({{M}}_{3}\right) \\ {\boldsymbol{P}}\left({{M}}_{2}\right) ={\boldsymbol{P}}\left({{M}}_{4}\right) \\ {\boldsymbol{P}}\left({{M}}_{3}\right) =0.1{\boldsymbol{P}}\left({{M}}_{5}\right) +0.9{\boldsymbol{P}}\left({{M}}_{4}\right) \end{array} \right.$ |
由于
本文研究了基于状态的可观映射下随机离散事件系统是否具有随机无穷步不透明性和随机
[1] |
SAMPATH M, SENGUPTA R, LAFORTUNE S, et al. Diagnosability of discrete-event systems[J].
IEEE Transactions on Automatic Control, 1995, 40(9): 1555-1575.
DOI: 10.1109/9.412626. |
[2] |
THORSLEY D, TENEKETZIS D. Diagnosability of stochastic discrete-event systems[J].
IEEE Transactions on Automatic Control, 2005, 50(4): 476-492.
DOI: 10.1109/TAC.2005.844722. |
[3] |
QIU W, KUMAR R. Decentralized failure diagnosis of discrete event systems[J].
IEEE Transaction on Systems, Man, and Cybernetics-part A:Systems and Humans, 2006, 36(2): 384-395.
DOI: 10.1109/TSMCA.2005.853503. |
[4] |
LIU F C, QIU D. Safe diagnosability of stochastic discrete event systems[J].
IEEE Transaction on Automatic Control, 2008, 53(5): 1291-1296.
DOI: 10.1109/TAC.2008.921035. |
[5] |
ZAYTOON J, LAFORTUNE S. Overview of fault diagnosis methods for discrete event systems[J].
Annual Reviews in Control, 2013, 37(2): 308-320.
DOI: 10.1016/j.arcontrol.2013.09.009. |
[6] |
JACOB R, LESAGE J, FAURE J. Overview of discrete event systems opacity: models, validation, and quantification[J].
Annual Reviews in Control, 2015, 48(7): 174-181.
|
[7] |
ZHANG B, SHU S, LIN F. Maximum information release while ensuring opacity in discrete Event systems[J].
IEEE Transactions on Automation Science & Engineering, 2015, 12(3): 1067-1079.
|
[8] |
BÉRARD B, CHATTERJEE K, SZNAJDER N. Probabilistic opacity for Markov decision processes[J].
Information Processing Letters, 2015, 115(1): 52-59.
DOI: 10.1016/j.ipl.2014.09.001. |
[9] |
HADJICOSTIS C N, KEROGLOU C. Opacity formulations and verification in discrete event systems[C]// Proceedings of the 2014 IEEE Emerging Technology and Factory Automation (ETFA) , Barcelona: IEEE, 2014, 1-12.
|
[10] |
ANOOSHIRAVAN S A, HADJICOSTIS C N. Verification of initial state opacity in security applications of discrete event systems[J].
Information Sciences, 2013, 246(14): 115-132.
|
[11] |
DUBREIL J, DARONDEAU P, MARCHAND H. Opacity enforcing control synthesis[C]// 2008 9th International Workshop on Discrete Event Systems, Gothenburg: IEEE, 2008, 28-35.
|
[12] |
SABOORI A, HADJICOSTIS C N. Opacity-enforcing supervisory strategies for secure discrete event systems[C]// 2008 47th IEEE Conference on Decision and Control, Cancun: IEEE, 2008, 889-894.
|
[13] |
SABOORI A, HADJICOSTIS C N. Verification of K-step opacity and analysis of its complexity[C]// Proceedings of the 48h IEEE Conference on Decision and Control (CDC) held jointly with 2009 28th Chinese Control Conference, Shanghai: IEEE, 2009, 205-210.
|
[14] |
YIN X, LAFORTUNE S. A new approach for the verification of infinite-step and K-step opacity using two-way observers
[J].
Automatica, 2017, 80: 162-171.
DOI: 10.1016/j.automatica.2017.02.037. |
[15] |
XIANG L, LI Z, WANG W, et al. Infinite-step opacity and K-step opacity of stochastic discrete-event systems
[J].
Automatica, 2019, 99: 276-274.
|