定时感知的信息流类型系统及其在类JavaCard字节码中的应用

理论计算机科学电子笔记141（2005）163-182www.elsevier.com/locate/entcs类JavaCard字节码丹尼尔·赫丁1大卫·桑兹2计算机科学系瑞典哥德堡摘要常见的保护机制无法提供端到端的安全性;无法阻止合法访问秘密信息的程序将其泄露给世界。信息流感知分析通过程序跟踪信息流以防止此类泄漏，但通常忽略通过隐蔽渠道的信息流，即使它们构成严重威胁。一个典型的隐蔽通道是利用某些事件的时间来携带信息。我们提出了一个定时感知的信息流类型系统的低级语言类似于一个顺序的Java字节码的非平凡的子集。类型系统在语言指令的时间模型和执行低观测等价的算法上被参数化，用于防止隐式和定时溢出。关键词：隐蔽通道，信息流，安全性，字节码1介绍随着具有可扩展功能的移动设备越来越多地被采用，安全性变得越来越重要。当今常见的保护机制包括沙盒和应用防火墙，沙盒通过运行具有有限功能的程序来保护系统，应用防火墙防止两个应用程序访问彼此的私有数据或代码。这些系统的安全性-1http://www.cs.chalmers.se/~utter2http://www.cs.chalmers.se/~dave1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.031164D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163chine这些技术的共同之处在于它们无法提供所谓的端到端安全性。没有什么能阻止一个程序合法地访问一个秘密，把这个秘密告诉全世界，不管是偶然的还是恶意的。最近的研究集中在静态确定程序何时满足端到端保密属性的问题上[14]。程序披露信息的方式通常分为显式和隐式泄漏，以及通过其他隐蔽通道泄漏。显式泄漏相当于使用某些公共通信信道直接泄漏秘密。当程序控制流依赖于秘密时，可能会出现隐式流--一种隐蔽通道的形式。如果秘密的值可以通过程序选择执行路径，则对环境的修改和这样的路径中的公共输出可以用于间接编码秘密的属性。使用普通的保护机制可以很容易地阻止显式信道，而隐式信道需要某种信息流感知机制。隐蔽信道是一种不用于通信的介质的总称，用于传输信息[10]。某些可观察事件的时间可以被用作隐蔽通道，这是在本文中考虑。隐通道是一个微妙的问题，可以使用类似于隐通道的技术来处理，但往往会导致非常严格的系统。因此，在信息安全中，它们常常被故意忽略，以显得更“实用”。 然而，隐蔽渠道构成了一个真实而严重的威胁，不能仅仅为了方便而忽视。作为示例，假设攻击者只能在差异为0.5秒的量级时可靠地观察到可观察事件的定时的变化。即使在如此低的带宽（对应于攻击者通过繁忙的网络观察系统），在不到2分钟的时间内泄漏相当于VISA卡号的信息也是相当合理的在[14]中描述的大多数研究中描述的保护机制在它们都是自动的方面是相似的。不受信任的代码在执行之前被静态验证，或者在执行期间被监视，而不需要用户交互。实际上，在建立动态下载的代码的安全属性时假设任何用户交互可能是不合理的。然而，任何不对计时进行建模的自动安全检查都可能接受通过计时泄漏信息的程序，无论泄漏是多么明显。 程序将被允许运行，更糟糕的是，验证过程将在用户和程序之间建立信任。D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163165在本文中，我们探讨了一个简单的字节码语言的端到端的信息流的安全性问题，我们的模型和防止某些类的定时攻击。分析低级语言是困难的，但有几个潜在的好处。高级程序使编译器成为可信计算基础的一部分。开发、实现和维护一个值得信赖的编译器是一项艰巨的任务。从时序特性的角度来看，低级语言要详细得多，因此允许细粒度的时序模型。这通常不可能在源代码级别执行，因为编译过程决定了时序行为的许多方面。本文的其余部分组织如下。第2节考虑了相关的工作，第3节介绍了语言及其语义，第4节讨论了计时，时间模型和非干扰，第5节探讨了类型系统中更有趣的部分，第6节总结了。2相关工作我们的工作建立在基于类型的程序分析的思想之上。在基于类型系统的信息流安全性的更完整的处理中，我们发现了FlowCaml [15，13]和JIF[12]，分别处理OCaml和Java的大子集。关于低级语言的类型系统，Stata和Abadi[16]提出了一个Java字节码子集的类型系统，专注于常规字节码验证提供的保证。对于汇编语言，康奈尔大学的TAL3关于Java字节码，Morisett等人在基于堆栈的类型化汇编语言（STAL）[11]中的工作是最相关的。直到最近才开始研究低级语言的信息流安全问题Barthe和Rezk[4，5]为顺序字节码语言提供了一个对数据流敏感的类型它们的基本类型结构类似于Stata和Abadi的作为大多数分析的标准（源于Denning [6]最初概述的方法），通过禁止修改安全类型低于当前上下文的环境部分来禁止隐式加密。 例如，如果当前程序计数器值取决于secret的值，则代码不得向下写入到较低的安全级别。建立了该型系统的不干涉定理。3http://www.cs.cornell.edu/talc166D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163Genaim和Spoto[7]强调处理一个完整的语言，提出了一个完整的Java字节码的组合信息流分析。分析使用布尔函数来编码信息流。在另一端，Kobayashi和Shirane[8]为Java字节码的一小部分（不包括数组、对象和方法）的信息流分析提供了无干扰证明。他们工作的主要重点是扩展Stata和Abadi的类型系统，并具有信息流意识。与上述工作不同的是，还简要考虑了定时信道。Kobayashi和Shirane提出了一种处理定时的方法，该方法源于他们的主要定理，该定理说，如果一个程序在一个环境中以m步的公共值终止，那么对于任何低等价环境，对于某个常数c，它将在c/m步内终止。为了处理时间，Kobayashi和Shirane建议，给定这个常数c，当所有秘密值都设置为0时，测量执行的步骤数，并在返回之前插入一个延迟，以便返回总是在（c）+ 1）n步。他们的方法假设可以测量程序中语句的执行时间，并将结果延迟指定的时间。在许多情况下（例如多功能智能卡），两者都不可能。关于定时感知系统，Agat[2]提出了一种用于小型While语言的定时感知类型系统，该类型系统包括一个转换，该转换将程序转换为等效程序，而不会出现定时泄漏。在[1][Paper II]中，Agat实现并评估了Java字节码的一个小子集的转换该分析只是非正式地指定，但足以测试某些定时泄漏确实可以消除，基于对特定字节码解释器的观察。我们的方法从Agat的初步实验中获得本文的主要贡献是一个类型系统，这是paramerized的定时和模型的指令，允许不同程度的定时敏感性处理，包括简单形式的缓存敏感定时。3语法和语义该语言相当于Java字节码的顺序子集，包括对象和数组，但不包括异常处理和jsr/ret指令对。D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）1631673.1语法一个程序，由P表示，是一个类的集合一个类，由C表示，是零个或多个字段和方法。一个由F表示的场，由它的类型和它的标识符定义。一个方法，由M表示，由它的标识符、类型和指令列表定义。类别、方法和字段标识符分别按C、M和F排列。语法包含对类型语言的引用：τ，μ是在5.1节中定义的安全类型。让l在程序标签上范围。方案P* = C1. Cn级别C：：= classcname [extendsscname]{F1;. F n; M1. M n}菲尔兹·F ：：=τ vname;方法M：：= mname μ{[l1] inst1. [ln]instn}Fig. 1. 语法指令集I，由inst表示，如图2所示。pop，dup，swap，constZ，loadN，storeN，add，sub，mul，div，rem，if @ ll，gotol，newC，get fieldF，put fieldF，invokeMτ，return，outputH|L，铸造C，重新τ，负载，存储，长度其中@∈ {eq，ne，le，ge，lt，gt}。图二. 指令3.2语义该语义是一个普通的小步操作语义的配置为一个给定的程序，增加了两个显式的终止转换对应于正常和异常终止。源自具有公共可观察行为的指令的转换用该可观察行为来注释。我们假设原始程序已被重新标记，因此程序中的每条指令都有一个唯一的标签。设PC是由pc和l覆盖的指令标签的集合，设p覆盖对象指针P tr，并且设ap覆盖数组指针AP tr。如图3所示，原始值（范围为vp）是整数、对象指针和数组指针。对象和数组分别是从域标识符或自然数到原始值的映射。对象和数组包含它们的安全类型，定义见5.1节。堆是从指针到堆实体、数组和对象的映射。执行环境由e表示，是一个由操作数栈、寄存器、堆和帧栈组成的4元组。操作数堆栈，范围为st，是一个原始值的堆栈。一个寄存器组，范围为r，是从寄存器号到168D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163原始值vp：：= Z|p|AP对象o：：= V C，F1：v p1，.，Fn：v pn阵列a：：= πτ，v p1，.，v pn堆oe：：=（p1→o1，.，ap1›→a1，.. . ）环境e：：=fst，r，oe，fs操作数堆栈st：：=|v p·st寄存器组r：：=（v p0，.，vp255）帧堆栈fs：：=|f·fs帧f：：=（st，r，pc）图三. 价值观和环境原始值。帧栈是帧的栈，由fs覆盖。一个帧，范围为f，由保存的操作数堆栈，寄存器和程序计数器组成在本文的其余部分，我们将寄存器、堆栈位置和堆实体的字段统称为环境位置。Let Oe是可观测行为的集合，LetOe表示行为o ∈ O或无可观测行为的概率。语义是公式化的w.r.t. 一个给定的程序P，其规则如下：.........（pc， e）→o（pc， e）（pc i，ei）→ e e（pci，ei）↓伊伊伊表示具有可能的可观察行为的执行的一个步骤，从左到右为正常和异常终止。一个程序可以在任何一个静态方法中启动，该方法将一个整数数组作为参数。4定时和不干扰互不干扰是信息流安全中最常用的概念之一不干涉的一般思想是，程序可用的秘密值的变化不应产生公开可观察行为的变化。粗略地说，程序环境分为秘密（安全级别H）和非秘密（安全级别L）。非干扰性是指如果你在任何两个非秘密部分相等的环境中启动程序，那么，当程序终止时，结果环境的非秘密部分也必须相等。如果是这种情况，则环境的秘密部分不能干扰非秘密部分，并且因此不能从非秘密推断出关于秘密的信息。两个环境具有相等的非秘密部分的判断通常被称为低等价（5.3节），通常以等价关系w.r.t.形式化。环境安全类型（第5.1节），描述环境的哪些部分被认为是秘密的，哪些不是。D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163169互不干扰的成功来自于它的通用性，它允许实例化覆盖广泛的信息流。任何可以在语义上建模的行为都属于不干涉的范围例如，显式和隐式超高速缓冲存储器流，而且还有定时、高速缓存感知定时和其它隐蔽信道。不干涉的缺点是制定的严格性。泄漏不是量化的，只是定性的，这使得这个概念不能用于自然必须包含泄漏的程序。但这超出了本研究的范围。我们建议读者参考[14]，以了解基于语言的信息流安全的调查。为了处理时间，我们需要一个时间模型，即。描述语言指令的时序行为的模型对于汇编语言，指令的时序取决于计算机体系结构：CPU及其周围环境。对于解释的字节码，情况要复杂得多底层硬件不仅要考虑时序模型，还要考虑运行时环境的实现时序模型非常重要，系统的安全性直接关系到模型的质量。有几种可能性：最简单的模型是给所有指令分配相同的单位时间。这就相当于数数在操作语义中的转换，并且是在例如[8]的一项建议。常数时间模型显然，并非所有指令都需要相同的时间。一种改进是将不同的常数时间分配给不同的指令。这是在[1]中找到的模型。功能时间模型下一个改进是让时间模型成为指令参数的函数。像创建大小为n的数组的new这样的指令不是常数时间。在[2]中，这是通过禁止这样的指令来处理的，当它们有秘密值作为参数时。历史敏感时间不幸的是，某些指令的定时不仅仅是指令操作的当前状态的函数。对于引用内存的指令，高速缓存的状态是一个重要参数，可能会对所用时间产生显著影响 来执行指令。我们对时间模型的表述涵盖了这四种情况。170D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）1634.1历史和时间模型为了允许不同的模型，我们用历史扩展了标准语义，积累了关于执行的信息。历史是计算抽象时间的基础，抽象时间用于确保可观测时间与秘密值无关。对于给定的程序，时间模型是语义时间模型SM和对应的类型时间模型TM的对（SM，TM）。对此的看法是，SM提供了时间的语义，而TM提供了类型规则中使用的类型判断。TM和SM之间的连接是一种非干涉型要求，类似于下面的轨迹。为例如，如果指令的时间4取决于其参数中的第一个而不是第二个，则该指令的时间的安全类型由第一个参数而不是第二个参数的安全类型决定。历史通常由多个子历史构建，例如，当前时间和数据高速缓存的状态，这些子历史通过指令彼此相关，但仍然相对独立。[5]因此，我们将历史定义为子历史的有序产物，并将相同的结构强加于自身。安全类型的历史。这允许（部分）独立子历史的充分分离。4.1.1语义时间模型设E是环境的集合，范围为e。语义时间模型是一个四重模型H、T、hist、time，• H是表示执行历史的集合，在结构上根据子历史的有序积来定义，每个子历史都有一个独特的空元素和相等操作，• T是时间的抽象域，配备了等式运算，• hist：I ×E×H→H是一个部分函数，它接受一条指令、当前状态和迄今为止的历史，并产生对应于计算的下一个状态的扩展历史• time：I ×E×H→T给出了在历史H中执行下一个步骤之后的可观察时间。4根据语义时间模型5可以想象这样的情况：数据缓存的状态反映秘密信息，而时间D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163171~−→~4.1.2类型接口设ET为环境类型的集合（5.1节）。类型系统的接口是一个三重类型HT，φ，φ，其中• HT是由H的结构通过向每个子历史分配安全级别来定义的历史安全类型的集合，• φ：I ×ET×HT→HT，是与如下定义的hist一致的类型函数，• I：I ×ET×HT→σ，是提取与时间一致的时间类型的类型函数，定义如下。例如，设σ是σ范围内的所有安全级别的集合（第5.1节）。对于步数计数方法，H=T=N，hist=λ（i，e，h）.h+ 1，以及time=λ（i，e，h）.h+ 1。 作为型界面，我们得到HT=σ和φ=λ（i，et，ht）.ht和φ=λ（i，et，ht）.ht为了对简单的（数据）缓存行为建模，我们可以将H取为当前时间和到目前为止执行的存储器访问序列的对，以及任意时间函数，仅取决于当前指令和历史。类型接口是HT=σ×σ，φ和φ是与上面定义4.1.3增强操作语义操作语义被增强以维护当前历史，这反过来使得时间能够被计算和操作为可观察输出的一部分。标准语义随时间的扩展被指定为沿着S. 6个跃迁（pc，e）→0 （pcJ，eJ）we定义o，时间（pc，e，h）（c）（Furthermore，用于存储、存储和管理数据的增量数据的任何向量of，t对于程序点P，我们定义一个辅助转移关系P，它描述了不超出P中程序点的可观察步骤序列。更准确地说，如果t=（o1，t1）， . . ，（on，tn），则of，t（pc0，e0，h0）P（pcn，en，hn）当且仅当（pc， e， h）→n~o1，t1· · ·→n~on，tn（pc， e， h）0 0 0P P n n n6不可观测跃迁的扩展是相同的pc，e，hist（pc，e，h））JJ172D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163其中最后的程序pcn可能是P中的程序点之一。该关系用于制定低可观察等效性，定义见下文第5.3节。4.2顶级不干涉在本节中，我们简要地陈述了我们的类型系统旨在验证的语义标准。为了描述攻击者（系统的低事件的观察者）是否可以了解系统的高输入，我们需要精确地了解攻击者可以观察到什么。我们假设唯一可观察的输出是输出指令产生的值，以及输出的时间。这一提法隐含着这样一种假设，即不能直接观察到终止，也不能直接观察到终止的原因。要看到这一点，考虑三个程序都没有公共输出，其中第一个正常终止，第二个崩溃，第三个发散。在只有公共产出是可观察的假设下，这三个方案是等价的。这个模型与攻击者是一致的，攻击者只通过系统的输出来观察系统的运行，而不能看到终止，正常或其他情况。在某些情况下，忽略除直接可观察输出之外的所有内容可能会导致每次运行泄漏多达一位信息。另一方面，完全忽略时间泄漏是一个更严重的问题，正如我们在第1节中所讨论的那样。终止不可观察的假设让我们以比其他可能的方式更自由的方式处理秘密数据上的部分指令和循环（参见C.F.[2，17]）然而，一旦我们在高数据上循环在这个意义上，我们说我们的安全标准是弱终止敏感的。现在我们可以阐述我们对不干涉的提法。我们假设一个方法M接受一个数组作为参数。数组的长度是公开的，但包含秘密内容。我们说M是无干扰的，如果公共输出或输出发生的时间没有变化，- 一对初始环境e1和e2，其仅在秘密数组中存储的值上不同：别这样，别这样。（M）og，t1（e）og，t2（男、女、女）=t12初始化1~我爱你初始化2约1t2其中，=t是来自t是向量，而o_t、o_t、o_t是输出向量1 2时间分别。D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）1631735类型系统我们提出了一个组合的，定时感知的信息流类型系统的方法作为组成单元。类型系统的结构在精神上类似于STAL[11]，具有静态类型标签和多态堆栈类型，但表达性较低。我们并没有模仿字节码的原始类型系统，相反，我们在某些方面偏离了它。然而，我们认为所有考虑中的程序都经过了字节码验证，因此，某些不变量在程序执行期间保持不变。为了简单起见，我们排除了静态字段、接口和异常处理。 前两个是微不足道的延伸。 JIF向我们展示了一种方法 处理异常（[5]中的解决方案可以被视为一种特殊形式），这些异常可能可以适应我们的设置，尽管时间使它一件微妙的事情。由于篇幅限制，我们只能介绍一小部分类型系统。要了解更多信息，我们建议读者阅读本文的主页7，其中提供了完整的类型系统和原型实现。所有信息流感知类型系统的共同点是它们必须跟踪隐式流.如前所述，当控制流依赖于秘密时，即来自条件分支时，会出现隐式分支为了使类型系统的公式化变得平滑，字节码程序必须被预处理以重新获得一些结构信息，例如分支指令的（最小）合并点。非正式地，合并点是从指令的目标开始的所有跟踪通过的第一个程序点。对于给定的控制流图，这是一个简单的图问题。缺少动态分支，即可能的目标不是静态已知的分支，使得（方法间）控制流是静态可判定的。[7]关于这个问题的更深入的讨论。5.1类型语言在图4中定义的形式安全级别，范围为σ，由两个实际安全级别H（高或秘密）和L（低或公开）组成，以及安全变量H（α1，.，α n）。安全级别形成了一个格，其中L是最小元素，H是顶部元素，以及它们之间的正式连接，通过变量的集合包含来排序。我们把H（α）写成α原始的安全类型，范围为τ，是从内部类型构建的7http://www.cs.chalmers.se/174D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163安全级别σ：：= L|H| H（α1，.，αn）Prim. 安全类型τ：：= aptr σ，στ|int σ|ptr σ，σC方法定量 上下文Δ m：：=·|α，Δ mBB Quant。 上下文Δ ε ：：=·|γ方法类型μ：：=μ[Δm ]中。τ，σ，→τ，σ，τ操作数堆栈类型s：：=|γ|τ·s寄存器组类型r：：=（τ0，.，τ255）BB类型ε：：=<$[Δε].s，r，σ，<$见图4。 类型语言tegers、对象指针和带有安全级别注释的数组指针。整数的安全级别与整数的值相关联。指针有两个安全级别：第一个与指针的实际值相关联，第二个与所指向对象的结构相关联。数组的结构是大小，对象的结构是（主）类。这种区分允许更好地处理指针解引用指令。指针类型还携带所指向对象的安全类型。在方法和基本块的类型中有一个特殊的安全级别，称为pc类型。 这种pc类型与JIF的pc类型有关，但又不同。正如我们将看到的，pc类型跟踪由执行部分指令的结果编码的信息。成功完成告诉您partial指令的参数不在会导致指令失败或崩溃的值范围内。基本块类型，范围为ε，在堆栈类型中可以是多态的，如通用量化的堆栈类型变量上下文Δε所指示的。从左到右，该类型由堆栈类型（由s表示）、寄存器组类型（由r表示）、pc的安全级别和历史类型（由r表示）组成。栈可以是空的，一个原始的安全类型，后跟一个栈或一个栈变量γ。寄存器组类型是从寄存器编号到原始安全类型的映射。方法类型是最复杂的类型。方法类型在由安全变量上下文Δm定义的安全级别中是多态的。一种方法是让人兴奋。ττ，σ， τσ→ctxτ，σ， τcepts aparameterofasubtypetoo伊奥普奥τi，可以在一个节点中创建一个值，该值的类型是σip的子类型，历史类型是σ i p的子类型，返回的值是τ，一个新的pc型σop和一个新的历史型σo。方法类型也具有相同类型的侧射约束，示例类型中的σctx，如在例如[5，3]中发现的边效应约束公共产出，边效应约束较大σD. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163175ξ<：ξ<：类似于PC，但是用于在存在对秘密对象的动态调用时保持组合性。5.2分型我们以标准的方式定义结构子类型关系例如，如果τ1：τ2，则τ1是τ2的子类型。方法子类型由（普通）参数、历史参数和pc参数中的协方差、侧效应约束中的不变性以及所有返回中的协方差定义类型侧效应约束中的不变性通过确保如果一个方法不受低侧效应影响，则具有相同名称的所有方法必须不受低侧效应影响来确保在存在对秘密对象的动态调用的情况下的组合性。τ2：τ1σ4：σ13 1σ2=σ5τ1：τ2σ3：σ62 4[·]。τ，σ， τ→σ2 τ，σ，τ<：[·]。τ，σ， τ→σ5 τ，σ，τ1 1 11 322 432 6 45.3低等同性如第4节所述，非干扰通常是根据环境的低等效关系来制定的。简而言之，两个环境是低等效w.r.t.一个环境类型，如果环境中所有被环境类型分类为公共的部分都是相等的。 例如考虑两个环境E1和E2都包含变量A。如果变量a被环境类型分类为public，那么a的值在e1和e2中应该相等。该方案处理堆的直接扩展是要求两个环境的有根低可达图是同构的。由这个同构相关的位置然后被要求具有相等的值。图5通过描绘两个环境来说明这个想法，e1在左边图的一半，右边是e2，低可达树的根在前几个寄存器中，虚线弧表示同构。寄存器r1（ptr L L）的类型指示对象的结构（类）与对象的内容相同。寄存器r2的类型强制寄存器的内容相等。进一步进入树，C的第一个字段的类型要求对象的（共享）低内容相等，但不要求指向对象的结构相等。这种解释的安全性取决于字节码指针的不透明性。5.4类型规则本节介绍并讨论了一小部分类型规则，选择这些规则来解释类型系统的关键思想。指令的规则是176D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163Hptr LLLC堆（e1）寄存器堆（e2）HEHDR2R2Hptr L HR1R1ptr L HCe1 e2图五.低等同性形式：p1...pn;其被读取为指令i在静态环境中是类型正确的，该静态环境由所考虑的程序、方法的返回类型和其它约束以及产生环境的环境Γ组成，rJ.令Γ和Γ表示所有规则中的初始环境和静态环境。Γ的范围是无量化器的环境类型。所有规则的共同点是历史前提φi（Γ）=φ2，对于指令i。这个前提通过产生以下结果将规则与时序模型- 来自初始环境类型的新历史类型，其包含旧历史类型，并且在必要时包含指令的参数的类型5.4.1直接时间和终端泄漏我们假设攻击者不能直接看到终止和终止的原因。这允许我们有带秘密参数的部分指令。如果终止是直接可观察的，则关于（部分）参数的信息将泄漏。例如，如果除法运算的执行没有崩溃，我们就知道除数的值不同于0。在我们的例子中，非终止性只能通过公共输出向外部发出信号。因此，只要在对秘密信息执行部分指令之后禁止公共输出，就不会泄露任何内容，这使得我们有可能在低通信停止之后继续对秘密信息主要使用D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163177在输出L指令的类型规则中，L（r）= L（r 1）：L σ p：L φ<（l， e）of，t+（lJ，eJ）<$（lJ，eJ）<$re（lJ，eJ））1 1~lse112 2~lse2211lse，θ22θJ。（l1，e1）→lseeJ⇐⇒(l2,e2)→lseeJ)∧θ⊆θJ∧eJ=θJ，ΓeJ）自然，由于对象可以在高安全性上下文内分配，因此我们允许部分双射扩展以包括它们。为了简单起见，我们假设环境的域单调增长，即没有垃圾收集器。边条件侧条件的作用是表达秘密分支在一般情况下不受隐式流的影响，而不强制执行算法的实现。使用这样的副条件的好处是，它允许你用不同的实现实例化类型系统，只要它们保证副条件所要求的属性如果我们暂时忽略时间，近似边条件的一种方法是广泛使用的技术，禁止从高安全上下文修改公共环境位置。这可以很容易地看出近似于语义侧条件（假设整个程序已经被类型化）：如果禁止低修改，那么低输出也是如此，并且，很简单，所有低输出都是相等的。此外，由于高安全上下文的主体被禁止修改存储器的低部分，因此不能分配新的低对象，并且所有公共环境位置必须保持不变。eD. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163179H高安全性上下文乐如[1][Paper II]中所示，我们可以制定利用这一事实，我们可以通过（语法上）要求每个高调制都与高“非调制”匹配来近似侧条件，每个低调制（包括低输出）都与锁步中的等效低调制匹配。虽然这对于现实世界的程序来说似乎是一个不合理的要求，但对于使用[2]中的交叉复制思想转换的程序来说，它非常有用。虽然Agat只论证了功能时间模型的正确性，但这种方法对于简单的基于历史的缓存模型也是合理的，因为它保留了内存访问的顺序。作为隐式流的唯一来源，if @-指令的类型规则是唯一使用sid条件的地方。 假设bran_c_h，i_f@l1，l2，l_e是高安全上下文的头部（即，具有秘密参数），通过使用语义侧条件要求从l1和l2直到合并点l_e的所有迹线的低观测等价性来禁止隐式追踪。令δ在同时封闭Γ和Γe的替换上值域。l1 l2φif@（r）=φ2Γ J= s，r，σ p，σ2型（ε，l e）= ε[Δ ε]. ΓeσL=σLδ。δ（σ）=H=δ（ΓJ），δ（Γe）l1{l e}2n;intσ·s，r，σp，1if@l1，l2，le j见图6。 条件分支为了验证边条件的使用和并行安全级别，考虑图7中的小程序，其中寄存器r1在高安全上下文内是公共的，但在合并点处是秘密的，因为它根据采取的分支而具有不同的值，而寄存器r2可以被认为是公共的，即使它在上下文内是秘密的，因为它在到达l4时总是等于1。因为没有使用部分指令，所以这段代码在pc类型中是多态的。假设一个常数时间模型，我们看到程序将在不同的时间到达l4，这取决于采取哪一个分支，这是由标签l4类型上的时间类型H180D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163...l1：（s：（int H）. a）（r1： intL，r2： intH）pct if l2 l3 l4l2：（s：a）（r1：intL，r2：intH）pctconst1备份存储1商店2转到l4l3：（s：a）（r1：intL，r2：intH）pctconst2存储1常数1存储2l4：（s：a）（r1：int H，r2：int L）pc H...见图7。 条件分支指针类型类型语言的另一个显著特征是指针的类型，它在指针值的安全级别和所指向对象的结构之间进行区分，这在长度指令的类型规则中进行了说明，φlength（Γ）=φ2σ1，σ2τ·s，r，σp，σ1τtht其中返回的长度类型仅反映数组指针的结构类型，这是安全的，因为长度指令无法区分两个大小相似的数组。这个特性与Agat风格的边条件一起可能是有用的，它允许精确近似低可观测性。 pc不受指针类型的限制，如果我们将空指针的长度定义为0，这是安全的。5.4.3程序、方法和基本模块如果程序的所有方法都是类型正确的，则程序是类型正确的一个方法是类型正确的，如果它的所有基本块都是类型正确的。方法的返回类型。此外，初始基本块的类型应该与执行兼容方法类型提供的环境如果基本块的指令序列在基本块的入口类型中是类型正确的，则基本块是类型正确的，从而产生与所有类型兼容的退出类型D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163181基本块的后继者。6结论和今后的工作我们已经制定了一个时间感知的信息流类型的系统的一个子集的字节码类语言。我们的方法概括了以前的尝试，通过参数化的语义和类型系统的时间模型。该项目仍处于初期阶段，还有许多工作要做。如上所述，类型系统已经制定了正确性证明，但任何这样的证明仍然是未来工作的重要组成部分。我们已经创建了一个原型实现，并开始通过一系列基本测试进行初步评估，包括模幂运算的实现[9]。原型实现只做类型检查，由于类型的大小，它不能很好地扩展到实际大小的程序。在本文中，我们提出了稍微简化的对象类型，每个类有一个安全类型。这对于整个程序分析来说是令人满意的，但在组合性和可推断性方面是有问题的，因为对于一个类的字段没有最一般的安全类型。如果一个字段既不是强制公开的，也不是强制秘密的，我们可以选择其中之一，但这两种选择都不适合所有程序。例如，假设我们创建了一个容器类。如果我们选择元素是公开的，我们就不能将秘密存储到容器中，反之亦然。如果没有类型系统的支持，我们最终将不得不实现两个不同的容器：一个用于公共信息，一个用于秘密信息。对于两级安全网格，这可能是可接受的，但对于更丰富的结构，这肯定是不可接受的。 这个问题的一个自然的补救办法是允许对象类型在限制为统一递归的安全级别中是多态的，以避免循环对象的问题。我们相信这些类型是可推断的，推理的实现即将到来。鸣谢感谢裁判，感谢Tobias Gedell，Ulf Norell，Andrei Sabelfeld和凯尔·罗斯提供有用的建议。这项工作得到了瑞典战略研究基金会（SSF）、VR和Vinova的部分资助。引用[1] J. 阿加特隐通道消除和寄存器分配的基于类型的技术。博士论文，查尔姆斯理工大学和哥德堡大学，瑞典哥德堡，2000年12月。[2] 约翰·阿加特。把时间泄露的东西换掉。见POPL，第40[3] A. Banerjee和D.瑙曼安全的信息流和指针配置在一个类似java的语言。在Proc. IEEE计算机安全基础研讨会，第253-267页，2002年6月。182D. Hedin，D.Sands/Electronic Notes in Theoretical Computer Science 141（2005）163[4] Gilles Barthe，Amitabh Basu，and Tamara Rezk.安全类