理论计算机科学电子笔记180（2007）35-53www.elsevier.com/locate/entcs安全时间自动机1纪尧姆·加尔代 约翰·穆林斯 奥利维尔·H Roux102∗ IRCCyN/CNRSB P 921011rueeddelaNoée44321NantesCedex3France。EschericheE'colePolytechniquedeMontr'ealP.O. Box 6079，Station Centre-ville，Montreal（Quebec），Canada，H3C 3A7.摘要本文首次研究了用时间自动机的一种扩展模型建立的多级安全稠密时间离散事件系统的无干扰控制器的综合问题。我们首先讨论了密集实时系统的非干扰概念，该概念改进了文献中存在的概念，并研究了密集时间属性的验证问题所提出的可判定性问题。然后，我们证明了这些定时非干扰属性的定时控制器的合成问题的可判定性，提供了这样一个象征性的方法来合成一个控制器，确保他们。保留字：无干扰，控制综合，验证，可判定性，时间自动机。1介绍不干涉。 如今的计算环境允许用户使用从不同站点发送或获取的程序来实现他们的目标，无论是在私人还是在组织中。这样的程序可以作为代码运行以进行简单的计算任务，或者作为交互式通信程序运行以进行IO操作或通信。有时，它们处理秘密信息，例如用户的私人数据或组织的分类数据。类似的情况可能发生在多个用户共享公共计算资源的任何计算环境在这种情况下，一个基本的关注点是确保程序不会将敏感数据泄露给第三方，无论是恶意的还是无意的。这是安全问题的关键方面之一，通常被称为保密。 的信息1由NSERC赠款（加拿大政府）和ACI赠款（法国政府）支持的工作实时开放系统2CurrentlyatheE′ colePolytechniquedd eMontr′eal1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.04636G. Gardey等人/理论计算机科学电子笔记180（2007）35当程序中的信息流是安全的（即高级信息永远不会流入低级通道）时，流分析通过澄清条件来解决这一问题。这些条件称为非干扰属性，捕获高级动作和低级行为之间的任何因果依赖关系。它们的特性已经迅速地超出了系统验证界在过去25年中所实现的系统特性的安全性分类的范围。此外，近年来，信息流安全的验证已成为计算机科学研究的一个新兴领域，并在它在分析密码协议中的应用，其中已经提出了许多统一和简洁的信息流安全属性（例如，机密性、认证、不可否认性或匿名性）的不干扰性的特征。时间非干扰验证问题。实时系统验证的重要性日益增加，自然导致了下一个问题，即在非定时设置中开发的证明技术是否可以推广到定时系统，以便能够捕获除了逻辑信息流之外的时间相关干扰，例如定时隐蔽信道[8]。文[9]中研究的信息流的一些基于非定时互模拟的非干扰性质在文[17]中被重新表述为离散时间设置。在文献[5]中，利用时间自动机在稠密时间环境中引入了一些基于状态和基于迹的非干涉性质。定时无干扰控制问题。安全验证的一个自然概括是安全控制，这在自动化安全系统设计的背景下很有用。这里的问题不是验证系统是否满足给定的安全策略，而是以满足安全策略的方式控制系统。在这个框架中，一个系统，通常被称为工厂，通常被视为开放的，并与“敌对”的环境相互作用。然后，问题是合成一个控制器，使得无论环境如何表现，受控计划都满足给定的安全策略。控制器只能控制工厂的一部分动作，称为可控动作，而不可控动作代表环境动作。在实时框架中，使用离散或连续时钟。最近的研究提出了时间自动机的符号控制综合算法[14，2，7]。文件的组织和贡献。在本文中，我们通过在[9]中研究的信息流的一些非定时互模拟的非干扰性质和引入定时非干扰的基于协模拟的概念（第3节），完成了[ 5 ]中开始的非干扰的稠密时间图。此外，我们调查的可判定性问题所提出的问题，他们的验证作为实时要求的有限状态系统。然后，我们集中（第4节）基于状态和基于协同仿真的定时无干扰性质，并证明了其定时控制器综合问题的可判定性。本文的主要结果是一种符号化的方法来综合一个G. Gardey等人/理论计算机科学电子笔记180（2007）353700212000012控制器确保这些属性。最后，给出了一个例子（第5节）来说明这种方法的时间无干扰性能的协同模拟为基础。在下一节中，我们将简要介绍本文中使用的时间自动机的概念。2时间自动机在本节中，我们回顾时间自动机的定义（2.2节）和它们的一些构造器。但是首先，在2.1节中给出了一些关于时间变迁系统及其行为的描述，以表达时间自动机的语义。2.1时间转换系统定义2.1[时间转移系统]动作集上的时间转移系统（TTS）−→R≥0）×Q是一个函数。 对于（q，e，qJ）∈−→，我们可以得到e q − − e →q j。定义2.2[时间相似]设S1=（Q1，Q1，N，−→1）且S2=（Q2，Q2，，−→2）是两个TTS，±是Q1×Q2上的二元关系。对于（s，SJ）∈ ±，我们记为s±sj。±是S1乘S2的强（定时）模拟关系，如果：1）如果s1∈Q1，则s2∈Q2s.t。s1±s2;2）ifs1−→d1sJ 其中d∈R≥0，s1±s20 01thens2−→d2sJforrsomesJ，andndsJ±sJ;3）ifs1−→a1sJ其中a∈n且s1±s2a2 2121thens2−→2sJandsJ±sJ.TTSS2强模拟S1，如果存在强（定时）模拟关系：S1，S2。在这种情况下，我们记为S1±S2当S1与S2之间存在强模拟关系±，S2与S1之间也存在强模拟关系±J时，我们就存在强（定时）协同模拟关系。当±J=±−1，我们有一个强的（定时的）互模拟关系，我们写S1<$S2。设S=（Q，Q0，ε，−→）为TTS.我们现在使用ε-抽象TTSSε =（Q，Qε，ε，−→ε），通过：• q−→d当d≥R≥0时，εqJqJ，其中Untimed（ρ）=ε，并且持续时间（ρ）=d，• q−→aεqJwitha∈itheeisarunρ=q−→qJ，其中Untimed（ρ）=a，并且持续时间（ρ）= 0，• Qε={q|<$qJ∈Q0|qJ−→q和持续时间（ρ）= 0<$Untimed（ρ）=ε}。定义2.3[弱时间模拟]设S1=（Q1，Q1，ε，−→1）和S2=（Q2，Q2，ε，−→2）是两个TTS，±是Q1×Q2上的二元关系。±是S1乘S2的弱（定时）模拟关系，如果它是强定时模拟Sε与Sε的关系TTSS2弱模拟S1，如果存在弱（定时）S1与S2模拟关系。在这种情况下，我们记为S1±WS238G. Gardey等人/理论计算机科学电子笔记180（2007）35当S1与S2存在弱模拟关系±，S2与S1也存在弱模拟关系±J时，则存在弱（定时）协同模拟关系.当±J=±−1时，我们有一个弱（定时）互模拟关系，我们写S1<$WS2。注2.4注：如果S1±S2，则S1±WS2，如果S1±WS2，则L（S1）<$L（S2）。特别是，弱时间互模拟细化了弱时间协模拟，它细化了时间语言（或跟踪）等价。最后，我们引入了由一组状态诱导的TTS的定义，它非正式地将TTS限制在给定的一组状态。定义2.5[由一组状态诱导的TTS]设S=（Q，Q0，N，→）a TTS且Y<$Q。由Y在S上诱导 的TTS 是TTSSY = （Y ， Q0<$Y ，n ， →i ） ， 其中→i 定义为 ：（q，·，qJ）∈→i惠q∈ Y<$qJ∈Y<$（q，·，qJ）∈→2.2时间自动机时间自动机（TA）是由Dill [3]提出的，并得到了广泛的研究。该模型是具有（密集时间）时钟的有限自动机的扩展，使人们能够指定实时系统。定义2.6[时间自动机]时间自动机A是一个元组（L，l0，X，εε，E，Inv），其中：L是位置的有限集合;l0∈L是初始位置;X是正实值时钟的有限集合; ε = εε{}是动作的有限集合，ε是无声动作;EεL× C（X）×ε× 2X×L是边的有限集合，e=<$l，γ，a，R，lJ <$∈E表示从位置l到位置lJ的边，带有保护γ，标签a和重置集R<$X;Inv∈ C（X）L为任何位置分配一个不变量我们将不变量限制为形式x≤r的项的合取对于x∈X和r∈N且≤∈ {<，≤}.定义2.7[时间自动机的语义]时间自动机A=（L，l0，X，ε，E，Inv）的语义是一个时间转移系统SA=（Q，q0，ε，→），其中Q=L×（R≥0）X，q0=（l0，0）是初始状态，→定义为：⎧⎪⎨γ(v)=tt,（l，v）−→a （lJ，vJ）i ∈f（l，γ，a，R，lJ）∈Es.vJ=v[R <$→0]⎪J JtJJ.l=lJvJ=v+t，Inv（l）（v）=tt（l，v）−→（l，v）it0≤tJ≤t，Inv（l）（v+tJ）=tt对于A的状态集，我们记为QA。A的游程ρ是SA的初始游程。A接受的时间语言是L（A）=L（SA）。状态空间抽象TA的分析基于对有限图（区域图）的探索，其中节点是符号状态，即时钟值的等价类。通过分析初始区域的后继者（前向）来建立状态空间⎩G. Gardey等人/理论计算机科学电子笔记180（2007）3539分析[3]。实际上，使用区域的有效前向（和后向）算法不编码区域，而是区域，区域的有限凸联合，因为区域是组合爆炸的子集，并且很难操作。构造函数最后，让我们在时间自动机上引入一些构造器，以表示并发时间系统中的时间信息流。为了将系统描述为时间自动机的并行组合，我们使用了基于同步器的类A`laArnold-Nivat。设X={x1，···，xn}是一组时钟，A1，. . .，An是n阶时间自动机，其中 Ai= （ Ni ， li ， 0，X ，n ， Ei ， Invi ）.一个同步函数f是一个从（<$$>{·}）n<$→n的部分函数，其中·是一个特殊的符号，当一个自动机不参与全局系统的一个步骤时使用。我们用（A 1）表示|......这是什么？|An)fthe parallel composition of the Ai’s w.r.t. F. A的配置（1|......这是什么？|An) farepairs (l, v) with l = (l1,...，l n）∈N1×. 其中vi是时钟xi∈X的值。定义2.8[隐藏时间自动机]设A=（L，10，X，ε，E，Inv）为TA，且Γ为零。我们定义了一个Γ-隐藏TAA/Γ =（L，l0，X，（λ\ Γ）ε，E/Γ，Inv）（具有隐藏的Γ-转移）：<$l，γ，a，R，lJ <$∈E/Γi <$（1）a∈（λ\ Γ）ε和<$l，γ，a，R，lJ <$∈E或（2）a=n，且存在一个跃迁<$l，γ，b，R，lJ <$∈E，其中b∈Γ.标记为Γ的跃迁被替换为π跃迁，模拟信息的隐藏定义2.9[限制时间自动机]设A=（L，10，X，ε，E，Inv）为TA，且Γ为 π.我们定义了Γ-限制TAA\Γ =（L，10，X，（ε\ Γ）ε，E\Γ，Inv）（无Γ-跃迁）由<$l，γ，a，R，lJ<$∈E\Γ i <$a∈（<$\Γ）ε和<$l，γ，a，R，lJ<$∈ E.所有标记为Γ的转换都是从时间自动机上切下来的3安全定时自动机的定时无干扰在这一节中，我们重新制定了一些非干扰性质的信息流分析在密集时间离散事件系统以前研究的非定时[9]或离散时间[17]设置。因此，我们重新定义了[5]中引入的时间自动机的时间无干扰概念。强非确定性非干扰（SNNI）。SNNI的基本思想是系统的公共行为不受其私人行为的影响。我们定义这个属性关于3.3节中的不同行为概念：迹等价，弱协同模拟，弱互模拟和可达性等价。然后，我们将这些属性进行分类，并解决验证所提出的可判定性问题。在3.2节中给出了一个基于时间自动机的时间安全模型。40G. Gardey等人/理论计算机科学电子笔记180（2007）35x1≤3x1≤ 3s0H1S2L1L1S1S3图1.一、非干涉自动机与干涉时间自动机3.1一个介绍性的例子让我们以一个简单的例子开始，非正式地考虑信息流禁止是如何在相互作用的过渡系统中出现的。首先考虑图1左侧所示的过渡系统。假设我们为每个动作附加了保密级别，例如h1∈nipriv和l1∈nipub。直觉上，这意味着我们希望在h1的交互是秘密的，而在l1的交互可能被更广泛的公众所知：任何私人行为都可以在h1和l1交互，而公共行为只能在l1交互。没有一个公共观察者，即只允许观察（或反应）公共行为的观察者，有可能知道是否发生了与h1换句话说，任何公共观察者都不能推断出私人行为的因果关系。然而，在这个过渡系统上增加时间限制可能会将禁止的信息从私人层面引入公共层面。 作为一个例子，假设l1不能在2个时间单位之前从s 0发生，如图1右侧的时间自动机所示，那么任何公共观察者都有可能知道在l 1在2个时间单位之前从s 2发生的可能性中是否发生了与h 1的交互，即 在一些私人行为和一些公共观察之间存在着关联。3.2一种时间安全模型我们正在研究扩展的时间自动机，以模拟在不同信任级别上交互的计算实体的过程和计算定义3.1 [安全时间自动机]安全时间自动机是一种时间自动机，其可见动作集合被划分为2个集合：pub，priv。集合Rupriv表示可以附加保密性的高级用户的操作。低层是低层用户的操作集合。3.3定时信息流属性第3.1节中讨论的介绍性示例激发了以下定义。3.3.1定时强非确定非干扰s0x1≥1，h1S2x1≥2，l1L1S1S3G. Gardey等人/理论计算机科学电子笔记180（2007）3541Wx1≤3x1≤ 3x1≤ 3x1≤ 3图二. 定时CSNNI：干扰和非干扰TASNNI首先由Focardi [9]提出，作为并发系统无干扰的基于迹的推广。定义3.2 [Timed SNNI]设A，一个安全时间自动机。 A满意度定时强非确定性非干扰（定时SNNI）当且仅当L（A/Apriv）=L（A\Apriv）这个定义代表一个定时系统是定时的SNNI，如果一个低级别的用户只能观察到A\priv的定时单词。于是，观察系统的定时字的低级别用户不可能推断出高级别上的信息。3.3.2基于时间协同仿真的SNNI我们现在给出一个弱时间协同模拟非干扰定义。定义3.3 [基于时间协同仿真的SNNI]设A为安全时间自动机。A满足定时协同仿真非确定性非干扰（定时CSNNI）当且仅当SA/Spriv±W SA考虑图2右侧所示的时间自动机。很容易看出它是定时CSNNI。实际上，公共观察者在low1处交互的能力与hi1的出现不相关，而对于左手侧描绘的时间自动机存在这样的假设。对于1≤x1 2，在low1处的任何公共交互与hi1的出现相关。<下一个结果给出了定时协同仿真非确定性非干扰（定时CSNNI）在协同仿真方面的表征，并将经常被用作Def的替代方案3.3在续集中定理3.4安全时间自动机A满足时间协同仿真非确定性非干扰（时间CSNNI）iSA/Apriv±WSA\Apriv（1）SA\npriv±JSA/npriv（2）证据 公式1由定义3.3得到：当A/Rupriv定义为在Rupriv上时，我们有SA/Rupriv±WSA优惠SA/优惠 ±WSA\endash 方程2直接得到l0x1≥1，hi1L2x1≥2，低1低1L1低级2L4L3l0x1≥2，hi1L2x1≥2，低1低1L1低级2L4L342G. Gardey等人/理论计算机科学电子笔记180（2007）35WWWx1≤3x1≤ 3x1≤ 3x1≤ 3图三. 定时BSNNI：干扰和非干扰TA根据时间自动机的定义，隐藏和限制：对于任何TA，PRIVSA/Apriv.此外，±J不一定等于±-1。Q3.3.3基于时间互模拟的SNNI我们现在给出[9]中提出的强非确定性非干扰的基于互模拟的定义的定时版本实际上，[9]中提出的任何基于双模拟的信息流属性都可以以类似的方式进行重铸。图2和图3说明了CSNNI和BSNNI之间的差异定义3.5 [基于时间双模拟的SNNI]设A为安全时间自动机。满足基于定时互模拟的强非确定性非干扰（定时BSNNI），当且仅当S A/非专利北京赛车pk10图3表示干扰和非干扰时间自动机。左手边的一个是干扰，因为对于1≤x12，在low1处的任何低水平相互作用与hi1的发生相关。<3.3.4定时状态NNI在文献[5]中，作者提出了一种基于状态的时间非确定性非干扰的可判定概念.我们将其重新表述如下：定义3.6[Timed State NNI]设A是一个环上的安全时间自动机（环=环pub环priv）。A被称为定时状态非确定性非干扰（定时StNNI），当且仅当：QA/Q A/QA=QA\QA =QA\ Q A让我们注意到，由于QA\npriv\nQA，则定时StNNI等于QA/npriv\nQA\n优先级 即QAQA\priv.l0x1≥1，hi1L2x1≥2，低1低1L1L3l0x1≥2，hi1L2x1≥2，低1低1L1L3G. Gardey等人/理论计算机科学电子笔记180（2007）35433.4性质间的序关系定理3.7（定时非干扰分类）（3）第一次见面（4）第一次世界大战期间的军事行动证据公式3直接遵循备注2.4。关于严格蕴涵式4，我们在这里给出最后一个蕴涵式的一个反例。让我们考虑图2右侧所示的时间自动机。它是定时的CSSNI，然而不是定时的BSNNI，因为公共观察者在与low1交互之后现在具有检测与hi1的发生相关的死锁的能力。Q注3.8定时StNNI与此处给出的任何先前的非干扰定义之间没有排序。注3.9可以证明在[5]中引入的0迹无干扰等价于定时StNNI。3.5可判定性结果定理3.10（定时SNNI可判定性）定时SNNI是不可判定的。证据 我们证明了TA的普遍性问题可以归结为一个定时SNNI问题。设A是TA除以A。安全时间自动机Af是由A通过从A的初始局部性到新局部性lu添加标记为h/∈f的新边来构造的，并且对于每个动作a∈f，lu上标记为a的循环。我们设置pub=和priv={h}。很明显，A接受通用定时语言iAf是定时跟踪非干扰的。由于普遍性问题对于TA是不可判定的，因此时间SNNI问题也是不可判定的。Q定理3.11（定时BSNNI、CSNNI和StNNI可判定性）定时BSNNI、定时CSNNI和定时StNNI是可判定的。证据模拟[1]和互模拟[12]对于TA是可判定的，然后定时BSNNI和定时CSNNI是可判定的。由于可达性[3]对于TA是可判定的，定时StNNI也是可判定的。Q4定时无干扰可控性4.1介绍最近的研究提出了时间自动机的符号控制综合算法[20，14，2]。这种算法的目的是设计一个代理（也称为控制器或监督器），它限制初始系统的行为，以便由受控系统（也称为闭环系统）对感兴趣的属性进行建模。44G. Gardey等人/理论计算机科学电子笔记180（2007）3500uQCCu在这样的框架中，模型的动作集被经典地划分为可控和不可控的动作。控制器可以禁止、延迟或强制与系统动作相对应的可控动作，而不可控动作则不能限制环境动作。为了解决安全时间自动机的符号控制合成，这里的动作集或多或少是任意的，分为两个集合pub，priv。Rupub是不可控动作的集合，Rupriv是可控动作的集合。实际上，分区的选择将取决于什么被认为是入侵者我们在以下定义中形式化安全时间自动机的控制器：定义4.1 [控制器]设A =（L，10，X，N，E，Inv）是环N（N = N pub Npriv）上的安全赋时自动机。A的控制器C =（L C，l C，X，E C，InvC）是环A上的时间自动机，使得AC=（A|其中AC=（LC，（10，1C），X，λ，EC，Inv C），LC∈ L × LC，fc是控制同步函数，定义为fc（a，a）= a.控制器必须不限制以下意义上的不可控行为：设（1A，1C）AC的局部性，(i) A，γ，a，R，lJ∈ E s.t. a ∈ <$pub，有一条边<$（lA，lC），γ，a，R，（lJ，lJ）<$∈A ACEC，(ii) 如果$k（lA，lC），γ，a，R，（lJ，lJ）k∈EC且a∈kpriv则InvC（lA，lC）=InvC（lA）一个C第一个条件要求控制器不能防止不可控制边缘的触发。第二个条件背后的理由如下：我们不能强制触发一个不可控的转移，但另一方面，如果从一个状态，可以触发一个不可控的转移和一个可控的转移，那么只要不可控的转移不被触发，我们就可以通过时间约束强制触发可控的在时间框架中，控制问题解决方案的基石是可控制的前代算子表示为π（X）[14，2，19]。定义4.2[可控前置]设X_Q是安全时间自动机S的一组状态。X的可控前驱集合定义为：π（X）={q∈Q|（（qJ∈X，q−→δ−→aqJ）<$（<$δ∈IR≥0<$qJ∈X，q−→δqJ））如果au∈，则δu∈IR≥ 0低 ，qJ/∈X，q−δ→u−a→uJthen<$δcδuac∈<$priv，<$qJ∈Xq−δ→c−a→cqJ}非正式地说，q是Xi的可控前身• X的状态QJ可通过时间流逝和触发转变而到达G. Gardey等人/理论计算机科学电子笔记180（2007）3545• 对于偏离X的任何不可控过渡，控制器可以在较早的日期做出决定，以将系统约束在X中。4.2定时无干扰控制问题在本节中，我们定义并提出一些定时无干扰控制问题的解决方案。我们证明了定时StNNI和定时CSNNI的控制问题的可判定性，通过给出保证这两个属性的控制器的合成算法与时间自动机的安全控制问题一样，该算法给出的TTS解既可以解释为闭环系统，也可以解释为控制器。对于所有这些问题，控制器，禁止任何可控制的行动都是一种解决办法，但不一定是最宽容的。4.2.1定时StNNI控制问题首先，我们考虑时间状态无干扰控制问题。定义4.3[Timed-StNNI控制问题]设A是环上的安全赋时自动机（A = ApubApubpriv）。 A的StNNI控制器C（根据def. 4.1）是一个时间自动机在上，使得：Q（（A|C）fc）/Δpriv=Q（（A|C）fc）\nprivI.E. Q（A|C）fc=Q（（A|C）fc）\npriv让我们考虑A上的安全控制问题的解决方案，即找到满足Q（A）的约束rC|C）fcQA\npriv.支持4. 4如果C是C_（？）问题Q（A）的唯一解|C）fc=QA\npriv，C是Timed-StNNI的解，当且仅当：<$q∈Q（A|C）fcρ= τ1· 低1 ... τn · 低n∈S（A|C）fc，lowi电子邮箱使得qρ0−→q我的律师。 使fetycont的解决方案无法生成Q（A|C）fcQA\npriv.如果C是时间-StNNI的解，则Q（A|C）fcQ（（A|C）fc）\npriv.为Q（（A）的所有状态选择适当的参数|C）fc）\r\n\r\|C）fc.相反的情况很简单。Q这个特征给出了定时StNNI控制问题的决策过程：定理4.5（定时StNNI控制问题的可判定性）定时StNNI控制问题是可判定的，并且存在基于状态的控制器C，使得（A| C）fc是定时-StNNI。46G. Gardey等人/理论计算机科学电子笔记180（2007）3522证据其主要思想是使用一个经典的可控前导算法，扩展了一个步骤，该步骤确保计算的所有状态都是通过一系列低级动作（Ruppub）从初始状态可达的，即（（A）的状态|C）fc）\n优先级由于控制器可以限制系统的行为，所以该步骤确保计算的状态属于（A）的状态集合|C）fc）\n优先级为了更详细，让我们考虑A，R的区域图[3]。R_n有有限个区域，X_0=QA\npriv−−−−−−→i+1iiPost新闻发布i对于TA。设所得到的最大不动点记为X。X射线对A诱发的TTS时间为-StNNI。很简单，TTS验证了命题4.4的条件，Q4.2.2定时CSNNI控制问题在本节中，我们将证明定时CSNNI是可判定的，并且控制器是可计算的。直观地，我们提出的计算方法首先包括计算STAA的（可控以及不可控的）非干扰行为，即A的行为与由乘积（A）给出的\n priv| A\npriv）f同步于pub和free的操作关于反腐败的行动。可控行为保证不干扰然后从该结果中提取属性定义4.6[Timed-CSNNI控制问题]设A是一个安全赋时自动机，其上的安全赋时自动机为：A的CSSNI控制器C（根据定义4.1）是一个时间自动机，它在时间上是：S（A）|C）/优先级 ±W S（A）|C）\n私有现在让我们定义一个模拟关系，我们将用它来证明定时CSNNI问题是可判定的：定义4.7【模拟关系】设q =（l1，l2，v）∈Q（A| C）/λpriv和QJ=（LJ，LJ，VJ）∈Q（A| C）\npriv：q±qJ惠l2= lJ\npriv = vJ12 2由于S（A| C）\npriv±SA\npriv（控制器限制A的行为），我们还将注意到q±qj，对于任何q =（l1，l2，v）∈Q（A| C）\npriv和qJ=（lJ，vJ）∈QA\npriv，如果且仅当L2=LJ且V=VJ时。4.8.8 [A在（A）上展开|设A =（L，10，X，E，Inv）是环A = Lpub LpubLpiv上的TA.设AJ=（LJ，（LJ，LJ），X，n，EJ，InvJ）），其中LJ∈L×L，00a TA定义为AJ=（A| A\na∈pub.priv）f其中f（a，·）=a，如果a∈Npriv且f（a，a）=aTAAJJ =（LJJ，（l0，l0），X，n，EJJ，InvJJ），其中LJJ∈（L×L）<${bad}是A在AJi <$上的开折：G. Gardey等人/理论计算机科学电子笔记180（2007）3547privx≤3l0x≥2，低低L2(i) LJJ=LJ{bad}见图4。A和A\n优先级(ii) <$eJ=<$（li，lj），γJ，a，RJ，（lJ，lJ）<$∈EJ使得e= <$li，γ，a，R，lJ<$∈Ei j i我们有<$（li，lj），γ，a，R，（lJ，lJ）<$∈EJJ，I j(iii) εe= εl，γ，a，R，lJ ε ∈E使得a ∈εpub，ε（l，li）∈LJ且（lJ，lj）∈LJ我们有<$（l，li），γ，a，R，（lJ，lj）<$∈EJJ，(iv) εe=εl，γ，a，R，lJε ∈E使得a∈εpub，ε（l，li）∈LJ且（lJ，lj）/∈LJ我们有<$（l，li），γ，a，R，（bad）<$∈EJJ，(v) l=（li，lj）∈LJJ，Inv（l）=Inv（li）第二个和第五个要求放松了继承自一 个 私 人的第三和第四个要求增加了（A）所提出的公共行动的优势|A\npriv）f. 我们使用位置bad作为导致位置不在LJ中的边的目的地。注4.9 AJ很容易被视为Timed-CSNNI（见图5）。 通过将A与A同步\n ，我们隔离了A的所有非干扰行为。 然后我们将使用AJ来计算A的控制器。注4.10 A在AJ上的开折具有与AJ相同的离散结构，但扩展了A的行为。这个时间自动机将被用来隔离状态，并计算确保定时CSNNI属性的控制器定义4.11[A的状态JJ类似于A的状态\npriv 让我们考虑一下时间自动机AJJ和AJ的状态集：QAJ<$QAJJ。我们注意到SiSt（AJ）状态集合，其定义如下：SiSt（AJ）={q∈QAJ|iflow∈pubst. q−l−o→w∈EJJn∈QA\nprivst. q±qJ<$qJ−l−o→w∈EA\npriv}低x≤3l0x≥2，低L2x≥0，hx≥0，hix≥1，低L148G. Gardey等人/理论计算机科学电子笔记180（2007）35privprivpriv我ΣΣn1i pub011x≤3l0 l0x≥2，低l2l2低x≤3l0 l0x≥2，低l2l2低x≥0，hx≥2，低x≥0，嗨x≥1，低x≥0，hx≥2，低x≥0，嗨x≥1，低x≤3l1l0l1l2x≤3l1l0l1l2图五. AJ=（A|Af和AJ JSiSt（AJ）包含与A\n的状态弱相似的所有状态。也就是说，对于每个状态q =（l1，l2，v），使得在TTS中转换低是可能的由AJJ定义，则存在salouchatansition（l2，v）−l−o→w在TTS中，好吧。 考虑图5的例子，（l1，l0，x = 1）/∈ SiSt（AJ）， 因为（l0，x=1）−/l−o→w对于A\npriv。然后，找到控制器的方法的草图如下：(i) 计算AJ（这是定时CSSNI）和A的展开AJJ。(ii) 计算保持定时CSNNI性质的SiSt（A，j）的最大可控子集，即S（A，j）的状态|C）/npriv弱定时类似于一个状态S（A）|C）\n私有非正式地，在每次迭代中，计算一组可控安全状态，然后进行细化以匹配定时CSNNI属性。更详细地，让我们考虑算法1，其中R\npriv（X）={q∈X|格0∈Q0，τi∈（R≥0）n，<$（low）∈（<$）n，q−τ→1q−l−ow−→1qJ·· ·−l−ow−→nJ =qi，qi，qJ是只有elaps才能到达的状态的集合时间或低级别操作（countpub）的执行，以使所有中间状态保持不变JρJ在 X，Predpriv（十）={q∈Q|格∈X，<$ρ ∈<$privq−→q}是一个集合通过离散可控跃迁序列（CQPRIV）来描述XPred low（X）={q∈Q| <$qJ∈X q−l−o→wqJ，low∈{pub}，是离散X的前代，由一个不可控的过渡，PredYpriv（X）={q∈Y|q−h−i→1q−h−i→2q2.. . −h→nq nq，q1，. q n−1∈Y，q n∈Y∧ ∀i, hii∈Σpriv} is the set of通过一系列离散的可控转变，使所有π（X）是经典的可控前趋算子，Sim（X，Y）={q∈X| <$qJ∈Yq±qJ}是与Y相似的状态X的集合。算法1（Alg）注意ALG的以下定点算法：一曰： X0←SiSt（AJ）2：重复3： Xi+1 ←π（Xi）QG. Gardey等人/理论计算机科学电子笔记180（2007）3549ΣC4： Xi+1←Sim（Xi+1，R\npriv（Xi+1））5：for alll∈pubdo6：Y←Predpriv（Pred低（Xi+1））7：Z←PredXi+1（PredXi+1（Xi+1））∗priv8：XJ←Xi+1\（Z\Y）9：直到XJ=Xi低命题4.12如果Alg收敛，我们记X为解。X射线对SAJJ诱发的TTS为CSNNI。证据我们必须证明（SX<$）±（SX<$）。强生SX公司简介强生\n优先级JX轴AJJ\n设q∈QJJ 根据算法的第4行，这样，q±qJ。 Itheexistaf iringin g sequenc e q−h−i1−. .−。h−i→n s−l−ow−→1 rthenq±s（和dsoSXqJ±s）和|rJ∈QAJJ| rpriv使得r±rJ（第4行）. 我们也有与线5-8 ，s，r ∈ X. Sinces−l−ow−→1randqJ±s，qJ−l−ow−→1RJ. SoqJ−l−ow−→1RJ和r± RJ。因此，q和qJ满足弱定时模拟（通过将所有的hii替换i）。对于连续跃迁，证明也是类似的。Q命题4.13算法Alg终止。证据算法的收敛性由区域图R[3]保证：族序列（Xi）在有限域R上是单调的（Xi+1<$Xi）。Q作为命题4.12和4.13的推论，我们得到以下结果：定理4.14（Timed-CSNNI控制问题可判定性）Timed-CSNNI是可判定的，并且控制器是可计算的。实际上，由于同步函数（fc）是全的，所以由算法给出的TTS解既可以被解释为闭环系统，也可以被解释为系统的控制器（如TA上的安全控制问题）。完整的方法将在下一节中通过一个简单的示例进行5CSNNI控制问题-一个简单的例子让我们考虑图6的安全时间自动机A和A上的CSNNI控制问题。按照4.2.2节中提出的方法，我们计算AJ=（A| C）f. 一个J如图7所示。然后我们能够计算QAJ（表1）。给定QAJ和AJJ ，我们就可以计算出SiSt（AJ）（表2）。例如，在状态（l2，l0，x1= 1）下，对于AJ J，低1的触发是可能的，而对于AJ中的状态（l0，x1= 1）是不可能的。因此，这种状态必须被抛弃。控制器的目的将是防止这种状态可达。算法1的解是表3的状态集合，它可以转换成图9的时间自动机。ΣS∗50G. Gardey等人/理论计算机科学电子笔记180（2007）35地方时钟空间l0l 0x1≤3l1 l1x1≥2l4 l4x1≥2l2l 01≤x1≤ 3l3 l12 ≤x1l5 l11 ≤x1Table'1QA地方时钟空间l0l 0x1≤3l1 l1x1≥2l4 l4x1≥2l2l 02≤x1≤ 3l3 l11 ≤x1l5 l11 ≤x1坏∅表2SiSt（AJ）地方时钟空间l0l 0x1≤3l1 l1x1≥2l4 l4x1≥2l2l 02≤x1≤ 3l3 l12 ≤x1l5 l1∅坏∅表3控制算法1的解G. Gardey等人/理论计算机科学电子笔记180（2007）3551x1≤3x1≤ 3x1≥1，hi1l0 l0l2 l0x1≥2，低1x1≥2，低1l1l1低级2l4l4l3l1Hi2l5l1x1≤3x1≤ 3x1≥1，hi1l0 l0l2 l0x1≥2，低1低1l1l1低级2l4l4l3l1Hi2l5l1低3坏x1≤3x1≤ 3x1≥2，hi1l0 l0l2 l0x1≥2，低1低1l1l1低级2l4l4false，hi2l3l1l5l1x1≤3l0x1≥2，低1L1低级2L4见图6。控制示例：A和A\n优先级见图7。控制示例：AJ见图8。控制示例：AJJ见图9。 A上CSNNI控制问题的求解6结论和今后的工作在本文中，我们重新制定了SNNI在密集的时间设置的安全时间自动机的四个语义我们还首次讨论了定时CSNNI和定时StSNNI的控制综合问题，并在每种情况下提供了计算相关控制器的算法。在下文中，我们想强调四个具体方面，我们打算集中注意力，鉴于进一步的发展：定时BSNNI控制器，定时BNDC的验证和控制器综合，定时控制与部分x1≤3x1≤ 3x1≥1，hi1l0l2x1≥2，低1低1L1低级2L4L3Hi2L5低3L652G. Gardey等人/理论计算机科学电子笔记180（2007）35可观测性和时间不传递不干涉。定时BSNNI的控制综合技术。当然，要完成本文所描述的画面，还需要将控制综合扩展到定时BSNNI。定时BNDC的证明和控制综合技术 在[9]中，提出了基于双模拟的非演绎合成（BNDC）作为最自然的非定时信息流性质：如果对于任何私有层用户S，S的公共行为不受其与用户的交互的影响，则系统S满足BNDC。下一个问题是在我们的理论与相关的证明和控制综合技术的BNDC的密集时间重新制定的扩展。具有部分可观性的定时无干扰控制综合 取决于植物的性质，不可控的动作可以是可观察的（完全可观察性）或只有一个适当的子集（部分可观察性）可以由控制器观察。在定时设定下，部分可观性假设不仅适用于不可控行为，也适用于安全系统的时钟定时不传递无干扰控制综合。非干扰确保了信息流的缺失。但是，信息缺失流作为机密的描述很少是非常有趣的，因为许多实际应用程序都旨在保留机密，但仍然泄漏信息。另外，另一个重要的问题是不及物动词的稠密时间重构的扩展非干扰（INI）。这个术语指的是所需的信息流属性在降级器这样的系统中，信息在两个用户之间间接传播是合法的，但不是直接传播。在[18]中可以找到INI的一个聪明而完整的开发。它是在Moore和Mealy机器的基础上根据吹扫制定的。清除涉及到对系统的历史应用一个函数，直到删除所有那些不应该影响给定代理所看到的部分。INI的这种基于清除的定义也在[11]中根据Lin和Wonham [13]引入的离散事件系统（DES）背景下的可观测性进行了
我的内容管理
展开
