[所有分类]课件9：第434节信息流控制机制

4.3 信息流控制机制综述 n 信息流的控制机制的设计与实施方法：n 一是 在编译时刻检查与验证信息流的安全性；n 二是 在执行时刻验证与检查信息流的安全性；n 三是 利用程序正确性证明技术去验证程序的安全性，这种方法建立在 “ 格模型与 Hoar功能正确性推理系统 ” 上的信息流演绎系统，可以给出一个更为精确的安全性实施机制，但这一部分内容要求的理论基础比较深， 4.3.1 安全性与精确性 n 设 F是一个信息流系统中所有可能信息流的集合，n E是在给定的流控制机制下可执行的 F的子集，n P是给定策略下授权的流。n 如果 EP， 即所有可执行的流都是授权的，那么系统是 安全的 。n 如果 E=P， 即所有授权的流都是可执行的，那么安全系统是 精确的 。安全性与精确性图示（非授权的流）P（ 给定策略下授权的流）E（ 给定机制下可执行的流）F所有可能的流n 设 s0是一个初态， s0肯定是授权的，因为流都与状态转换相关，此时没有状态变化，也就没有流。n 再设 s是通过执行命令序列 从 s0推出的状态，那么 s是授权的当且仅当所有流 xs0ys都是授权的，即 SC(xs0)SC( ys)。n 根据关系 的传递性，如果系统中每一状态转换引起的流都是授权的，该系统就是安全系统。 n 同时支持访问控制策略和信息流控制策略的系统的 统一安全性定义 ： n 如果 si是授权的，那么通过执行命令 c从状态 si转换到状态 si+1， si+1是授权的，当且仅当 c是安全保持的，即 c满足访问控制策略和信息流动策略。n 一个保护系统 是安全的 ，当且仅当（ 1）初始状态是授权的，并且（ 2）每一状态转换所得状态也是授权的。 n 例 1 考虑赋值语句 “y := kx”。n 假定在一个策略中， SC(k)SC(y) 成立，但SC(x)SC(y) 不成立。n 如果总是禁止其执行，是安全的，但不精确。n 如果 k=0或 H(x)=0， 执行语句不导致流 xy的发生。n 设计 “ 仅对实际流 xy证明关系 SC(x)SC(y)” 的机制，远比设计 “ 对能够潜在地引起流 xy的任何运算，证明关系 SC(x)SC(y)” 的机制困难。n 对于进一步复杂的问题，一个给定的系统是否安全的或精确的，一般而言是不可判定的。 构造一个既满足安全性又满足精确性的机制是困难的。 n 例 2 考虑语句n if f(n) halts then y:=x else y:=0其中 f是任意函数，且关系 SC(x)SC(y) 不成立。n 考虑两个系统，一个总是允许该语句的执行，而另一个则禁止执行它。显然，不解决 停机问题 ，第一个系统是否安全，或第二个系统是否精确的都是不可判定的。n 研究结果表明，构造一个既是安全的、又是精确的机制在理论上是不成立的。 n 在一个安全系统中，任何客体 y的安全类至少和存储在 y中的信息的安全类一样高。n 可变类 SC(y)的安全级可增可降，不一定在时间上必须单调增加的。n 实际上，如果高安全类信息从 y清除后，那么 SC(y)可以降低。 n 只要不违反系统的安全策略，在任何时刻都可以提高或降低一个客体的安全类n 例 3 考虑下述语句序列y:=x；z:=y；y:=0；n 在第一条语句执行前， SC(y)必须满足SC(x)SC(y) 以符合流 xy的要求，在第一条语句执行后，就有 SC(y)=SC(x)。n 执行最后一条语句后， y中的内容被清空了，不再含有关于 x的信息。因此， SC(y)可以低于 SC(x)。4.3.2 流的信道 n 1、正规信道 （ Legitimate channels）。 通过设计者指定的信息传送渠道（如进程参数）在程序或进程间传送信息的。n 2、存储信道 （ Storage channels）。 是指由多个进程或程序共享的客体，例如通过共享文件或程序中的全局变量传递信息。n 3、隐蔽信道 （ Cover channels） 是指不被设计者或用户所知道的泄漏系统内部信息的信道，例如， 通过观察某个进程的操作规律，判断这个进程在干什么。这种信道也并不完全面向信息交换，例如， 进程在系统加载过程中产生的某些效果。n 正规信道的安全防护最简单 。存储信道的安全防护要困难得多，因为每一个客体（可能是文件、变元和状态比特）都需要保护。 n 例 4 一个进程 P可以通过共享文件 F的锁定位把一个值 X传送给另一个进程 Q， 虽然限制 X只能被 P使用，不能被 Q直接访问。n 方法是： P首先根据 X的二进制值在规定的时间区段内安排文件的打开或者关闭，使文件 F的打开与关闭次数与 X的二进制值关联起来；n 进程 Q在同样的时间段内，请求使用该文件，根据请求是否被允许的次数就可以决定 X的相应二进制值。 n 问题在于 可以将信息用某种外部观察者可检测的物理现象编码。n 例如， 一个进程可以使它的 执行时间 正比于它所读到的某机密变量 X的值，通过测量独立于系统运行时钟上的运行时间，另一个进程（或用户）可以确定 X的值。n 这种类型的隐蔽信道称为 “时钟信道 ”，其他资源，如电力消耗，甚至控制台上的内部寄存器显示灯等都有可能被用作隐蔽信道。隐蔽信道的防范是困难的n 对隐蔽信道的 唯一技术解决办法 是要求作业事先说明它们的资源要求。n 所请求的资源都交给作业控制，即使作业未运行完，系统也必须精确地在指定的时间内把这些资源收回。n 应用这种策略后，很难从事先不知道的执行时间或资源推导出某些东西。n 即使如此，用户仍能从他们的程序是否成功地结束而推出某些东西。 4.4 基于执行的机制 n 在执行时刻检查信息流安全性方法的原理比较直观，这种机制相对容易理解一些；n 在编译时刻（程序未执行的情况下）验证信息流的安全性，需要了解一些编译的知识和一些比较抽象的验证技术，因而基于编译的执行机制理解起来比较困难。 4.4.1 流安全的访问控制 n 在访问控制机构中增加流控制是合理的，方法如下： n 给每个进程 p指定一个安全类 SC(p)， SC(p)说明 p可以读入的最高类和可写入的最低类。n P(in: x1,x2, xm, out: y1,y2, yn)n 访问控制允许 p对客体 x获得读访问仅当SC(x)SC(p),n 允许 p对客体 y获得写访问仅当 SC(p)SC(y)。n 因此 p能够从 x1， x2， ， xm读出而向 y1，y2， ， yn写入，仅当n SC(x1)SC(x2) SC(xm)SC(p) SC(y1)SC( y2)SC( yn) n 显然， 该关系保证了进程内部的所有流（显式的或隐式的）安全性。 SC(y1) SC(y2) SC( yn) 输出安全类SC(y1)SC(y2) SC(yn) 最大下界SC（ p）SC(x1)SC(x2) SC(xm) 最小上界SC(x1) SC(x2) SC(xm) 输入安全类图 4-8 结合流控的访问控制机制 P(in: x1,x2, xm, out: y1,y2, yn)n 动态可变的安全类（即动态指派）方式会导致信息流泄漏（后面举例说明）；n 采用固定安全类方式，不会出现泄漏问题。n 为了安全起见，大多数基于访问控制机制约束的客体与进程只能使用固定的安全类。n 进程 p的安全类在初始化 p时就被确定了。 例 1 考察表 4-1中所示的 copy1过程。 x是一个参数，设 x=0或 1，则该过程完成把 x的值传送给 y的操作n Procedure copy1 (x : integer; var y: integer); /* 把 x拷贝到 y */Var z: integer;Beginy :=0 ; z :=0 ;if x=0 then z :=1 ; /* 执行后 SC(z)=SC(x) */if z=0 then y :=1 ; /* 执行后 SC(y)=SC(z) */endend copy1 表 4-1 copy1程序 存在隐式流 xzn 假定 copy1由两个并发进程 P1和 P2共同执行，在某一时刻被分裂为：P1： if x=0 then z :=1 ; P2： if z=0 then y :=1 ; n 进程 P1和 P2可以通过 全局变元 z通信，而 z具有动态可变安全类 。n 再假设 SC(P1)和 SC(P2)被置为对读或写操作的所有客体安全类的最小上界（ ）， y和 z初始时为 0都为 LOW类；n 仅当对 z进行赋值时， SC(z)也随着修改，n 仅当对 y进行赋值时，检查对 y的流的安全性。n 下面讨论 P1， P2执行 copy1的执行情况： P1： if x=0 then z :=1 ; P2： if z=0 then y :=1 ;n （ 1） 当 x=0时， P1以 z=1终止，此时由于 P1有读 x与写 z的操作，根据约定有 SC(z)= SC(P1) =SC(x)； 因此 SC(P2)通过读 z被置为SC(x)。n 在 P2中测试条件 “z=0”失败，所以不执行向 y的赋值操作（ y的值仍为 0），因而 关系SC(P2) SC(y)未得到验证。n P1： if x=0 then z :=1 ; P2： if z=0 then y :=1 ;n （ 2） 当 x=1时， 测试条件 “ x=0” 失败， P1读过 x以SC(P1)=SC(x)终止；由于 z :=1未被执行，所以 （z， SC(z)） 仍保持为（ 0， LOW）， 因此 SC(P2)也为 LOW；n 在 P2中测试条件 “ z=0” 成立，执行向 y的赋值操作后， y变为 1，且关系 LOWSC(y) 得到验证。n 在上述两者情况下， copy1的最后结果都为 y=x， 但都没有检验关系 SC(x)SC(y) 是否成立 。所以当关系 SC(x)SC(y) 不成立时，便产生了信息泄漏问题。n 当客体和进程都有固定安全类时，就不会产生这样的问题。n P1： if x=0 then z :=1 ; P2： if z=0 then y :=1 ;n 假定 P1以读 x所需的最小类执行，即SC(P1)=SC(x)， P1将不会被允许向 z写入，除非SC(x)SC(z) 成立，n 类似地， P2将不允许读 z， 除非 SC(z)SC(P2) 成立，并且 P2也不允许写入 y， 除非 SC(P2)SC(y)成立。n 因此，没有信息能够从 x流到 y， 除非满足SC(x)SC(z)SC(y) 。 n 流安全访问控制 为在用户进程内提供一个简单和有效的信息流控制机制。n 在这种机制下，由于在一个进程内不区别不同类的信息，还有局限性。n 例如 ，一个进程 P既读机密的（ HIGH）， 又读非机密的（ LOW） 数据，那么 SC(P)必须是 HIGH， 被 P写的任何客体也必须有 HIGH类。n P不能对 LOW类的客体写访问，因为没有办法知道传送给这些客体的信息是机密的或非机密的。所以，进程不能把仅从非机密的输入推出的信息给 LOW客体。 n 一般而言， 仅用访问控制 来实现 “ 同时处理不同类信息的进程 ” 中的安全性 是不可能的 。n 这就排除了 应用访问控制去实施 “ 必须访问不同类信息，但又要和不同类进程通信” 的某些操作系统进程的安全性。n 另外， 在系统进程内部的流必须是安全的， 以免 其他进程利用这一点通过系统状态变元来建立泄漏信道。n 例如 ，文件编辑程序中的特洛伊木马程序，可以利用这种信道泄漏正在编辑中的绝密信息给具有较低安全类的用户。 4.4.2 基于执行机制的模型 n 数据标记机 是一种研究执行时生效机制的保护系统模型，它是 Fenton,J.S.,于 1973年在其博士论文（信息保护系统）中提出的。n 模型机的设计应该是简洁的。数据标记机是一台扩充的 Minsky机，它包含为每一类寄存器（存储器单元）的安全类所作的标记。 n 一台 Minsky机含有 3条指令：x :=x+1 /* 加 1指令 */if x=0 then goto n else x :=x-1 /* 零条件分支或减 1 */halt /* 停机指令 */n 这里， x是一个寄存器， n是语句标号，n 尽管它很简单，但它可以计算所有可计算的函数，只要至少有两个（无限的）寄存器和一个含有 0的寄存器。 表 4-2 数据标记机指令语义 指令 执行效果（ pc是程序计数器）1、 x :=x+12、 if x=0then goto nelse x :=x-12、 if x=0 then goto nelse x :=x-13、