安全自动机控制器的建模和综合

理论计算机科学电子笔记179（2007）31-46www.elsevier.com/locate/entcs从安全自动机的建模到综合1法比奥·马丁内尔2Istituto di Informatica e Telematica - C.N.R.，意大利比萨Ilaria Matteucci3Istituto di Informatica e Telematica - C.N.R.，意大利比萨DipartimetodiSien zMatem ichediediSien e di Si e n ed i Si Si e n e d i Si e n e d i Si Si e n e d i Si Si e n e d i SiSi e n e d i Sis摘要我们定义了一组进程代数算子，我们称之为控制器算子，能够模仿Schneider在[17]和Ligatti等人在[3]中引入的安全自动机的行为。安全自动机是一种强制执行安全策略的机制，这些策略指定了可接受的程序执行。在这里，我们给出了四个控制器的语义，这些控制器通过监视系统中可能的不可信组件来执行某些安全策略。此外，利用时间逻辑的满意度结果，我们展示了如何自动构建这些控制器为给定的安全策略。关键词：部分模型检查，安全性能，控制器的自动综合1概述最近，几篇论文讨论了强制执行安全策略的机制的正式定义（例如，参见[2，3，6，10，11，17]）。安全策略指定可接受的程序执行。安全策略的例子有信息流、可用性、访问控制等（见[17]）。本文的重点是研究Schneider在[17]中引入的执行机制和 Ligatti等人在[3，6]中开发的安全自动机安全自动机监视某些系统的执行步骤，这里称为目标，1部分得到CNR项目“动态联盟的可信电子服务”和欧盟资助项目“面向服务的覆盖计算机软件工程”（SENSORIA）以及欧盟资助的project “Secure Software and Services for Mobile Systems2电子邮件：Fabio. iit.cnr.it3电子邮件：Ilaria. iit.cnr.it1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.08.02932F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）31q∈QJ并且如果目标将要违反正在实施的安全策略，则终止目标在这里，我们通过进程代数运算符（参见[12]）对这些安全自动机进行建模，作为控制器运算符。我们提出了一个合乎逻辑的方法来监控系统的问题，以享受安全政策。事实上，我们用一个时态逻辑公式来表示安全策略，并利用进程代数和时态逻辑的理论来综合控制器操作符。在[17]中，Schneider将安全自动机定义为三元组（Q，q0，δ），其中Q是一组状态，q0是初始状态，而Act是安全相关动作的集合，δ：Act× Q →2Q是转移函数。安全自动机处理一系列动作a1a2. 一个接一个对于每个操作，当前全局状态QJ是通过最初从{q0}开始计算的。 当读取每个ai时，自动机在δ（a，q）中改变QJ 如果自动机能完成我在给定的动作上，即QJ不为空，则允许目标执行该动作。行动上自动机的状态根据转换规则而改变。否则，目标执行被终止。可以以这种方式强制执行的安全属性对应于安全属性（根据[17]，属性是安全属性，如果每当它在跟踪中不成立时，它就不会在该跟踪的任何扩展中成立）。从上述Schneider的工作开始，Ligatti和al.在[3，6]中定义了四种不同的处理有限动作序列的安全自动机：截断自动机，它可以识别坏的动作序列，并在违反安全属性之前停止程序执行，但不能以其他方式这些自动机的行为类似于Schneider的安全自动机的行为。抑制自动机除了能够停止程序执行之外，还可以抑制单个程序操作，而不会立即终止程序。第三个自动机是插入自动机。它能够将一系列动作插入程序动作流以及终止程序。最后一个是自动编辑.它结合了抑制和插入自动机的功能，因此它能够截断动作序列，并可以插入或抑制安全相关的行动。本文引入了四个进程代数算子YdKX，其中X是目标，Y是程序控制器，即控制目标行为的进程，K是相应自动机的名称。这些操作符能够模仿上面简单描述的安全自动机的行为。为了表达安全策略，我们使用μ演算公式，因为系统的许多属性都是通过固定点自然指定的，并且它非常具有表达性。利用基于进程代数的安全分析的庞大理论，并使用μ演算的满足性过程，我们展示了如何根据所选择的安全自动机类型自动合成程序控制器Y此外，对于截断自动机，我们给出了一种方法来建立最大模型。这项工作是对以前工作的重大贡献（见[3，6，7，17]），F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）3133其中没有解决安全自动机的合成问题。事实上，大多数相关的著作处理的是验证问题，而不是综合问题。此外，其他方法通过将组件X视为整个兴趣系统来处理监控组件X以享受给定属性的问题。然而，通常并不是所有的系统都需要检查（或者只是不方便将其作为一个整体进行检查）。一些组件可以被信任，并且人们希望有一种方法来仅约束不受信任的组件（例如，下载的applets）。类似地，不可能为整个分布式体系结构构建引用监视器，而可以为它的某些组件构建引用监视器。在我们的方法中，我们实际上从一个属性φ开始，当系统S与一个可能不可信的组件X组合时，它也必须享有这个属性。通过使用部分模型检查技术，将属性φ投影到另一个属性上，比如φJ，仅取决于S和φ，只有分量X必须满足。这允许一个用于仅监视系统的必要/不可信部分，这里是X。因此，我们现在可以通过使用适当的控制器YDKX来迫使X享受φJ。（注意，作为特殊情况，我们有机会将X视为一个整体系统，就像在其他系统中一样。方法）。本文的组织结构如下。第2节介绍了进程代数和（广义）结构化操作语义（GSOS），逻辑和安全自动机的必要背景。第三节描述了一些与安全自动机相对应的进程代数算子（控制器）。第4节展示了如何自动构建控制器程序来执行所需的安全策略。第5节展示了如何建立截断自动机的最大模型第6节给出了一个简单的例子，第7节总结了本文。2背景2.1操作语义与进程代数我们还记得一个正式的方法，给操作语义的一个给定的语言。这种方法被称为广义结构化操作语义（GSOS）（见[4]）。它允许对程序（项）的行为进行组合推理。2.1.1GSOS格式设V是一组变量，范围为x，y，. 设Act是一组有限的行为，由a，b，c……排列。. . 签名是一对（F，ar），其中：• F是一组函数符号，与V不相交，• ar：F<$→N是一个秩函数，它给出函数符号的元数;如果f∈F而ar（f）= 0，则f称为常数符号。给定一个签名，设WV是一组变量。可以定义W上的n-项集为最小集合，使得W中的每个元素都是项，并且如果f ∈ F，ar（f）= n且t1，.。.. ，tn）是一个术语。也是34F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）31K可以将赋值定义为从变量集合到项集合的函数γ，使得γ（f（t1，...，t n））= f（γ（t1），.γ（t n））。给定一个项t，设V ars（t）是t中的变量集。如果V ars（t）=0，则项t是闭合的。现在我们可以描述GSOS格式。GSOS规则r的格式如下：国际新闻报{xy}1≤i≤kbij{x1≤i≤ki−→ij1≤j≤mii−→}1≤j≤ni（一）f（x1， . . ，x）−→cg（x，y）其中所有变量都是不同的;x和y分别是所有xi和yij变量的向量;mi，ni≥0，k是f的arity。我们说f是规则（op（r）=f）的算子，c是作用。GSOS系统G由签名和GSOS规则的有限集合给出给定签名f =（F，ar），赋值f对于项f（s1，.，s k）和规则r，如果：(i) n（xi）=si，其中1≤i≤k;国际新闻报(ii) 对所有i，j，其中1≤i≤k且1≤j≤mi，有<$（xi）−→<$（yij）;bij(iii) 对于所有i，j，其中1≤i≤k且1≤j≤ni，它成立，<$（xi）/−→，术语的形式语义由标号转换系统（LTS）描述也就是一个对（E，T），其中E是项的集合，T是三元关系T（E×Act×E），称为转移关系。 之间的过渡关系可以在下面的表格中定义隐藏项：我们具有（s1， .. . ，sn）−→csi对于具有操作符f和动作c的规则r，存在有效的赋值f，使得s=f（g（x，y））。GSOS系统存在唯一的跃迁关系（见[4]），并且这个跃迁关系是无限分支的。2.1.2示例：CCS进程代数Milner的CCS（参见[13]）是一种描述并发系统的语言在这里，我们提出了一个制定米尔纳主操作符是进程间的并行组合，即E F，因为正如我们稍后更好地解释的那样，它允许对进程的并行组合进行所考虑的通信的概念是同步的，即两个进程必须同意同时执行通信。它通过同步动作（或内部动作）τ表示的互补动作的同时执行来建模。L etLb e afit e s etfacti t e|a∈L}是一个比较简单的运算的集合，其中a<$=a，ActbeLL<${τ}，其中τ是特殊的action表示内部计算步骤（或通信），并且可以是一组常量符号，可以用于定义递归过程。为了给出处理全球SOS的CCS的公式，我们定义签名 *CCS=（FCCS，ar）如下。FCCS={0，+，}{a. |L<$L <$L <$}{ [ f ]|f：Act<$→Act}不对称。|f: Act›→Act}∪Π.函数ar的定义如下：ar（0）= 0，对于每个π∈Π，我们有ar（π）= 0，π和+是二元算子，其余的是一元算子.F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）3135−→→Prefixing：选择：a. x−a→xx−a→xJx+y−a→xJy−a→yJx+y−a→yJ平行：x−a→xJy−a→yJx−→lxJy<$l yJxy−a→xJyxy−a→xyJx−a→ xJxy−τ→xJyJx−a→ xJ限制：a重新贴标签：x\ L−→ xJ\Lf（a）Jx[f]−→x[f]表1CCS的全球SOSCCS封闭项的操作语义通过表1中的GSOS系统给出，并通过LTS描述。我们用Der（E）表示一个（闭）项E的导数的集合，即通过转移关系可以到达的过程的集合非正式地说，一个（封闭的）术语a.E表示一个进程，它执行一个动作a，然后表现为E。项E+F表示过程E和F之间的非确定性选择.选择两个组件中的一个组件的操作术语EF表示两个过程E和F的平行合成。如果两个进程中的一个可以执行某个操作，则它可以执行该操作，并且这不会阻止另一个进程的功能并行组合的第三条规则是这种演算的特征，它表示进程之间的通信发生在两者都可以执行互补动作的时候。由此产生的过程是由每个组件的后继者的并行组合分别给出的。过程E\L是有像E，但在LL 为了让我们的孩子-对于并行进程间的一个动作，我们必须设置约束算子。 E[f]过程类似于E，但这些区域被重命名为viaf。2.1.3行为关系：模拟通常有必要比较使用不同术语表达的过程，以了解两个过程之间是否存在某种行为关系，以及哪一个（见[13]）。我们提出观察关系的概念如下。EτEJ（或EEJ）ifE→τEJ（其中τ是一个具有特殊性和特殊性的位置）ofthe→τrelation）;EEJifEτ→aτEJ。4现在我们可以给出以下定义。定义2.1设（E，T）是并发进程的LTS，设R是进程集合E上的二元关系。则称R为模拟（用≤表示）if，当ver（E，F）∈R时，ifE→aEJthenFJ∈E s.t. F∈aFjandd（EJ， FJ）∈R.4τ aJτJ J注意，它是E<$Eτ→Eτ<$E的一个简短符号，其中Eτ和Eτ表示中间态(not在我们的框架内）。36F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）31ρρ<$T）J=S <$F）J= S<$X）J =ρ（X）<$A1<$A2）J=<$A1）J<$A2）Jρ ρ ρ ρ ρ ρ<$A1<$A2）J=<$A1）J<$<$A 2）J <$<$A<$A）J={s|{sJ：s→asJandsJ∈A）J}ρ ρ ρ ρ ρ（A）J ={s|sJ：s→aSJ蕴涵SJ∈<$A）J}我们用H来表示不相交环境的并集。设ρ是环境（从变量到值的函数），σ在{μ，ν}中，则σU.f（U）表示函数f在一个变量U中的σ定点。<$）ρ= []<$X=σADJ）ρ=<$DJ）（ρH[UJ/X]）H[UJ/X]其中U J= σU。A）JJ和ρJ（U）=<$DJ）（ρH[U/X]）。（ρH[U/X]Hρ（U））它非正式地说，（X=σA）D的解是下式的σ定点解UJA）其中方程D列表的其余部分的解被用作环境。表2方程μ演算2.2方程μ演算与部分模型检验方程式μ演算是一种过程逻辑，非常适合于系统的规范和验证，其行为可以通过动作的状态变化自然地描述。 它允许表达许多有趣的属性，如安全性和活性属性，以及允许表达LTS上的等价条件。 为了递归地定义给定系统的性质，这种微积分使用定点方程。设a在Act中，X是一个在有限个变量集V上变化的变量。正如我们已经说过的，方程μ-演算是基于定点方程来代替递归算子的。X=μA是一个极小定点方程，其中A是一个断言（即一个没有递归算子的简单模态公式），X=νA是一个极大定点方程。断言（A）和等式列表（D）的语法由以下语法给出：A：：= X|不|F|A1A2|A1A2|⟨a⟩A|[a] AD：：= X = νAD|X = μAD|ϵ其中，符号T表示真，F表示假;是公式的标准合取的符号，即A1<$A2成立i<$A1和A2都成立，并且<$A是公式的析取，所以当A1和A2中至少有一个成立时，A1<$A2成立此外，A是（可能性运算符）。这意味着另一方面，[a]A是（必要性运算符），意味着粗略地说，方程列表D的语义是对应于D的方程组的解。根据这种记法，其中D（X）是变量X的值的集合，而E| = D↓X可用作E∈D）（X）的简短符号。形式语义见表2。下面给出的μ-演算的标准结果将有助于本文的后续工作。定理2.2（[18]）给定一个公式φ，可以在指数时间内决定F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）3137JX//[f]=XaA//[f]=b：f（b）=a<$b<$（A//[f]）[a]A//[f]=b：f（b）=a[b]（A//[f]）A1<$A2//[f]=（A1//[f]）<$（A2//[f]）A1<$A2//[f]=（A1//[f]）<$（A2//[f]）T//[f]=T F//[f]=F表3重标记算子的部分求值函数如果存在一个φ的模型，也可以给出一个这样的模型的例子。部分模型检测（Partial model checking，pmc）是一种最初为并发系统（进程）的组合分析而开发的技术（参见[1]）。为了解释部分模型检测是如何工作的，我们给出了它背后的直观思想，描述了pmcw.r.t.并行算子如下：证明E<$F满足公式φ（E<$F| = φ）等价于证明F满足一个修改的规范-φ//E（F| = φ//E），其中//E是部分模型检验函数w.r.t.并行复合运算符（形式定义见[1]）。 公式φ为通过使用方程式μ演算来指定。下面是部分模型检查的一个有用结果引理2.3（[1]）给定过程E<$F和公式φ，我们有：E<$F| = φ iF| = φ//E。简化公式φ//E仅取决于公式φ和过程E.不需要关于过程F的信息，过程F可以代表可能的敌人。因此，给定某个系统E，就有可能找到敌人成功攻击该系统所必须满足的性质。值得注意的是，部分模型检查函数可以从用于定义语言语义的语义规则中自动导出。因此，所提出的技术是非常灵活的。一个类似于引理2.3的引理适用于由GSOS建模的大范围的进程代数操作器（参见[1，8]）。表3给出了重标记算子的部分模型检验函数。2.2.1特征公式特征公式是一个等式μ演算公式，它完全表征了LTS中的（状态）行为模行为关系的选择概念。按照[5，14]中使用的推理，我们描述了一个过程w.r.t.模拟如下。定义2.4给定一个有限状态过程E，它的特征公式（w.r.t.模拟）DE↓XE由以下等式定义：对于每个EJ∈Der（E），XEJ=νa∈Act（[a]（E一：EEJJ X EJJ））。以下命题成立。JJ38F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）31，q）（σ，q）=（σ，q）引理2.5设E是一个有限状态过程，φE，≤是它的特征公式w.r.t. 模拟，则F≤E惠F| = φ E，≤.2.3执行机制和安全自动机本文采用Ligatti等人在[3]中给出的方法来描述四种不同类型的安全自动机的行为一个安全自动机至少由一个（可数的）状态集，比如Q，一个动作集Act和一个转移（部分）函数δ组成。 每种自动机都有 一种稍微不同的过渡函数δ，这些差异解释了它们表达能力的变化。δ的精确定义是每种自动机定义的一部分。我们用σ表示动作序列，·表示空序列，τ5表示内部动作。每种不同类型的安全自动机K的执行由下式指定：一个带标签的操作语义。基本的单步判断具有（σ，q）−a→K（σJ，qJ）的形式，其中σJ和qj是独立的，自动机采取单步之后的动作等式和状态，a表示动作由自动机产生单步判断可以推广到一个γ6J J多步判断（σ，q）=γK（σ，q），其中γ是一个动作序列，如下所示：低点。（σ，q）−a→KJJJJJJ JJ γKJ J.（回复）a;γJ J（翻译）（σ，q）=<$K（σ，q）（σ，q）=<$K（σ，q）下面给出了每个安全自动机的操作语义截断自动机。截断自动机的操作语义是：如果σ=a;σJ且δ（a，q）=QJ（σ，q）−a→T（σJ，qJ）（T-Step）否则（σ，q）−τ→T（·，q）（T-停止）镇压机器人。 它被定义为（Q，q0，δ，ω），其中ω：Act×Q → {−，+}表示所讨论的动作是否应该被抑制（-）或发射（+）。如果σ=a;σJ和δ（a，q）=qJ和ω（a，q）=+（σ，q）−a→S（σJ，qJ）（S-StepA）若σ=a;σJ且δ（a，q）=qJ且ω（a，q）=−（σ，q）−τ→S（σJ，qJ）（S-StepS）5在[3]中，内部动作用·表示。根据进程代数的标准表示法，我们使用τ表示内部作用。6假设v是单一行为的序列，其中γ=a1，. . ，an. 我们的报告并不涉及自动化设备。在我们使用相同的符号进行进程代数计算之前。从上下文中可以清楚地看出这个符号的含义。（σF. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）3139否则（σ，q）−τ→S（·，q）（S-Stop）插入自动机。它被定义为（Q，q0，δ，γ），其中γ：Act× Q →Act× Q，指定将动作插入到程序的动作序列中需要注意的是，在[3，6]中，自动机插入了一个有限的动作序列，而不是只有一个动作，即，使用函数γ，其控制是否执行错误动作。如果它成立，自动机插入一个有限的动作序列，因此中间状态的数量有限。不失一般性，我们认为它只执行一个动作。这样，我们就可以公开地考虑所有的中间状态。 注意，γ的定义域与δ的定义域是不相交的，以便有一个确定性自动机。若σ=a;σJ且δ（a，q）=qJ（σ，q）−a→I（σJ，qJ）（I-Step）若σ=a;σJ且γ（a，q）=（b，qJ）（σ，q）−→bI（σ，qJ）（I-Ins）否则（σ，q）−τ→I（·，q）（I-停止）编辑自动机。它被定义为（Q，q0，δ，γ，ω），其中γ：Act×Q →Act×Q指定在程序的动作序列中插入有限的动作序列此外，这里ω和δ具有相同的域，而γ的域与δ的域不相交，以便具有确定性自动机。如果σ=a;σJ和δ（a，q）=qJ和ω（a，q）=+（σ，q）−a→E（σJ，qJ）（E-StepA）若σ=a;σJ且δ（a，q）=qJ且ω（a，q）=−（σ，q）−τ→E（σJ，qJ）（E-StepS）若σ=a;σJ且γ（a，q）=（b，qJ）（σ，q）−→bE（σ，qJ）（E-Ins）否则（σ，q）−τ→E（·，q）（急停）40F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）313基于进程代数在本节中，我们给出了一些过程代数算子的语义，记为Y dKX，其中K∈{T，S，I，E}7，它们充当控制器算子。这些允许在给定控制程序Y的行为的情况下控制（可能不可信的）组件X的行为。3.1进程代数在这里，我们通过显示它们的行为和语义规则来定义控制器操作符我们用E表示程序控制器，用F表示目标。在不失一般性的情况下，我们在附加的假设下工作，即E和F从不执行内部作用量τ。3.1.1截断自动机：dTE→aEJF→aFJEdTF→a EJdT FJ该运算符对类似于Schneider的自动机的截断自动机进行建模见[3，6]）。它的语义规则规定，如果F执行动作a，并且E执行相同的动作（因此在自动机的当前状态下是允许的），则E dT F执行动作a，否则它停止。命题3.1设Eq=Σa∈Act\{τ}⎧a.EqJi <$δ（a，q）=qJ100OTHW设F为控制过程，设F为目标。作为截断自动机（Q，q0，δ）的输出的每个动作序列也可从E qd TF导出，反之亦然。3.1.2抑制自动机：dSE→a EJF→aFJE−−→aEJF→aFJEdSF→a EJdS FJEdSF→τEJdS FJ其中−a是不在Act中的控制动作（因此它不允许互补动作）。对于截断自动机，如果F执行E执行的相同动作，则E dS F也执行它。相反，如果F执行E不执行的动作a，并且E可以执行控制动作-a，则E dS F执行抑制动作a的动作τ，即，a从外部观察变得不可见。否则，E dS F停止。7我们选择这些符号来表示四个操作符，它们分别具有截断，抑制，插入和编辑自动机的相同行为。F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）3141命题3.2设Eq，ω=ω⎧EqJ，ωi <$ω（a，q）=+且δ（a，q）=qJ⎨−a.EqJ，ωi <$ω（a，q）=−且δ（a，q）=qJ⎪100OTHW设F为控制过程，设F为目标。作为抑制自动机（Q，q0，δ，ω）的输出的每个动作序列也可从E q，ωd SF导出，反之亦然。3.1.3插入自动机：dIE→a EJF→aFJE→/aEJE−+→a. bEJF→aFJ8EdIF→aEJdI FJEdIF→bEJd I其中+a是不在Act中的动作。如果F执行了一个动作a，而E也能执行，那么整个系统就会执行这个动作。如果F执行了一个动作a，而E没有执行，并且E通过执行一个控制动作+a和一个动作b来检测它，那么整个系统执行b。可以注意到，在[3]中插入自动机的描述中，γ和δ的域是不相交的。 在我们的例子中，这是由第二个规则的前提保证的，在第二个规则中，我们有，Ea→EJ，E−+→a。bEJ. 如果air（a，q）不存在于ma中，在δ的定义域中，它在γ的定义域中，这意味着作用量a和状态q是不兼容的，因此为了改变状态，必须执行与A不同的动作。值得注意的是，它能够插入新的动作，但不能抑制F执行的任何动作。⎧εa.EqJ，γi <$δ（a，q）命题3.3设Eq，γ=Σ⎪⎨a∈Act\{τ} ⎪ +a.b.EqJ，γi <$γ（a，q）=（b，qJ）联系我们设F为控制过程，设F为目标。作为插入自动机（Q，q0，δ，γ）的输出的每个动作序列也可从Eq，γd IF导出，反之亦然。3.1.4编辑自动机：dE为了同时进行插入和抑制，我们定义以下控制器算子。它的规则是dS和dI规则的结合。E→aEJF→aFJE−−→aEJF→aFJE→/a EJE+→a. bEJF→aFJEdEF→aEJdE FJEdEF→τEJdE FJEdEF→bEJd E该运算符结合了前两个运算符的功能。8+abJ这意味着E −→ Ea −→ E。然而，我们认为+a.b是一个单一的动作，即。 状态Ea是hide，我们在Der（E）中不考虑它。⎪⎪a∈Act\{τ}42F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）31a∈Act\{τ}命题3.4让⎧EqJ，γ，ωi <$δ（a，q）=qJ和ω（a，q）=+⎪Eq，γ，ω=Σ⎪⎨−a.E qJ，γ，ωi <$δ（a，q）=qJ且ω（a，q）=−EqJ，γ，ωi <$γ（a，q）=（b，qJ）我的意思是，设F为控制过程，设F为目标。作为编辑自动机（Q，q0，δ，γ，ω）的输出的每个动作序列也可从E q，γ，ωd EF导出，反之亦然。重要的是要注意，我们在dS的语义中引入了控制动作-a，在dI的语义中引入了+a，以便分别找到与抑制和插入自动机尽可能相似的运算符。其他定义也是可能的，尽管我们在定义易处理的语义上做了一些尝试。4控制器程序的综合利用我们的框架，我们可以构建一个程序控制器Y，它允许为任何目标系统X强制执行所需的安全属性。我们将对[10]进行这里我们有四个不同的操作符，特别是我们必须处理控制操作。假设S是系统，并且假设X是可以动态改变的一个组件（例如，下载的移动代理），我们认为它可能是不可信的。我们希望对于X的任何实际行为，系统S<$X享有由逻辑公式φ表示的安全性质，即，X（S |= φ。为了保护系统，我们可以在每个进程X执行之前简单地检查它的正确性，或者，如果这是不可能的（或不可取的），我们可以定义一个控制器，在任何情况下，强制每个进程正确地运行在这里，我们在这里研究如何建立一个程序控制器，以迫使未知组件正确的行为。因此，我们要找到一个控制程序Y，使得：X（S|= φ（2）通过使用[9]中提出的部分模型检查方法，我们可以专注于Y dKX的属性，即：Y|= φJ（3）其中φJ=φ//S。为了处理（3）中的泛量化，我们证明以下命题。F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）3143=φK支持4. 1.当fK是依赖于K的重标号函数时，对于任意的K∈{T，S，I，E}YdKX≤Y[fK]成立。特别地，f T是Act 9上的恒等函数，⎧如果a=−afS（a）=奥苏河⎧如果a=+a fI（a）=奥苏河⎧如果a∈ {+a，−a}fE（a）=奥苏河现在我们把自己限制在方程μ-演算公式的一个子类中，用Frμ表示。这个类由方程μ-演算公式组成，好吧很容易证明这组公式在部分模型检验函数下是封闭的，并且下面的结果成立。命题4.2设E和F是两个有限态过程，φ∈Fr μ。如果F≤ E则E| = φF| = φ。在这一点上，为了满足公式（3），具有：YY[fK]|=φJ为了进一步减少前面的公式，我们可以使用部分模型检查功能的重新标记操作。因此，对于每个K∈ {T，S，I，E}，我们计算JJ JK//[fK]. 因此，我们得到：YY|= φJJ第十条（四）这样，我们得到了μ-演算中的一个可满足性问题，它可以通过定理2.2来解决。5极大模型在前一节中，我们已经展示了为3.1节中定义的每个控制器算子合成程序控制器的方法。 事实上，我们发现不执行τ操作的确定性过程，是给定μ演算公式的模型。在本节中，我们定义了极大模型w.r.t.的概念。仿真关系，并显示它是如何可能的，以综合一个最大的程序控制器Y的运营商YdTX。我们定义了极大模型的概念。模拟的关系如下。过程E是给定公式φ i <$E的极大模型|= φ和ΔEJs. t。EJ|= φ，EJ≤E（见[15，16]）。非正式地，最大程序控制器Y是尽可能少地限制目标X的活动的进程。[9]在这里，必须考虑通过控制行动来充实既定法案即使进程Y执行某些动作τ，也可以从Y获得另一个进程YJ，它只具有可见的动作，这是φ的确定性模型。φ44F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）31为了找到最大模型，我们利用Walukiewicz在[19]中提出的理论。通常，发现的模型是一个不确定的过程。为了找到一个确定性模型，我们考虑F rμ的一个子集的公式，不带。这套公式称为泛合取μ-演算公式，简称μC。很容易证明，在部分模型检查函数下，μC是封闭的（参见[5]）。命题5.1给定一个公式φ∈ φ∈μC，存在这个公式的一个极大确定性模型E。为了生成最大模型E，我们找到了φ的模型，其中X=να∈Ac t\{τ}（[α]F<$（<$α<$X<$[α]X））. 对于mulapermitt，所有的行动都在行动。利用Walukievicz的理论，我们发现了一个确定性的不执行τ动作的φ的模型E这显然是φ的一个模型。以下引理成立。引理5.2设EJ|= φ，其中φ ∈μC。 那么φ E的模型是这样的，EJ≤ E。因此，E是φ的最大模型。6一个简单的例子考虑以下等式定义φ=Z，其中Z=ν[τ]Z<$[a]W，W= ν[τ] W<$[c] F。它断言在每个动作a之后，不能执行动作c。 LetAct={a，b，c，τ，a<$，<$b，c<$}b e te Aplyingh epari al对平行算子的求值，经过一些简化，我们得到下面的方程组，我们用D表示。Z//S=ν[τ]Z//S[ a<$]Z//S J[a]W//SW//S JZ//0=TW//SJ=ν[τ]W//SJ[<$b]W//0<$[c]FW//0=TZ//SJ=ν[τ]Z //S J<$[<$b]Z //0<$[a]W // SJW//S=ν[τ]W//S<$[a<$]W//S J<$[c]FwhheS−a→SJsoSJisb.0的情况。通过部分模型检查获得的信息可用于实施安全策略。特别地，选择四个算子中的一个并使用其定义，可以简单地定义一个函数Y[fK]，其中K依赖于chosn控制器，这是前面公式的模型。在这个简单的例子中，我们选择控制算子dS。因此，我们将重新标记函数fS的部分模型检查应用于前面的公式，我们简化了用T替换W//0和Z//0（并假设Y只能抑制C动作）。我们得到D//fS如下。F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）3145--S S SS，fSSS，fS////SZ//S，f =ν[τ]Z//S，f[−c]Z//S，f[a<$]Z//JW//JWJ=ν[τ]WJ<$[−c]WJ<$[<$b]T<$[c]FS，fSS，fSS，fSZJ=ν[τ]ZJ<$[−c]ZJ<$[<$b]T<$[a]WJS，fSS，fSS，fSS，fS S西/西，f=ν[τ]W//S，f[−c]W//S，f[a<$]WJS，fS [c]F我们可以注意到过程Y = a。− c. 0是D//f的模型.然后，对于任何组件，X，我们有S（Y d SX）满足φ。例如，考虑X = a. c。0的情况。看看dS的第一个规则，我们有：（S（YdSX））=（a.b. （a. −c. 0dSa.c. 0））−a→（a.b. 0（−c. 0dSc. （0））使用第二个规则，我们最终得到：（a.b.）0（−c. 0dSc. 0））−τ→（a.b. 00dS0）因此系统仍然保持其安全性，因为组件X所执行的动作已经被防止在外部可见。7结论和今后的工作我们说明了一些结果，走向一个统一的理论，加强安全性质。有了这项工作，我们扩展了一个框架的基础上进程演算和逻辑技术，已被证明是非常适合的建模和验证几个安全属性，也解决安全系统的合成问题。作为未来的工作，我们计划实现这里所示的理论，以生成程序控制器，并将其扩展到其他应用场景，如基于时间的。确认我们感谢STM 06的匿名审稿人提供的宝贵意见，这些意见帮助我们改进了本文。引用[1] Andersen，H.R.，部分模型检查，在：LICS[2] Bartoletti，M.，P. Degano和G.Ferrari，访问控制的策略框架，在：2005年安全理论问题研讨会的会议记录，长滩，加利福尼亚州，2005年，pp.5[3] 鲍尔湖J. Ligatti和D.沃克，更可执行的安全策略，在：I。Cervesato，编辑，计算机安全基础：FLoC'02计算机安全基础研讨会论文集95比104[4] Bloom，B.，S. Istrail和A.R. Meyer，互模拟[5] Gnesi，S.，G. Lenzini和F. Martinelli，通过部分模型检查，软件验证与确认国际研讨会（SVV），ENTCS。（2004年）。[6] Ligatti，J.，L. Bauer和D. Walker，Edit automata：Enforcement mechanisms for run-time securitypolicies，International Journal of Information Security4（2005）.SSS46F. 马丁内尔岛Matteucci/Electronic Notes in Theoretical Computer Science 179（2007）31[7] Ligatti，J.，L. Bauer和D. Walker，Enforcing non-safety security policies with program monitors，in：第10届欧洲计算机安全研究研讨会（ESORICS），2005年。[8] Martinelli，F.，“Formal Methods for the Analysis of Open Systems with Applications to Security 锡耶纳大学论文（1998年）。[9] Martinelli，F.，Partial model checking and theorem proofing for ensuring security properties，in：CSFW[10] Martinelli，F.和I. Matteucci ，Partial model checking，process algebra operators and satisfiabilityprocedures for（automatically）enforcing security properties，在计算机安全基础国际研讨会（FCS 05）上发表。[11] Martinelli ， F. 和 I. Matteucci ， Modeling security automata with the process algebras and relatedresults（2006），在第六届国际安全理论研讨会（WITS '06）上发表[12] 米尔纳河，综合沟通行为，载于：第七届MFCS会议记录，波兰，1978年。