信息流与安全类型系统

信息流

信息安全需要解决的问题

访问控制问题：访问控制的基本任务时保证对客体的所有直接访问都是被认可的。它通过对信息的读，写，更改和删除的控制，保证系统的安全性和有效性，以免受偶然的和蓄意的侵犯。访问控制是一套为信息系统规定的安全策略和支持这些安全策略的执行机制来实现的。

信息流控制问题：信息流是Denning首先提出的，如果A信息影响了B信息的值，那么就存在从A到B的信息流。信息流控制策略是规定客体能够存储的信息的安全类和客体安全类之间的关系，其中包括不同安全类客体之间信息的流动关系。如果系统的访问控制机制是完善的，但缺乏适当的信息流策略或因缺乏实现信息流策略的适当机制也会造成信息的泄露。

基于句法分析的安全信息流研究状况和进展

安全策略，安全模型和安全机制

安全策略，安全模型和安全机制是安全设计的三个等级。安全策略定义什么行为是合法的，它是最高级的；模型是系统的抽象，它校验策略是否满足；机制是设计的最低级，用于模型和策略的实现。因为三个级别是分离的，从而一个策略可以由不同的机制来实现；一个机制可以对应不同的策略。

信息流安全

Denning等人最先注意到静态分析能用于控制信息流，静态分析方法增加分析的精度并减少运行时间开销。信息流的静态分析已经用定理证明得以实现。类型校验是静态分析信息流的一种方法，它已经在JIF编译器中实现。在类型检验中，每个程序表达式都有一个安全类型，安全类型包含两部分：

普通类型：例如整形，实形等

标签类型：描述被标注的值的使用

这里的标签完全是静态的。程序运行时并不计算标签。使用类型校验时，标签在标注数据上定义了一种信息流对策：类型校验强制安全；编译器读有标注类型的程序并校验程序，以确保在运行时程序不会有不适当的信息流。这种语言的类型系统就是强制信息流对策的安全类型系统。

    精确跟踪隐含信息流是信息流控制静态强制的主要优点。静态检验还能改变精确性，原因是动态强制只有单个程序执行的信息；而编译时间类型检验能证明：如果语句含有不安全的赋值，那么就没有可能的执行路径。保密性不是单一执行路径的特性，而是所有可能执行路径集合的特性。

    Benjamin C.Pierce 给出了类型的定义。Christian Skallka对类型系统进行静态安全强制并提供了一个静态类型安全系统以检验静态访问。Andrew C.Myers 给出了静态检验信息流的语言JFLOW。Dennis Volpano使用类型系统证明了Denning 工作的可靠性。Xavier Leroy注意类型化程序的安全特性。

不干扰

    如果用户要保密某些数据，该用户提出一个策略确保受保数据影响的数据不会被其他用户观察到。程序的低级输出不会揭示任有关保密数据保密的信息，策略允许程序控制和改变保密性数据。保密数据不干扰公用数据，这类策略就是不干扰策略。

    假定攻击者（或无权用户）允许观看公用信息，证明不干扰成立的一般方法是：如果仅有保密输入改变，那么攻击者不能观察到执行结果的不同。不干扰可有程序执行的语义模型自然表示。

类型系统方法

    在类型判断中，类型规则描述给定安全级的程序，这些程序的安全级以其子程序的安全级为基础。类型判断在安全语境中确定程序的安全级。表达式类型和安全语境是一特殊的安全级。在这样的安全类型系统中，对给定的语境，如果信息流是安全的，那么表达式只类型化的。

    在安全信息流的早期工作中，为校验程序中的安全信息流，Denning等人提出了一个静态证明方法。给定程序客体一个安全级，并假定这些安全级形成一个格。每个程序客体绑定的安全级在程序声明中确定。对有效的安全信息流，这是一种基于类型的方法。Denning等人非形式化地证明这种方法是可靠的，也就是说，Denning 等人的方法只能证明安全程序。后来，Volpano等人开发了一个面向句法的类型系统，支持具有安全级的变量，命令和过程参数。并证明他们的类型系统确保不干扰。

    安全信息流的类型系统是不完备的，一旦在程序语言中增加新的表达式，就需要扩展类型系统。

类型系统

    类型系统是在计算机科学中，类型系统用于定义如何将编程语言中的数值和表达式归类为不同的类型，如何操作这些类型，这些类型如何相互作用。类型可以确认一个值或者一组具有特定的意义和目的（虽然某些类型，如抽象类型和函数类型，在程序运行中，可能不能表示为值）。类型系统在不同语之间有非常大的不同，也许，最主要的差异存在于编译时期的语法，以及运行时期的操作实现方式。

    编译器可能使用值的静态类型以优化所需的存储区，并选取对值运算时的较佳的算法。类型的约束程序以及评估方法，影响语言的类型。更进一步，编程语言可能就类型多态性部分，对每一个类型都对应了一个极度个别的算法的运算。类型理论研究类型系统，尽管实际的编程语言类型系统，起源于电脑架构的实际问题，编译器实现，以及语言设计。

    程序通常对每一个值关系一个特定的类型（尽管一个类型可以由一个以上的子类型）。其他的实体，如对象，模块，依赖关系，或者纯粹的类型自己，可以和一个类型关系。例如：

数据类型：一个数值的类型

类型：一个对象的类型

种类：一个类型的类型

在每一个编程语言中，都有一个特定的类型系统，保证程序的表现良好，并且排除违规的行为。作用系统对类型系统提供更多细微的控制。

类型检查：类型检查所进行的检验处理以及实行类型的约束，可发生在编译时期（静态检查）或运行时期（动态检查）。静态类型检查是在编译器所进行语义分析中进行的。如果一个语言强制类型规则（即通常只允许以不丢失信息为前提的自动类型转换）就称此处理Wie强类型，反之称为弱类型。

类型检查

    类型检查所进行的检验处理以及实行类型的约束，可发生在编译时期（静态检查）或运行时期（动态检查）。静态类型检查是在编译器所进行语义分析中进行的。如果一个语言强制实行类型规则（即通常只允许以不丢失信息为前提的自动类型转换）就称此处理为强类型，反之称为弱类型。

动态检查

    如果一个编程语言的类型检查，可在不测试运行时表达式的等价性的情况下进行，该语言即为静态类型的。一个静态类型的编程语言，是在运行时期和编译时期之间的处理阶段下重视这些区别。如果程序的独立模块，可进行各自的类型检查（独立编译），而无需所有会在运行时出现的模块的那些信息，该语言即具有一个编译时期阶段。如果一个变成语言支持运行时期（动态）调度已标记的数据，该语言即为动态类型的。如果一个编程语言破坏了阶段的区别，因而类型检查所需要测试运行时期的表达式的等价性，该语言即为依存类型的。

安全，有了类型系统以后就可以实现类型安全，这时候程序就变成了一个严格的数学证明过程，编译器可以机械地验证程序某种程序的正确性，从而杜绝很多错误的发生。

抽象能力，在安全的前提下，一个强大的类型系统的标准是抽象能力，能将程序中很多东西纳入安全的类型系统中进行抽象，这在安全性的前提下又不损耗灵活性，甚至性能也很优化。动态语言的抽象能力可以很强，但安全性和性能就不行了。

工程能力，一个强类型的编程语言比动态类型的语言更适合大规模软件的构建，哪怕不存在性能问题，但是同样取决于前两点。

对于编译器来说能清楚程序的意图，对于人来说也是如此。一个函数或者类似的东西，说白了就是一个映射关系，Pyhton中这些映射关系都是没有很明显地约束，要靠约定和默契才能维持，对大型软件来说这是不行的。一个优秀的强类型的程序，很多函数都不需要文档，光看函数申明就可以了。而在安全的前提下的抽象，也是很不容易引发灾难的。不过，同时类型检查和标注增加了学习成本和编码时间成本（类型推导不是万能的），编译不过也会挫伤初学者的信心，不像动态语言上马就能干，边干边学。不过个人觉得值。

数据流分析的方法

    安全信息流的类型系统实现简单，但往往不精确。类型系统过于关注局部信息泄露，把许多"安全"程序判定为"不安全"，但局部信息泄露的存在并不意味着程序有信息泄露。例如程序：

                         L:=H;L:=0

这里L是滴安全级变量，H是高安全级变量。安全类型系统将拒绝这个程序，因为第一赋值存在从高安全级到低安全级的信息流。然而程序显然满足不干扰。基于类型系统的方法拒绝任何带有不安全子程序的安全程序。

    为了研究被类型系统方法拒绝的安全程序，我们用基于句法分析的另一种方法——数据流分析的方法来研究带有不安全子程序的安全程序。

    假定信息仅有低密级（L）和高密级（H）两个安全级，且L<H。程序中的每个变量x都绑定一个初始安全级，表示为x。在数据流分析中，我们引入两个表示符和，其中表示存在从任意H变量到L变量X的信息流时，L变量x的密级升级；表示存在从L变量到H变量x的信息流时，H变量x的密级降级。我们的研究表明：如果在给定的程序终止出，不存在密级已升级的变量，那么久能保证该程序是安全的。这样，我们就可以接受许多被类型系统拒绝的安全程序。

安全类型系统在编译技术中的应用研究

类型系统是一种设计和研究程序设计语言的形式化方法和工具。构造程序设计语言的类型系统可以为描述语言的语义提供好的数学模型，便于严格、准确、正确地设计实现语言；也可以为研究语言的语义以及其他性质建立模型。编译器实质上是一个翻译程序，它将高级程序语言书写的源程序翻译为低级语言（机器语言或汇编语言）书写的目标程序。在程序设计语言的编译器中实现类型系统，对提高语言的编译效率、程序的安全性和程序的正确性有重要意义。本文通过定义安全类型系统进行信息流的静态分析来检测程序中的类型信息和信息流的安全漏洞，进而保证程序的信息安全，实现程序设计语言的正确、安全编译。

类型系统的形式化定义

在程序设计语言中，类型是对程序的某种限制，是对底层数据表示，使用的某种约束，而类型系统是将类型表达式指派到程序各部分的一组规则，通常给程序加上一个静态类型结构，给所有常数，变量以及函数符号附加上类型信息。

定义 1（项）项是语言中的语法成分，或称为语法单位，记作T。如每个文法产生式的右部是项，一个赋值表达式是项。项是类型系统操作的的对象，一个程序也可看作一个项。

定义2 （类型）类型可以按照如下规则递归定义：

1. 基类型是类型
2. 类型变量是类型（有无限多个）
3. 若是有n个参数的类型构造子，是任意类型，则是类型。
4. 除此之外，没有别的是类型。

   其中，基本类型是原子类型，如integer,char,Boolean与real等都是类型；类型变量是可以任意类型为值的变量；类型构造子是类型道德函数，它以类型为参数，当应用在类型上时，得到一种新的类型。

定义3 类型陈述是形如的公式，其中T是项，是谓词。意思是："被指派给T"或"T具有类型"

定义4 基础或合适环境是一无限或有限公式集合,,即主词互不相同。

定义 5 （类型系统或类型指派系统）类型指派系统TAS是一个自然演绎的形式系统，由公式，演绎规则两部分组成。

安全类型系统

    在这里，我们扩展类型系统中类型的定义，称为安全类型。每个安全类型分为两部分：一部分是前面我们定义的普通类型，如整型（int）；另一部分是安全标识，用来标记项的安全级别，我们这里具体指机密性等级，比如L(Low)、M(Medium)和H(High)，当然可以推广到任意级别。

安全类型系统在编译技术中的应用

    程序设计语言编译器的任务时读入用源语言书写的程序设计语言编译器必须检查源程序是否符合源语言规定的语法和语义要求，检测并报告程序中某些类型的错误，这种检查称为类型检测。类型检测是通过类型系统完成的。类型推理是指以类型系统为项指派类型的过程。当程序中有足够的类型信息时，类型系统值检测程序中变量或函数的使用是否与所给的类型一致，即进行类型检测；如果程序中给出较少甚至不给出类型信息时，编译时由类型系统根据程序中变量的使用情况推导出所缺类型信息，即进行类型推理或类型重构。当程序有足够的类型信息时，类型推理就简化为类型检查。

    安全类型系统在编译过程中的地位如下图所示。

    使用安全类型系统的编译器读取带有安全标识的源程序不但可以检测类型错误，还可以检测到程序中非法的不安全信息。这样程序在运行时就不再带有非法信息流，从而可以保证目标程序的正确性和安全性。