0

软件分析课程期末复习笔记

 1 year ago
source link: https://mengzelev.github.io/2021/01/07/static-program-analysis/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.

软件分析-期末复习

课程主页

感谢两位老师的精彩教学！

参考标准：每节课最后的The X You Need To Understand in This Lecture

中文为主，中英文使用纯看心情

Introduction

  • 静态分析与动态分析的区别
    • 在运行程序$P$之前就知道它是否满足某些性质
  • 理解soundness, completeness, false positive/negative
    • 想象3个圆：sound > truth > complete
    • false positive = sound-truth
    • false negative = truth-complete
  • 为什么静态分析一般选择soundness
    • 对于重要的应用方面来说更加关键（e.g. 编译优化、程序验证
    • 在bug detection中，soundness意味着能找到更多bug
    • static analysis：保证soundness，在precision和speed之间做trade-off
    • 每一种静态分析算法都是在保证safe的基础上，在precision和efficiency之间做trade-off
  • 如何理解abstraction & over-approximation
    • abstraction: 把具体问题的domain映射到抽象的domain上
    • over-approximation: transfer function定义了如何用abstract values计算不同的程序语句，不可能穷尽所有的可能性因此会损失精度，如flow merging

中间代码表示

  • 编译器与静态分析器之间的关系
    • 发生在IR生成后、机器代码生成前，一般用于进行代码优化
  • 理解三地址码（3AC）和它的common form (in IR Jimple)
  • 如何在IR的基础上构建基本块
  • 如何在基本块的基础上构建控制流图(CFG)

三地址码（3AC）

  • 右侧至多只能有一个操作符
  • 每条指令至多只能有3个地址；地址可以是：变量名/常数/临时变量

构建基本块

  • 输入：程序$P$的三地址码序列
  • 输出：一系列基本块
  • 算法：
    • 决定基本块的leader：程序的第一条指令、跳转语句的目标语句、跳转语句的下一条语句
    • 根据leader划分基本块

构建CFG

  • 基本块之间连边条件
    • 存在从A的结尾到B的开头的跳转语句
    • 在原来的执行顺序中B紧跟在A的后面，并且A不能以无条件跳转结束
  • 再加上ENTRY和EXIT

数据流分析-应用

  • 理解三种数据流分析：到达定值、活跃变量、可用表达式
  • 能够说出三种数据流分析的异同
  • 理解迭代算法并且能说出它为什么能终止
到达定值 活跃变量 可用表达式
Domain Set of definitions Set of variables Set of expressions
Direction Forward Backward Forward
May/Must May May Must
Boundary OUT[ENTRY]=$\emptyset$ IN[EXIT]=$\emptyset$ OUT[ENTRY]=$\emptyset$
Initialization OUT[B]=$\emptyset$ IN[B]=$\emptyset$ OUT[B]=$U$
Transfer Function OUT=gen$\cup$IN-kill OUT=gen$\cup$IN-kill OUT=gen$\cup$IN-kill
Meet $\cup$ $\cup$ $\cap$
  • 一个definition能不被kill掉地到达某一点
  • Data Flow Values/ Data Facts: the definitions of all the variables in a program (Abstraction)
  • transfer function:
    • gen：被定值
    • kill：定值被覆盖
  • 活跃变量：某一个变量在之后可能会被用到
  • transfer function（可以画图理解）在基本块内
    • 先use再def：gen
    • 先def再use：kill

可用表达式

  • 可用表达式：从程序开始到当前程序点的每一条路径都计算了这个表达式，并且计算之后表达式每个分量的值都没有被覆盖（意味着在该程序点，可以把求值换成该表达式上一次求值的结果）
  • transfer function
    • gen: 计算了这个表达式
    • kill：表达式的分量的值被覆盖

数据流分析-基础

  • 理解迭代算法的函数视角
  • lattice和complete lattice的定义
  • 理解不动点定理
  • 如何在lattice上总结may/must分析
  • MOP与迭代算法解的关系
  • Worklist算法

函数观点看迭代算法

  • CFG中$k$个结点的data flow values可以看成一个k-tuple 变量
  • 每一次迭代就相当于将函数$F: V^k\to V^k$作用在这个k-tuple上
  • 迭代终止条件：$X=F(X)$，没有数据流值发生变化，即到达函数的不动点
  • 偏序：自反+反对称+传递
  • 最小上界（lub）：$\sqcup S$； 最小下界（glb）：$\sqcap S$
  • 当只有两个元素时，$a\sqcup b$表示$a$和$b$的最小上界 (join)；$a\sqcap b$表示$a$和$b$的最大下界 (meet)
  • 格：偏序集中任意两个元素都存在lub和glb，那么这个偏序集就是一个格
  • Complete Lattice：偏序集中任意一个子集$S$内的元素都存在lub和glb，那么这个偏序集就是一个complete lattice
    • Complete lattice 都有最大元素$\top$ (top) 和最小元素$\bot$ (bottom)
  • 有限格一定是complete lattice
  • Product Lattice：一系列格的笛卡尔积
    • 如果每个格都是complete lattice，那么它们的product lattice也是complete lattice

数据流分析&格

  • 数据流分析框架$(D,L,F)$
    • $D$：分析方向（Forward/Backward）
    • $L$：格，所有data flow values的集合$V$+ meet/join operator
    • $F$：transfer function $V\to V$
  • 数据流分析可以看成：在格的values上迭代地应用transfer function和meet/join operation
  • 单调性+最优性：不一定只有一个不动点，但迭代算法能得到解且得到的是最优解
    • 不动点定理：给定一个complete lattice $(L, \sqsubseteq)$，如果满足：函数$f:L\to L$单调且$L$有限，那么
      • $L$的最小不动点可以通过迭代$f(\bot), f(f(\bot))\ldots ,f^k(\bot)$至达到不动点得到
      • $L$的最大不动点可以通过迭代$f(\top),f(f(\top)),\ldots,f^k(\top)$至达到不动点得到
  • 关联数据流分析框架与不动点定理
    • 每次迭代得到的结果都在一个product lattice中
    • 函数=transfer function + join/meet : 单调
      • transfer function本身单调，因为gen和kill是固定的
      • join/meet单调：$\forall x,y,z\in L, x\sqsubseteq y\Rightarrow x\sqcup z\sqsubseteq y\sqcup z$
  • 终止性：迭代算法一定能终止吗？
    • 格的height为$h$（从$\top$到$\bot$的最长路径长度），CFG结点数为$k$，则从$\bot$出发至多走$h*k$步可以到达$\top$（$k$个格，每个格走$h$步）

一点说明（以MAY-analysis为例）

  • Unsafe为bottom，trivially safe为top
  • Truth在这之间，truth之下为unsafe results，之上为safe results
  • Dataflow analysis从bottom开始往上走，越过truth（分析算法的设计本身保证走的方向一定是向上+能走过truth），到达某一个fixed point
  • Fixed points都位于truth上方，dataflow analysis到达的一定是位于最下方的最小fixed point
  • 越往上走precise越差，因为最上面的top是最不precise的结果

Meet-Over-All-Paths Solution (MOP)

  • MOP：用所有路径meet/join的结果作为最终结果 v.s. Ours：单纯对结点进行meet/join处理
  • MAY-analysis而言，MOP: $F(x)\sqcup F(y)$; Ours: $F(x\sqcup y)$
    • 根据单调性，有$F(x)\sqcup F(y)\sqsubseteq F(x\sqcup y)$, 这说明MOP更precise一些
    • 当$F$ distributive时，上式取等号，两者结果相同；
    • 之前的三个dataflow analysis都是distributive的（Bit-vector, gen-kill都是distributive的）
    • 但也存在不distributive的dataflow analysis，如常量传播
  • $x$在某个程序点是否一定具有某个常量值
  • Forward
  • Must-analysis
  • Top: UNDEF, Bottom: NAC
  • meet function：
    • NAC $\sqcap$ $v$ = NAC
    • UNDEF $\sqcap$ $v$ = UNDEF
    • $c$ $\sqcap$ $c$ = $c$
    • $c_1$ $\sqcap$ $c_2$ = NAC
  • transfer function: for assignment, kill=${x, _}$
    • x = c: gen=${(x,c)}$
    • x = y: gen=${(x, val(y))}$
    • x = y op z:
      • if $val(y),val(z)$ are constants, gen=${(x, val(y)\; op\; val(z)}$
      • if $val(y)=$NAC or $val(z)=$NAC, gen=${(x, \text{NAC})}$
      • otherwise, gen=${(x, \text{UNDEF})}$ —— 这么设计是为了满足单调性
  • For non-assignment statements, transfer function is the identity function

Worklist算法

（以Forward analysis为例）

OUT[ENTRY] = \emptyset
for each Basic Block B\ENTRY:
	OUT[B] = \emptyset
WL = [all basic blocks]
while WL is not empty:
	B = pick a Basic Block from WL
	old_OUT = OUT[B]
	IN[B] = meet all predecessors of B
	OUT[B] = gen + (IN[B] - kill)
	if OUT[B] != old_OUT:
		add all successors of B to WL
  • 维护一个Worklist
  • 初始化将所有Basic Block都放进去
  • 每次从里面取一个Basic Block进行迭代
  • 如果该Basic Block的结果发生改变，则把后继都加入Worklist中

过程间分析

  • 如何通过CHA建立call graph
  • 过程间CFG的概念
  • 过程间数据流分析的概念
  • 过程间常量传播

Call Graph

  • 程序中调用关系的一种表示
  • 从call-site到target methods (callee)的call edges的集合

Class Hierachy Analysis (CHA)

  • Java中的函数调用类型

    | | Static call | Special call | Virtual call |
    | —————- | ————– | ———————————————————— | —————————– |
    | 指令 | invokestatic | invokespecial | invokeinterface/invokevirtual |
    | Receiver Object | × | √ | √ |
    | Target Methods | Static methods | Constructor; Private instance methods; Superclass instance methods; | Other instance methods |
    | # Target Methods | 1 | 1 | >=1 (多态) |
    | Determinacy | Compile-time | Compile-time | Run-time |

    • 对Virtual Call的处理是OOP语言建立call graph的关键
    • 函数签名=class type + 函数名 + descriptor
    • descriptor = return type + parameter type
    • e.g. <C: T foo(P, Q, R)>

  • 运行时方法分配Dispatch($c,m$)

    • $c$: receiver object的class type
    • $m$: 待分配的method call
    • 如果$c$类中含有与$m$函数名descriptor都一致的非抽象方法，则返回该方法；否则在$c$的superclass中继续Dispatch
    • 需要类间的等级信息（继承结构）
    • 基于callsite上的receiver variable的declared type来分析virtual call
    • 假设属于某一个类的receiver variable可能指向它自己以及它的所有子类

  • CHA - Call Resolution

    Resolve(cs):
    	T = {} // 所有可能被调用的方法集合
    	m = method signature at cs
    	if cs is a static call:
    		T = {m}
    	if cs is a special call:
    		c^m = class type of m
            T = {Dispatch(c^m, m)}
        if cs is a virtual call:
        	c = declared type of receiver variable at cs
        	for each c' is c itself or a subclass (direct/indirect) if c:
        		add Dispatch(c', m) to T
        return T
    • 静态方法：它自己
    • special call：直接去方法所在的类Dispatch
    • virtual call：去receiver variable对应的类本身、所有直接或间接子类都找一遍
    • 快：只考虑receiver variable的类型和继承结构；忽略了数据流和控制流信息
    • 不准：容易引入伪目标

用CHA建立Call Graph

BuildCallGraph(m^entry):
	WL=[m^entry], RM={}, CG={}
	while WL is not empty:
		remove m from WL
		if m not in RM:
			add m to RM
			foreach call site cs in m:
				T = resolve(cs)
				foreach target method m' in T:
					add cs -> m' in CG
					add m' to WL

return CG
  • 对Worklist中每一个新加入的方法进行Resolve、将得到的所有可能的目标方法加边并加入Worklist中

过程间CFG (ICFG)

  • ICFG = CFG + call edge + return edge
    • call edge: call site - entry node of callees
    • return edge: return statement - return site (call site的下一条语句)
    • 原CFG中call site - return site之间的边保留：为了不让数据流信息去国外兜一圈
  • transfer function = node transfer + edge transfer
    • call edge transfer: 传递参数值
    • return edge transfer: 传递返回值
    • node transfer: 与过程内基本相同 + 需要kill掉LHS变量，如$b=f(a)$要kill掉$b$
  • 什么是指针分析
  • 理解指针分析的key factors
  • 理解指针分析的分析对象

什么是指针分析

  • 分析每个指针可能指向哪块内存地址
    • 对于OOP语言而言：分析每个变量/field可能指向哪个对象
  • May-analysis (over-approximation)
  • 别名分析（alias analysis）：两个指针能否指向同一个对象
    • 和PTA不是同一个问题，但PTA的结果可以回答这个问题

Key Factors

  • 堆抽象 Heap Abstraction
    • 如何对堆进行建模（如何表示不同的对象）
    • 把无穷的实际对象抽象为有限的抽象对象
    • 最常用的：Allocation-site Abstraction. 用创建点给对象命名，在同一个创建点创建的对象就是同一个对象
  • 上下文敏感性 Context Sensitivity
    • 如何对上下文进行建模
    • 上下文不敏感：合并一个方法的所有上下文，一个方法只需要分析一次——可能会损失精度
    • 上下文敏感：区别同一个方法不同的上下文，每个上下文分析一次
  • 流敏感性 Flow Sensitivity
    • 如何对控制流进行建模
    • 流敏感：保留语句执行顺序，在每个点维护一个points-to relation的map
    • 流不敏感：把整个程序看成语句的集合，整个程序只维护一个points-to relation map
  • 分析范围 Analysis Scope
    • 分析程序的哪些部分
    • Whole program v.s. Demand-driven
  • 只关心会影响指向关系的语句（pointer-affecting statements）
  • Java中的指针：局部变量、静态域、实例域（instance field）、数组（课程只关心local variable & instance field）
  • 影响指针的语句（5种）：New, Assign, Store, Load, Call

上下文不敏感的指针分析

  • 理解指针分析的rules，包括method call
  • 理解pointer flow graph
  • 理解过程间指针分析的算法
  • 理解on-the-fly的call graph construction

过程内指针分析

Rules

  • 定义域与符号标记
    • Variables: $x,y\in V$
    • Fields: $f,g\in F$
    • Objects: $o_i, o_j\in O$
    • Instance fields: $o_i.f, o_j.g\in O\times F$
    • Pointers: Pointer$=V\cup (O\times F)$
    • Points-to relation: $pt: \text{Pointer}\to\mathcal{P}(O)$
Kind Statement Rule
New i: x = new T() $$\frac{}{o_i\in pt(x)}$$
Assign x = y $$\frac{o_i\in pt(y)}{o_i\in pt(x)}$$
Store x.f = y $\frac{o_i\in pt(x)\quad o_j\in pt(y)}{o_j\in pt(o_i.f)}$
Load y = x.f $\frac{o_i\in pt(x)\quad o_j\in pt(o_i.f)}{o_j\in pt(y)}$
  • 实现关键：当$pt(x)$发生改变时，需要将改变的部分传播到和$x$有关的指针上
  • PFG：表示指针间的关联关系，将改变部分传播到一个指针的所有后继
    • 表达了对象如何在指针间流动的有向图
    • Nodes: Pointer
    • Edge: Pointer $\to$ Pointer
    • $x\to y$: $x$指向对象会流向$y$，$y$也会指向$x$指向的对象
  • 建立PFG和在PFG上传递指向关系是互相依赖的——PFG是动态更新的

过程内指针分析-算法

伪代码略，见过程间指针分析的算法

  • 准备工作
    • 为所有的New语句创建对象并加入WL
    • 为所有的Assign语句加边
  • 主循环：
    • 迭代WL中的<目标指针，待传播对象>二元组
    • 先对该二元组进行差量传播
    • 如果目标指针是变量而非instance field，就迭代所有待传播对象和该变量的所有Load/Store语句，进行加边操作
  • AddEdge($s,t$) 加边操作
    • 判断要加的边是否已经存在，如果是新的边再进行后续操作
    • 在PFG中加上这条边（唯一会修改PFG的操作）
    • 如果边的起点已经有一些指向对象，就放入WL中，方便后续把这些对象传播到终点上
  • Propagate($n, pts$) 传播操作
    • 如果待传播的对象集合是空集，就什么都不做
    • 把待传播的对象集合加到目标指针$n$的$pt$集中（唯一会修改$pt$集合的操作）
    • 把目标指针的后继和待传播对象都加入WL，以便后续传递
    • 差量传播：减少冗余信息的传递。一个指针如果已经在某个结点的$pt$集中，就不用进行二次传播了

过程间指针分析

Rules

对于语句l: r = x.k(a1, ..., an)
$$
\frac{o_i\in pt(x),\quad m=\text{Dispatch}(o_i, k)\
o_u\in pt(a_j),\; 1\le j\le n\
o_v\in pt(m_{ret})}
{o_i\in pt(m_{this})\
o_u\in pt(m_{p_j}),\; 1\le j\le n\
o_v\in pt(r)}
$$

  • 规则做了三件事：
    • 传递this变量的对象
    • 传递参数的对象
    • 传递返回值的对象
  • PFG加边
    • 对应参数间：实参$\to$形参
    • 返回值间：方法返回值$\to$LHS variable
    • receiver object到$m_{this}$间不加边，否则会损失精度
  • Call Graph的建立：从入口方法开始逐渐探索可达世界——到不了的都是死代码，提升精度和速度

过程间指针分析-算法

Solve(m_entry):
	WL=[], RM={}, PFG={}, CFG={}, S={}
	AddReachable(m_entry)

while WL is not empty:
		remove <n, pts> from WL
		delta = pts - pt(n)
		Propogate(n, delta)
		if n represents a variable x:
            foreach o_i in delta:
                foreach x.f = y in S:
                	AddEdge(y, o_i.f)
                foreach y = x.f in S:
                	AddEdge(o_i.f, y)
               	ProcessCall(x, o_i)

AddEdge(s, t):
	if s->t not in PFG:
		add s->t to PFG
		if pt(s) not empty:
			add <t, pt(s)> to WL

Propogate(n, pts):
	if pts not empty:
		pt(n) += pts
		foreach n->s in PFG:
			add <s, pts> to WL

AddReachable(m):
	if m not in RM:
		add m to RM
		S += S_m
		foreach i: x = new T() in S_m:
			add <x, {o_i}> to WL
		foreach x = y in S_m:
			AddEdge(y, x)

ProcessCall(x, o_i)
	foreach l: r = x.k(a1, ..., an) in S:
		m = Dispatch(o_i, k)
		add <m_this, o_i> to WL
		if l-> m not CG:
			add l->m in CG
			AddReachable(m)
			foreach parameter p_j of m:
				AddEdge(a_j, p_j)
			AddEdge(m_ret, r)
  • 准备工作
    • 初始化Worklist($WL$), 可达方法集合$RM$, PFG, CFG, 所有语句的集合$S$
    • 将入口方法标记可达
  • 主循环（基本同过程内，多了一步ProcessCall）
    • 迭代WL里所有的<目标指针，待传播对象>二元组
    • 对目标指针做差量传播
    • 如果目标指针是个变量，就迭代所有待传播对象：对所有Load/Store语句，进行加边操作；处理该变量的所有方法调用
  • AddReachable($m$) 标记可达
    • 如果该方法已经在可达集合内，就什么都不做
    • 将该方法加入可达集合
    • 将该方法的所有语句加入语句集合
    • 处理该方法内的所有New语句和Assign语句，同过程间分析的准备工作，New加WL，Assign加边
  • ProcessCall($x, o_i$) 处理某个变量的所有方法调用
    • 迭代该变量的所有方法调用，迭代Dispatch出的所有目标方法
    • 将当前对象与目标方法的this变量加入WL，以便后续传播
    • 如果调用点至目标方法的边($l\to m$)已经在CG中，就什么也不做
    • 更新调用关系：将调用边加入CG；将$m$标记可达；参数和返回值间PFG加边（注意方向）

上下文敏感的指针分析

  • 上下文敏感的概念（C.S.）
  • 上下文敏感堆的概念（C.S.heap）
  • 为什么C.S.和C.S.heap能提升精度
  • 上下文敏感指针分析的rules
  • 上下文敏感指针分析的算法
  • 常见的context sensitivity variants
  • 不同variants的区别和关系

上下文敏感

  • 上下文不敏感：不同的数据流通过参数和返回值被merge到了一起，造成不准
  • 上下文敏感：通过区分不同上下文的不同数据流来建模calling context
  • clone-based上下文敏感
    • 方法被不同的context复制成多份
    • 变量也被不同的context复制成多份
  • 上下文敏感的堆抽象：
    • 抽象对象也区分不同的上下文（成为堆上下文）
    • 堆上下文一般直接使用分配时所在方法的上下文

Rules

  • 定义域与符号
    • 所有元素都会被上下文修饰（field挂靠在对象上，对象已经被上下文修饰，所以field不需要额外的修饰）
    • Context: $c, c’, c’’\in C$
    • Context-sensitive methods: $c:m\in C\times M$
    • Context-sensitive variables: $c:x, c’:y\in C\times V$
    • Context-sensitive objects: $c:o_i, c’:o_j\in C\times O$
    • Fields: $f,g\in F$
    • Context-sensitive instance fields: $c:o_i.f, c’:o_j.g\in C\times O\times F$
    • Context-sensitive pointers: CSPointer=$(C\times V)\cup (C\times O\times F)$
    • Points-to relations: $pt: \text{CSPointer}\to \mathcal(C\times O)$
Kind Statement Rule
New i: x = new T() $$\frac{}{c:o_i\in pt(c:x)}$$
Assign x = y $$\frac{c’:o_i\in pt(c:y)}{c’:o_i\in pt(c:x)}$$
Store x.f = y $\frac{c’:o_i\in pt(c:x)\quad c’’:o_j\in pt(c:y)}{c’’:o_j\in pt(c’:o_i.f)}$
Load y = x.f $\frac{c’:o_i\in pt(c:x)\quad c’’:o_j\in pt(c’:o_i.f)}{c’’:o_j\in pt(c:y)}$

Call: l: r = x.k(a1, ..., an)
$$
\frac{c’:o_i\in pt(c:x),\
m=Dispatch(o_i,k),\quad c^t=Select(c,l, c’:o_i)\
c’’:o_u\in pt(c:a_j),\; 1\le j\le n\
c’’’:o_v\in pt(c^t:m_{ret})}
{c’:o_i\in pt(c^t:m_{this})\
c’’:o_u\in pt(c^t: m_{pj}),\; 1\le j\le n\
c’’’:o_v\in pt(c: r)}
$$

上下文敏感指针分析-算法

只在不敏感算法的基础上加上了上下文，以及ProcessCall的时候多了一步创建上下文的Select

  • 初始上下文为空（[]）
  • 注意Call Graph也是带有上下文的
Solve(m_entry):
	WL=[], RM={}, PFG={}, CFG={}, S={}
	AddReachable([]:m_entry)

while WL is not empty:
		remove <n, pts> from WL
		delta = pts - pt(n)
		Propogate(c:n, delta)
		if n represents a variable c:x:
            foreach c':o_i in delta:
                foreach x.f = y in S:
                	AddEdge(c:y, c':o_i.f)
                foreach y = x.f in S:
                	AddEdge(c':o_i.f, c:y)
               	ProcessCall(c:x, c'o_i)

AddEdge(s, t):
	if s->t not in PFG:
		add s->t to PFG
		if pt(s) not empty:
			add <t, pt(s)> to WL

Propogate(n, pts):
	if pts not empty:
		pt(n) += pts
		foreach n->s in PFG:
			add <s, pts> to WL

AddReachable(c:m):
	if c:m not in RM:
		add c:m to RM
		S += S_m
		foreach i: x = new T() in S_m:
			add <c:x, {c:o_i}> to WL
		foreach x = y in S_m:
			AddEdge(c:y, c:x)

ProcessCall(c:x, c':o_i)
	foreach l: r = x.k(a1, ..., an) in S:
		m = Dispatch(o_i, k)
		c^t = Select(c, l, c':o_i)
		add <c^t: m_this, {c':o_i}> to WL
		if c:l-> c^t:m not CG:
			add c:l-> c^t:m in CG
			AddReachable(c^t:m)
			foreach parameter c^t:p_j of m:
				AddEdge(c:a_j, c^t:p_j)
			AddEdge(c^t:m_ret, c:r)

Context Sensitivity Variants

C.I.可以看成一种特殊的上下文

  • k-limiting
    • 保证context有限，程序可以终止（递归警告）
    • 防止context过大原地爆炸
    • 设置context长度上限为k，只保留最后k个context
    • k一般取小数字（$\le 3$
    • 方法上下文和堆上下文的$k$可以不同
  • Call-site sensitivity
    • context: a list of call sites (call chain)
    • callee context: 把call site加到caller context的末尾
    • 又称k-CFA
  • Object sensitivity
    • context: a list of abstract objects
    • callee context: 把receiver object加到caller context的末尾
  • Type sensitivity
    • context: a list of types
    • callee context: 在caller context的末尾加上包含receiver object的allocation site的方法的类型（注意不是receiver object本身的类型）
  • 三者比较
    • 统一来说没有哪种最好
    • 在Java这样的OOP语言中，$k$相同时
      • 精度：Object> Type > Call-site
      • 效率：Type > Object > Call-site

静态分析for Security

  • 信息流安全性的概念
  • Confidentiality（保密性）and integrity （完整性）
  • Explicit flow（明流） and covert channels（隐藏信道）
  • 使用污点分析来检测不想要的信息流

Information Flow Security

  • Security：考虑对手存在的情况下达到某些目的
  • 信息流
    • 信息流$x\to y$: 变量$x$中的信息会传播到变量$y$
    • 把程序中的变量分成不同security level，最基本的模型是2-level policy (high/low security)
    • 安全等级可以建模成格
  • Information Flow policy
    • 限制了信息流如何在不同的security level之间流动
    • Noninterference policy: high-security变量中的信息不能流动到low-security变量中，否则就可能通过观测low变量反推出high变量
    • 保证了信息流在格中只能向上（高机密性方向）流动

保密性与完整性

  • 保密性
    • 阻止重要信息的泄露
    • 不能让高的写入低的
  • 完整性：
    • 阻止危险信息进来
    • 不能让低的写入高的
  • 二者是对偶关系
  • 完整性——广义定义
    • Correctness 正确性：对于信息流完整性而言，就是上面的侠义定义，关键数据不能被危险数据污染
    • Completeness: e.g. 数据库系统应该完整地存储所有数据
    • Consistency: e.g. 文件交换系统需要确保收发端的文件保持一致

Explicit flow & covert channels

  • Expilict flow: 通过直接拷贝（赋值）传递信息流
  • Covert channels 隐藏信道
    • 信道：mechanisms for signaling information through a computing system
    • 隐藏信道：主要目的并非传播信息的信道
    • e.g. implicit flows (通过控制流泄露机密信息), termination channels (观察循环是否会终止), Timing channels (观察程序执行时间), Exceptions (观察程序是否会抛出异常), 用电量，cache命中率，…….
    • 能泄露的信息有限+攻击难度大，所以一般不去专门预防

  • 把程序中的数据分为两类

    • Tainted data 污点数据：给关心的数据打上标签，就像同位素标记一样
    • 其他数据：不关心的数据
    • Sources 源：污点数据来的地方，一般是某些方法的返回值
    • 污点分析关注污点数据在程序内流动的方式，会不会留到某些关心的地方（sink），sink一般是一些敏感的方法
    • 保密性：Source: 秘密数据的来源； Sink：泄露部位
    • 完整性：Source: 不信任的数据来源；Sink：关键的计算步骤

  • 与指针分析：

    • 把tainted data看成一个抽象对象
    • Source: 看成Allocation site
    • 使用指针分析来传播数据

  • 定义域与符号

    • 比指针分析多了一个Tainted data: $t_i, t_j\in T\subset O$
    • $t_i$指来自$i$这个call site的污点数据
    • 输入：
      • Source: 一系列会返回污点数据的方法
      • Sink: 一系列sink methods，污点数据一旦流进这些方法就意味着违反了security policy
    • 输出：
      • Taintflows: 一系列<污点数据，sink method>二元组，表示污点数据可能会流动到这个sink method

  • Rules

    • 指针分析rules + 对Source和Sink的处理

    • Source rule: l: r = x.k(a1, ..., an)
      $$
      \frac{l\to m\in CG\m\in Sources}
      {t_l\in pt(r)}
      $$

    • Sink rule: l: r = x.k(a1, ..., an)
      $$
      \frac{l\to m\in CG\
      m\in Sinks\
      \exists i, 1\le i\le n, t_j\in pt(a_i)}
      {\langle t_j, m\rangle\in TaintFlows}
      $$

  • 一些特殊的API（如String的拷贝赋值）需要特殊处理

  • 注意：给指针添加污点数据的时候别忘了把正常的指向对象也加进去

基于Datalog的程序分析

  • Datalog language
  • 如何用Datalog实现指针分析
  • 如何用Datalog实现污点分析

Datalog

  • Datalog是一种命令式的逻辑编程语言，是Prolog的子集

  • Datalog = data + logic: 无副作用、无函数、无控制流；因此不是图灵完备的

  • Predicate (Data)

    • relation, a set of statements
    • a table of data

  • Atoms

    • Datalog的基本元素是relational atom，是一类具有如下形态的Predicate：P(X1, X2, ... Xn)，其中P为Predicate的名称，X1,... Xn是Argument(Term)
    • Term可以是变量或者常数
    • e.g. Age(person, age), Age("Xiaoming", 18)
    • P(X1, X2, ..., Xn)求值为true当且仅当表P包含元组(X1, X2,..., Xn)
    • Datalog也有arithmetic atom, e.g. age >=18

  • Datalog Rules

    • Rule用来表达逻辑的推里关系
    • Rule的形式为H <- B1, B2, ..., Bn.
      • H: Head, 结果，是一个Atom
      • B1, B2, ..., Bn：Body, 前件，每个Bi都是一个Atom，是subgoal
      • 含义：head is true if body is true
      • 逗号表示逻辑与，Body里每一个subgoal都为true时才能推出Head为true
      • e.g. Adult(person) <- Age(person, age), age >= 18.
    • Rule的解读：H(X1, X2) <- B1(X1, X3), B2(X2, X4), ..., Bn(Xm).
      • 枚举所有变量可能的取值的组合
      • 如果某种变量取值的组合能使subgoals全部为true，则在这个取值组合下Head也为true
      • Head Predicate包含了所有true atoms，也是一张表

  • EDB & IDB Prdicates

    • Datalog Program = Facts + Rules = EDB + IDB + Rules
    • EDB (extensional database): 提前准备好的谓词；不可变（虽然有些Datalog的实现中也许可变）；可以看成程序输入；相当于给定的Facts
    • IDB (internal database): 通过Rules推断出来的谓词，可以看成程序输出；
    • 对于一条Rule来说，Head必须是IDB，Body里的subgoals可以时EDB也可以是IDB
    • Head相同的不同规则可以表示逻辑或
    • 分号也可以用来表示逻辑或，e.g. Otaku(person) <- Suki(person, anime); Suki(person, manga); Suki(person, galgame)
    • 逻辑与的优先级更高（仿佛是什么业界共识）
    • Body里的Subgoal可以是否定形式，表示为!B(...)
    • e.g. MakeupExamStd(student) <- Student(student), !PassedStd(student)

  • 递归rules

    • IDB predicate可以我推我自己（直接或间接）

    • Reach(from, to) <- Edge(from, to).
      Reach(from, to) <- Reach(from, node), Edge(node, to).
    • 递归让datalog可以表示复杂的程序分析问题

  • Rule Safety

    • 当每一个变量都至少出现在一个非否定形式的relational atom中，一条规则才是安全的
    • 有无限表项的Predicate是unsafe的
    • Datalog只会允许safe rules

  • 递归和否定必须分开，不然会出现自相矛盾的rules，e.g. A(x) <- B(x), !A(x)

  • Datalog Program的执行

    • Datalog Engine从EDB开始推断所有能推断的facts，直到没有新facts为止
    • Datalog Rules的单调性和facts的有限性确保了程序一定能终止

Datalog实现指针分析

  • EDB：程序语句

    • New(x: V, o: O)
    • Assign(x: V, y: V)
    • Store(x: V, f: F, y: V)
    • Load(y: V, x: V, f: F)

  • IDB：指针的指向关系

    • VarPointsTo(v: V, o: O)
    • FieldPointsTo(oi: O, f: F, o: O)

  • Rules：直接翻译就完事了

    | Kind | Statement | Rule | DataLog Rule |
    | —— | —————- | ——————————————————— | ———————————————————— |
    | New | i: x = new T() | $$\frac{}{o_i\in pt(x)}$$ | VarPointsTo(x, oi) <- New(x, oi) |
    | Assign | x = y | $$\frac{o_i\in pt(y)}{o_i\in pt(x)}$$ | VarPointsTo(oi, x) <- Assign(x, y), VarPointsTo(oi, y) |
    | Store | x.f = y | $\frac{o_i\in pt(x)\quad o_j\in pt(y)}{o_j\in pt(o_i.f)}$ | FieldPointsTo(oi, f, oj) <- Store(x, f, y), VarPointsTo(x, oi), VarPointsTo(y, oj) |
    | Load | y = x.f | $\frac{o_i\in pt(x)\quad o_j\in pt(o_i.f)}{o_j\in pt(y)}$ | VarPointsTo(y, oj) <- Load(y, x, f), VarPointsTo(x, oi), FieldPointsTo(oi, f, oj) |

  • Method Call

    • Domains: Statements - S, Methods - M

      • 调用语句 VCall(l: S, x: V, k: M)
      • Dispatch(x: V, k: M, m: M)
      • ThisVar(m: M, this: V)
      • Argument(l: S, i: N, ai: V)
      • Parameter(m: M, i: N, pi: V)
      • MethodReturn(m: M, ret: V)
      • CallReturn(l: S, r: V)
      • Reachable(m: M)
      • CallGraph(l: S, m: M)

    • Rules: 分三条表述

      // 处理调用关系和this变量
      VarPointsTo(this, o),
      Reachable(m),
      CallGraph(l, m) <-
      	VCall(l, x, k),
      	Dispatch(x, k, m),
      	ThisVar(m, this),
      	VarPointsTo(x, o).

      // 处理参数
      VarPointsTo(pi, o) <-
      	CallGraph(l, m),
      	Argument(l, i, ai),
      	Parameter(m, i, pi),
      	VarPointsTo(ai, o).

      // 处理返回值
      VarPointsTo(r, o) <-
      	CallGraph(l, m),
      	MethodReturn(m, ret),
      	CallReturn(l, r),
      	VarPointsTo(ret, o).

      // 额外增加（修改）
      // 入口规则
      Reachable(m) <- EntryMethod(m).

      // 阻止分析不可达方法
      VarPointsTo(x, o) <- Reachable(m), New(x, o, m).
    • 利
      • 受益于现成的Datalog Engine
    • 弊
      • 表达能力有限
      • 不理解内部实现，无法控制performance

Datalog实现污点分析

在指针分析的基础上加一点东西就可以了

    • Source(m: M)
    • Sink(m: M)
    • Taint(l: S, t: T)：把taint data和call site联系起来
    • TaintFlow(t: T, m: M)

  • Rules

    VarPointsTo(r, t) <-
    	CallGraph(l, m),
    	CallReturn(l, r),
    	Source(m),
    	Taint(l, t).

    TaintFlow(t, m) <-
    	CallGraph(l, m),
    	Sink(m),
    	Argument(l, _, ai),
    	VarPointsTo(ai, t),
    	Taint(_, t).

Soundiness

  • 理解soundiness的动机和概念
  • 理解为什么Java的反射机制和native code难以分析

Soundiness-动机

  • 现实中很难实现Soundness，因为存在很多hard language features(静态分析难以处理的feature)
  • 实际分析时，一般指关心sound core，对hard language features采取不处理或简略处理的态度——可能会误导读者——所以提出了Soundiness

Soundiness-概念

  • Soundy analysis：mostly true + well-defined unsound treatments to hard/specific language features
  • Soundness, soundiness, unsound
    • sound: 捕捉所有的动态行为
    • soundy: 尽量捕捉所有动态行为，一些hard language feature在合理限度内unsound
    • unsound：出于某些目的忽略掉一些行为

Java 反射机制

  • 为什么难分析：哪个类、哪个方法完全是Run-time决定的
  • 当前解决方法
    • String Constant Analysis + PTA
    • Type Inference + String Analysis + PTA
    • 动态分析（不sound，结果取决于实际执行路径）

Java Native Code

  • Java Native Interface (JNI): JVM的一个模块，允许Java与Native C/C++ code进行交互
  • 为什么难分析：对于Java的分析器来说，你不知道native code里面发生了什么（自己写的）
  • 当前解决方法：替换成功能相同的java code

CFL-Reachability

  • 理解CFL-Reachability
  • 理解IFDS的基本思想
  • 理解IFDS能解决什么样的问题

CFL-Reachability

  • Realizable path: return和call相匹配的路径

    • 不一定会执行到，但unrealizable path一定不会执行到（所有路径 > 可执行路径 > 实际执行路径）
    • 识别出Realizable path，防止Unrealizable path污染结果 —— 括号匹配问题

  • CFL-Reachability

    • A到B可达，仅当A到B存在一条路径，该路径上所有边的label拼起来构成给定的CFG中一个合法的单词

    • 在call/return匹配这里，合法的单词就是正常匹配的左右括号
      $$
      \begin{align}
      realizable &\to matched\quad realizable\
      &\to (_i\quad realizable\
      &\to \varepsilon\
      matched &\to (_i\quad matched \quad)_i\
      &\to e\
      &\to \varepsilon\
      &\to matched\quad matched
      \end{align      }
      $$

  • 基于图可达性的一个程序分析框架

  • Interprocedural, finite, distributive, subset

  • MRP (Meet-over-all-realizable-path) solution

    • Path function可以看成路径上的flow function复合后的结果
    • MRP就是把所有可行路径的path function meet/join起来

  • Overview: 给定程序$P$和分析问题$Q$

    • 为程序$P$建立supergraph $G^$, 基于$Q$定义$G^$中边上的flow function
    • 通过把flow function转换成representation relations(graph), 建立exploded supergraph $G^#$
    • $Q$可以通过应用Tabulation algorithm解决图可达性问题来解决

  • Supergraph

    • 每个方法首位加上入口节点和出口节点，所有方法调用拆成调用点和返回点，根据调用关系连接起来
    • Flow function: possibly-unintialized variables, 在某个程序点上可能未被初始化的变量，用lambda函数的形式表示

  • Exploded Supergraph

    • 每个flow function都可以用2(D+1)个结点的图来表示，D是dataflow facts的有限集合

    • Representation relation of flow function $f$: $R_f\in (D\cup 0)\times (D\cup 0)$
      $$
      \begin{align}
      R_f=&{(0,0)}\cup {(0,y)\mid y\in f(\emptyset)}\cup{(x,y)\mid y\in f(x)\wedge y\notin f(\emptyset)}
      \end{align      }
      $$

    • 0->0边：为了让data facts能传递下去

  • Tabulation Algorithm

    • 求解从<$s_{main}, 0$> 到<$n,d$>是否存在可行路径，若存在则$d\in MRP_n$
    • $O(ED^3)$
    • 当处理出口结点时开始进行call-to-return matching

  • Distributivity: flow function必须要满足Distributivity，诸如$x\wedge y$这样的需要依赖多个变量的关系表达不出来，因此IFDS不能用来实现CP或者PTA（别名关系无法表达）


report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK