没有合适的资源?快使用搜索试试~ 我知道了~
可在www.sciencedirect.com在线获取理论计算机科学电子笔记332(2017)3-20www.elsevier.com/locate/entcs使用类型Rakan Alsowail和Ian Mackie英国萨塞克斯大学信息学系摘要授权用户意外滥用共享文件是一个主要问题。本文提出了一种著名的静态分析方法,即类型系统,以防止这种意外的误用。 我们开发一种类型系统,它截获文件系统中用户发出的命令,并在每个文件上执行策略。使用者发出的操作文件的命令,须接受类型系统的类型检查。然后保证类型检查的命令不会违反文件的策略。本文的重点是一个特殊的政策,允许所有者的文件(用户谁创建文件),以指定次数的文件可以通过限制文件可以复制的次数来读取。因此,一个文件可以被阅读,就像它可以被复制一样。 如果文件无法复制,则只能读取一次。 这种方法可以扩展其他属性。保留字:文件共享、安全类型、类型检查1引言文件共享已成为我们日常生活中不可或缺的一部分。共享文件可能是敏感的,因此,它们的机密性,完整性和可用性应该受到保护。这种保护可能是针对由未经授权的用户发起的外部威胁或由授权用户发起的内部威胁。我们的主要兴趣是内部威胁,特别是可能意外违反文件政策的可信授权用户。最广泛使用的保护共享文件的技 术 是 访 问 控 制 , 如 自 主 访 问 控 制 ( DAC )[9 , 7] 和 基 于 角 色 的 访 问 控 制(RBAC)[14]。虽然访问控制对于指定谁可以访问哪些信息很有用访问控制关注的是信息的发布,而不是信息的传播。它保证信息仅向授权用户发布。然而,一旦信息被发布给授权用户,它可能会被恶意或意外泄露给未经授权的用户,而没有任何进一步的控制。信息流控制是访问控制的一种补充方法,用于防止信息泄漏。它跟踪信息在程序执行期间如何传播,以确保程序不会泄漏敏感信息。http://dx.doi.org/10.1016/j.entcs.2017.04.0021571-0661/© 2017作者。出版社:Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章(http://creativecommons.org/licenses/by-nc-nd/4.0/)。4R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)信息流控制可以静态地[4,5,15,16]或动态地[13,2]实施。前者在程序执行之前分析程序中的信息流,而后者在执行过程中分析信息。静态地实施安全信息流的主要方法是使用类型系统。本文提出了一种新的方法,使用类型系统来解决问题的意外滥用共享文件的可信授权用户。例如,当受信任的授权用户意外地将文件传播给未授权用户时,会发生这种滥用,写入只读文件,或者复制一个只读一次的文件,之后该文件应该被擦除。因此,滥用是违反文件政策的行为。我们设计了一种命令语言来操作文件,并在类Unix文件系统中指定它们的策略,以及一个类型系统来执行这些策略。在这种设置中,文件与代表安全策略的安全类型相关联,程序是要在文件上发出的命令集,例如读取,复制,移动等。类型系统扮演引用监视器的角色,拦截并静态分析要在文件上发出的每个命令,并确定该命令是否可以安全执行。安全命令是指在执行过程中不会引起错误的命令。这些错误可能是由违反与文件相关联的安全策略或违反其自身要求的命令(例如,文件必须存在才能删除)。因此,如果对命令进行了类型检查,则文件和命令策略不会被违反,并且可以安全地执行。在本文中,我们专注于执行特定的策略,即限制文件可以读取的次数。然而,同样的基本思想可以扩展到执行第6节中指出的其他政策。本文的其余部分组织如下。第2节介绍了文件的安全类型和策略。第3节描述了操作文件的语言语法和语义,定义了安全错误和检查语法错误的算法第4节描述了类型系统,并包括属性。第五节介绍了一个类型检测算法,并证明了它的可靠性和完备性。在第6节中,我们简要回顾了相关的工作,最后我们在第7节结束了论文。2安全类型和策略我们限制文件可读取次数的方法是限制文件可生成的副本因此,一个文件可以被阅读,就像它可以被复制一样。如果一个文件不能被复制,那么它可以被读取一次。为执行此政策,我们需要限制对复制操作的访问,并限制由所有操作引起的信息流,从而不违反文件对复制为了控制对文件的复制操作的访问,我们定义了三种安全类型,即UC、LCn和NC,每种安全类型都指定了一种不同的策略,即如何对它们执行复制操作UC代表Unrestricted Copy,这意味着与此类型相关联的文件可以不受限制地复制。UC类型文件的复制版本应该被允许以同样的方式复制,因此也应该是UC类型LCn代表线性复制,这意味着R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)5⇐⇒与此类型相关联的文件可以复制n次,之后该文件将无法再复制。但是,与UC不同的是,LCn类型文件的复制版本不应再复制。NC代表No Copy,这意味着与此类型相关联的文件根本无法复制。 因此,LCn类型文件的复制版本应该是NC类型NCLCnUCFig. 1. 安全类型为了控制文件之间的信息流,我们的安全副本类型形成了一个网格(τ,±),其中τ ={NC,LC n,UC},部分由±排序(见图1)。NC和UC分别是集合τ的上界和下界。最少限制的类型是UC,而最多限制的类型是NC。因此,信息只允许在格中向上流动,这意味着从限制较少的类型到限制较多的类型。应注意,LCn±LCn ′当且仅当n≥NJ。为了正式声明我们需要执行的策略,我们定义了以下函数和符号。函数dst代表目的地,对于给定类型的文件,函数dst为该文件的复制版本找到适当的类型。 也就是说,dst(UC)= UC和dst(LC n)= NC,其中n > 0。 函数red代表reduction,对于一个给定类型的文件,函数red在复制时根据需要减少该类型它主要用于类型LCn,以限制该类型可以复制的次数。也就是说,red(UC)= UC和red(L Cn)=LCn−1n>0。注意我们没有定义dst(L Cn≤0)n或dst(NC)或red(LC n≤0)和red(NC),因为这些类型的文件不允许复制,因此,对它们应用函数会导致错误。 设T(f)表示与文件f相关联的类型,T(f1)HT(f2)表示f1和f2的类型的最小上界。也就是说,如果T(f1)= NC且T(f2)= UC,则T(f1)HT(f2)= NC。设f1→copyf2表示由复制操作引起的从f1到f2的信息流,f1→of2表示由除复制之外的其它操作(例如mv、cat等)引起的信息流, 并且f1∈ types表示f1与安全类型相关联。下面我们给出了类型系统要执行的策略的定义定义2.1<$f1,f2∈类型。f1→of2总是允许的,前提是f2必须将其类型更改为T(f1)HT(f2),并且f1必须在执行操作后被消耗。定义2.2<$f1,f2,f3∈类型。f1,f2→of3总是允许的,前提是f3必须将其类型更改为T(f1)HT(f2)HT(f3),并且在执行操作后必须消耗f1和f2。6R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)nn>0定义2.3 <$f1,f2∈类型。 f1→复制f2是允许的 当且仅当T(f1)∈{UC, LC},并且f2必须将其类型更改为dst(T(f1))HT(f2),并且f1必须更改在执行操作后,其类型变为红色(T(f1应该注意的是,当一个文件被消耗时,该文件必须不能用于任何后续操作(即该文件必须被擦除)。接下来,我们介绍我们的语言语法和语义,定义安全错误的概念,以及检查语法错误的算法。3语言学与语义学设f是给定文件系统的一组有效文件名。该语言的语法由以下语法给出⟨p⟩ ::= 100cs| ⟨f ⟩cs|cc|rm f |mkf ft |rd f|猫|mv ff⟨t⟩* = NC|LC| UC上面的语言由短语组成短语是命令列表(cs)或文件名(f)。命令可以是单个命令(c)或命令序列(c;cs)。我们包括复制,删除,制作,阅读,连接和移动文件的命令。这些命令在我们表示为一组文件的文件系统δ上操作。一个文件有一个名字,内容和类型,我们写f(c):τ对于一个名字为f,内容为c,类型为τ的文件。 比如说,δ ={f1(c1):τ1,f2(c2):τ2,...,f n(c n):τ n}.在后面的章节中,我们可能只将δ作为文件名的集合(例如,δ ={f1,f2,.,fn})或仅具有类型的文件名的集合(例如,δ ={f1:τ1,f2:τ2,.,fn:τn})。从我们所指的δ的上下文来看,这是显而易见的。我们使用以下符号:C(f)和T(f)分别表示文件f的内容和文件f的类型。C(f1)+C(f2)和T(f1)HT(f2)分别表示连接f1和f2的内容以及f1和f2的类型的连接。我们写δ[f2<$C(f1)]用于用文件系统δ中的f1的内容更新f2,和δ[f2<$T(f1)]用于用δ中的f1的类型更新f2。这两种运算都要求f1和f2必须存在于δ中。如果f存在于δ中,我们写δ[−f]从δ中移除f,如果f不存在于δ中,我们写δ[+f]将f添加到δ中。我们写δ[f3<$C(f1)+C(f2)]来用f1和f2的连接内容更新f3,写δ[f3<$T(f1)HT(f2)]来用f1和f2的类型的连接更新f3。 这两种运算都要求f1,f2和f3必须存在于δ中。最后,我们写c,δ→δJ,用于计算δ中的命令c,从而产生新的文件系统δJ。例如,如果δ={f1(c1):τ1,f2(c2):τ2},则 → {f2(c2):τ2},τmvf1f2,δτ -{f2(cl):T(fl)HT(f2)},以及若f附加f1f2f3,δf → {f3(C(f1)+C(f2)):T(f1)HT(f2)}.如果有任何限制应用于δ的操作的不满意,然后评估配置c,δ注意,可以按照从左到右的顺序将一系列操作应用于δ。例如,符号R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)7Jδ[+f,−f]表示先添加文件f,然后从δ中删除文件f。我们现在可以把所有这些想法放在一起,根据计算规则给出命令的语义。这些建议如下。cpf1f2, δrmf,δmkfft,δ第二个f,δ→δ[−f]C1f1f2f3,δα→δ[f3<$C(f1)+C(f2)][f3<$T(f1)HT(f2)HT(f3)][−f1,−f2]mvf1f2,δ从单步转换中,我们可以将命令序列的语义定义为(小步)操作语义,如下所示c,δCSC10;cs,δC10C10,δC10c,δ我们像往常一样写,因为的自反和传递闭包。因此,命令序列可以通过下式计算:3.1安全错误安全错误可以分为语法错误和类型错误。当应用于δ的运算的约束不满足时,就会发生语法错误。例如,如果δ={f1(c1):τ1,f2(c2):τ2},那么计算配置rmf4,δ应该导致错误,即rmf4,δ→Err,因为运算δ[−f4]要求f4存在于δ中。另一方面,当函数应用于文件类型的约束不满足时,就会发生类型错误例如,如果T(f1)= NC,则Δcpf1f2,δε →Err,因为函数dst(NC)导致误差。语法和类型约束如表1和表2所示可以看出,表1中的内容更新操作(即δ[f2<$C(f1)]和δ[f3<$C(f1)+C(f2)])要求文件名是不同的。 这种约束对于排除由计算配置(例如,将f1擦除两次的f1catf1f3,δ)导致的错误,以及排除由计算配置(例如,将f1擦除两次的f1catf1f2f1,δ和将f1mvf 1 f 1,δ)导致的文件的意外擦除非常重要,这与计算配置(例如,将f1擦除两次的f1cat f 1 f 3,δ和将f1mvf1,δ)具有相同的效果。接下来,我们提出我们的算法检查语法错误。3.2语法正确性在一个命令中出现一个文件名决定了该命令是否可以在一个特定的文件系统δ中成功地被求值。有些命令,如(rmf),要求文件名在δ中存在,而另一些命令,如(mkfft),要求它们不存在。针对特定的C8R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)操作约束dst(τ)τ∈ {UC,LCn>0}红色(τ)τ∈ {UC,LCn>0}表2应用于类型的表1应用于δ的运算约束文件系统不工作。例如,考虑文件系统δ={f1(c1):τ1,f2(c2):τ2},则配置函数rmf1; rmf1,δn将无法求值,因为第一个命令将从δ中删除f1,因此第二个命令将生成错误。类似的情况也出现在构型<$mkf f3t; mkf f3t,δ中。在这种情况下,第一个命令会成功,但第二个命令会失败,因为文件f3已经存在。因此,由于命令求值会改变δ,因此在检查文件名的出现时,后续命令必须考虑这种我们定义一个算法来检查命令的一致性,方法如下。对于给定的命令cs,我们计算一个4元组(H,N,C,E),它给出了对起始文件系统δ的约束,以便它可以无错误地执行。H表示必须存在于δ中的文件名集合,N表示必须不存在于δ中的文件名集合。C表示由命令序列创建的文件名集合,这些文件名最初不一定必须在δ中。E表示被命令序列擦除的文件名的集合,因此这些文件最初不一定在δ中是自由的。表3给出了算法的核心。如果一个原子命令c满足表中的条件,我们写c(H,N,C,E)=(HJ,NJ,CJ,Ej),其中(HJ,NJ,CJ,EJ)是由命令c更新的集合。然后通过组合计算命令序列:c;cs(H,N,C,E)=cs(c(H,N,C,E))。 该算法以(,)开始。TermHNCE条件cpf1f2H({f1,f2}−C)NCEf1∈/E,f2/∈E,f1=/ F2rmfH({f}− C)NC-fE{f}f∈/Emkff tHN({f}− E)C{f}E−{f}f∈/CRDFH({f}− C)NC-fE{f}f∈/E类别f1f2f3H({f1,f2,f3}−C)NC−{f1,f2}E({ f1,f2}f1/E,f2/E,f3/E,f1=/ f2,f1=/ f3,f2/=f3mvf1f2H({f1,f2}−C)NC−{f1}E{ f1}f1∈/E, f2/∈Ef1=/ F2表3用于语法检查命令的使用该算法的一个例子是命令cpf1f2:cpf1f2(n,n,n,n)=({f1,f2},n,n,n).这意味着文件{f1,f2}必须是文件系统的一部分,操作约束δ[+f]f/∈δδ[−f]f∈δδ[f2←T(f1)]f1,f2∈δδ[f2←C(f1)]f1,f2∈δ≠f1/=f2δ[f3←T(f1)HT(f2)]f1,f2,f3∈δδ[f3←C(f1)+C(f2)]f1,f2,f3∈δεf1=/ f2,f1/=f3,f2=/ F3R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)9|►命令被执行。第二个例子是命令序列mkff1t;rmf1:mkff1t;rmf1(n,n,n,n)=rmf1(mkff1t(n,n,n,n))Sincef1∈/C,then=rmf1(n,{f1},{f1},n),且由于f1∈/E,theNn=(,{f1},,{f1})这意味着在δ中不需要任何文件来成功执行这些命令,如果有任何文件,则不能使用 文 件 名 f1 当 命 令 不 满 足 表 中 的 条 件 时 , 算 法 失 败 。 考 虑 一 个 命 令 序 列mkff1t;mkff1t:mkff1t;mkff1t(,)=mkff1t(mkff1t(,))Sincef1∈/C=mkff1t(n,{f1},{f1},n)然而,由于条件f1∈/C不满足,则mkff1t(f 1,{f1},{f1},f 1)失败。类似地,命令序列(如rmf1;rm f1:rmf1;rmf1(n,n,n,n))=rmf1(rmf1(n,n,n,n)). Sincef1∈/E,THEN=rmf1({f1},n,n,{f1})然而,由于条件f1E不满足,那么,rmf1({f1},n,n,{f1})应该失败。表3说明了这样一种想法,即需要必须在δ中的文件名必须没有被以前的命令删除,并且任何不需要在δ中的命令的文件名必须没有被以前的命令创建。此外,命令的文件名必须不同。我们可以通过以下结果将这些语法约束与操作语义联系起来,该结果表明,如果文件系统满足上述命令所需的约束,则它将成功执行(即,没有错误)。从本质上讲,这个关键结果给出了文件系统的约束:哪些文件必须存在,哪些文件必须不存在。定理3.1对任意命令序列cs,若cs(ε,ε)=(H,N,C,E),则对任意文件系统δ,若H ε δ和N ε δ = ε,则存在文件系统δJ使得εcs,δε δJ。4类型系统现在我们介绍类型系统,它将在执行之前检查命令以确保它们没有语法和类型错误。类型判断具有形式Γ|其中,r是类型为f:τ的文件列表。我们为空列表写。例如,r = f1:τ1,f2:τ2,f3:τ3,.,f n:τ n。 应该注意的是,在上下文中的文件是唯一的,符号“,”是不相交的并运算,因此在Γ中的文件列表不包含重复。判断ΓrJp:τ意味着在上下文Γ i中键入类型τ的短语p 上下文为rJ。换句话说,上下文Γ和ΓJ表示键入短语p之前和之后的文件集。请注意,短语p可以是命令或10R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)文件名。类型规则如图2所示规则(f)说从上下文中输入一个文件会消耗上下文中的文件规则(cs)指出,如果键入类型为void的命令c将上下文Γ更改为ΓJ,并且键入类型为void的命令cs将上下文ΓJ更改为ΓJJ,则按顺序键入这些命令将上下文Γ更改为ΓJJ。规则(cp)说,如果我们可以从上下文Γ中键入f1和f2,并且f1的类型是UC或LCn>0,那么我们可以键入void类型的命令cpf1f2,并且f2的类型被改变为其类型和dst(f2)的类型的最小上界,并且f1的类型被改变为red(f1)的类型。规则(rm)和(rd)说,如果我们可以从上下文Γ中键入f,那么我们可以分别键入void类型的命令rmf和void类型的命令rdf规则(mkf)指出,键入类型为void的命令mkfft将把类型为t的f添加到上下文Γ。规则(cat)说,如果我们可以从上下文Γ中键入f1,f2和f3,那么我们可以键入类型为void的命令catf1f2f3,并且f1和f2将从上下文Γ中消耗,而f3的类型被改变为其类型的最小上界,f1的类型和f2的类型。规则(mv)说,如果我们可以从上下文Γ中键入f1和f2,那么我们可以键入类型为void和f 1的命令mv f1f2,并且将从上下文Γ中消耗,而f2的类型被改变为其类型和f 1的类型的最小上界。命令派生的示例在附录A中给出。r,f:τ|τ f:τ(f)第(1)款Γ |Γ jc:无效Γ J|Γ jj cs:void(cs)Γ |Γ jjc; cs:voidΓ |r Jf1:ττ ± LC n>0|Γ jjf2:τ JΓ|Γ JJ,f1:red(τ),f2:τ JH dst(τ)<$cpf1f2:void(cp)Γ |r Jf:τΓ |Γ jrmf:void(rm)Γ |Γ,f:tmkfft:void(mkf)Γ |r Jf:τ(rd)r |f:voidΓ |r Jf1:τr J|Γ jjf2:τ JΓJJ|Γ jjjf3:τ JJ(cat)Γ |Γ JJJ,f3:τ Hτ JH τ jjcatf1f2f3:voidΓ |r Jf1:τr J|Γ jjf2:τ J(mv)Γ |Γ JJ,f2:τHτjmvf1f2:void图二. 类型规则4.1类型系统的属性我们证明了我们的类型系统的操作语义方面的健全性和完整性。通过证明稳健性的两个性质,即保序性和进步性,证明了稳健性传统上,进度定理认为程序要么是一R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)11个值,要么可以进行一步求值。然而,在我们的例子中,程序是对文件系统中的文件进行操作的命令,并且应该始终采取评估步骤。因此,如果一个命令c在一个特定的文件系统δ中是可类型化的,那么命令c必须采取一个求值步骤12R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)JJ定理4.1(进步)如果Γ = δ且Γ |Γ Jc:τ,则c,δ/→ Err。证据我们继续由情况下对类型的推导c。有六个案例,我们只展示了两个。(i) c=cpf1f2我们知道有一个类型推导c通过使用规则(cp)与结论:|Γ JJ,f1:red(τ),f2:τJHdst(τ)<$cpf1f2:void.我们还必须有带结论的子导子:|ΓJ<$f1:τ,τ± LC n>0和Γ J|Γ jjf2:τJ. 现在我们可以利用规则(1)得到δcpf1f2,δcp →δ [f2<$C(f1)][f2<$T(f2)Hdst(T(f1))][f1←red(T(f1))]. 由于构型为πcpf1f2,δπ要求f1∈δ和f2∈δ和f1f2在没有语法错误,我们有f1∈Γ和f2∈Γ和f1f2在Γ中,因为Γ不允许文件名重复,且Γ = δ。然后,δ εcpf1f2,δε f →sErr。此外,由于运算dst(T(f1))和red(T(f1))需要δ中的(T(f1))± LC n>0,因此我们 在 Γ 中 有 T ( f1 ) ± LC n>0 , 且 Γ = δ 。 然 后 , 根 据 需 要 , Δcpf1f2 ,δε/→Err。(ii) c=rdf我们知道有一个类型推导c通过使用规则(rd)与结论:|f:void. 我们还必须有一个带结论的子推导: Γ |r Jf:τ. 现在我们可以使用规则(4)来获得f的值,δ→δ[−f]。 由于配置函数f∈rdf,δ<$要求f∈δ被无语法错误地求值,我们有f∈Γ和Γ =δ。则δτf,δτ/→Err。Q传统上,保存定理指出,当我们评估一个程序时,它的类型在每个评估步骤都被保存。然而,程序操作文件及其类型,我们需要确保在计算过程中保留文件的类型。因此,如果一个命令在一个特定的文件系统δ中是可键入的,那么我们通过键入该命令获得的文件类型必须保存在我们通过评估该命令获得的文件 此属性显示以下内容的一致性:具有操作语义的类型系统,即不仅类型化的命令求值没有错误,而且求值后的文件系统中的文件类型与键入命令后的文件类型相对应。定理4.2(保持性)若Γ = δ且Γ |Γ J<$c:τ,且<$c,δε →δJ,则r =δ。证据 我们继续讨论δc,δj →δJ的情形。 有6个案例,我们只展示了两个。(i)c=<$cpf1f2,δ<$→δ[f2<$C(f1)][f2<$T(f2)Hdst(T(f1))][f1<$red(T(f1))]利用规则(cp)我们知道c有一个类型导子,结论如下:Γ |Γ JJ,f1:red(τ),f2:τJHdst(τ)<$cpf1f2:void.我们还必须有带结论的子导子:|Γ J<$f1:τ,τ± LC n>0和Γ J|第二章:τJ。为了简化证明,设δJ=δ[f2<$C(f1)][f2<$T(f2)Hdst(T(f1))][f1<$red(T(f1))]。现在我们有6个基于类型f1和f2的案例,我们展示了两个R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)13/下一页J他们(a) :Γ|Γ J∈f1:LC n>0,Γ J|第二章:UC在这种情况下,c的类型派生必须具有形式Γ |Γ JJ,f1:LC n−1,f2:NCcpf1f2:void.设Γ J= Γ JJ,f1:LC n−1,f2:NC. 我们不知道因为Γ(f1)f=Γj(f1)和Γ(f2)=f,所以Γ = Γ jΓJ(f2),即LC n>0= LC n−1和UC/=NC。我们也知道δ/=δJ,因为δ(f1)/=δJ(f1)和δ(f2)δJ(f2),即LCn>0/ = LCn−1和UC/ = NC。 因为Γ1 = ΓJ,因为Γ(f1)= ΓJ(f1),因为δ(f1)δJ(f1)和δ(f2)δJ(f2),和ΓJ(f1)=δJ(f1),即LCn−1 = LCn−1和ΓJ(f2)=δJ(f2),即NC =NC,和Γ =δ。然后,根据需要,ΓJ=δJ(b) :Γ|Γ J∈f1:LC n>0,Γ J|Γ jjf2:NC在这种情况下,c的类型派生必须具有形式Γ |Γ JJ,f1:LC n−1,f2:NCcpf1f2:void.设ΓJ = ΓJJ,f1:LCn−1,f2:NC. 现在我们知道了,因为Γ(f1)/= ΓJ(f1),即LCn>0 = LCn−1。我们还知道δδJ,因为δ(f1)/=δJ(f1),即LCn>0/ = LCn−1。由于Γ = ΓJ,因为Γ(f1)= ΓJ(f1),δ=δJ,因为δ(f1)=δJ(f1),且ΓJ(f1)=δJ(f1),即LCn−1 = LCn−1且Γ =δ。然后,根据需要,ΓJ=δJ(ii)c=rmf,δ→δ[−f]我们知道有一个类型推导c通过使用规则(rm)与结论:|j 我们还必须有子导子,其结论为:|r Jf:τ. 我们知道Γi = ΓJ,因为fi ∈ΓJ。我们也知道δ/=δ[−f],因为f/∈δ[−f]。因为f/∈ΓJ且δ因为f/∈δ[−f],且Γ =δ。 然后,根据需要,ΓJ =δ[−f]。δ[−f]Q现在我们展示类型系统相对于操作语义的完整性。完整性属性是有用的,因为它表明操作语义没有不必要地受到类型系统的限制。也就是说,类型系统不提供假阴性结果。完备性定理指出,如果一个命令c可以在一个特定的文件系统δ中计算而没有错误,那么命令c必须是可类型的。定理4.3(完备性)若σc,δε/→Err且Γ = δ,则为Γ |r Jc:τ对于一些r。证据 我们按命令c的情况进行。有六个案例,我们只展示了两个。(i) c=cpf1f2若f∈f1,f ∈f2,δ∈ f/→Err,则f∈f1,f∈f2,δ ∈f1,f∈ f2且δ(f1)∈ {UC, LCn>0}.因此,由于Γ =δ,我们知道对于f1和f2存在类型导子,并且Γ(f1)∈{UC, LCn>0}:Γ |Γ − {f1}<$f1:τ(f)第(1)款Γ |Γ−{f2}<$f2:τ J14R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)(f)第(1)款R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)15现在,通过(cp)规则,还有一个推导:Γ |Γ − {f1}f1:ττ ± LC n>0 Γ − {f1} |Γ − {f1,f2}<$f2:τ JΓ|Γ − {f1,f2}+{f1:red(τ),f2:τ JH dst(τ)}<$cp f1f2:void(ii) c=rdf(cp)如果f,δ∈ f/→Err,则f ∈ δ必是这种情况。 因此,由于Γ = δ,我们知道f有一个类型推导:(f)第(1)款Γ |Γ − {f} f:τ现在,根据(rd)规则,还有一个推导:Γ|Γ − {f} f:τ(rd)Γ |Γ − {f}第二个f:空Q这是有用的,表明我们的语言中的命令是单调递增的,在这个意义上,文件的类型在命令评估期间永远不会减少。这是一个简单的属性,因为我们只允许命令将文件的类型更改为其类型和源类型的最小上限。由于任何两个类型的最小上界至少与它们的限制性一样,文件的类型永远不会减少。定理4.4(文件类型的单调性)如果Γ |Γ J<$c:τ,则<$f,f J∈Γ≠ ΓJ,若 Γ(f)±Γ(fJ),则ΓJ(f)±ΓJ(fJ)5分类算法这里我们给出一个输入命令的算法T。我们定义了一些辅助函数:check(α,β)如果类型兼容则返回true。注意,任何两个不同的基本类型都是不兼容的,例如,check(LCn,void)将失败。less(τ,τJ)如果τ±τJ则返回true。lub(τ,.,τ n)返回其所有参数的最小上界,即,τH... Hτn.使用这些函数,我们现在可以定义类型检查算法T:其中:T(A,e)=(τ,AJ)(i) 如果e是文件名f,且f:α∈A,则τ=α,AJ=AZ{f:α}。(ii) 如果e是一个命令序列,则c;cs令(β,A1)=T(A,c)check(β,void)(α,A2)=T(A1,cs)check(α,void)16R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)则τ=空,AJ=A2。R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)17(iii) 如果e是命令cpf1f2,(β,A1)=T(A,f1)小于(β,LCn>0)(α,A2)=T(A1,f2)则若f1,f2A2,则τ= void,AJ =A2<${f1:red(β),f2:lub(α,dst(β))}.(iv) 如果e是命令rmflet(α,A1)=T(A,f),则τ= void,AJ =A1.(v) 如果e是命令mkfft,则如果f/∈A,则τ= void,AJ =A<${f:t}。(vi) 如果e是命令rdflet(α,A1)=T(A,f),则τ= void,AJ =A1.(vii) 如果e是命令catf1f2f3,(β,A1)=T(A,f1)(α,A2)=T(A1,f2)(δ,A3)=T(A2,f3)则若f3/∈A3,则τ= void,AJ =A3<${f3:lub(β,α,δ)}.(viii) 如果e是命令mvf1f2,(β,A1)=T(A,f1)(α,A2)=T(A1,f2)则若f2/∈A2,则τ= void,AJ =A2<${f2:lub(β,α)}.5.1算法T的性质如果T找到一个命令的类型,那么这个命令就有一个派生。这个性质被称为可靠性,这意味着算法不会给出错误的答案。我们首先证明了可靠性,然后证明该算法可以找到所有的导数,一个称为完整性的属性。定理5.1(T的可靠性)如果T(A,e)继(τ,AJ),则存在以A结尾的导子|AJe:τ.证据我们通过归纳法来研究命令e的结构。有8个案例,在这里我们展示了其中的一个(i) 如果e是文件名f,且f:τ∈A<${f:τ},则T(A<${f:τ},f)紧接着(τ,A)。使用(f)规则,有一个以A,f结尾的推导:|Af:τ(根据需要)。(ii) 如果e是命令序列c;cs,则T(A,c)以(β,A1)成功,check(β,void)成功,T(A1,cs)以(α,A2)成功,并且check(α,void)也成功。现在,通过两次归纳假设,有推导A|A1c:void和A1|A2位数:无效。使用(cs)规则,有一个推导A|A2c; cs:根据需要无效。18R. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)(iii) 如果e是命令cpf1f2,则T(A,f1)以(β,A1)为后接,T(A1,f2)以(α,A2)为后接。通过两次归纳假设,存在以A结尾的派生词|A1αf1:β和A1|A2f2:α。 由于(β,LC)较小,我们有 β±LC,现在我们可以使用(cp)规则来推导A|A2,F1:β,f2:αHdst(β)cpf1f2:按要求空。(iv) 如果e是命令rmf,则T(A,f)以(α,A1)成功 通过归纳假设,A有一个推导|A1f:α。现在我们可以使用(rm)规则来推导A|A1rmf:根据需要无效。(v) 如果e是命令mkfft且f/∈A,则T(A,(mkfft))立即以(void,A<${f:τ})成功。 使用(mkf)规则,有一个推导 一|A,f:tmkfft:根据需要无效。Q定理5.2(T的完备性)如果有一个导子以A结尾|Aje:τ,则T(A,e)以(τ,AJ)成功。证据我们通过归纳法来研究命令e的结构。有8个案例,在这里我们展示了其中的一个(i) 如果e是文件名f,f:τ∈A∈ {f:τ},则根据(f)规则,存在一个以A结尾的导数,f:τ|Af:τ。现在,T(A<${f:τ},f)根据需要与(τ,A)成功。(ii) 如果e是命令序列c; cs,则根据(cs)规则,存在以A结尾的推导|A2c; cs:void,由两个派生词组成:A|A1c:void和A1|A2位数:无效。通过两次归纳假设,T(A,c)在第一次求导时成功地得到(void,A1),T(A1,cs)在第二次求导时成功地得到(void,A2)现在T(A,(c,cs))以(void,A2)成功(iii) 如果e是命令cpf1f2,那么根据(cp)规则,有一个以A结尾的派生|A2,f1:β,f2:α H dst(β)<$cp f1f2:void由两个导子组成:A|Aj1f1:β和A|A2f2:α。通过两次归纳假设,由于β±LC我们有更少的(β,LC),T(A,f1)在第一次求导时成功地得到(β,A1),T(A1,f2)在第二次求导时成功地得到(α,A2现在T(A,(cpf1f2))以(void,A2<${f1:β,f2:lub(α,dst(β))})成功。(iv) 如果e是命令rmf,则根据(rm)规则,存在以A结尾的推导|A1rmf:void,由一个派生组成:A|A1βf:β。 通过归纳假设,T(A,f)成功于(β,A1).现在T(A,(rmf))以(void,A1)成功。(v) 如果e是命令mkfft且f/∈A,则根据(mkf)规则,存在以A结尾的导子|A,f:τmkfft:无效。现在,T(A,(mkfft))根据需要以(void,A<${f:τ})成功。QR. 阿尔索韦尔岛Mackie/Electronic Notes in Theoretical Computer Science 332(2017)196相关工作和讨论Denning[5]率先使用静态分析来确定程序的信息流是否满足特定于应用程序的保密策略。在他们的工作之后,许多安全类型系统已经被开发出来[1,8,17],从Volpano等人开始。[15]和Volpano和Smith[16],他们是第一个将Denning的安全信息流分析[4,5]制定直觉是,如果程序被正确地进行了类型检查,则可以保证程序的安全信息流关于这方面的大量工作的全面调查可以在[12]中找到。大多数安全类型的系统集中于强制执行称为非干扰的属性[6,15,12,11]。机密性的非干扰要求公开输出独立于秘密输入,完整性要求可信输出独立于不可信输入。然而,非干扰性是一个非常受限的特性,因为它不允许安全级别从高到低的降级,我们对不干涉采取不同的方法,并将我们的安全属性定义为不存在由违反文件策略的命令引起的运行时通过这种方式,我们可以很容易地用命令来增强我们的语言,这些命令可以解密信息的安全级别,并允许文件的所有者执行这些命令。因此,由不是所有者的用户执行这样的命令应该会导致错误。此外,强制非干扰只能控制信息如何从一个安全级别流向另一个安全级别;但不能控制如何操
下载后可阅读完整内容,剩余1页未读,立即下载
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)