基于类型的双向工程安全保证方法：往返工程中的访问控制规则扩展编程语言的类型机制

可在www.sciencedirect.com在线获取理论计算机科学电子笔记292（2013）83-94www.elsevier.com/locate/entcs基于类型的双向工程安全保证方法海梅·APavlich-Mariscal帕夫利什-马里斯卡尔1，2Departamento de Ingeniería de SistemasPonti fiscia Universidad JaverianaBogotá，Colombia.Departamento de Ingeniería de Sistemas y ComputaciónUniversidad Católica del Norte智利安托法加斯塔Ariel Lopez4Departamento de Ingeniería de SistemasPonti fiscia Universidad JaverianaBogotá，Colombia.摘要安全保证是一种属性，它确保应用程序代码的行为与设计级别指定的访问控制策略一致。 只要软件工程师不修改生成的代码，安全保证证明就是有效的。这种假设在Round-Trip Engineering中不成立，因为程序员可以修改生成的代码，模型会自动重新生成。本文提出了一种访问控制的往返工程方法，该方法在从模型生成代码时保持安全保证，反之亦然。这种方法是用额外的规则来扩展编程语言的类型机制，这些规则确保模型和代码之间的一致性，即使代码被程序员任意修改。本文提出了一个正式的描述的解决方案和所需的正确性证明的初步草图。正在进行的工作是开发一个原型，以自动化的过程中的大部分及其验证的案例研究。保留字：模型驱动软件工程，往返工程，安全保证，访问控制1介绍访问控制的定义是：访问控制是一1这项工作是“利用往返工程软件进行安全工作的市场开发”项目的一部分2电子邮件：jpavlich@javeriana.edu.co，jpavlich@ucn.cl3 电子邮件地址：lfranky@javeriana.edu.co4电子邮件：ariel. javeriana.edu.co1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2013.02.00784J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）83确保敏感信息安全、未损坏和可用的重要组件因此，访问控制成为软件开发过程的首要关注点是非常重要的。总的来说，激励这项研究的一般问题是：需要一个安全的软件工程过程，在软件开发过程的每个阶段都包含访问控制[39]。作者在这一领域的前期工作包括访问控制建模和安全代码生成的框架[40，38]。在设计层面，该框架提出了对UML的几个扩展，以定义基于角色的访问控制（RBAC）[41]，强制访问控制（MAC）[10]和自主访问控制（DAC）[18]的访问控制策略。重点是将访问控制关注点与设计模型中的其他需求在代码层面，作者已经开发了两个独立的作品。其中之一是CincoSecurity，这是一个基于细粒度角色和Java EE应用程序安全配置文件的安全模块[24]。另一项工作是一组面向对象的策略，以保持访问控制关注点与其他需求的分离[38]。在代码级别，一个非常重要的问题是安全保证[40]。在本研究的背景下，安全保证意味着从设计上确保代码正确地实现访问控制。正确的实现意味着应用程序的行为完全符合策略的意图，只有在访问控制设计中的规则允许的情况下，才允许主体访问应用程序资源为了支持安全保证，作者以前的工作包括一个过程，以正式证明访问控制策略和实现它们的代码之间的一致性[40]。上述证明提供了基于模型是主要开发工件的假设的安全保证。这个前提在一些模型驱动的方法中是有效的，其中设计人员创建访问控制策略，然后自动生成代码来实现策略，并且代码没有进一步修改[29]。然而，上述假设在往返工程（RTE）中不成立[29]。在RTE中，从模型生成代码后，程序员可以修改它。可以使用逆向工程过程从修改后的代码自动重新生成模型。这种情况可能会破坏访问控制模型及其代码实现之间的一致性，因为某些代码配置可能无法映射到有效的访问控制模型。为了解决上述问题，本文提出了一种方法来保持访问控制模型和代码之间的一致性，在往返环境。图1描述了该方法。在设计级别创建应用程序的模型自动生成代码以实现设计。程序员可以修改生成的代码，并且可以使用逆向工程自动重新生成模型为了确保访问控制策略和代码之间的这些额外的规则限制了允许对代码的修改，从而在执行逆向工程时，仅生成有效的访问控制模型J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）8385图1.往返安全保证的拟议办法本文的其余部分详细介绍了这种方法。第2节解释了CincoSecurity模块[24]的基本概念，该模块将用作案例研究来说明该方法。第3节详细介绍了所提出的方法，形式化的基本概念和定理的安全保证。第4节使用基于CincoSecurity模块的案例研究来开发往返安全保证证明。第5节介绍了一些相关的工作。第六节是本文的结论。2CincoSecurity模块为了说明所提出的方法，本文使用CincoSecurity模块作为案例研究来证明往返安全保证。CincoSecurity模块由作者之一开发[24]，为Java EE应用程序提供访问控制实施 CincoSecurity扩展了标准访问控制功能 Java EE [47]与Seam [48]，提供：增强的用例实现和模块化，细粒度角色，资源保护，安全配置文件，会话和身份验证服务。细粒度角色将在本节中解释，因为这是本文用于案例研究的主要角色通常具有访问特定会话bean和在会话bean上执行操作的在CincoSecurity中，访问特定会话Bean的角色名称与Bean的名称相同。细粒度角色只有一个特权，即执行会话bean的方法。 访问会话bean的操作的角色名称具有以下格式：86J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）83为了保护对资源的访问，CincoSecurity使用注释。要约束对会话bean的访问，方法是向bean类添加一个形式为@Restrict（“#{s：hasRole（其中role对应于访问会话bean的角色，并且它与会话bean具有相同的名称。要限制对会话bean中操作的访问，方法是使用bean方法，即表单@Restrict（“#{s：hasRole（其中role对应于访问会话bean的角色，operation对应于方法的名称。当代码在JavaEE应用服务器中执行时，服务器解释上述注释并自动控制对注释资源的访问。在访问受到限制的情况下，服务器抛出一个异常，程序员可以管理该异常以引入适当的行为。CincoSecurity还添加了保护JSF页面的代码，但由于在案例研究中没有使用3保持访问控制策略和代码在Round-Trip Engineering中，设计人员创建系统模型，并使用代码生成器自动创建实现这些模型的代码此外，程序员可以修改生成的代码。最后，逆向工程过程解析修改后的源代码以重新生成模型[29]。在常规的往返环境中，该过程可以在没有进一步修改的情况下工作。例如，假设设计人员使用UML类图对应用程序结构建模，并使用序列图对其行为建模[34]。可以很容易地生成代码来实现这些图。对代码的进一步修改可以使用标准CASE工具进行逆向工程到模型中[29]。尽管在这个过程中可能会丢失一些信息，比如UML类关联，但是可以将广告数据包含到代码中，以便在逆向工程过程之后保留这些信息[26]。总的来说，只要模型和代码中的元素之间完全对应，就可以假设往返过程将保持两个域之间的一致性。然而，一些应用问题对往返工程提出了挑战。特别地，对于访问控制，可能存在在逆向工程过程之后可能破坏与访问控制要求的一致性的一些代码。为了更好地理解这个问题，考虑一个课件应用程序，它包含一个CourseManagement角色，该角色对方法getSyllabus具有权限，该方法检索课程的教学大纲。假设生成代码以使用Java EE和Seam实现访问控制模型[48]。生成的代码将包括表单J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）8387@Restrict（“#{s：hasRole（'CourseManagement'）}”）在所有被授权用于课程管理的方法中。没有机制来保护这些注释不受程序员可能做出的更改的影响，例如，更改角色名称、定义新角色等。当使用CincoSecurity [24]实现安全性时，会出现更复杂的情况。对于授予CourseManagement的每个方法，必 须 使 用 “role”_“operation” 形 式 的 名 称 创 建 细 粒 度 角 色 对 于 上 面 的 示 例 ，getSyllabus方法中的注释的形式@Restrict（“#{s：hasRole（'CourseManagement_getSyllabus'）}”）。在这种情况下，不仅注释不受程序员更改的保护。还有一个风险是，修改后的代码在执行逆向工程时不会产生有效的模型。例如，如果程序员将注释中的总体而言，无法保证对代码的修改将符合先前定义的访问控制要求。为了解决这个问题，所提出的方法是增强目标编程语言的类型化规则，以包括对由访问控制模型和安全库施加的任何规则的自动检查。这些类型规则应该只允许对代码进行修改，以产生有效的访问控制模型。从这些扩展的类型规则中，可以通过形式化地证明生成的代码和模型满足某些一致性属性来在往返环境中提供安全保证。往返安全保障在往返工程项目中，有几个基本元素：表示系统的模型，从模型到代码的映射（代码生成器），实现模型的代码，以及逆向工程映射（从代码生成此外，模型有一组约束，确保模型是有效的，通常由用于创建它们的CASE工具验证。例如，对UML类模型的一个约束是，在一个类中不能有两个具有相同名称和参数的类似地，代码有一组类型规则，确保代码是格式良好的，并且它们通常在编译时进行验证例如，Java程序中的一个类型规则是，作为参数传递给方法调用的变量的类型必须与相应方法的参数的类型相对于本文的其余部分，往返方案指的是四个元素的集合：模型上的约束、代码生成映射、类型规则和逆向工程映射。往返安全保证的基本思想是保持访问控制模型和使用给定往返方案开发的代码之间的一致性。更正式地说，往返安全保证是通过正确性证明来实现的，其中往返方案是88J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）83∈∈→∈→→∈⟨ ⟩→如果：（a）生成的代码正确地实现了访问控制策略，(b)代码无论是否修改，都可以在逆向工程过程之后产生有效的访问控制模型。定义3.1到3.6形式化了模型、代码和往返方案的组成部分定义3.1M是所有可能的应用程序模型的集合，I是编程语言中所有可能的实现定义3.2给定一组约束K，模型m M在K上有效，如果m满足K中的所有约束。定义3.3给定一组类型规则T，如果I满足T中的所有类型规则，则实现I I是良类型的。定义3.4给定模型mM的应用程序和实现代码生成是一个函数g：MI，它将模型映射到它们相应的实现。定义3.5逆向工程是一个将实现映射到模型的函数re：IM定义3.6往返方案是一个元组g，re，K，T，其中g：MI是代码生成函数，re：IM是逆向工程函数，K是 一组约束来确定模型的有效性，T是一组用于实现的类型规则。上述定义是有目的的抽象。没有给出关于模型和代码的细节利用这些定义，定理3.7将往返安全保证形式化为正确性证明，其声明如果从有效模型生成的代码是良好类型的，并且从良好类型的代码生成的模型是有效的，则往返方案是正确的。定理3.7给定一个约束集K，一个类型化规则集T，一个K下所有有效模型的集合M valid_M，以及一个T上所有良好类型实现的集合Iok_I。一 个往返方案<$g，re，K，T <$是正确的，如果g（m）在T下是良型的，对所有m ∈ M有效，re（I）在K下有效，对所有I ∈ Iok.4CincoSecurity的正确性证明为了说明第3节定义的使用，本节利用CincoSecurity模块作为案例研究，形式化一个简单的应用程序模型，包括访问控制、使用CincoSecurity的代码的映射、模型约束和程序键入规则。然后，它使用所有这些定义来证明给定往返方案的安全保证。定义4.1至4.6对模型的组成部分进行了更详细的形式化（见定义3.1）。为简单起见，本案例研究中的模型仅包括应用程序的操作（方法）和访问控制策略，访问控制策略指示J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）8389∈⟨⟩⟨ ⟩∈⟨⟩∈ ⟨⟩∈ ⟨⟩操作可以访问每个角色。没有显式地包含关于类的信息定义4.1R是与应用程序交互的角色集。定义4.2Op是应用程序的操作（方法）集。定义4.3Obj是应用程序的对象集定义4.4授权是一个元组r，op，其中r R是与应用程序交互的角色，op Op是角色可以执行的应用程序的操作（方法）。定义4.5访问控制策略P是一组授权。定义4.6应用程序的模型M是元组Op，P，其中Op是应用程序的操作（方法）集合，P是应用程序的访问控制策略。定义4.7到4.9描述了实现模型的代码的基本元素。为了简单起见，只包括Java EE的基本元素：操作（方法）实现和注释。注释被表示为元组a，op，v，这等价于在方法op上的@a（v）形式的Java注释。注释可以在（v）中包含任何对象，但为了这个案例研究的目的为了充分解释注释中的字符串，定义4.9包含了一个辅助函数来获取角色或操作的字符串表示定义4.7Annotation是一个元组a，op，v，其中a是annotation名称，op是被注释的操作，v是一个对象v∈Obj。定义4.8应用程序实现II是一个元组IOp，A，其中IOp是一组操作实现，形式为op，t的元组，其中op是一个操作，t是它在编程语言中的实现。A是IOp中操作上的一组注释。定义4.9元素的字符串表示，记为[e]=s，是从模型或实现元素e∈E到其对应的字符串表示s∈String的映射[]：E→String。在符号滥用中，e可以是角色或操作E=OpR。定义4.10规定了使用CincoSecurity模块的往返方案代码生成函数将带有操作和策略的模型作为输入，并输出带有操作和Restrict注释的实现（有关这些注释的更多详细信息，请参见第2为简单起见，Restrict注释中的文本只包含角色和操作的基本信息所有额外的语法都被删除，以降低示例的复杂性类似地，逆向工程映射将使用CincoSecurity的实现作为输入并输出模型。90J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）83模型必须满足一组Kcs约束，这确保访问控制策略中的所有per-mission引用模型中的同样，实现必须满足三个类型规则。前两个是Java中的类型规则的抽象：规则（6）表明在实现中不能有重复的操作，规则（7）表明注释必须引用实现中的现有操作（方法）。规则（8）代表Java类型规则的扩展，以确保在执行逆向工程时，使用CincoSecurity的任何实现仅产生有效模型此规则指示每个Restrict注释的字符串必须包括角色名称和操作名称，并且操作名称必须与注释引用的操作对应定义4.10CincoSecurity往返方案是一个元组gcs，rcs，Kcs，Tcsgcs（PQOp，PQp）=PQOpcs，AcsPQp，使得（一）IOpcs=斯托普山|op∈Op⎫⎪⎬⎪⎩∧¬∃⟨op,t´⟩∈IOps.tt t ´⎪⎭（二）（三）（四）（五）A cs={RRestrict，op，[r]_[op] R}|r，oprecs是逆向工程映射recs（ΔIOp，ΔOp）=ΔOp，ΔOp，使得Op cs={op |op，tP cs={\r\，op\r}|<$Restrict，op，[r]_[op]<$∈ A}Kcs是模型有效性的一组约束条件Kcs={k_r，op_r ∈Pcs op∈Opcs}并且Tcs是一组类型规则Tcs={tr1，tr2，tr3}，其中（六）（七）tr1=op，t∈IOp<$op，t′∈IOpcs，t=/t′tr2=a，op，v∈Acs op，t∈IOpcs（八）tr3=∞Restrict，opi，[r]_[opj]∞∈Acs，opi=opj要为上述往返方案提供安全保证，必须证明这是正确的定理4.13是定理3.7的应用，证明了定义4.10的方案的正确性。为了便于证明，引理4.11证明了代码生成映射gcs的正确性，引理4.12证明了逆向工程函数recs的正确性。J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）8391⟨⟩⟨⟩引理4.11对所有有效模型m=Op，P在K cs下，g cs（m）在T cs下是良型的。为了证明gcs（m）在Tcs下是良型的，首先必须证明：gcs（m）满足Tcs中的每个约束。• 根据（1），IOpcs是op，t形式的元组的集合，其中没有两个元组具有相同的op。因此，满足Tcs的规则（6）92J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）83⟨ ⟩ ⟨⟩∈∈ ⟨ ⟩ ∈• 根据（2），Acs是Restrict，op，[r]_[op]形式的元组的集合，其中r，op属于m的策略P。由于m满足Kcs（5）的约束，P中的所有运算op也属于Op。因此，对于生成的注释中的所有op，Restrict，op，[r]_[op]，op∈IOpcs，满足Tcs的规则（7）。• 根据（6）、（5）和（2），规则（8）也得到满足。Q引理4.12对于T cs下的所有良类型实现II，recs（I）是K cs下的有效模型。为了证明recs（I）的有效性，必须证明recs（I）满足Kcs（5）中的约束根据（3），对于每个op，t IOp，存在操作op Opcs。由于I满足（7）和（8），从（4）可以得出，Pcs中的所有运算op也属于Opcs，它满足Kcs中的约束。Q定理4.13 CincoSecurity的往返方案是正确的。证明 直接从定理3.7，引理4.11和4.12。Q5相关工作有几个作品将访问控制纳入软件。在设计层面，UMLSec [28]，AuthUML[6]，Doan等人[17]提出了对UML的扩展，以建模RBAC，MAC或两者的不同方面。Song等人[45]和Mouheb等人[32]定义面向方面的机制来转换软件模型，以纳入访问控制需求。这些工作都没有解决从模型规范生成安全代码的问题。在代码层面，也有几项工作。Farias [21]，Evans et al. [20]、Pandey等人[37]和Erlingsson等人[19]提供了不同平台中的编译过程，以纳入安全前提检查。类似地，Mourad等人[33]，Alhadidi等人[7]，Bodkin [11]，Dantas [14]，De Win [15]，Huang等人[27]，Shlowikowski等人[44]，Sewe [43]和Viega等人[50]使用面向方面的编程来限制基于权限的访问诸如JPA Security[2]、FleXive [1]和Seam [48]等框架提供了Java EE中的访问控制机制。Centonze等人[12]和Fischer等人[22]提供了验证Java EE中访问控制策略一致性的方法。这些方法都没有提供从RBAC、MAC或DAC中的设计模型到代码的可跟踪链接，反之亦然。上面的大部分工作要么关注模型，要么关注代码，但不是两者都关注。唯一的例外是Basin等人的工作。[9]提供了将模型转换为代码和配置文件的机制。然而，他们的工作并没有提供任何逆向工程机制模型和代码之间的一致性问题可以推广到双向转换问题[13]。查询-视图转换语言（QVT）[36]提供了对双向转换的支持，然而，正如Stevens等人指出的[46]，QVT规范中有几个问题限制了其对模型同步的适用性。 Diskin等人[16]提供了双向转换的正式代数规范，重点是J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）8393模型同步DiskinFoster等人[23]提出了类似的工作，重点是双向树转换。Hermann等人[25]提出了一种基于三重图文法（TGG）的模型同步方法[42]。类似地，Anjorin等人[8]使用三重图语法来建模和编码，并将语法映射到元模型。Anjorin等人的方法在模型级使用TGG，并且元模型TGG是从模型级的TGG自动导出的。然而，这依赖于抽象语法树元模型是固定的假设[8]。这种假设在MDE环境中是无效的，因为需要为多种语言和平台生成代码[30，31，35]。最后，有几个工具支持通用模型的代码生成和反向工程[3，4，5]。据我们所知，没有明确解决往返工程中访问控制要求的工具。6结论和今后的工作提出了一种往返环境下访问控制模型和代码正确性的形式化证明方法。在使用CincoSecurity模块的案例研究中说明了其适用性。从案例研究中可以推断，所提出的方法是适用于代码生成和逆向工程映射，只要模型和代码是足够抽象的。因此，这是迈向访问控制的全功能往返工程机制的第一步正在进行的工作是开发一个概念验证原型，实现所有提出的形式化，自动检查访问控制代码的扩展类型规则未来的工作包括从模型中的约束和代码生成映射自动导出扩展的类型规则并验证正确性。这将需要探索证明助手和约束检查工具，这可能为这种应用提供基础这项工作的未来结果预计将有利于代码生成和逆向工程，提高安全性的定义往返工程方案。减少在映射中的信息的损失是预期的，以符合正确性条件。此外，由于扩展的类型规则与代码相关联，因此可以将它们合并到标准IDE工具中。这些工具中的自动打字规则验证预计将减少错误的可能性，从而改善整个往返过程。引用[1] [XieXive]-下一代开源内容存储库|www.juexive.org。 http://www.flexive。org/.[2] JPA安保http://jpasecurity.sourceforge.net/网站。[3] 博兰在一起http://www.borland.com/us/products/together/，2010年。94J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）83[4] Gentleware -商业模式：gentleware主页。http：//www.gentleware.com/，2010年。[5] IBMdeveloperWorks：Rationalrose.http://www.ibm.com/developerworks/rational/products/rose/，2010年。[6] K. Alghathbar和D. Wijesekera。AuthUML：一个三阶段框架，用于分析用例中的访问控制规范。2003年ACM安全工程正式方法研讨会论文集，2003年。[7] D. Alhadidi，N. Belblidia，M. Debbabi，and P. Bhattacharya. \\lambda\\ _saop：一个安全AOP演算。计算机杂志，2009年。[8] A. Anjorin，M. P Lauder，M. Schlereth和A.舒尔支持双向模型到文本转换。电子通信的东部，36，2011年。[9] David Basin，Jurgen Doser，Torsten Lodderstedt.模型驱动的安全性：来自UML模型访问控制基础设施。ACM Transactions on Software Engineering and Methodology，15（1）：39[10] D. 贝尔和L.拉帕杜拉安全计算机系统：数学基础模型。技术报告，Mitre公司，1975年。[11] R.博德金企业安全方面。在应用级安全研讨会的AOSD技术会议记录中，第9卷，2004年。[12] Paolina Centonze，Gleb Naumovich，StephenJ Fink，and Marco Pistoia.基于角色的访问控制一致性验证。2006年软件测试与分析国际研讨会论文集，ISSTA'06，第121-132页，美国纽约州纽约市，2006年ACM。ACM ID：1146253。[13] Krzysztof Czarnecki ， J.Foster ， Zhenjiang Hu ， Ralf Lämmel ， Andy Schürr ， and JamesTerwilliger.双向转 换：跨学科的 视角。在Richard Paige，编辑 ，Theory and Practice of ModelTransformations，Lecture Notes in Computer Science，第5563卷，第260- 269页中283. Springer Berlin/ Heidelberg，2009.[14] 丹塔斯分析函数式面向方面编程语言中的安全建议。普林斯顿大学博士论文，2007年。[15] B.德温通过面向方面的软件开发实现应用级安全。博士论文，计算机科学系，K.U.鲁汶，鲁汶，比利时，2004年。[16] Zinovy Diskin ， Yingfei Xiong ， Krzysztof Czarnecki ， Hartmut Ehrig ， Frank Hermann ， andFernando Orejas.从基于状态到基于增量的双向模型转换：对称情况。在Jon Whittle，Tony Clark和Thomas Kühne， 编辑，模型驱动 工程语言和系 统， 计算机科 学讲义第6981卷， 第304-318页。Springer Berlin/ Heidelberg，2011.[17] 唐端一个基于UML的软件安全框架。博士论文，康涅狄格大学，2008年。[18] 国防部 可信计算机系统评估标准。5200.28-标准 国防部，1985年[19] Erlingsson和Schneider安全策略的SASI实施：回顾。WNSP：新安全范式研讨会。北京：人民出版社，2000年。[20] 大卫·埃文斯和安德鲁·特威曼。灵活的策略导向代码安全。安全和隐私，IEEE研讨会，第0032页，1999年。[21] A.法瑞斯面向Java的安全问题。博士论文，Vrije Univeriteit Mushesel，2001年。[22] Je Escherey Fischer，Daniel Marino，Rupak Majumdar，and Todd Millstein.使用对象敏感角色的细粒 度 访 问 控 制 。 在 Proceedings of the 23rd European Conference on ECOOP 2009 - Object-OrientedProgramming，Genoa，第173-194页，柏林，海德堡，2009年。史普林格出版社ACM ID：1615197。[23] 作者：Michael B.作者：Jonathan T.作者：Benjamin C.皮尔斯和艾伦·施密特。双向树变换的组合器：视图更新问题的语言学方法SIGPLAN不。，40（1）：233[24] María Consuelo Franky Toro C和Victor Manuel。CincoSecurity：使用细粒度角色和安全配置文件自动化Java EE应用程序的安全性。International Journal On Advances in Security，4（3 and 4）：245[25] Frank Hermann，Hartmut Ehrig，Fernando Orejas，Krzysztof Czarnecki，Zinovy Diskin，andYingfei Xiong.基于三重图文法的模型同步正确性。在Jon Whittle，Tony Clark和Thomas Kühne，编辑 ， 模 型 驱 动 工 程 语 言 和 系 统 ， 计 算 机 科 学 讲 义 第 6981 卷 ， 第 668-682 页 。 Springer Berlin/Heidelberg，2011.[26] 休眠。 Hibernate持久性库。 2012. http://www.hibernate.org/网站。J.A. Pavlich-Mariscal等人理论计算机科学电子笔记292（2013）8395[27] M.黄角Wang和L.张某迈向可重用和通用的安全方面库。AOSD：AOSDSEC，第4卷，2004年。[28] J. Jurjens UMLsec：为安全系统开发扩展UML。2002年第五届统一建模语言国际会议[29] 史蒂文·凯利和尤哈·佩卡·托瓦宁领域特定建模：实现完整的代码生成。Wiley-IEEE Computer SocietyPr，第一版，2008年3月[30] 斯图尔特·肯特。模型驱动工程。计算机科学讲义第2335卷，第286-298页。Springer Berlin/Heidelberg，2002.[31] StephenJ. MELLOR 、 Kendall Scott 、 Axel Uhl 和 Dirk Weise 。 MDA 蒸 馏 。 Addison-WesleyProfessional，2004年3月。[32] Djedjiga Mouheb ， Chamseddine Talhi ， Vitor Lima ， Mourad Debbabi ， Lingyu Wang ， andMakan Pourzandi.将 安全 方 面 编织 到 UML 2.0 设 计模 型 中 。 在Proceedings of the 13th workshop onAmmon-oriented modeling，pages 7-12，Charlottesville，Virginia，USA，2009中。ACM。[33] 阿扎姆·穆拉德，马克-安德烈·拉弗迪埃，穆拉德·德巴比。一个用于软件安全加固的高级面向方面的框架。Information Security Journal：A Global Perspective，17（2）：56，2008.[34] OMG. UML 2.0超结构。 技术报告，对象管理组，2005年。[35] OMG.模型驱动架构（MDA）。http://www.omg.org/mda/，2009年。[36] QVT OMG。Meta object facility（MOF）2.0查询/查看/转换规范。技术报告，2008年。[37] R. Pandey和B.桥井通过二进制编辑为移动程序提供细粒度访问控制。技术报告TR-98-08，1998年。[38] J. A. 放大图片作者：Steven A.Demurjian，and Laurent D.米歇尔可组合访问控制特性的框架计算机安全，29（3）：350[39] J.A.帕夫里希-马里斯卡尔一个可组合安全特性的框架：保持安全关注点从模型到代码的。博士论文，康涅狄格大学，2008年。[40] J.A. 放大图片作者：Steven A.Demurjian，and Laurent D.米歇尔访问控制执行代码安全保证框架计算机安全，出版中，接受Mandarin，2010。[41] R. Sandhu，D. Ferraiolo和R.库恩。NIST基于角色的访问控制模型：迈向统一标准。第五届ACM基于角色的访问控制研讨会论文集，2000。[42] 安 迪 · 舒 尔 和 菲 利 克 斯 · 克 拉 15 年 的 三 重 图 语 法 。 在 Hartmut Ehrig ， Reiko Heckel ， GrzegorzRozenberg和Gabriele Taentzer，编辑，Graph Transformations，计算机科学讲义第5214卷，第411-425页。Springer Berlin/ Heidelberg，2008.[43] Sewe，Bockisch，and Mezini.方面和基于类的安全性：建议编织和java 2安全模型之间的交互调查在VMILACM。[44] P. Shlowikowski和K.Zielinski。面向方面安全与容器管理安全的比较研究AAOS2003：面 向 方面软件的分析。20 0 3 年与ECOOP合作举办讲习班。[45] E.歌一种基于方面的访问控制策略建模方法。博士论文，科罗拉多州立大学，2007年。[46] 珀迪塔·史蒂文斯QVT中的双向模型转换：语义问题和开放问题。 Gregor Engels，Bill Opdyke，Douglas Schmidt ， and Frank Weil ， editors ， Model Driven Engineering Languages and Systems ，Volume 4735 ofLecture Notes in Computer Science，pages 1-15. Springer Berlin/ Heidelberg，2007.[47] 太阳 Java EE。http://java.sun.com/javaee/，2010年。[48] 接缝JBoss团队Seam框架-API和参考文档。http://seamframework.org/Seam3/APIAndReferenceDocumentation的网站。[49]ATIS Telecom. 2000年词汇表。T1.523-2001。2001年[50] J. Viega，J. T. Bloch和P.钱德拉将面向对象的编程应用于安全性。Cutter IT Journal，2001年。