Pre
在之前的文章中我简单的介绍了一种描述计算机安全常用的方式: Non-interference模型(GMNI)。 再用一句话来回顾一下什么是non-intererence, 在一个系统中如果我们去掉所有的高安全输入，系统的低安全等级输出并不会发生任何变化。 在这个模型的基础上我们可以进一步来定义什么样的信息流是安全的(这里的信息流可以直接理解成数据流，即程序运行中变量值变化的轨迹)。GMNI模型是要求程序是deterministic的， 接下来所有的讨论依然会只关心 与程序终止无关的程序片段。
安全信息流
我们可以用如下方式更加详细的描述程序中什么样的数据流是安全的 ：
给定一个程序
, 其中变量集合
是高安全等级变量 ，
是低安全等级变量， 称程序
中的变量的值不依赖与
中变量的初始值。
在实践中我们可以用给程序中的变量打上label的方式来标记程序变量的安全等级。这里的label最简单的可以只有两种安全等级， 高和低。也有一些比较复杂的系统比如去Barbara Liskov的去中心化标记模型(decentralized label model), 这个我会在后面的文章里面讲(希望我能一直更新hhhh)。为了方便，本文只会讨论最简单的label系统。
我们也可以用更加形式化的语言来描述：
给定一个程序
有
,
其中记号 表示一个store中只与变量集合X中有关的部分， 比如
。
代表程序终止。
safety
通常来说程序的安全性的定义与程序的执行轨迹(trace)相关，就像在最原本GMNI模型中定义的那样， Micheal Clarkson在Hyperproperties论文中展示了一个比较简洁直接的定义。
在这里我不想展开讲，后面单独写hyperproperties的时候再仔细写
store和trace有很强的联系，如果我们只看程序最终的store，那么可以得到如下的定义。
Pr是某一程序语言的程序集合，那么这种语言的安全性(safety)可以用如下的方式来描述：
对于,存在逻辑表达式
满足，
这里不难看出安全数据流问题边并不是一个严格意义上的“安全问题”。因为很明显的可以看到前面安全数据流的定义中我们是在对两个值进行quantify，但是safety的定义中全称量词只有一个。这一点在McLean 94年的A general theory of composition for trace sets closed under selective interleaving functions. 里面给了详细的证明。
2-safety
在计算机安全中数据流安全是很重要的一种性质，之前的讨论已经可以看出，数据流安全重点在于讨论对于任意两次不同的程序执行，我们希望能够的得到某种性质。对于上面的safety定义我们可以稍稍修改就可以得到任意两次版本的安全性质：2-safety。
Pr是某一程序语言的程序集合，那么这种语言的安全性(safety)可以用如下的方式来描述：
对于满足，
这种类型的性质还可以继续推广得到k-safety,就是为了分类那些要对多条轨迹进行quantify的那些性质。这里的2啊，k啊的名字已经慢慢的暗示我们，单纯的性质(property)可能还不能满足我们对于程序运行安全性质的描述需求，我们需要对性质再进行抽象得到一种类似二阶性质，也就是超性质(hyperproperty)。
技巧： Self-Compose
如果我们希望对一种现实中存在的语言进行数据流安全的验证，一种非常常见和直接的做法是，设计一个类型系统，在这种类型系统中，每一个变量的类型中还需要加上label。Jif就是这种思路的一个非常好的实践， Jif中的label系统还是比较复杂的，他就使用了我之前提到的decentrialized label model.通过类型check，来自动的验证程序中的信息流安全。这种方式扩展了程序的类型系统语义(Jif就是扩展了Java的类型系统)。但是如果我们仔细观察2-safety的定义，对于数据流安全这样的2-safety问题，既然是论证程序的两次运行，那么我们为什么不直接让程序跑两次呢？自组合(self-compose)就是这种思路最好的体现。
对于程序P, 表示所有P中的变量，C(P)是对程序P的一个拷贝， 其中所有的变量名全部替换为原来的变量名加上
'.
S是是一个2-safety性质, 对于某个逻辑表达式
,自组合规约可以定义为
其中
;代表程序顺序执行。
使用自组合可以重新定义信息流安全：
给定一个程序
光看定义很复杂但是其实非常简单，用人话说就是把一个程序复制一遍贴在原来的程序后面，然后把里面所有的变量名全都换成原来的名字加一撇，然后信息流安全就是说假设输入的时候所有的低安全级别的输入都相同，程序最终结束的时候两次运行的低安全变量的结果相同
看个例子吧， 原本的程序如下：
z := 1;
if (h) then x := 1 else skip;
if (¬h) then x := z else skip;
l := x + y
其中变量h是高安全等级的变量，其他是低安全等级的变量。我们可以让他跑两次，self-compose一下：
z := 1;
if (h) then x := 1 else skip;
if (¬h) then x := z else skip;
l := x + y;
z ′ := 1;
if (h′) then x′ := 1 else skip;
if (¬h′ ) then x′ := z ′ else skip
l′ := x ′ + y′
这时候比如我们想要检测l有没有信息泄露我们只需要令程序运行之前所有的除h外的变量和他们的复制变量都相等， 最后结束的时候保证l=l'。 从霍尔逻辑的角度来说就是给一个前条件，{x=x',y=y',z=z',l=l'}, 后条件{l=l'}，验证一下就行。 如果是用coq之类的东西去做证明，这种方式比最原本的那个GMNI模型要容易很多。后面等空了我也会亲自写一下再比较两种方法证明上的差异。
其实这个例子还可以看出self-compose对于传统使用类型系统的方式是有一定的优势的。如果是传统的使用label type这个程序是要被判定为不安全的，因为l的值是要用到和h有关的分支中的值的，但是实际上由于我们对信息流的安全讲的是一个最终的程序状态，这个程序最终l不管h如何取值都是y+1。如果我们使用self-compose的方式， 这种情况我们就可以给证出来是安全的。
Dafny是一个z3的wrapper， 使用这个语言我们可以给程序增加前条件和后条件的方式，我们可以轻松的验证一下self-compose变换以后的测试程序
// test.dfy
method test(x:int,y:int,z:int, h:bool, hp:bool) returns (l: int, lp: int)
ensures l == lp
{
var x1 := x;
var x2 := x;
var y1 := y;
var y2 := y;
var z1 := z;
var z2 := z;
z1 := 1;
if h {
x1 := 1;
}
else {
x1 := z1;
}
l := x1 + y1;
z2 := 1;
if hp {
x2 := 1;
}
else {
x2 := z2;
}
lp := x2 + y2;
}
不出所料dafny接受了上面的程序，正常编译。如果我们把原来程序中的z:=1替换成z:=2, self compose 变换后的dafny程序就会是
// test.dfy
method test(x:int,y:int,z:int, h:bool, hp:bool) returns (l: int, lp: int)
ensures l == lp
{
var x1 := x;
var x2 := x;
var y1 := y;
var y2 := y;
var z1 := z;
var z2 := z;
z1 := 1;
if h {
x1 := 2;
}
else {
x1 := z1;
}
l := x1 + y1;
z2 := 1;
if hp {
x2 := 2;
}
else {
x2 := z2;
}
lp := x2 + y2;
}
这一次 dafny 就会报错。说名其中的信息流就不再安全了， l的值会和h有关。
1 A postcondition might not hold on this return path.
Reference
Barthe, G., D'argenio, P. R., & Rezk, T. (2004, June). Secure information flow by self-composition. In Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004. (pp. 100-114). IEEE.
Terauchi, T., & Aiken, A. (2005, September). Secure information flow as a safety problem. In International Static Analysis Symposium (pp. 352-367). Springer, Berlin, Heidelberg.
Myers, A. C., & Liskov, B. (1997). A decentralized model for information flow control. ACM SIGOPS Operating Systems Review, 31(5), 129-142.
Jif 3.0: Java information flow Software release, July 2006. Andrew C. Myers, Lantian Zheng, Steve Zdancewic, Stephen Chong, and Nathaniel
Clarkson, M. R., & Schneider, F. B. (2010). Hyperproperties. Journal of Computer Security, 18(6), 1157-1210.Leino, K. R. M. (2010, April).
Dafny: An automatic program verifier for functional correctness. In International Conference on Logic for Programming Artificial Intelligence and Reasoning (pp. 348-370). Springer, Berlin, Heidelberg.
