在软件安全中,最常见的漏洞有注入类漏洞(Injection)和信息泄露(Information Leak),而本节课将介绍的Information Flow 分析方法可以有效处理以上漏洞,具体来说,就是我们常用的污点分析技术。
Information Flow Security
Information Flow
Information flow: if the information in variable x is transferred to variable y, then there is information flow x → y.
信息流[1] 指程序中的变量信息的流动,如有语句y = x
,那么存在信息流 $x\rightarrow y$,可以看出,信息流分析很像先前的指针分析。
Access Control v.s. Infomation Flow Security
访问控制用于检查信息访问的权限,但是无法检查有权限的用户做什么
信息流安全用于检查程序处理数据的安全性,是端到端的信息安全
实际系统中通常需要访问控制和信息流控制两者配合使用。
Information Flow Security
信息流安全主要有两步骤:
- 将变量划分为不同安全等级(Security Levels)
- 对不同等级的信息流做不同策略(Information Flow)
Security Levels
通常对信息流分为两级——高级(H)和低级(L),表示秘密和公开信息。
Dorothy 等人[2] 曾提出用格表示信息流,即 $L\leq H$
实际中也可以有更多级。
Infomation Flow Policy
高密级信息不能影响低密级信息,即高密级不能流向低密级,如下图所示:
Confidentiality and Integrity
保密性(Confidentiality):阻止秘密信息被泄露,可以看出先前的策略就是保证了保密性,信息泄露类漏洞就是违反了保密性;
完整性(Integrity):保证重要信息不被不可信信息污染,注入类漏洞就是违反了完整性。
下图可以看出Confidentiality和Integrity是对称的,可以视为信息的读安全和写安全:
这也意味着,可以用相同的技术解决以上两类漏洞。
Explicit Flow and Convert Channels
显示流(Explicit Flow)指直接通过赋值传递信息的流,如:
x = y
x = y + z
隐秘信道(Convert Channels)[4]指通过控制流影响保密数据的信息流,例如如下代码:
1 | secret = getSecret(); |
可以看出,根据 publik
数据可以推测 secret
正负。
通常来说,隐秘信道有以下表现形式
隐式流(Implicit flows)
if (secret < 0 ) p = 1; else p = 0;
终止信道(Termination channels)
while ( secret < 0 ) {...};
时间信道(Timing channels)
if ( secret < 0 ) for(...) {...};
异常(Exceptions)
if ( secret < 0 ) throw new Exception("...");
然而,隐藏信道泄露数据量较小,一般分析至针对显示流。
Taint Analysis
污点分析将数据分为两类,被污染数据和未被污染数据。
- Source:污点传播源,污点数据常常是一些函数的返回值;
- Sink:污点传播至关键点,也叫sink点,常常是敏感函数的参数。
对于 Confidentiality,可以其做如下定义:
- Source:保密数据
- Sink:泄露点
对于 Integrity,可对其做如下定义:
- Source:不可信数据
- Sink:敏感函数
Taint and Pointer Analysis
污点分析与指针分析非常类似,将污点分析做如下调整,就可以借助指针分析做污点分析:
- 将污点数据作为特殊objects
- 在allocation sites中产生source
- 借助指针分析完成污点分析
以上下文不敏感的指针分析为例:
首先定义数据抽象:
在数据抽象中加入污点数据(Taint Data),$T\subset O$
分析的输入为定义的 source 和 sink,输出为 TaintFlows,记为$
在 call statments 中根据source产生污点 $t_l$:
剩下的污点传播规则与指针分析一致:
在call statements中检查污点是否传播到sink:
下图举例说明了一个在指针分析的同时做污点分析的过程:
注意,这里只介绍了最简单的污点分析,真实情况比样例复杂很多,当需要处理其他语句和方法,比如 Java 中字符串拼接方法append()
,但是基本思路是不变的。
References
- Dorothy E. Denning and Peter J. Denning, “Certification of Programs for Secure Information Flow”. CACM 1977.
- Dorothy E. Denning, “A Lattice Model of Secure Information Flow”. CACM 1976.
- Ken Biba, “Integrity Considerations for Secure Computer Systems”. Technical Report, ESD-TR-76-372, USAF Electronic Systems Division, Bed-ford, MA, 1977.
- Butler W. Lampson, “A Note on the Confinement Problem”. CACM 1973