理论计算机科学电子笔记180（2007）17-34www.elsevier.com/locate/entcs异步顺序进程的安全信息流Isabelle Attali、Denis Caromel、Ludovic Henrio1和Felipe Luna Del AguilaINRIA Sophia Antipolis，CNRS - I3S - Univ. Nice Sophia Antipolis2004，Route des Lucioles，BP 93-F-06902 Sophia Antipolis Cedex，France{ia@ sophia.inria.fr摘要本文提出了一个在ASP（异步顺序进程）框架下的数据保密的精确安全模型ASP是基于活动对象、异步通信和数据的.流同步。我们扩展了它的安全级别附加到活动（活动对象）和传输的数据。我们设计了一个安全模型，保证应用程序中的数据机密性;这个安全模型同时利用了强制和自主访问模型。我们扩展了语义的ASP谓词条件，提供了一个正式的安全框架，动态检查未经授权的信息流。最终，所有授权的通信路径都是安全的：不会发生任何信息泄露。这种理论上的贡献可能会对基于分布式对象的应用程序产生强烈的影响，这些应用程序在Internet上越来越多，并且对机密性要求越来越高，它也会引起数据机密性的新问题：安全信息的授权和传输（通过期货的意思）通过无担保的组件。关键词：访问控制，分布，对象，未来。1介绍这项工作的主要贡献是为异步分布式基于对象的应用程序提供数据确认和安全的信息流所提出的安全模型严重依赖于具有强制执行的安全策略规则来控制信息流。虽然信息流通常是静态验证的[20，3，15，14，25，22，16，10]，但我们的注意力集中在动态验证上。为了实现这一点，我们的模型有一个信息控制策略，其中包括自由裁量的规则，因为这些规则本质上是动态可执行的，我们可以利用动态检查来同时执行所有强制性检查。1 威斯敏斯特大学-哈罗计算机科学学院-哈罗，HA 1 3 TP（英国）1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.04518I. Attali等人/理论计算机科学电子笔记180（2007）17作为这种方法的另一个优点，动态检查不需要修改编译器，不需要改变编程语言，不需要修改现有的源代码，并在运行时提供可扩展性。因此，动态检查很适合中间件层，以非侵入性的方式为上层应用程序提供并确保安全服务。我们的底层编程模型[8]基于活动对象、异步通信和数据流同步。在安全方面，安全级别用于独立标记通信事件中涉及的实体：活动对象和传输的数据。然而，这些强制性规则和自由裁量规则相结合，可以放松强制性规则所施加的严格控制概述由于活动不共享内存，我们的安全机制将安全级别与每个活动相关联此外，级别可以与活动之间传输的数据（请求参数和创建的活动）相关联。我们的机制是基于从Bell-LaPadula [ 4 ]模型中获得的“不写”和“不读”的严格概念动态检查在活动创建、请求和应答通信时执行。这种方法的优点有两方面：坚实的基础该安全模型建立在强大的理论背景上，即ASP演算[7，6]，与众所周知的形式主义[14，13，10，9]相关。我们用谓词条件扩展了ASP的形式语义。这为我们的模型提供了一个形式化的基础，并使得动态检查未经授权的访问成为可能。最后，为了证明安全模型的正确性，定义了一个直观的安全信息流性质，并证明了该性质是通过应用访问控制模型来保证的。可扩展性和可扩展性。我们还针对此模型的实际使用，并将其实现到中间件中，例如ProActive [21]。我们定义安全模型的粒度是为了使其既有效（因为活动内部没有安全检查）又可微调：级别可以在活动上定义，但可以为通信数据提供特定级别这项工作的影响在于最近的变化，在分布式计算领域的范例。ASP面向服务的特性使得通信不对称（请求和应答）和异步。据我们所知，这一安全框架是第一个适应这些通信具体情况的框架。这项工作揭示的主要新问题之一是第一类期货的情况（期货是答复的承诺），以及一些安全信息流，在其他安全框架中是不可能的，可以设想安全的异步服务。I. Attali等人/理论计算机科学电子笔记180（2007）1719a，b∈L* *=x| [l i= b i; m j=<$（x j，yj）a j]i∈1.. nj ∈1..M|a.l i| a.l i：= b|a. mj（b）| 克隆（a）| 活性（a，m j）| 发球（m1，..， mn）n>0| ι| a、b变量，对象，字段访问，字段更新，方法调用，表面复制，对象激活、服务原语、位置（不在源代码中）。a，续设b第2节回顾了对象和通信的基本模型。第3.1节介绍了一个可以为ASP实现的访问控制模型部分3.2定义并验证了直观的安全信息流属性：如果所有活动创建、请求和回复传输都是安全的，则信息流是安全的。第3.3节分析了面向服务计算的安全模型的特性接下来，在第4节中讨论与现有工作的关系。附录给出了一个示例，展示了我们能够确保的安全策略类型以及我们模型的具体性。2对象和通信分布在（单线程）活动上，没有共享内存。活动通过异步方法调用进行通信，并通过future进行响应，从而导致数据流同步。Futures允许延迟隐藏而不会丢失，既不容易编程也不高效。本文将对这种最新的编程方法（异步面向服务编程）的信息流2.1分布式对象模型ASP演算是异步通信进程占优势的Imp演算[1]的扩展。这些流程或活动并行运行，但其内部操作按顺序执行使它突出的是活动对象、必要性等待和未来的概念。活动对象是一个表1给出了ASP语言的语法。用于语义描述的经典顺序归约规则可以在[7]中找到。表1ASP演算语法重要的是要注意，一个活动只由一个主动对象组成，许多被动对象（即，经典的）对象以及对其他活动对象的许多引用作为示例，图1显示了活动α和β，其中活动α（以及其他实体）具有自己的主动对象、两个被动对象和对活动β的引用。此外，没有共享内存：被动对象只能被引用20I. Attali等人/理论计算机科学电子笔记180（2007）17我我但是任何对象都可以引用一个活动对象。ASP的主要贡献之一是形式化的未来和请求-应答通信模式。Future是表示回复承诺的广义引用，可以作为经典对象进行操作（即在活动内部和活动之间复制和传输），而不需要它们的真实值。需要对象值的操作（例如字段访问）将被阻止，直到必要的回复出现。这种自动和透明的同步机制称为按需等待。Fig. 1.并行配置回顾ASP语法和语义，并行配置是以下f的活动集合（α，β，γ∈Act）： P，Q：=α[a;σ;i;F;R;f]β[· · ·]···其中a是要缩减的当前项;σ是包含属于活动α的所有对象的存储;i是活动对象位置;F是将所服务的请求的每个结果与其未来相关联的列表;R是未决请求的列表;并且f是当前任期的未来。附加的语义符号是：位置i和未来标识符fi是活动本地的;未来fα→β根据请求由标识符fi、对活动α的活动对象的引用用AO（α）表示;对未来的引用用fut（f α→β）表示。非正式地，ASP语义在于将对象划分为由单个线程操作的不同活动（没有共享内存这些活动通过异步请求-响应机制进行通信：当一个对象执行一个方法调用一个活动对象（即，远程对象），则请求在被调用方排队I. Attali等人/理论计算机科学电子笔记180（2007）1721我我我（a，σ）→S（AJ，σJ）→S不克隆未来α[a;σ;i;F;R;f]<$P−→α[aJ;σJ;i;F;R;f]<$Pγ新鲜活度<$J/∈dom（σ）（当地）σJ={iJ<$→AO（γ）}：：σ σγ=copy（iJJ，σ）α[R[Active（iJJ，m）];σ;i;F;R;f]<$P−→（nEwact）α [R [iJ];σJ;i;F;R;f] γ [iJ J]。mj（）;σγ;iJj;]PJσα（i）=AO（β）<$JJ/∈dom（σ） fα→β新未来β我If/∈dom（σα）σJ=CopyMerge（σα，iJ;σβ，iJJ）βσJ={i›→fut（fα→β）}：：σααF我（答复）α [R][i]。mj（iJ）];σα;iα;Fα;Rα;fα]<$β[aβ;σβ;iβ;Fβ;Rβ;fβ]<$P−→α[R[i];σJ;iα;Fα;Rα;fα]<$β[a;σJ;i;F;Rfαββββjβ：：[m;iJJ;fα→β];f]αP我βR=RJ：：[mj;<$r;fJ]：：RJJmj∈M<$m∈M，m∈/RJα[R[Serve（M）];σ;ι;F;R;f]<$P−→α[1]。mj（ir）<$f，R[[]];σ;i;F;RJ：：RJJ;fJ]<$P（sERvE）IJ/∈dom（σ） FJ=F：：{f<$→IJ}σJ=CopyMerge（σ，i;σ，iJ）（EndsERvICE）α[i<$fJ，a;σ;i;F;R;f]<$P−→α[a;σJ;i;FJ;R;fJ]<$Pσα（i）=fut（fγ→β）F（fγ→β）=i J我β我Fσ=Copy&Merge（σ，i;σ，i）αβfα（reply）α[aα;σα;ια;Fα;Rα;fα]<$β[aβ;σβ;ιβ;Fβ;Rβ;fβ]<$P−→α[aα;σJ;ια;Fα;Rα;fα]αβ[aβ;σβ;ιβ;Fβ;Rβ;fβ]αβα调用者接收一个future（一个空对象，将用请求的结果填充）。表2平行还原2.2通信模型ASP通信模型基于表2中所示的并行归约规则。这些规则基于执行深度复制的复制（i，σ）以及CopyMerge（σβ，iJ;σα，i），其在存储σα的位置i处附加在位置iJ处开始的存储σβ的深度副本。在这些归约规则中，只有通信规则（newact、request和reply）涉及安全框架。newact归约规则创建一个新的Activityγ，其中包含对象的深层副本。对这个活动AO（γ）的广义引用存储在源活动α中。在请求缩减规则中，Activityα向Activityβ发送新请求。 新请求[mj;iJJ;fα→β]由目标方法mj、参数的位置iJJ在请求消息中传递，以及未来标识符fα→β，它将与请求产生的响应相关。 注意，在位置Ijj中，传递给目标方法的参数的副本。回复缩减规则，一个对未来的引用，并用它的值更新它对未来的参考必须存在于一个活动α中，相应的价值必须在另一个活动β中计算出来。请注意，未来的fγ→β可以在活动差异中更新从请求的起源（γ α）开始。22I. Attali等人/理论计算机科学电子笔记180（2007）173安全模型在本节中，我们定义了一个安全模型，该模型保证了多级安全系统的数据机密的经典属性：具有适当权限的特定用户将仅被授予访问他/她被允许处理的信息的权限。这种数据保密的概念不能与加密机制提供的保密（即信息模糊）混淆。安全术语使用主体-对象关系[24]，并且因为“对象”一词在我们首先回顾访问控制模型的通常概念，并根据实体和安全通信定义我们的模型;这意味着我们正式将ASP扩展为安全ASP。然后，我们提出了活动之间的安全信息流的概念，具有数据保密的重要属性。最后，我们指出了面向服务的计算的3.1访问控制模型访问控制模型通常分为强制性（MAC）和自主性（DAC）模型。MAC模型可以通过多级安全（MLS）模型来最好地描述，该模型基于分配给子节点和目标的安全级别的网格。一旦级别被分配，“普通用户”和进程都不能MLS模型适合于解决信息流中的保密问题，但其不便之处在于，在某些情况下，它不足以满足实际系统的要求。DAC模型基于一个访问控制矩阵，该矩阵将主体的权限与目标相关联，其中权限可以由“正常用户”或其进程“自行决定”分配我们提出的解决方案是基于MLS的概念，类似的概念我们首先描述我们的安全框架中涉及的所有实体• S是作为主体和/或目标的活动的集合：α，β，γ，. ∈ S;• D 是 在 REQUESTS 的 参 数 中 发 送 的 对 象 的 集 合 ;REQUEST 现 在 被 Rqα→β（d），其中d=σα（iJ）∈ D，• R是与future相关联的对象的集合，并在REPLIES中返回; REPLIES现在写作Rpβ→α（r），其中r=σ β（i f）∈R。设A是安全机制中涉及的动作的集合，即，请求，居住和新闻。以下符号被添加到ASP：• 安全级别λ取自有限集合L，由以下关系部分排序：≤，λi∈S <$D <$R，λi∈ L，• T S × S × A表示授权的动作（源、目的地、动作），I. Attali等人/理论计算机科学电子笔记180（2007）1723• 矩阵M：S × S→P（A）给出了为给定动作的给定数据分配水平的显式（自由裁量）权利。对于每一对主体-目标，矩阵包含一组授权行动，涉及指定安全级别。P（A）经典地表示动作集合的集合。经典的主体-目标-动作矩阵被扩展为包括（允许的）安全级别。该矩阵可以是使用安全策略文件实现（例如XACML策略文件[11]）。这导致了以下行为特征• Nw（γ，λγ）是修改的活动创建规则（NEWACT），以便为创建的活动γ分配安全级别λγ，• Rqα→β（d，λin）是修改后的REQUEST传输规则，用安全级别标记传输的数据（程序员为数据d提供安全级别），• Rp β→α（r）是一个与原始ASP相同的REESTs传递规律。总而言之，a∈ A当且仅当a=Rqα→β（d，λin）<$a=Rpβ→α（r）<$a=Nw（γ，λγ）。此外，准确地说，M只有REQUEST或NEWACT中的值这就是说，在我们的模式中，不可能给予答复一种酌处权。主体、目标、数据和响应的安全级别反映了活动处理图2显示了这种形式的通信。所有Activity都标记有安全级别，其中包含的所有对象及其方法将自动继承该级别（a和b是对象，ms是源Activity的调用方法，mt是目标方法）。请求传输中使用的每个数据d也标记有安全级别，但该级别独立于源活动的级别。主题目标图二、安全标记的活动之间的通信程序员负责为数据d分配安全级别。因此，传输数据的级别将被添加到方法调用的语法中（见表3）。即使在下面没有详细描述，默认行为也应该包括将发送者活动的级别分配给作为请求参数发送的数据d。反过来，在回复传输中返回的每个值r将自动标记目标方法的安全级别（从活动继承的级别）。这种形式的标记允许输出数据在处理方法中独立于输入数据，换句话说，输出数据的安全级别不取决于输入数据的级别，而是取决于数据本身的处理然后根据我们的通信策略推导并形式化ASP中安全通信的条件： SM不x=b.m（tdh）d处理数（任务）勒维特一个小女孩24I. Attali等人/理论计算机科学电子笔记180（2007）17我我我我定义1（安全活动创建）<$α，γ∈S，（α，γ，Nw（γ，λγ））∈T <$$>（λα≤λγ）<$Nw（γ，λγ）∈ M（α，γ）如果活动创建的级别大于或等于源活动的级别，则活动创建Nw（γ，λγ）被授权。否则，如果α想要降级数据（即，对象），则必须存在允许这种操作的显式权限定义2（安全请求传输）<$α，β∈S，（α，β，Rqα→β（d，λin））∈ T惠0（λin≤λβ）<$1（（λα> λin）<$Rqα→β（d，λin）∈M（α，β））@λ（λα ≤λin）Afγ，δ，fi，d=fut（fγ→δ）如果所传输的数据d的安全级别λin小于或等于目标活动β的安全级别λβ，则请求传输Rqα→β（d，λin）被授权;或者，当具有级别λα的源活动α试图向数据d分配级别λin（即，数据降级）时，存在显式权利（自由裁量规则M（α，β））安全请求传输背后的哲学是只向持有适当许可的目标提供信息。如果数据λin的安全级别大于或等于源λa的安全级别，我们也有一个安全的请求传输。在这种情况下，我们有λα≤λin≤λβ，表明活动α安全地释放数据d，因为d具有更高的安全级别，并且在同时，活动β接收较低级别的数据。此外，当将未来参考fut（fγ→δ）作为数据处理时，也实现了安全的请求传输。未来的引用可以在活动之间自由传输，因为它们不包含任何有价值的信息。我们回顾，关联到期货持有信息，但期货引用仅持有指向期货的地址或方向。从这个意义上说，如果未来引用是已知的，这并不意味着我们可以直接获得未来值，因为无论如何，未来值传输将由安全应答传输执行并提交给安全应答传输的安全规则。定义3（安全回复传输）<$α，β∈S：（α，β，Rpβ→α（r））∈T<$α（λβ≤λα）<$（<$γ，δ，fi，r=fut（fγ→δ））如果目标β的安全级别λ β小于或等于主体α的安全级别λ α，或者如果所发送的结果r仅由对未来f γ→δ的引用组成，则授权安全应答传输REFRp β → α（r）。表3显示了安全ASP演算和原始演算（表1）之间的差异：安全信息被添加到激活和方法调用项中在为每个活动附加安全级别后，现在可以进行并行配置：P，Q：：=αλα[a;σ;i;F;R;f]βλβ[· · ·]· · ·最后，表4给出了安全并行ASP演算的语义这些语义规则保证了信息流的安全。他们利用安全信息I. Attali等人/理论计算机科学电子笔记180（2007）1725γ新鲜活动<$J/∈dom（σ）σJ={<$J<$→AO（γ）}：：σσγ=copy（<$J，σ）（α，γ，α[R[Active（i，m）];σ;i;F;R;f]<$P−→λλJJ（SecnEwact）一Jαλ [R [iJ];σJ;i;F;R;f]<$γλa[iJ J]。mj（）;σγ;iJj;]Pσα（i）=AO（β）ιJJ/∈dom（σ）fα→β新的未来If/∈dom（σα）σβ=复制合并（σα，1;σβ，1）Jβ我JJJσJ={i›→fut（fα→β）}：：σααf我（α，β，Rq→（σ（i，J），λ））∈Tα βα in（第二次要求）αλα[R [i. mj（iJλin）];σα;iα;Fα;Rα;fα]<$βλβ[aβ;σβ;iβ;Fβ;Rβ;fβ]<$P−→α[R[i];σ;i;F;R;f]β[a;σ;i;F;R ：：[mj;iJJ;fα→β];f]！CUPλαJλJfααααβαβ ββ ββ我βσα（i）=fut（fγ→β）F（fγ→β）=iσJ=CopyMerge（σ，i我β我Fαβf;α）（β，ασ，ι，Rp σ（i））∈Tβ→α（βFαλα[aα;σα;ια;Fα;Rα;fα]<$βλβ[aβ;σβ;ιβ;Fβ;Rβ;fβ]<$P−→（秒回复）α[a; σ; i; F; R; f]β[a;σ;i;F;R;f]PλαJλα αα ααβαββββββa，b∈ LJ：：=a. mj（bλin）| 有效λa（a，mj）| . . . ...这是什么？方法调用，对象激活，表3安全ASP演算：修改的原语表4安全并行归约规则附加到激活和方法调用项（Nw（γ，λa）和Rqα→β（d，λin）规则中的λa和λin），以验证之前定义的安全传输和活动创建（定义1，2和3）。当通信未被授权时，从形式上看，它只是被封锁了。在实践中，应提出并适当处理专门的例外。3.2对象模型中的安全信息流我们正式定义了活动之间信息流的概念所考虑的实体是活动及其被动对象，而不是被动对象本身。由于活动可以分布，因此与非干扰相关的概念[12]不能直接应用于我们的模型。其次，用路径来描述系统范围内的信息流，路径是信息传播的路径，它由一系列通信活动构成，其中主体活动是路径的起点，目标活动是路径的终点在每一个活动中观察到的每一个信息传递都将用于构造一条路径，这条路径将被称为下行路径。流路径fp是活动列表（fp：=1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.···）。它们由给定信息流的中转活动例如，δγ.δ（α，β）表示某些信息通过活动γ和δ从活动α传递到活动β。下行路径fp和fpJ的级联由fp.fpJ表示。通 过 将安全机制应用于非安全信息流，路径，第一个属性结果：如果所有活动创建，请求和回复传输，则26I. Attali等人/理论计算机科学电子笔记180（2007）17是安全的定义4（安全信息流）基本的信息流要么基于请求的发送，要么基于回复的发送，要么基于活动的创建。信息流是由若干基本信息流依次组成的。任何信息流的中间路径都是中间活动的串联，它允许我们检索原始的基本信息流。安全信息流是由基本的安全信息流串联而成的，这些基本的安全信息流是安全通信：安全请求、安全应答或安全消息。形式上：（α，β，Rqα→β（σ（ιJ），λin））∈TSecε（α，β）（β，α，Rpβ→α（σα（ιf）∈ TSecε（β，α）（α，γ，Nw（γ，λγ））∈TSecε（α，γ）Secfp1（α，γ） Secfp2（γ，β）Secfp1.γ.fp2（α，β）以下属性声明，当且仅当满足以下条件时，信息流才是安全的它遵循一条安全的路径。属性（信息流的安全路径）当且仅当信息流由基本安全信息流组成时，信息流才是安全的。Secγ1·· ·γn（α，β）<$$> Sec（α，γ1）<$Sec（γ1，γ2）<$· ··<$Sec（γn，β）这一性质的证明是直接的;它是通过对信息流路径长度的归纳和对定义4的规则的案例分析得到的。该属性没有利用我们模型的MAC方面。 实际上，使用纯DAC方法可以获得相同的属性。这一属性表明，我们对信息流的特定和某种程度上限制较少的定义不会损害安全的信息流。使用我们的安全策略的MAC方面的安全信息流属性超出了本研究的范围。更一般地说，研究强制性与自由裁量规则与Bertino等人的工作密切相关。[5]。与其它方案相比，我们的安全信息流是一个复杂的基本流的简单组合这是由于安全形式主义适应了特定的面向服务的框架。基本流程的复杂性来自ASP通信的不对称和异步特性一旦确保了这种基本的安全通信，信息流的安全性就可以以简单直观的方式得到验证。因此，安全信息流的可靠性是由前一节中对信息的精确定义以及第3.1节中定义的安全通信确保每个信息流必须验证安全策略的事实来确保的。还要注意的是，我们的自由裁量权矩阵的构建方式允许我们设想一个关于所涉及的（动态）实体的精确调优，以及在降级时可以分配给数据的级别。I. Attali等人/理论计算机科学电子笔记180（2007）1727223.3面向服务计算前面的部分展示了如何将经典的MAC和DAC安全原则适应ASP并进行扩展，最终确保可扩展性和可扩展性。未来引用是第一类对象，可以在活动之间传递（称为自动延续的功能），因此它们对信息的安全流有重要的影响。事实上，如果没有自动延续，一串回复将直接遵循与一串请求相反的路径换句话说，在经典的强制规则系统中，请求-应答通信模式只能发生在具有相同安全级别的实体本文件的第一个贡献是授权对这些关于请求传输的数据级别的规则的酌情例外这允许在请求发送非机密数据时出现某种请求-应答模式活动对象要求活动对象要求活动对象AO（AOAO（）F2f1f图三.一个典型的例子：授权传输未来引用的可能性导致了一个非常适合面向服务计算的模型。让我们关注图3的配置。这种配置可以通过一个经典的场景来获得：β向γ（未来的f2）发出请求;但β只是一个中间人，并委托δ负责计算最终结果（未来f J）。 假设λ δ≤ λ β<λ γ，即也就是说，中间活动γ具有（太）高的安全级别（这可能是委托请求的原因）。如果没有自动延续，γ就不能返回future f2的值，因为它是对fj的future引用。无论如何，δ可以回复γ（因为λ δ<λ γ），但γ不能将这个结果值转发给β，因为λβ<λ γ。实际上，将结果从δ传递到β的推导不能由前述规则推导（不能应用未经授权的均值归约规则）：λδ<λγ（δ，γ，Rpδ→γ（result））∈TSec（δ，γ）没有授权（γ，β，Rpγ→β（RJ））∈/TSecondarybonemarrowtransplantation（γ，β）Secγ（δ，β）我们可以期待一个更好的行为，因为从δ到β的直接回复应该根据安全模型进行授权：δ不能回复只是因为有一个中间活动γ。实际上，如果请求在γ之前没有被传递，28I. Attali等人/理论计算机科学电子笔记180（2007）172将被授权。这就是为什么安全通信规则规定，未来可以自由传输（记住，未来不包含有价值的信息）;因此，如果响应仅限于未来引用，则γ可以回复β之后，δ可以直接回复β，因为λ δ≤λ β，而β获得与f2相关的实值。r=fJγ→δ（γ，β，Rpγ→β（r））∈TSecondarybonemarrowtransplantation（γ，β）λδ≤λβ（δ，β，Rpδ→β（r））∈T秒速时时彩（δ，β）这个例子证明了自由传输未来引用的可能性，并展示了一种通信模式，如果没有未来的表达性和我们机制中存在的特定安全规则，这种通信模式是不可能的。然而，在ASP中，未来更新发生的顺序对程序的执行没有影响，这个例子表明，在安全ASP中，采用方便的未来更新策略是很重要的。4相关工作Henessy和Riely提出了π演算的扩展[18，19]，这是一种针对分布式系统的演算，通过使用（安全）类型进行扩展[14]。我们不使用显式通道进行通信，但读和写操作类似于接收或发送请求和回复（当接收到请求或回复时读取，当发送请求或回复时写入）。此外，它们的过程可能与我们的活动类似，但一般来说，安全策略是不兼容的，即使使用类似的概念，它们也不能在我们的模型中编码。Bertino等人[5]处理面向对象系统中基于异常的信息流控制。他们扩展了Jajodia，Kogan，Sandhu [17]和Samarati等人[23]的密切工作，以包括严格的安全策略通常不允许的操作（异常）。它们使用ACL（自主控制）对写和创建操作进行操作，并且在允许的例外情况下，它们放松了对这些操作施加的严格策略。使用例外来改变[5]的严格适用强制性规则类似于我们框架中的自由裁量条件。这两种机制都允许人们绕过严格/强制性访问控制的严格应用。Attali、Caromel和Contes提出了高级规则，这些规则定义了基于主动式的GRID应用程序的安全策略[2]。它基于一种自行酌定的方法，其中实体遵循等级结构并依赖于公钥基础设施。相比之下，我们的工作只关注通信行为，研究信息流中的保密性，具体到面向服务的应用程序，并使用自由裁量和强制性的方法。在实践（实现）方面，包含信息流控件的类Java语言（如[3，20]）可以与我们的模型互补。它们控制程序内部的信息流，因此它们可以被增强以控制与分布式或协作系统中的其他本地和非本地程序的所有通信交互。I. Attali等人/理论计算机科学电子笔记180（2007）1729与以前的工作相比，定义1和2将独立的强制性和自由裁量控制组合在一起，但仅在传输涉及数据降级情况时才评估自由裁量这并不代表策略执行的标准方式，因为我们还能够验证新活动（即封装数据的整个实体）和单个传输数据（即在请求中发送的数据）的安全级别。此外，定义4隐含地基于Bell-LaPadula模型，其中运行时的安全性考虑具有初始安全状态的状态机，并且如果不违反访问规则，则其从状态到状态的转换是安全的5结束语和今后的工作针对ASP中的安全信息流，提出了一个精确的安全模型该解决方案主要基于三个基石：信息流的概念、活动的安全级别以及适用于所有通信的安全规则的定义。安全策略（涉及安全级别的分配、使用和定义）也考虑了我们模型中处理信息的方式。当涉及机密性时，可能存在需要与低级别活动通信的高级别活动（通常被“不写”的强制性访问规则拒绝）。因此，通过用安全级别标记数据，我们获得了灵活性，因为强制性规则没有被打破，并且仍然在广告自由裁量规则的帮助下，我们保证这种行为是明确允许的。然后根据特定的安全规则控制通信。在强制性规则的情况下，这些规则是预先定义的，其中总是比较和应用流程和数据的安全级别;在判断性规则的情况下，它们是外部定义的（例如，在描述整个系统的权限的文件通过允许任意例外的强制性规则，我们得到了一个高度表达的系统。因此，由于我们没有利用我们模型的MAC方面，因此所得到的属性相当弱;然而，通过对DAC规则施加一些一致性要求，可以保证更强的属性最后，我们展示了我们的安全机制的特性：它在面向服务的计算中的应用，通过期货的方式进行回复，以及我们的通信机制所产生的具体问题该安全模型的原型已经在用于分布式和移动（网格）计算的主动中间件[21]中实现，并且目前正在对真实大小的示例进行可扩展性和可扩展性的评估。在未来，计划研究更具体的移动性方面，并使用基于角色的访问控制（RBAC）方法，以扩展和改进对活动的自主访问。30I. Attali等人/理论计算机科学电子笔记180（2007）17引用[1] 马丁·阿巴迪和卢卡·卡德利对象的理论。Springer-Verlag，1996.[2] Isabelle Attali，Denis Caromel，and Arnaud Contes.网格应用程序的层次和声明式安全性。高性能计算国际会议，HIPC，印度海得拉巴，12月17-20日，Springer Verlag，2003年。计算机科学讲义。[3] Anindya Banerjee和David A.瑙曼用类java语言实现安全信息访问控制第16届IEEE计算机安全基础研讨会（CSFW-16），2003年7月。[4] David E.作者声明：by Leonard J.安全计算机系统：统一的解释和多元解释。技术报告MTR-2997版本1，MITRE Corporation，Bedford，MA，1976年3月。[5] 埃莉萨·伯蒂诺，萨布丽娜·德·卡皮塔尼·迪·维默卡蒂，埃琳娜·法拉利，和皮安杰拉·萨马拉蒂。面向对象系统中基于异常的信息流控制。ACM Transactions on Information and System Security（TISSEC），1（1）：26[6] 丹尼斯·卡罗梅尔和卢多维克·亨里奥。分布式对象理论。Springer-Verlag，New York，2005.[7] 丹尼斯·卡罗梅尔，卢多维克·亨里奥，伯纳德·塞尔佩特。异步和确定性对象。第31届ACM SIGPLAN-SIGACTSymposium on Principles of Programming Languages，POPL 2004，第123-134页。ACM Press，2004.[8] 丹尼斯·卡罗梅尔，威尔弗里德·克劳泽和朱利安·维西埃尔java中的无缝计算和元计算。Concurrency：Practice and Experience，10（11-13）：1043[9] 阿 戈 斯 蒂 诺 · 科 尔 特 斯 和 里 卡 多 · 福 卡 迪 。 移 动 环 境 中 的 信 息 流 安 全 在 国 际 并 发 和 协 调 研 讨 会（ConCoordElsevier，2001年7月。[10] Silvia Crafa，Michele Bugliesi，and Giuseppe Castagna.信息流在盒装环境中的安全性电子笔记在理论计算机科学，卷66：3。Elsevier，2002年。[11] 可扩展访问控制标记语言。http://www.oasis-open.org/committees/tc_home.php? wg_焦距v =xacml.[12] 里卡多·福卡迪和罗伯托·戈列里。证券财产的分类（第一部分：信息流程）。在安全分析和设计的基础（FOSAD2000）-计算机科学讲义第2171卷，第331-396页。Springer-Verlag，2001.[13] 马修·亨尼西安全性和不干涉性。Journal of Logic and Algebraic Programming，2003。出现。[14] 马修·亨尼西和詹姆斯·莱利异步π演算中的信息流与资源访问。计算机科学技术报告2000：03，苏塞克斯大学，2000年。[15] 彼得·赫尔曼构件化应用程序的信息流分析。第17届计算机安全应用年会应用计算机安全协会（ACSA），2001年。[16] 本田康平，瓦斯科·瓦斯康塞洛斯，吉田伸子。安全信息流作为类型化进程行为。在Programming Languagesand Systems，卷1782计算机科学讲义。Springer-Verlag，2000.[17] Sushil Jajodia，Boris Kogan和Ravi S. Sandhu一种多级安全的面向对象数据模型。在马歇尔D.Abrams，Sushil Jajodia，and Harold J.Podell，编辑，信息安全：综合论文集，第596-616页IEEE ComputerSociety Press，1995.[18] 罗宾·米尔纳通信和移动系统：π-演算。 1999年5[19] 罗宾·米尔纳，约阿希姆·帕罗，大卫·沃克。移动过程的演算，第一部分。100：1[20] Andrew C.迈尔斯实用的多静态信息流控制。第26届ACM Symposium on Principles of ProgrammingLanguages（POPL 99），第228ACM Press，January 1999.[21] 积极主动。http://www-sop.inria.fr/oasis/proactive/网站。[22] 安德烈·萨贝尔菲尔德。同步对并发程序中安全信息流的影响。第四届系统信息学展望国际会议，计算机科学讲义第2244卷。Springer-Verlag，2001年7月。I. Attali等人/理论计算机科学电子笔记180（2007）1731[23] Pierangela Samarati，Elisa Bertino，Alessandro Ciampichetti，and Sushil Jajodia.面向对象系统中的信息流控制IEEE Transactions on Knowledge and Data Engineering，9（4）：524-[24] 皮安杰拉·萨马拉蒂和萨布丽娜·迪·卡皮塔尼·迪·维默卡蒂。访问控制：策略、模型和机制。在安全分析和设计的基础：计算机科学第2171卷，第137页。Springer-Verlag，2001.[25] Steve Zdancewic、Lantian Zheng、Nathaniel Nystrom和Andrew C.迈尔斯不受信任的主机和配置：安全的程序分区。第18届ACM操作系统原理研讨会ACM Press，October 2001.A例A.1上下文我们专注于专门面向股票市场的金融应用程序。全球情景有以下参与者：证券交易所市场、几家银行和一些客户。在这种情况下，主要的想法是转换一些源信息，以产生另一种类型的信息，后者用作贸易决策过程的支持（即，在股票市场上买卖行为的决策）。从这个意义上说，证券交易所市场将充当原始或源信息的提供者，将其传递给其直接客户，在这种情况下是银行。银行A贸 易研 究结果客户端1证券交易所市场原贸易订单B银行贸易订单客户端2客户机n信息C银行组Z图A.1. 金融应用程序的通用业务模式通过展开一般银行流程（图A.1），我们注意到它是由其他子流程组成的。图A.2用BPMN符号展示了银行流程的组成。接收过程接收来自证券交易所的信息，并根据一些过滤和再分配规则，将可能缩小的信息发送到指定的目标。目标可以是外部业务伙伴，也可以是内部业务伙伴。在银行的内部或私人工作流程之后，在股票经纪人流程接收到信息之后，所提供的信息被传递到统计分析，然后面对历史预测，市场专家研究的结果，产生买入和
我的内容管理
展开
