使用体系结构推理信息安全的研究与方法

→→+Ⓧ使用体系结构推理信息安全斯蒂芬·庄，哈佛大学Ron VAN DER MEYDEN，UNSW澳大利亚我们证明，通过一些例子，信息流的安全属性可以证明从抽象的架构描述，它只描述了系统的因果结构和本地属性的可信组件。我们指定这些体系结构的描述系统概括不传递的不干扰政策承认的能力，过滤通信域之间传递的信息。这种系统架构的细化的概念，支持自上而下的发展，抽象的信息安全属性的架构规范和证明我们还表明，在一个具体的设置中，因果结构是强制执行的访问控制，静态检查的访问控制设置加上本地验证的可信组件足以证明，广义的不传递不干扰政策是满意的。CCS概念：安全和隐私形式化的安全模型; 安全和隐私逻辑和核查8附加关键词和短语：信息流安全，认知逻辑，系统架构，内在不干涉ACM参考格式：斯蒂芬·庄和罗恩·范德梅登。2015.使用架构来推理信息安全。ACM Trans. Info.系统安全18，2，第8条（2015年12月），30页。DOI：http://dx.doi.org/10.1145/28299491. 介绍系统架构是一种高级设计，它描述了系统的组件及其交互的总体结构。对架构建模语言的建议（例如，AADL[2009]和Acme [Garlan et al.2000]）在细节和内容的层次上有所不同，但在最抽象的层次上，体系结构指定了系统。多独立安全级别（MILS）方法[Alves-Foss et al.2006; Vanfleet et al.2005; Boettcheret al.2008]建议使用架构作为高保证系统保证案例的关键部分。MILS愿景的细节仍在开发中[Blasum et al.2014年]。 正如Boettcher所言，这篇文章的早期版本在2009年流传，并在文献中被引用。目前的版本包括一个重大的返工的结果，架构完善，从该版本。在ACSAC 2012的分层保证研讨会上，介绍了访问控制实施结果的论文版本。本版本增加了这些早期版本的所有结果和一组扩展的例子充分证明。这项工作得到了空军科学研究办公室、澳大利亚研究委员会发现基金DP1097203和国家科学基金会基金1054172的支持。作者作者：John A.哈佛大学保尔森工程与应用科学学院，剑桥，MA 02138;van der Meyden，澳大利亚新南威尔士大学计算机科学与工程学院，悉尼，新南威尔士州2052，澳大利亚。允许制作部分或全部本作品的数字或硬拷贝供个人或课堂使用，不收取任何费用，前提是复制品不以营利或商业利益为目的制作或分发，并且复制品在第一页或显示器的初始屏幕上显示此通知以及完整的引用。版权的组成部分，这项工作所拥有的其他人比ACM必须尊重。允许用信用进行提取复制，再版，张贴在服务器上，再分发到列表，或在其他作品中使用本作品的任何组成部分，需要事先特定的许可和/或费用。可向出版部索取，ACM，Inc. 2 Penn Plaza ， Suite 701 ， New York ， NY 10121-0701 USA ， 传 真 ： 1 （ 212 ） 869-0481 ， 或permissions@acm.org。c 2015 ACM 1094-9224/2015/12-ART8 $15.00DOI：http://dx.doi.org/10.1145/2829949ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月8：2 S. Chong和R.范德迈登等人[2008]，它包括一个两级设计过程，包括一个政策级和一个资源共享级。在策略级别，系统由图形式的架构描述在这方面，该架构就像一个不可传递的不干涉安全策略[Haigh and Young 1987; Rushby 1992; van der Meyden 2007]。在策略级别，还可以指定哪些组件是受信任的，以及这些组件受信任执行的本地策略根据MILS的愿景，根据体系结构构建系统，通过组成满足其本地策略的组件，应该导致系统满足全局安全性和安全属性。在资源共享层面，MILS设想使用一系列基础设施机制来确保架构信息流策略得到执行，尽管组件共享资源，如处理器、文件系统和网络链接。这些机制可能包括物理隔离、分离内核、周期处理、加密和分离网络基础设施。该基础设施的目的是达到高保证水平，以便通过对可信组件和系统基础设施的保证案例进行组合，获得系统保证案例。希望这将为基础设施机制和可信组件提供一个类似COTS本文的主要贡献是通过几个例子来证明，正如MILS文献中所设想的那样，从可信组件及其体系结构的高级规范中组合地获得有趣的信息安全属性实际上是可能的。我们专注于组合推理的信息流安全属性。我们提出了一个框架，允许规范的系统架构与一些系统组件的本地约束。为了给架构结构一个精确的含义，我们扩展了van der Meyden [2007]开发的不传递不干涉策略的语义。这些策略以图形的形式出现，其中顶点对应于系统组件，从组件u到组件v的边指定允许信息从u直接流向v。该语义以异步计算模型表示，并捕获无法访问定时信息的攻击者可用的信息的概念之前已经给出了这种语义的架构解释[van der Meyden2012]。 为了表达对可信组件的约束，我们通过标记组件之间的边缘来扩展架构，这些边缘具有进一步限制允许沿边缘流动的信息的功能。的工作的贡献之一是给一个正式的语义丰富的架构，包括这些新类型的边缘。我们还开发了一个理论，这些丰富的架构，使自上而下的，正确的保护发展的建筑规范细化。它还允许使用该体系结构的抽象来获得复杂体系结构上的信息安全属性的简单证明我们展示了使用的框架，通过系统有趣的安全要求。这些措施包括多级安全数据库，星光互动链接[安德森等。1996]，一个可信的降级，和一个简单的电子选举系统。在每个示例中，存在要强制执行的以知识逻辑表达的应用程序特定的信息流安全属性。为了执行这些属性，我们确定，在每个例子中，一个架构结构和数学上精确的一组本地约束的可信组件。我们表明，对于每个例子，其特定的安全属性产生的局部约束和建筑结构的相互作用的结果在每个示例中，我们的结果表明，对于任何符合该架构的系统，如果ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月⊆×A=使用架构推理信息安全8：3可信组件满足其局部约束，则系统满足全局信息流特性。示例中给出的信息安全属性提供了信息理论和特定于应用的保证。否定每个信息安全属性将构成攻击，其中特定类型的信息流向任何不允许拥有该信息的攻击者。由于我们得出的结论是信息论的，因此从我们的结果可以得出，不存在可用于异步攻击者的隐蔽信息通道（例如，组件之间的消息顺序），这可能违反信息安全属性。到目前为止，只有少数几个例子被提出来正式证明MILS方法对高保证安全系统的开发。Greve等人[2003]开发了一个例子，但是相对于我们考虑的抽象的“非干扰”风格的语义，它是一个更具体的模型（基于处理内存段访问控制的分离内核形式安全策略我们的策略级别模型更加抽象，并且允许实现更大的灵活性。然而，我们也考虑一个更具体的模型，系统的结构化状态受到“参考监控条件”[Rushby1992]。 我们表明，在这种情况下，要证明一个系统符合我们的扩展架构之一，它足以检查一个简单的条件的访问控制设置，并证明本地属性的可信组件。通过开发一个抽象的语义体系结构和规范的可信组件，并通过开发额外的例子，我们的工作进展的情况下，全球信息流的安全属性可以来自一个高层次的系统架构和本地约束的可信组件在这个架构中，推理的风格所设想的Boettcher等人。[2008年]。文章的结构如下。在第2节中，我们回顾了架构及其语义，并使用过滤器功能扩展了架构，这些过滤器功能允许细粒度地指定组件之间的信息流 这个扩展推广了van derMeyden [2007]的不传递不干涉的语义（定理2.6）。在第3节中，我们介绍了我们用来表达信息安全属性的认知逻辑。此外，我们提出的架构和信息安全的属性，这些架构意味着的例子我们还讨论了群体知识和分布式知识之间的区别，并表明，使用群体知识定义的信息安全属性被保持在体系结构细化（定理3.9）的基础上访问控制的具体模型在第4节。我们将van der Meyden[2007]的结果扩展到具有过滤函数的扩展架构（定理4.2和4.3），该结果表明本地访问控制条件增强安全性（定理4.1）在第5节中，我们考虑了可能用于展示访问控制模型保持的平台和技术。我们将在第6节讨论相关工作。第7节结束我们使用的例子来说明和激励的定义和结果。两个在线附录扩展了文章正文中的材料附录A扩展了以前关于体系结构细化的工作，以说明过滤器功能。附录B给出了本工作主体中所述所有结果的充分证明2. 架构与语义体系结构给出了系统结构的策略级描述 我们从一个简单的建筑概念开始，遵循van derMeyden [2012]。稍后将介绍一个更丰富的概念架构是一对（D，>），其中D是安全域的集合，并且二元关系>D D是信息流策略。关系>是自反的，但不一定是传递的。直观地说，只有当u > v时，信息才允许从域u流向域v。这种关系是自反的，因为它假设一个域中的信息流是无法阻止的，因此总是允许的ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月HLHL={}{}HSHS八点四分。Chong和R.范德迈登Fig. 1.建筑HS.在有关信息流策略的文献中，域通常被理解为对应于安全级别。我们使用更一般的解释，其中域也可以对应于系统中的系统组件或代理。直观地说，域对应于系统的接口，该接口由可以通过该接口进行的系统状态的观察以及该接口允许执行的动作定义在架构的实现中，单独的域不一定利用单独的资源。硬件、代码和数据可以在域之间共享。事实上，一个关键的挑战是，尽管共享资源，但要确保信息流动2.1. 示例：HL架构体系结构（H，L，（L，L），（H，H），（L，H））由两个安全域H和L组成，并且信息流策略指示除了自反信息流之外，还允许信息从L流到H我们可以用图形来描述，用矩形表示安全域，用箭头表示信息流我们省略了自反信息流的箭头。2.2. 示例：欣克-舍费尔已经为多级安全数据库管理系统（MLS/DBMS）提出了多种体系结构[Thuraisingham2005]。 在Hinke-Schaefer体系结构中[Hinke and Schaefer 1975]，几个（不可信的）单级DBMS在一个可信的操作系统中组合在一起。每个用户都与一个单级DBMS交互。操作系统在单级DBMS之间实施访问控制，允许限制性更强的DBMS读取限制性更弱的DBMS的存储文件，但反之则不然。图1显示了体系结构，它代表MILS策略级别上两个安全级别域H用户和域L用户分别表示高安全性DBMS和低安全性DBMS的用户;它们分别与单级DBMSHDBMS和LDBMS单级DBMS将它们的数据存储在表示为HF和LF的数据库文件中。注意，允许信息从HF和LF两者流向HDBMS，因为允许高安全性DBMS读取高安全性DBMS和低安全性DBMS两者的存储文件。Hinke-Schaefer架构也被称为这相当于决定在资源共享上实现策略级架构通过可信分离内核的方式来实现。ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月·∈∈∈×→→∈ ×→∈···∈∈∈联系我们∈ ∈=◦∈∈.生活α=G使用架构推理信息安全8：52.3. 机模型要指定实现满足架构意味着什么，我们必须首先定义什么是实现。我们使用状态观测机模型[Rushby1992]，它定义了确定性的基于状态的机器。机器具有一组动作A，并且每个动作与安全域相关联。直观地说，如果动作a与域u相关联，则a表示由u表示的系统组件所采取的决策、选择或动作。动作确定性地改变机器的状态，我们假设每个安全域的观察结果由当前机器状态决定。s机器是元组M=（S，s0，A，D，step，obs，dom），其中S是状态的集合0S是初始状态，A是动作集合，D是域集合，步骤：S一S是确定性的转移函数，dom：A D将域与每个动作相关联，并且观察函数obs：DSO描述了对于每个状态，每个域可以进行什么样的观测，对于某个观测集合O。我们假设可以在任何状态下执行任何动作：函数步是总的。给定动作序列αA，我们写sα表示从状态s开始依次执行每个动作所达到的状态。我们定义sα，使用转移函数step归纳定义，s·<$=ss·αa=step（s·α，a）对于αA和α A.(Here，<$表示空序列。）为了便于记法，我们将函数obs（u，）写成obsu，将函数obsu（s0α）写成obsu（α），其中αA≠ 0。我们使用术语组来指代一组域。1给定序列αA.a的群G的视图是群的观察和属于群成员的动作的序列。直觉上，G函数视图G定义域G的视图。我们首先通过obsG（s）=（obsu（s））u∈G（即，个体的观察元组u∈G）。然后，视图函数被归纳地定义为：视图G（<$）=obsG（s0）（a）若dom（a）∈G，则G（α）aobsG（αa）viewG（α）表示G（αa），否则对于αA和α A.为了说明语义是异步的，并且对观察的断续不敏感，定义使用了吸收连接运算符：对于集合X，序列αX，元素x X，αx如果x等于α的最后一个元素，则为α，否则为αx。当G u是单例时，我们为视图G写视图u。最后，对于任何动作序列α，对于α的子序列，我们记为αTG定义域在集合G中的动作的集合。2.4. 语义如果在机器的所有可能的执行中，信息流符合体系结构的信息流策略，则机器满足体系结构。我们使用van der Meyden [2007]提出的方法将其形式化，该方法涉及使用具体的操作模型来定义域允许学习的信息的上限。操作模型使用函数tau来捕获，该函数将动作序列αA映射到域u根据策略>在α之后被允许具有的最大信息的表示。（术语[1]在关于知识逻辑的文献中，“群体”一词通常用来指一组主体。ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月.taα=u=·联系我们F八点六分。Chong和R.范德迈登该定义纠正了van der Meyden [2007]在早期基于“不及物清除”语义[Rushby 1992]中发现的问题。只有当v>u时，v的动作才能向u传递信息。而且，传达的信息不应超过v被允许拥有的信息给定机器M=（S，s0，A，D，step，obs，dom），函数tau归纳定义为tau（<$）=且，对于α∈A<$且a∈A，（a）tau（α）ifdom（a）>/u（tau（α），ta dom（a）（α），a）否则。ta u的值域是基本元素A <$的嵌套元组的集合。 注意，tau（αa）的结果可以解释为一棵树，其中如果dom（a）> u，则根有三个孩子tau（α）和ta dom（a）（α）和a。注意，如果不允许信息从dom（a）流到u，则tau（αa）tau（α）（即，允许给U的最大信息不改变）。 如果允许信息从dom（a）流到u，则所传递的信息至多是域dom（a）被允许具有的信息（即， tadom（a）（α）），以及所执行的操作a。因此，在这种情况下，我们通过将信息（tadom（a）（α），a）添加到u在执行动作a之前被允许具有的最大信息tau（α）来获得u在α a之后可能具有的最大信息。如果一台机器有一组适当的域，并且对于每个域u，u在状态s0α中观察到的是由tau（α）确定的，则它符合TA换句话说，tau描述了u可以学习的最大信息：如果在两次运行中，α和αr的最大信息都是相同的（tau（α）=tau（αr）），那么u定义2.1（TA合规性）。一个系统M是TA-顺从于体系结构（D，>）的，如果它有定义域D，并且对所有u∈D和所有序列α，αr∈A，使得tau（α）=tau（αr），weeobsu（α）=obsu（αr）.TA-遵从性要求如果tau（α）=tau（αr），则u在状态s0·α和状态s0·αr中的第n个观测值s相等。下面的引理表明，事实上TA-顺应隐含t hat，如果tau（α）=tau（αr），则nviewu（α）=viewu（αr）。2.2. 若M对于体系结构（D，>）是TA相容的，则对于所有的agentsu和allα，αr∈A∈ u，满足tau（α）=tau（αr），我们有viewu（α）=viewu（αr）.2.5. 滤波函数到目前为止使用的架构强加粗糙，全局约束的因果结构的系统。如果u>v，则TA遵从性允许域u向域v发送其具有的任何和所有数据。但是，在许多系统中，关键安全属性取决于这样一个事实，即受信任的组件只允许某些信息从一个域流到另一个域。架构中信息流的更精细规范使我们能够证明更强的信息安全性能。我们通过引入过滤器功能来扩展架构的概念，以允许对域之间的信息流进行细粒度的规范我们定义这些扩展架构的语义，并提出了扩展的architec- tures让我们证明强大的信息安全属性的例子。扩展架构是一对A=（D，>），其中D是一组安全域，和>D×D×（L，{T}），其中L是函数名的集合我们写u>v，当（u，v，f）∈>，写作u> v作为f的简写。（u，v，f）∈>，且u>好吧（u，v，f）∈>。v作为简写ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月=T∈L不/=TF× ∈L∈A∈L→A=AI=∈ ∈=L使用架构推理信息安全8：7F直观地说，u>v表示从u到v的信息流是允许的，但可能受到约束。在情况f中，从u到v的信息流没有约束：任何可能由u拥有的信息都被允许传递给v。v当u作用时，就像TA服从的定义一样。如果f，则允许信息从域u流向域v，但需要通过f表示的函数进行过滤：只有该函数输出的信息才可能被传输从U到V如果u>v，则不允许从u到v在某些情况下，操作系统或网络基础设施可以强制执行给定的过滤功能。然而，一般来说，滤波器函数是局部控制器，F对系统的受信任组件的约束。换句话说，如果对于f，u>v，则组件u被信任以强制发送到v的信息被适当地过滤我们要求扩展架构具有以下属性：F(1) 对所有的u，v∈D，至多存在一个f∈L，n {T}使得u> v.(2) 关系>是自反的，因为对于所有u∈D，我们有（u，u，T）∈>。第一个条件要求从u到v的所有允许的信息流都使用单个标记边来表示。直观地说，任何具有多个这样的边的策略第二个条件是由前面已经提到的事实所激发的，即从一个域到它本身的信息流是无法阻止的。例如，下图显示了具有域H、D和L的扩展架构，旨在分别表示高安全域、可信解密器和低安全域。箭头指示域之间允许的流。从D到L的边缘上的标签指示从D到L的信息应该由函数rel过滤。在绘制扩展架构时，我们用过滤器函数名注释域之间的箭头。对于没有标签和省略的自反箭头，隐含的标签是。这允许将未扩展的体系结构图解释为扩展的体系结构图。（请注意，这个图解约定与我们在文本上下文中的约定不同，扩展策略>，我们写u>v，如果存在f∈L<${T}使得（u，v，f）∈>.）扩展架构不定义函数名的解释。如果（D，>）是一个扩展的架构，则对的解释是一个元组（A，dom，I），其中A是一组动作，dom：AD将这些动作分配给架构的域，而I是一个函数，将每个f映射到一个域为A的函数A（和任意的余域）。换句话说，对于每个f，函数I（f）是一个将动作序列和动作映射到某个值的函数。我们称之为（A，I）解释的扩展架构，或简单地解释的架构。直觉，如果u>v和α一个人和一个A是具有dom（a）u的动作，则I（f）（α，a）是当动作a在动作序列αA发生之后执行时允许从u流向v的信息。我们允许函数I（f）具有任意的共域，以允许在对由各种应用传输的具体数据值进行建模时的灵活性。然而，出于推理信息安全属性的目的，如果函数h是过滤函数的解释，ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月=∈−∈×I=不== ∈ ∈=--I=u八点八分。Chong和R.范德迈登关于h的重要信息是它的逆h−1如何划分域A<$A。换句话说，如果h（α，a）h（β，b）（对于序列α，βA和动作a，b A），则（α，a）和（β，b）在由h1强加的同一划分中，因此h揭示了关于迹αa的相同信息，就像它揭示了关于迹βb的相同信息一样。有一种特殊情况，I（f）（α，a）的值确实具有意义，即它取特殊值<$（空序列）。这种情况对应于不传输信息（不甚至一个动作已经被执行的事实），并且我们使用空字符串，因为在下面的定义中，它具有保持表示为字符串的信息的先前状态不变的效果。给定扩展架构（D，>）和架构解释（A，dom，I），我们定义一个函数ftau，其域为A，与tau一样，捕获最大值，域u在执行一系列动作后被允许拥有的加密信息。该定义是递归的，函数Tv，u，对于u，v∈D，映射序列α∈A∈ A和动作a∈A，其中dom（a）=v到如果v>u，Tv，u（α，a）=（ftav（α），a）如果v>Tu如果v>fu，则I（f）（α，a）为零。直觉上，Tv，u（α，a）表示当动作a在序列α之后执行时允许u知道的新信息。如前所述，值I（f）（α，a）是当在序列α之后执行动作a时可以跨f标记的边从v传输到u的信息的具体表示。当没有信息可以传输时，该项取特定值<$由于从v到u的边的缺失意味着从v到u的直接信息流总是被禁止的，在这种情况下，Tv，u（α，a）总是取值<$。在-标记边的情况下，从v到u的信息流没有约束。在这里，定义模型v传输所有允许的信息（由ftav（α）表示）以及动作a正在执行的事实函数ftau由ftau（<$）<$定义，对于αA<$和aA，ftau（αa）ftau（α）<$T dom（a），u（α，a）其中<$是将元素附加到序列末尾的操作。关于追加操作的一些重要技术要点是，对于任何序列σ，我们定义σ∈ <$σ（即，附加空序列<$没有效果），并且如果δ恰好是非空序列，则σδ是通过单个附加元素δ扩展序列σ的序列。例如，如果δ是序列ab，则σ<$δ的最后一个元素等于序列ab而不是b。展开定义，我们得到如果dom（a）>u，则f=u（α）ftau（αa）=ftau（α）n（ftadom（a）（α），a）如果dom（a）>Tu如果dom（a）>fu，则f∈ftau（α）∈I（f）（α，a）.前两个子句类似于tau的定义;第三个子句对此进行了补充，即沿着由函数名f标记的边流动的信息由in过滤解释I（f）. 注意如果I（f）（α，a）<$，wheredom（a）>fu，the nftau（αa）ftau（α）. 换句话说，过滤函数I（f）可以指定在某些条件下不应该有信息流动。还要注意，ftau和Tv，u具有隐式参数，即信息流策略>和架构解释（A，dom，I）.当我们需要使这些参数中的某些参数显式化，我们将表达式编写为sucha（>，I）或fta>u。ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月·一=/=∈∈ ∈LACAC使用架构推理信息安全8：9函数ftau与tau类似地用于定义域对于给定的动作序列被允许观察的最大信息然而，ftau比tau更精确，因为它使用过滤函数来绑定域之间发送的信息可以合理地假设，从u发送给v的信息是允许u拥有的信息。我们说一个函数是ftau兼容的，当它传递的信息是由u被允许拥有的信息决定的。定义2.3. 当对所有序列α，β∈A<$，ftau（α）=ftau（β）意味着对所有a∈A且dom（a）=u，我们有h（α，a）=h（β，a）时，定义域A<$× A的函数h是ftau如果函数h不是ftau兼容的，那么它可能会揭示域u不允许知道或甚至不可能拥有的信息例如，如果存在迹线α、βA，使得域u被允许在两个迹线中具有相同的信息ftau（α）ftau（β）），但h（α，a）h（β，a），则h（α，a）的值可能由域u一无所知的某个其他域v中发生的动作确定事实上，在从v到u的架构中可能没有直接路径，这意味着u永远不会了解v的任何信息。ftau兼容性的概念允许我们排除这样的功能，这些功能在架构的任何实现中都无法实现我们说解释I=（A，dom，I）与A=（D，>）相容，如果对于所有uD和边su>fv，其中f，函数I（f）是ftau相容的。 因此，我们要求解释与它们的体系结构兼容。如果一台机器具有适当的域和动作，那么它就符合解释的扩展架构，并且对于每个域u，u在状态s0α中观察到的是由ftau（α）确定的。我们称这样的机器为FTA兼容的。（定义2.4（符合FTA）。一个机器M=（S，s0，A，D，step，obs，dom）是FTA兼容的，具有一个解释架构（A，I），其中A =（Dr，>）和I =（Ar，domr，I），如果A = Ar，D = Dr，dom = domr，并且对于所有的代理u ∈ D和所有的α，αr∈Ar，如果ftau（α）=ftau（αr），则nobsu（α）=obsu（αr）。将扩展架构与它们的解释分离，确保了扩展架构可以完全由带有标记边的图形图表示它还允许我们处理扩展架构可以以各种方式实现的示例，并且对动作集和过滤函数集的弱约束足以强制执行感兴趣的安全属性我们将在下文中介绍几个这样的例子为了在语义级别上捕捉对架构解释的约束，我们使用架构规范的概念，它是一对（，），其中是扩展架构，是一套建筑学的解释。(In在这项工作中，我们将不尝试为体系结构规范开发任何语法符号。）定义2.5. 如果存在一个解释I∈C，使得机器M与解释的体系结构（A，I）是FTA兼容的，则机器M与体系结构规范（A，C）是FTA兼容的。下面的定理表明FTA-顺应性推广了TA-顺应性。因此，我们可以自由地将给定的架构解释为扩展架构。2.6. 设A1=（D，>1）是一个体系结构，A2=（D，>2）是扩展体系结构，使得（u，v，f）∈>2当且仅当f =T且（u，v）∈>1. 设M是一台具有域D、动作A和域函数dom的机器。设I =（A，dom，I）ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月==··====L不T T==关于我们--=∈=八点十分。Chong和R.范德迈登可以用这组动作和域函数对A2进行任何解释。则M是TA顺应A1的当且仅当M是FTA顺应（A2，I）的。FTA合规性要求满足ftau（α）ftau（αr），u在状态s0α和状态s0αr中的第n个观测值s相等. 下面的引理（类似于引理2.2）表明，如果ftau（α）ftau（αr），则n维有一个使u（α）视图u（αr）.对于这个结果，我们需要一个技术上的假设定义2.7. 一个解释结构（A，I）是非合并的，如果对所有的u，v∈D，如果u>fv且f/=T，n个作用为a，b∈A且dom（a）=u和dom（b）=v，且对所有的α，β∈A有I（f）（α，a）/=（ftav（β），b）.通过自反性y，u>fv，其中ff= T暗示uv。直觉上，在第五自由贸易v来区分传输给它的信息I（f）（α，a）的类型和v传输给它自己的信息（ftav（β），b）的类型。换句话说，v可以区分自己的行为对ftav的影响和其他域的行为的影响由于直观地说，v应该意识到它自己的行为，因此有理由期待这一点通常会得到满足。2.8.第一次 若M是FTA兼容的非合并解释结构（A，I），其中A =（D，>）且I=（A，dom，I），则对所有的主体u ∈ D和所有的α，αr∈ A，使得ftau（α）=ftau（αr），我们有viewu（α）=viewu（αr）.我们注意到，这个结果并不适用于合并解释架构。为例如，考虑一个结构，其中hdom（a）>fdom（b）和I（f）（α，a）（<$，b），以及一个系统，其中对所有uD和状态s，都有b u（s）。这个系统必须与架构兼容FTA，但我们有fta dom（b）（a） （<$，b）fta dom（b）（b）， 但有view dom（b）（a）和view dom（b）（b）b。然而，通过定义Ir（f）（α，a）（I（f）（α，a），x）或某个不在A中的固定值x，总是可以将一个解释I转换成另一个等价的非合并解释Ir. 在这个意义上，I（f）（α，a）I（g）（β，b）当且仅当Ir（f）（α，a）Ir（g）（β，b）是不等价的，所以I和I r的值的“信息量”是e。因此，我们可以推断，解释架构是非合并的。3. 信息安全属性我们使用（相当标准的）命题认知逻辑[Fagin et al. 1995]来表达信息安全属性。通常，更丰富的逻辑（例如，还包括临时操作员）可能是有用的。我们将自己限制在足以满足我们所呈现的应用程序的表达水平上语法定义如下：φ，φ：：=T|p |¬φ |φ ∧ ψ |K GφG的范围是域的群。如果Gu 是单例的，我们简单地写为Kuφ，对于KGφ。公式，p，φ和φ是命题逻辑的标准公式：总是满足，p是一个命题常数。认识公式KGφ说，被视为单个域的域群G知道φ。我们将前面描述的公式集（即，公式，可以建立起从和原始命题中）使用合取，否定，和模态算子KG。ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月∈∈/∈\∈≈ ⇐⇒=∈ =∈≈∈∈/==/∈⊆∈ = ∈∈使用架构来推理信息安全8：11图2.认知逻辑语义学。使用可能世界语义解释公式，其中世界是动作序列α一个小女孩。一个命题是一个集合X一个小女孩。我们说这个命题X是非平凡的，如果X和X A≠。解释函数π是从命题常数到命题的函数。我们使用满足关系M，π，αφ定义逻辑的语义，这直观地意味着公式φ在给定解释函数π和执行序列αA的机器M的情况下为真。图2定义了关系M，π，αφ。为了解释认知公式KGφ，我们对每个域G群使用一个不可否认关系，它描述了G认为什么样的动作序列是可能的，给出了它对实际动作序列的看法。两个动作序列αA和αr若G对两个序列的观点相同，则A∈G与整环群G不可区分，记为αGαr：α G α r view G（α）view G（α r）. 注意，机器M既决定了这个关系，也决定了容许序列α。还要注意的是，当G不是单例时，那么群G所拥有的知识不仅基于G的成员所观察到的事件，而且基于这些事件的总我们注意到，算子KG不同于通常的只使用了偏序：我们将在3.6节中解释。我们写M，π<$φ，如果对所有α我们有M，π，α<$φ。我们说φ有效，如果M，π<$φ对于所有系统M和解释π。G依赖命题系统M中的一个命题依赖于群G的作用，如果它的真值可以通过只改变群G中域的作用而受到影响。在我们的一些例子中，命题对群G的形式上，对于一个整环群G，α ∈ A<$，假设一个命题X <$A<$依赖于G在α处的作用，如果t存在βA，使得αTGβTG但αX当且仅当βX。（记法G是集合D G的简写，表示所有域不包括G中的那些）。直觉上，这意味着G的哪些动作发生了，以及它们相对于其他域的动作的位置，可以影响命题是否成立。我们说X处处依赖于G作用，如果X对所有αA∈α依赖于G作用。2该逻辑允许我们用术语来描述机器的信息安全属性领域的知识。我们现在通过几个示例来证明，架构可以提供足够的结构来证明给定的信息安全属性在符合该架构的所有机器中保持。我们从两个简单的例子开始，表明这已经是使用TA兼容性解释的架构的简单概念的情况，然后继续进行三个更详细的例子，其中需要扩展架构和FTA兼容性。[2]在本工作的早期版本中，我们使用了非平凡G-作用局部命题。命题X是G-作用局部的，如果对所有α，βA，如果αTGβTG，然后αXβX。很容易看出，一个非平凡的G-作用局部命题处处依赖于G-作用.因此，制定我们的结果使用的命题，依赖于G行动是更一般的。ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月∗=HL¬HLHS{}SL={∈|}⇒ ∈ ¬∈HL八点十二分。Chong和R.范德迈登图3.建筑SL。3.1. 示例：HL信息安全使用该架构，我们能够证明，在任何机器的任何执行中，，域L不知道任何依赖于H作用的命题。3.1. 如果M是TA顺应HL的，π（p）依赖于α处的H作用量，则M，π，α ∈ <$K Lp.注意，虽然这个结果是只用命题常数p来陈述的，但实际上对于任何公式φ，如果M是TA相容的，并且意义X（φ，M，π）β一 M中φ关于π的M，π，β<$φ依赖于H在α处的作用，则M，π，α<$KLφ.这是因为命题的量化是在语义层次上陈述的，我们可以取π（p）X（φ，M，π）作为一个新的命题，常数p因此，我们使用命题常数的陈述就像在公式和解释上量化的陈述我们经常在续集中使用这种模式的结果。3.2. 示例：欣克-舍费尔在Hinke-Schaefer数据库体系结构中，没有一个域Luser、LDBMS或LF知道关于域Huser、HDBMS或HF的任何事情。即使我们考虑Luser、LDBMS和LF的组知识，也是如此。3.2.让 系统 M被 符合TA标准 与 HS， 和 让 G={L用户，L DBMS，L F}。如果π（p）依赖于{H用户，H DBMS，H F}在α处的动作，则M，π，αGp.由于K upK G p对uG有效，因此M，π <$K up对u Luser，L DBMS，L F也有效。特别地，L用户不具有关于系统的高侧的任何信息。3.3. 示例：星光互动链接星光互动链接[安德森等人。1996]提供从高安全性网络到低安全性网络的交互式访问这允许高安全性网络上的用户以不同的安全级别在她的屏幕上打开窗口，同时确保没有高安全性信息进入低安全性网络。Starlight拥有硬件和软件组件。硬件设备连接到高安全性和低安全性网络，并连接有键盘和鼠标。有一个开关，可以切换之间的高安全性和低安全性的网络;输入从鼠标和键盘发送到网络当前选定的开关。Starlight允许数据从低安全性网络传输到高安全性网络，但反之亦然。Starlight软件组件包括代理窗口客户端和服务器，以允许窗口环境在Starlight硬件存在的情况下工作。图3显示了扩展的体系结构，即Starlight交互链路的体系结构.该体系结构使用过滤器功能来指定星光交互链接可以向低安全性网络发送哪些信息。ACM Transactions on Information and System Security，卷。号182、第8条，公布日期：2015年12月∈（SLASSL}C={∈|=C SL⎩SL CSLSL CSL拉瓜如果a=t或使用架构来推理信息安全8：13域H表示高安全性网络（包括用户请注意，从域L到域S没有边，因为没有信息直接从低安全性网络发送到星光交互链路。相反，来自低安全性网络的数据（例如，对窗口内容的更新）被发送到高安全性网络，从而发送到Starlight Interactive Link的软件组件。标记为sf的边限制了允许哪些信息从星光交互链路流到低安全性网络L。我们提出了一个架构规范的基础上，表达了对SF的解释约束。的解释，dom，I）包括在如果满足以下条件。让A S一dom（a）是属于域S的动作的集合。我们假设有一个杰出的actiont一个切换哪个网络正在接收输入事件的操作。直觉上，L被允许知道AS中任何t动作的发生和任何其他动作的发生（例如，键盘或鼠标输入），这在选择低安全性网络时发生（即，在奇数个触发动作之后我们通过