0%

静态程序分析课程笔记(安全)

在软件安全中,最常见的漏洞有注入类漏洞(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

信息流安全主要有两步骤:

  1. 将变量划分为不同安全等级(Security Levels)
  2. 对不同等级的信息流做不同策略(Information Flow)

Security Levels

通常对信息流分为两级——高级(H)和低级(L),表示秘密和公开信息。

Dorothy 等人[2] 曾提出用格表示信息流,即 $L\leq H$

实际中也可以有更多级。

Infomation Flow Policy

高密级信息不能影响低密级信息,即高密级不能流向低密级,如下图所示:
image-20200905193021433

Confidentiality and Integrity

保密性(Confidentiality):阻止秘密信息被泄露,可以看出先前的策略就是保证了保密性,信息泄露类漏洞就是违反了保密性;

完整性(Integrity):保证重要信息不被不可信信息污染,注入类漏洞就是违反了完整性。

下图可以看出Confidentiality和Integrity是对称的,可以视为信息的读安全和写安全:
image-20200905194503470

这也意味着,可以用相同的技术解决以上两类漏洞。

Explicit Flow and Convert Channels

显示流(Explicit Flow)指直接通过赋值传递信息的流,如:

  • x = y
  • x = y + z

隐秘信道(Convert Channels)[4]指通过控制流影响保密数据的信息流,例如如下代码:

1
2
3
4
5
6
secret = getSecret();
if (secret < 0) {
publik = 1;
} else {
publik = 0;
}

可以看出,根据 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
  • 借助指针分析完成污点分析

以上下文不敏感的指针分析为例:

首先定义数据抽象:

image-20200905202944738

在数据抽象中加入污点数据(Taint Data),$T\subset O$

分析的输入为定义的 source 和 sink,输出为 TaintFlows,记为$ \in TaintFlows$, 表示污点 $t_i$ 传入了敏感函数 $m$ 中。

在 call statments 中根据source产生污点 $t_l$:
image-20200905204725605

剩下的污点传播规则与指针分析一致:
image-20200905204756009

在call statements中检查污点是否传播到sink:
image-20200905205129601

下图举例说明了一个在指针分析的同时做污点分析的过程:

image-20200905205353856

注意,这里只介绍了最简单的污点分析,真实情况比样例复杂很多,当需要处理其他语句和方法,比如 Java 中字符串拼接方法append(),但是基本思路是不变的。

References

  1. Dorothy E. Denning and Peter J. Denning, “Certification of Programs for Secure Information Flow”. CACM 1977.
  2. Dorothy E. Denning, “A Lattice Model of Secure Information Flow”. CACM 1976.
  3. Ken Biba, “Integrity Considerations for Secure Computer Systems”. Technical Report, ESD-TR-76-372, USAF Electronic Systems Division, Bed-ford, MA, 1977.
  4. Butler W. Lampson, “A Note on the Confinement Problem”. CACM 1973