基于UMLsec的安全体系结构设计及验证方法研究

理论计算机科学电子笔记142（2006）31-46www.elsevier.com/locate/entcs设计安全体系结构JanJurjens1IT安全能力中心因此，我们的系统工程师，TUMünchen，Germany摘要开发安全关键系统是困难的，有许多众所周知的安全漏洞在实践中被利用的例子。特别是，到目前为止，很少有研究已经进行了健全的基础上设计的安全体系结构，这将是迫切需要开发安全系统的可靠性和有效性。在本文中，我们对支持安全体系结构设计的可靠方法进行了一些研究。我们概述了UML的扩展，称为UMLsec，它允许在架构设计规范中的图中表达安全相关信息。我们定义了安全架构设计模式的基础。 我们提出的工具支持已开发的UMLsec安全架构的方法。关键词：安全软件工程，安全体系结构，安全工程，安全验证，安全形式化方法，安全评估，安全模型，密码协议1动机安全关键系统的高质量开发是困难的。许多关键系统的开发、部署和使用都不能满足其安全要求，有时甚至会导致严重的攻击。特别是，到目前为止，很少有研究已经进行了健全的基础设计的安全体系结构，这将是迫切需要开发安全系统1http://www4.in.tum.de/juerjens。这项工作部分由德国联邦教育、科学、研究和技术部（BMBF）在Verisoft项目框架内资助，资助额为01 IS C38。这篇文章的责任在于作者。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.01232J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）31可靠和高效。安全系统开发的部分困难是正确性经常与成本相冲突。如果彻底的系统设计方法在人员培训和使用方面会造成高昂的成本，那么它们往往会被避免。在软件架构领域[2]，统一建模语言（UML）也被提议用作架构描述语言（ADL）。特别是，UML提供了一个前所未有的机会，高质量的安全系统开发，是可行的，在工业环境。• UML作为工业建模领域事实上的标准，大量的开发人员都接受过UML的培训。• 与以前的符号相比，用户社区的规模相当，UML是相对精确定义的。• 开发了大量的分析、测试、仿真、转换等工具来辅助使用UML的日常工作本文基于同一主题的教程[6]，简要介绍了如何使用基于形式的UML安全扩展UMLsec来为设计安全体系结构奠定基础。首先，我们回顾了UMLsec的简化片段的定义及其在本文中使用的形式基础。我们勾勒出如何可以使用原型，标签和约束来封装知识的安全体系结构，从而使其提供给开发人员可能不专门在安全系统。特别是，我们解释了如何使用基于形式的UMLsec提供安全的架构设计模式的基础。我们还演示了如何可以正式验证是否与原型相关的约束是在一个给定的安全架构设计中使用提供的工具支持填充。通过这种方式，人们可以在部署甚至实现系统之前找到设计中存在的错误。最后，我们将解释如何为基于Java安全体系结构设计安全系统提供基础。2安全体系结构分析我们简单回顾一下[5]中UMLsec的形式基础，它将在后面的章节中用于安全架构分析。 更多的细节可以在[5]中找到。J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）3133形式语义学对于一些用于定义UMLsec扩展的约束，我们需要参考行为方面的精确定义的语义。对于安全性分析，然后并入来自面向安全的定型的安全性相关信息。我们的UML简化片段的形式语义包括活动图、状态图、序列图、静态结构图、部署图和子系统，简化以保持一些更微妙的安全需求所必需的形式处理是可行的。子系统集成了不同类型图之间以及系统规范不同部分之间的信息。我们只概述了基本概念，完整的说明在[5]中，其中还包括本工作所基于的早期工作在UML中，对象或组件通过在其输入队列中接收并释放到其输出队列的消息进行通信。因此，对于给定系统的每个组件C，我们的语义定义了一个函数C）（），• 取输入消息的多集合I和组件状态S，• 输出一组（O，T）对（C）（I，S），其中O是输出消息的多集合，T是新组件状态（由于可能出现的非确定性，它是一组对）以及部件的初始状态S0状态图D的行为语义对UML状态图的运行到完成语义进行建模。作为一个特例，这为我们提供了活动图的语义。给定序列图S，我们定义每个包含的组件C的行为（S.C）（）。子系统将描述系统不同部分的图组合在一起：由子系统S给出的系统组件C可以包含子组件C1，. 、Cn. S的行为解释（S）（）定义如下：(1) 它接受多组输入事件。(2) 事件从输入多集合和连接子组件的链接队列中分发，并作为参数提供给定义S中预期接收者行为的函数。(3) 这些函数的输出消息被分发到连接消息发送者和接收者的链路的链路队列中，或者当接收者不是S的一部分时，作为S）（）的输出给出。在执行安全分析时，在最后一步之后，34J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）31可以以下面解释的某种方式修改链路队列的内容。安全分析对于给定UMLsec子系统规范S的安全性分析，我们需要对潜在的攻击者行为进行建模。我们对特定类型的对手进行建模，这些对手可以以特定的方式攻击系统的不同部分。为我们假设一个函数ThreatsA（s），它接受一个攻击者类型A和一个原型s，并返回{delete，read，insert}的子集。然后，我们将A型攻击者的实际行为建模为A型攻击者函数，该函数将S和状态S中的链路队列的内容非确定性地映射到S和新状态T中的链路队列的新内容：• 其中delete∈ThreatsA（s）的原型化的链接的内容可以被映射到删除，• 其 中 insert∈ThreatsA （ s ） 的 定 型 链 接 s 的 内 容 可 以 由 来 自 其 中read∈ThreatsA（t）的定型链接t的内容的元素来扩大。攻击者类型定义了攻击者可以将哪些动作应用于具有给定原型的通信链路。删除意味着对手可以删除相应链接队列中的消息，读取允许他读取链接队列中的消息，插入允许他在链接队列中插入消息。为了评估系统相对于给定类型的攻击者的安全性，我们将子系统S在存在A类型攻击者的情况下的执行定义为函数<$S）A（），该函数通过将攻击者函数应用于链路队列来定义，作为定义的第四步，（）如下：(4) 如上所述，A型对手函数被应用于链路队列。UMLsec profile使用了一种形式化的安全需求保密性，遵循形式化方法中的一种标准方法：它依赖于这样一种想法，即如果系统从未发送任何可以从中导出d的信息，即使在与对手的交互中（其中知识集收集对手获得的信息），则规范保留了某些数据d我们说子系统S保护表达式E的秘密不被类型A的对手发现，如果E在子系统S）A（）的执行过程中从未出现在AJ. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）31353UMLsec扩展：架构定型我们简单回顾一下UMLsec概要文件中与安全架构相关的一个简化片段。完整的记录可以在[5]中找到为了适应特定的应用领域，UML提供了三种标记值是将数据与模型中的元素相关联的大括号中的名称-值对。此外，可能会附加必须由图表满足的约束我们解释了一些UMLsec的原型和标记，并给出了例子。这些约束在安全要求应该保持的对手类型上被参数化;因此，我们确定了一个对手类型。A将在下面使用。有些限制是指第2节中的正式定义。可以使用[5]中提供的工具支持自动检查它们。因特网、加密、局域网部署图中链接上的这些构造型表示通信链接的各自类型。我们要求每个链接最多携带这些刻板印象中的一个。对于每个攻击者类型A，我们有 一 个 函 数 ThreatsA （ s ） ， 它 将 一 个 类 型 ∈{ （ （ encryptedummy ，（（LANummy，（（Interntttummy}）））}转换为一组字符串威胁A删除{delete，read，insert}。 这样我们就可以评估UML规范-阳离子使用节中解释的方法二、我们利用这个对轮廓的其余定型的约束作为威胁函数的示例，图1给出了默认类型的攻击者，这代表了一个具有适度能力的外部对手。安全链路这个原型可以标记子系统，用于确保物理层满足通信的安全性要求。更准确地说，该约束强制执行，对于不同节点n，m上的子系统或对象之间的每个依赖关系d立体类型（（保密），我们在n和m之间具有具有原型s的通信链路l，使得读∈/T hreatsA（s）。例如图2、给定默认对手类型，原型的约束（（安全链路安全）被违反：该模型不提供针对默认对手的通信保密性，因为互联网通信Web服务器和客户端之间的链接不提供根据威胁默认（Internet）方案所需的安全级别。36J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）31客户端机器获取密码客户端应用程序«保密»联系我们«互联网»服务器机器web服务远程访问 «安全链接»访问控制StereotypeThreatsdefault（）Internet{delete，read，insert}加密{delete}兰钢丝绳智能卡存储器POS设备发行者节点Fig. 1.来自默认攻击者的威胁保密（（调用对象或组件关系图中的依赖项）或（（发送对象或组件关系图中的依赖项）立体-typed（（security）类型的加密对象应该为作为操作或信号的参数或返回值发送的数据提供保密性这个原型被用在静态类型的训练中。安全依赖这个构造型用于标记包含对象图或静态结构图的子系统，确保对象或子系统之间的（（call对象和（（send对象之间的依赖关系符合对可能通过它们进行通信的数据的安全需求更确切地说，这个原型强制的约束是 ， 如 果 存 在 从 对 象 （ 或 子 系 统 ） C 到 对 象 （ 或 子 系 统 ） D 的（（call_parallel）或（（send_parallel）依赖，则满足以下条件。• 对于D未引用的任何消息名称，如果满足以下条件，则n将出现在C中的标记{secret}中图二. 安全链接使用示例J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）3137随机发生器密钥生成器«关键»{secret={newkey（），random联系我们newkey（）：Keyrandom（）：Realseed：Realrandom（）：Real«接口»随机数newkey（）：Key图三. 调生成子系统而且只有在D中才是• 如果由D表示的消息名称出现在C中的标记{secret}中，则依赖性是立体的（（secrec））。示例图3显示了一个密钥生成子系统，该子系统使用requiremet（（securedependencystructures. 他给了一个评价，他确信-straint，因为Random generator和（（call）依赖项不提供Key generator所需的random（）的安全级别关键这个构造型将对象的实例以某种方式标记为关键的，由相关标记{secret}指定，其值是当前对象的数据值或属性，其机密性应该受到保护。这种保护是由定型观念的约束来执行的（（数据安全级别）和（（无下行-下行级别）（取决于保密程度需要），其标记包含（（关键的可扩展对象）的子系统数据安全这个原型标签子系统有以下约束。子系统行为尊重由立体类型（ （critical）关键字和相关联的标签给出的数据安全性要求更确切地说，限制因素是，定型子系统保护由标签{secret}指定的数据的保密性，以对抗第2节中定义的A类对手。示例图4中的示例显示了一个简单安全协议的规范。发送方请求公钥K和证书。CateSignKCA（rcv：：K）从接收到的密钥中验证密钥的有效性，并将在K下加密的数据d发送回（这里{M}K是密钥的加密）。密钥生成«安全依赖»38J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）31SecureChannel«数据安全»{advertisement =default}send（d：Data）receive（）：DataS：接收器R：接收器输入/i：=0entry/j：=0SRs：entry/i：=i+1send（d）Requestr：request（）Wait/request（）/return（{SignK−1（kj：：j）}KS）Rentry/j：=j+1WaitTrmreturn（C）k：：= head（ExtKR（DecK−1（C）receive（）transmit（E）S[k∈Keys][尾（Deckj（E））=j]tail（ExtK（Dec−1（C）=i]接收RKS发送/返回（标题（Deck（E）J/transmit（{d：：i}k）«界面»«界面»发送接收send（d：Data）receive（）：Data发送方节点«LAN»接收方节点«LAN»Sendercomp«Internet»ReceivercompS：发送R《呼叫》R：接收方联系我们见图4。 安全协议具有密钥K的消息M，DecK（C）是使用K对密文C的解密，SignK（M）是使用K对消息M的签名，并且ExtK（S）是使用K从签名中提取数据。假设默认advertisement类型，并通过参考第2节中概述的advertisement模型，可以确定d的保密性得到保护。S：“严重”{秘密={d}}联系我们 R：接收器«临界»{fresh={k}}联系我们j：N; k， K−1， K：密钥俄.西i：N; K−1， K：键SRreceive（）：Datatransmit（e：Data）request（）：Expsend（d：Data）J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）31394安全架构设计模式的基础使用UMLsec设计安全体系结构有几个概念上的帮助。例如，在[5]中，我们解释了如何使用工具支持的技术，如细化和模块化。在本节中，我们简要地描述了如何在UMLsec的上下文中使用安全模式软件架构模式[1]通过呈现重复出现的设计问题和标准化的解决方案来封装软件架构师的设计知识。人们可以使用UMLsec模型的转换来在设计过程中引入模式。这种方法的一个目标是确保以一种以前已经被证明是有用和正确的方式引入模式。此外，具有使用变换引入模式的合理方式可以简化安全分析，因为可以在更抽象和更简单的级别上执行分析，并且可以导出更具体级别的安全属性，只要变换已经被示出为保持相关的安全属性。在我们的方法中，模式p的应用对应于函数fp，它接受UML规范S并返回UML规范，即当将p应用于S时获得的规范。从技术上讲，这样的函数可以通过定义它应该如何作用于某些子系统实例来表示，通过以组合的方式将其扩展到所有可能的UML规范。假设我们有一个子系统实例集合S，使得S中没有一个子系统实例包含在S中的任何其他子系统实例中。假设对于每个子系统实例S ∈S，我们给出一个子系统实例fp（S）。然后对于任何UML规范U，我们可以通过将U中的子系统实例S ∈S的每次出现替换为fp（S）来定义fp（U可能如何在技术层面上做到这一点超出了UMLsec第一篇介绍的范围在这里，我们只是通过一个例子来证明这个想法考虑不可信网络上的通信问题，如图5所示。这个问题的一个众所周知的解决方案是使用密钥交换协议对不可信链路上的传输进行加密，如图4所示。在[5]中给出了这种模式的详细解释。因此，安全信道模式可以直观地用公式表示如下：在诸如图5中的情况下，可以使用图5中的系统来实现执行安全要求所四、为了以正式的方式应用这个模式p，我们考虑通过重命名从图5中的子系统派生的子系统集合S：这意味着，我们在每次出现时用名称m替换任何消息、数据、状态、子系统实例、节点或组件名称n，以避免名称冲突40J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）31s：发送（d）等待发送/transmit（d）S：接收器R：接收器r：发送（d '）等待接收SRreceive（）/return发送节点«LAN»接收节点«LAN»SendercompReceivercompS：«加密»R：接收器联系我send（d：Data）receive（）：Data«数据安全»{advertisement信道receive（）：Data«界面»接收send（d：Data）发送«界面»S：“严重”{秘密={d}}联系我们R：接收器send（d：Data）receive（）：Datatransmit（d '：Data）图五. 安全体系结构模式示例：发送方和接收方然后fp将任何子系统实例S ∈S映射到通过相同的重命名从图4中给出的子系统实例导出的子系统实例这给了我们一个fp的表示，从中可以推导出任何UML规范上的fp的定义为：如上所示。因为可以表明图4中的子系统在精确意义上是安全的，如[5]中所解释的。这为在开发环境中以明确的方式重用安全工程知识提供了一种方便的方法。5Java安全体系结构的安全基础在本节中，我们将解释如何为基于Java安全体系结构设计安全系统提供基础。动态访问控制机制是安全体系结构（如JDK 1.2安全体系结构及其GuardedObjects）的一部分，J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）3141由于很容易忘记访问检查，因此很难管理[3]。如果不执行适当的访问控制，整个系统的安全性可能会受到损害。此外，访问控制可以通过授予对包含能够访问另一对象的签名密钥的对象的访问而间接地和无意地被授予我们展示了如何使用UMLsec的Java安全体系结构的上下文中，以解决这些问题，通过提供- ING手段的正确部署的安全体系结构机制，如守卫对象的推理授权或访问控制是计算机安全的基石之一。目的是确定请求的来源是否被授权批准该请求。分布式系统面临更多的挑战。可信计算基础（TCB）可以在各种位置并且处于不同的控制之下。沟通是在可能的对手面前进行的。使用了可能是恶意的移动代码。由于需要授权，也就是说，各实体可以代表其他实体行事，因此情况更加复杂。而且，许多安全要求是依赖于位置的.例如，用户在办公终端处可能比从家中登录时具有更多的权限。在Java中，这个问题通过提供Java安全体系结构在体系结构级别解决。特别是，从JDK 1.2开始，采用了细粒度的安全架构，提供了用户可定义的访问控制，以及受保护对象的复杂概念[3]。将权限授予保护域。保护域[7]是主体可访问的一组实体。在JDK 1.2中，保护域由类和对象组成。它们是根据代码的来源（由URL给出）和代码签名的密钥来指定的。由用户或系统管理员设置的系统安全策略由从类Java实例化的策略对象。安全政策安全策略将保护域映射到授予代码的访问权限集。存在类型化和参数化访问权限的层次结构，其根类是Java。安全权限和其他权限是从根类或它的一个子类派生的。目标由目标和行动组成。对于类FilePermission中的文件访问权限，目标可以是目录或文件，操作包括读、写、执行和删除。如果当前线程历史中的所有调用者都属于已被授予访问权限的域，则授予访问权限线程的历史记录包括当前堆栈上的所有类，并且在创建当前线程时还可传递地继承其父线程中的所有类。如果资源的提供者与使用者不在同一个线程中，并且使用者线程无法提供访问42J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）31一控制上下文信息，可以使用GuardedObject来保护对资源的访问资源的提供者创建一个表示资源的对象和一个包含资源对象的GuardedObject，然后将GuardedObject交给使用者。指定的Guard对象包含需要满足的检查，以便可以获得资源对象。为此，Guard接口包含方法checkGuard，接受Object参数并执行检查。要授予访问权限，Guard对象只需返回，要拒绝访问，则抛出SecurityException。GuardedObject是一种非常强大的访问控制机制。然而，它们的使用可能难以管理。例如，guard对象可以检查类文件上的签名。通过这种方式，可以间接地并且可能是无意地授予对对象的访问权，即通过授予对包含签名密钥的另一个对象的访问权，针对该另一个对象，对应的签名提供对第一个对象的访问权。因此，JDK 1.2安全体系结构的复杂访问控制机制并不那么容易使用。权限的授予取决于执行上下文。有时，访问控制决策依赖于多个线程。一个线程可能涉及多个保护域。查看给定的类是否将被授予某种权限并不总是容易的。在本节的剩余部分，我们将解释一些支持安全的UMLsec构造型。使用Java安全架构机制。保护访问子 系 统 的 这 种 构 造 型 意 味 着 子 系 统 中 的 每 个 被 构 造 型 化 的（（guarded对象只能通过附加到（（guarded对象的标记{ guard }指定的对象来 访 问。首先，我们有一个名字叫∈/p代表对手类型A在所考虑的情况下以及（（受保护的对象）的实例的每个名称这 意 味 着 参 考 文 献 不 是 公 开 可 用 的 。 此 外 ， 我 们 假 设 对 于 每 个（ （guarded） 对 象，都有一个对象的状态图规范，其名称在关联的标记{guard}中给出。通过这种方式，我们对引用的传递进行建模。我们用一个基于Web的财务应用程序的例子来说明这种刻板印象。有两个机构通过互联网向当地用户提供服务：一个是网上银行Bankeasy，另一个是财务顾问Finance。 要使用这些服务，本地客户端需要授予来自相应站点的小程序某些特权。通过GuardedObjects实现对本地财务数据的访问。局部系统部分的详细说明见图6。它包含Java安全架构的简化相关部分，该部分接收对象引用请求并将其转发给三个受保护对象的保护对象。由于（（受保护的加密对象StoFi、FinEx和KJ. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）3143MicSi只能通过其关联的防护来访问，子系统实例满足与原型关联的条件（（关于默认对手的防护访问权限）访问控制由Guard对象FinGd、ExpGd和MicGd实现，它们的行为是指定的。例如，由银行签名的小程序可以读写存储在本地数据库中的金融数据，但只能在下午1点到2点之间。这是由FinGd守卫对象强制执行的，我们假设条件槽被填充当且仅当时间在下午1点到2点之间把守这个原型标记了原型范围内的对象（（guarded access）），上面的对象应该是被保护的。它有一个标记值{guard}，它定义了相应的guard对象的名称作为一个例子，在图。在图6中，{guard}对象分别由{guard}对象Guard对象FinGd、ExpGd和MicGd来保护{guard }对象StoFi、FinEx和MicSi。6工具支持为了促进我们的方法在工业中的应用，自动化工具的UML模型使用建议的语义分析是必需的。我们描述了一个框架，其中包含了几个这样的验证器目前开发的TU M UMU？ 更多信息可以在[5]中找到。图7说明了满足所列需求的UML工具框架的体系结构。我们简要描述了它的功能。开发者创建一个模型，并将其存储在UML 1.5/ XMI 1.2文件格式中。该文件由基于Java的工具导入到MDR存储库中，该存储库是Netbeans库的一部分。该工具通过MDR库生成的JMI接口访问模型。检查器通过调用复杂的分析引擎，如一阶逻辑自动定理证明器e-Setheo、模型检查器Spin和基于Prolog的分析例程，解析模型并检查与原型相关的约束。结果以文本报告的形式交付给开发人员，描述发现的问题，以及修改后的UML模型，其中突出显示了违反约束的构造型。7经验与展望这里提出的方法已成功地应用于安全系统项目中，例如，在一个项目44J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）31当地«安全访问»getObject（Exp，Exp）：Exp StoFi.Read（）：Exp StoFi.Write（arg：Exp）FinEx.Read（）：ExpMicSi.Sign（req：Exp）：ExpJavaSecArch：returnFGdReturn？[obj=FinEx]/ExcGd.chkGd（sig）/return（FinEx）getObj（obj，sig）等待请求检查请求/return（MicSi）/MicGd.chkGd（sig）returnMGdReturn？[obj=MicSi][obj=StoFi]/ FinGd.chkGd（sig）JavaSecArch MicGd联系我们limit：BoolchkGd（）«call»chkGd（）«call»«call»«call»FinGd«call» ExcGd插槽：BoolchkGd（）chkGd（）ExcGd：chkGd（sig）等待请求检查请求[sig=cert]/returnFinGd：chkGd（sig）MicGd：chkGd（sig）等待 请求检查请求WaitReqCheckReq[sig=bank slot=true]/return[sig=finan limit=true]/return见图6。 金融应用规范：本地系统与一家大型德国银行合作，分析一个安全关键的互联网银行架构，并在德国电信公司的生物识别访问控制架构和德国汽车制造商的汽车紧急应用程序的Verisoft项目中分析项目，该项目由德国«守卫»StoFi{guard=FinGd}联系我们«guarded»FinEx{guard=ExcGd}FinData：ExpExcData：ExpRead（）：Exp写入（arg：Exp）Read（）：Exp«保护的»MicSi{保护=MicGd}MicroKey：钥匙签名（要求：Exp）：ExpJ. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）3145数据流“使用”UML模型（UML1.5/XMI 1.2）修改的UML模型文本报告结果JMIMDR动态链接模型和所需属性分析套件分析引擎静态检查器误差分析器UML编辑器(UML 1.5 / XMI 1.2兼容）例如Poseidon 1.6见图7。 UML工具套件科学技术部.特别是，这些经验表明，这一办法足以在实践中使用考虑到安全关键系统在实践中的现状，以及不断报告的许多弱点，将模型驱动开发应用于安全系统架构设计似乎是一个很有前途的想法，因为它使几乎没有安全背景的开发人员能够利用封装在广泛使用的设计符号中的安全工程知识。由于有许多非常微妙的安全要求，很难用“肉眼”来检查，即使是关键系统专家也可以从这种方法中获益。为了使这些想法在实践中受益，重要的是要有智能工具支持来帮助使用它们。如上所述，可以使用工具来机械地检查上面说明的约束，这通过在分析安全设计模型时节省时间和防止错误来支持该方法。更多的信息可以在书[5]和包括[4]的文章中找到46J. Jürjens/Electronic Notes in Theoretical Computer Science 142（2006）31引用[1] Buschmann，F.，R. Meunier，H. Rohnert，P. Sommerlad，and M. 面向模式的软件架构Wiley，1996年。[2] Garlan，D.，软件架构：路线图。第22届软件工程国际会议（ICSE 2000）：软件工程的未来，第91ACM，2000年。[3] 贡湖，Java 2平台安全性Addison-Wesley，Reading，MA，1999年。[4] 我是J. ，UMLsec：针对安全系统开发的Ext ending i ng UML。 INJ。-M. J'ez'equel，H. Hußmann和S. Cook，编辑，UML 2002Springer-Verlag，2002.[5] 我是J. ，安全系统与UML一起开发。 Sprin ger-Verlag，2004.[6] 我是J. 、用于S a fe和S ecure系统的两种方法的存档。在2004年的第五届软件架构大会上，IEEE计算机学会，2004年。半天辅导。[7] 萨尔茨， J.， 和M. 施罗德，保护信息 在计算机系统中。Proceedings of the IEEE，63（9）：1278