0%

program_analysis_NJU

学习南京大学的静态程序分析技术课程

课程主页:Static Program Analysis | Tai-e (pascal-lab.net)

共计32小时

Intro

PL的三个研究方向

  • 理论
  • 环境
  • 应用
    • 程序分析
      • 静态程序分析

image-20230831102930623

静态分析:在编译时对程序进行检测

静态程序分析的应用

  • 程序可靠性
  • 安全性
  • 编译优化
    • O(1)
  • 程序理解
    • IDE实现的call的提示:利用静态分析实现

image-20230831103339266

运行程序前了解程序的性质和行为(写一个程序来分析,分析器)

image-20230831104435688

  • 运行时可能指向同一地址吗
    • 需要加锁解决竞争问题

image-20230831104701170

对于一个正常的语言写的程序,我们感兴趣的运行时的性质是否满足 是不可判定的,即不存在完美的静态分析

perfect static analysis满足

  • sound:包含所有truth,过近似
  • complete:是truth的子集,欠近似

image-20230831105420735

不存在perfect,因此想要一种useful的静态分析,可以仅满足一种性质,妥协另一种性质

  • 满足soundness:存在误报,false positive
  • 满足complete:存在漏报,false negative

image-20230831105711467

绝大多数的程序分析都是sound,妥协complete

sound一般对应的是正确性,如下例,考虑到两条分支后才能得出正确的结论

image-20230831150753259

可能有两个结论,都是sound的

平常的思维是动态思维,静态分析无法获得运行时的数据

第一个结论需要维护path branch和一个条件,比较昂贵;第二个比较cheap,速度快

image-20230831151433500

确保(足够接近)soundness的情况下,在精度和分析速度上做平衡

抽象 过近似 是静态分析的核心思想

过近似包括transfer函数和控制流

抽象就是把具体值转变为符号

用bottom符号表示错误

image-20230831152709196

transfer functions定义了转换规则,根据分析的具体问题和语句的语义设计

image-20230831153019783

3说明静态分析会产生误报

image-20230831153355882

控制流:在每个merge的地方进行抽象,可能出现过近似,默认采用的方式

image-20230831153713197

image-20230831154741536

Intermediate Representation

南京大学《软件分析》课程02(Intermediate Representation)_哔哩哔哩_bilibili

直接分析源代码存在弊端

静态分析需要一种程序表示的形式,没有严格的定义,因此介绍主流的IR

不介绍对C/C++的LLVM

编译器和静态分析器

了解关系即可

编译的步骤:

  • 词法分析(符号和词的合法性),需要词法方法,正则表达式

    • 语法分析器parser,上下文无关文法
  • 语法分析,对AST进行分析,语义指简单的(类型检查)

  • 代码生成,静态分析器在IR基础上做

image-20230831163003482

正常的IR需要所有前端模块才能生成

AST vs. IR

3地址码3-address code

IR更接近于机器码,不依赖于编程语言(方舟编译器可以将不同语言生成为统一的IR)

AST缺乏对控制流的表达

image-20230831163353046

IR: 3AC

没有形式化的定义

image-20230831163931505

指令右端只有1个操作符,每个语句只包含3个地址

  • 变量名 a,b
  • 常量 3
  • 编译器自动生成的临时变量 t1

常见的形式

image-20230831164147119

Soot

java中最流行的静态分析器

https://github.com/Sable/soot/wiki/Tutorials

对应的IR是 Jimple,带有类型的3地址码

冒号是一种特殊的赋值

image-20230831165004862

image-20230831170458580

JVM中的4种调用

  • invokespecial: call constructor, call superclass methods, call private methods

  • invokevirtual: instance method call (virtual dispatch)

  • invokeinterface: cannot optimization, checking interface implementation 不能优化

  • invokestatic: call static methods

Java7 invokedynamic -> Jaava static typing, dynamic runs on JVM

meethod signature: class name, return type, method name, parameter types

image-20230831170815120

所有类的父类,java.lang.object

默认生成的构造函数init

clinit 类的初始化的函数,compiler加载引用的变量进行初始化 class load init

SSA

一种IR,有利于某些算法的设计,80年代提出的技术

和3AC的区别是每个变量的定义有新的命名,每个变量仅有一个等式

image-20230901090511569

如果有控制流,采用$\phi$函数

image-20230901090643097

为什么使用SSA

  • flow-sensitive 维护程序执行顺序,精度更高,SSA本身带有部分flow的信息

  • 数据的存储更清晰

为什么不用SSA

  • 引入变量太多
  • 译为机器码可能开销太大

image-20230901091235279

静态分析一般在CFG上分析,如何给定3AC建立CFG?

image-20230901091633485

Basic Blocks

basic blocks是最多的连续的3AC码的集合,满足以下指令:

  • 只能从第一个指令进入(没有其他控制流
  • 出口是最后一个指令

image-20230901091648122

  • 如果指令是goto的地址,只能作为入口
  • goto只能作为出口
    • goto的下一句一定是入口

image-20230901093246402

仅确定入口即可

BB是CFG的节点,补充边就有了CFG

image-20230901093928280

CFG

image-20230901094252846

条件jump有2两个出口

B2是B1的后继,前驱只能有一个,后继可以有多个

entry也可以有很多

image-20230901101340886

image-20230901101445829

IR和AST的区别

image-20230901101732041

企业可能认为content-insentive比较慢,学术界关注的是content-sensitive的技术

Data Flow Analysis Applications

编译后端优化的技术

3个应用

image-20230901142516251

Overview of Data Flow Analysis

研究数据怎样在CFG中流动

静态程序分析是过拟合的,输出可能是假阳

image-20230901143647456

过拟合和欠拟合都是安全的分析,应该将over改成safe

image-20230901143914835

image-20230901144138225

主要介绍不同的数据流分析的应用

Preliminaries of Data Flow Analysis

形式化方法

程序执行前后会产生状态变化,与程序点关联

顺序执行的语句前一条语句的输出和后一条的输入相关,具体还有分支的形式

image-20230901144554623

操作符是meet operator,可以是union或者其他运算符

数据流分析需要对每个程序点的所有可能状态的抽象(data flow value,绿色的)

domain是value的值域

image-20230901145243994

数据流分析是为了找到对输入输出状态的约束的解,有两类

  • 基于状态的语义(转移函数)
    • 前向分析
    • 反向分析(可能会对逆向的CFG进行前向分析)
    • image-20230901150349427
  • 基于控制流的约束
    • Basic Blocks里面的
      • $IN[s_{i+1}]=OUT[s_i],\text{for all }i\in\{1,\dots,n-1\}$
    • BB之间的
      • 复合函数
      • image-20230901150752423
      • image-20230901150828752
      • 红色的是反向的

Reaching Definitions Analysis

不涉及函数调用,讨论的是方法内的CFG

变量是别名的形式(指针分析,别名分析,指向分析)

image-20230901152313029

reaching definition

  • 存在一条路径能到达
  • 不能被二次赋值

image-20230901152523679

编译优化会用到,也可以用来分析undefined variable

是一种may-Analysis,过拟合

100个定义用100个definition来定义

image-20230901154814673

image-20230901155156563

给出了转移函数的定义

因为无法确定BB之间的前驱关系,所有定义了当前BB内的定义的语句都需要被kill掉

image-20230901155520326

对于control flow进行分析,定义

image-20230901155548910

入口的output为空,entry没有定义 (may analyse一般为空,must analyse一般考虑为undefined)

除了entry的BB的output都为空(程序都没运行)

当任何OUT改变的话

会停机吗?

image-20230901161421363

B3的Input=10110000

B3的Output=00000010 union (10110000 - 10001000) = 00000010 union 00110000 = 00110010

上一轮的BB的out都是空,全变了,再循环一轮

B2的out= 10111100

B3的out= 00110110

image-20230901171055532

根据转移函数的定义,当输入不变时输出不变

如何证明算法的收敛

$OUT[S]=gen_s\cup (IN[S] -kill_s)$

  • $gen_s \text{和}kill_s$不变
  • more facts加入后,只会让多+1而不会多kill,单调递增的感觉
  • facts是有限的

image-20230901171929909

为什么每个out不再变化就说明停机了?

Out不变,In不变,Out不变

image-20230901172108100

算法到达了不动点,和单调性相关

Live Variables Analysis

数据流分析的应用,归结为在格上求解不动点的问题

一般分析算法求出的是最大不动点和最小不动点

定义:某处变量的值是否能够在后面可以使用(用之前是live,不能被重定义)

live变量的信息可以用于寄存器分配,当寄存器满了的时候

image-20230904094328736

定义中指出是some path,因此是一种may analysis,定义的直观含义是某点的变量是否会被后续用到

变量和定义的区别在哪里?

都用bit vector表示

image-20230904100041064

采用backward的方法进行分析

In[B]= use_B union (Out[B] - redine[B])

通过具体情况枚举分析

use在define之前

image-20230904155628294

更正:此处的$OUT[B]=\cup_S IN[s]$

给定的out求in,边界条件为in=空

一般情况下may analyse的初始化是空,must analyse是all,和reaching definition定义很像

image-20230904160245948

0001000

B4有两个后继,out[b4]=in[b2] union in[b5] = 0001000 union 0000000 = 0001000

in[b4]= 0100000 union (0001000 - 1000000) = 0101000

B2的Input是 100 1001,因为m是在define后用的

B1的输入0011101

第二轮

0101001

image-20230904160646443

计算INPUT的顺序不同会影响迭代的次数

image-20230904162203684

Available Expressions Analysis

一种must analysis,为了实现对程序的优化而不是解决安全问题

从程序入口到p的所有路径必须经过表达式 $x\ op\ y$,并且表达式最后的求值之后,$x$和$y$不能被重定义

image-20230904162801564

类似于表达式简化的思想,p点之后对该表达式可以进行替代

首先给出抽象

image-20230904162854755

是一种前向分析

out = gen union (input - kill)

image-20230904165840491

两个分支后是available的

因为所有pass都必须available,输入是前驱输出的交集

image-20230904165925795

优化而不是找bug,不能误报

初始化为全1(因为要交)

image-20230904172544309

out[B1]=10000

out[B2]=01010 union (10000 - 10000)=01010

image-20230904172906013

B4 input=11111, Output= 00110 union (01010-00010) =01110

先算kill再算gen,根据定义

01010 union (00010 - 00111)=01010

image-20230904185613558

三类定义的对比

image-20230904190155676

image-20230904191638058

Data Flow Analysis Foundation

image-20230904192251591

image-20230904192304012

上节课3个应用的算法均是迭代式算法,回答存在的问题

从23的基础上定义格

复习核心内容是8

Iterative Algorithm, Another View

给定CFG,有k个statement,迭代算法每次更新节点的OUT[n]

image-20230904194220880

进行形式化

image-20230904194710101

实际上是不动点

image-20230904194725702

  • 迭代式算法一定能终止并给出一个解吗?
  • 假设能达到不动点,只有一个不动点吗?如果有若干个不动点,迭代式算法得到的不动点足够精确吗?
  • 迭代式算法到达不动点或得到解需要多长时间?(复杂度)

image-20230904195054862

Partial Order

参考 偏序与等价关系 - 知乎 (zhihu.com)

偏序集的定义$P,\subseteq$,带有偏序关系的集合,并满足以下关系

  • 自反性
  • 反对称性
  • 传递性

image-20230905100158884

整数集上的小于关系不是偏序关系

子串是偏序关系

image-20230905100307750

偏序集的含义是不是所有的元素互相之间必须满足偏序关系,如pin和sin没有偏序关系,但是{pin,sin,sing,gin}和singing构成偏序集

幂集

image-20230905100734386

Upper and Lower Bounds

image-20230905101107238

最小上界lub和最大下界glb

bound可以不在S当中,在P中即可

image-20230905101527501

image-20230905101943246

偏序集的glb和lub是唯一的

证明:反证法,反对称性

image-20230905102005722

Lattice, Semilattice, Complete and Product Lattice

在程序分析中学格(

每两个元素存在glb和lub的偏序集称为格

image-20230905102436174

半格:任意两个元素只存在glb或者lub

  • 只存在glb,称为meet半格
  • 只存在lub,称为join半格

image-20230905102707115

全格

格的任意一个子集,均存在glb和lub

image-20230905110741805

整数集的子集为什么不是全格,但是格?

image-20230905111254543

回顾格的定义,任意两个元素存在glb和lub即可;全格要求所有子集都有glb和lub

image-20230905110540907

有限的格一定是全格,complete的lattice一定是有限的吗,不是

image-20230905111616613

一般程序内的是有限的

积格的定义

image-20230905112107491

  • 积格的lub:实际上是每个格内两个元素的lub
  • 积格的glb:每个格内的两个元素的glb

性质

  • 根据定义,积格也是格
  • 积格是全格的积时,积格也是全格

Data Flow Analysis Framework via Lattice

介绍格是为了用格形式化数据流分析

image-20230905113959239

有点类似沿着控制流上升到上界

image-20230905114738987

试图回答第1个问题

image-20230905114859061

需要单调性和不动点定理

Monoticity and Fixed point Theorem

前面提到complete的格不一定是有限的,所以这里额外第二个条件是finite

从bottom出发,迭代f函数能够找到的第一个不动点叫做最小不动点;从top出发,求到的是最大不动点

image-20230905151443765

证明不动点的存在:

根据$\perp$的定义,有$\perp \subseteq f(\perp)$

根据单调性的定义,$f(\perp)\subseteq f(f(\perp))$

递归地有 $\perp \subseteq f(\perp) \subseteq \dots f^i(\perp)$

根据$L$的有限性,存在一个$k$,$f^k(\perp)=f^{k+1}(\perp)=f^{fix}$

即存在不动点,回答了问题1

(可以假设不存在不动点,则根据单调性和有限性推出矛盾)

image-20230905154855422

再证明得到的不动点是最小不动点

设存在另一个不动点为$x=f(x)$

根据$\perp$的定义,有$\perp \subseteq x$

根据单调性有 $f(\perp) \subseteq f(x)$ (数学归纳法的奠基)

采用数学归纳法,假设$f^i(\perp)\subseteq f^i(x)$

根据单调性,有$f^{i+1}(\perp)\subseteq f^{i+1}(x)=f(x)$

则有$f^{fix}=f^k(\perp)\subseteq f^k(x)=x$

即证明了求出的不动点是最小不动点,回答了问题2

间接证明了求出的不动点的唯一性

image-20230905155031011

依然存在的问题,仅回答了lattice上函数的性质,没有和迭代式算法建立联系

image-20230905160510624

Relate Iterative Algorithm to Fixed Point Theorem

image-20230905164944314

关键是F的单调性

image-20230905165647774

先证明两个运算的单调性

思路是利用最小上界的定义 偏序关系的传递性

证明下确界运算的思路类似

image-20230905172002679

最后解答复杂性的问题

先介绍格的高度的定义

image-20230905172123723

image-20230905172819265

复杂度取决于CFG节点个数和格的高度

May/Must Analysis, A Lattive View

image-20230905173425800

先抽象成一个积格进行理解,先看may alalysis

以reaching definition为例,作为一种may analysis 最下面No definitions can reach是所有变量都被初始化了,最上面是所有变量都可能被redefine,safe是指从找bug的角度,给所有变量报错是safe but useless,因此需要从下往上找到safe和unsafe的边界 truth

如何判断是否超过了truth(根据不动点

设计transfer function和cf merge的原则是safe approximation

根据单调性,求得的是最小不动点

image-20230905174535083

must analyse解决的是优化问题,从top出发,所有表达式都能优化显然是错误的,bottom是安全的但是没用的,没有表达式可以优化

must analyse的分析不能有误报,要求是complete

另一个维度理解may的最小不动点:transfer function是固定的,join是求最小上界,每次迭代走的是minimal step,因此得到的是最小不动点

Distributivity and MOP

考虑解的精确性,MOP是衡量的一个指标

总的transfer function就是各个f的组合

MOP是枚举所有的path的结果再join或meet(计算了每条路径最终的值

静态分析中有的路径可能是不可达的,导致结果不是完全精确的

实际上是不可枚举的

image-20230906103700614

和迭代式算法的区别

image-20230906103918799

x和y之间的关系

最小上界小于上界

所以MOP更准确

image-20230906104601252

当F满足分配律,两者一样准确

之前提到的bit-vector或Gen/Kill问题都是distributive

image-20230906104858404

Constant Propagation

这个DFA不是distributive的

image-20230906105336040

NAC: not a constant

一般不考虑未初始化的问题

对于两个常量分类讨论

image-20230906105930450

关注赋值语句,kill掉与被赋值相关的常量

image-20230906111532756

例子

image-20230906111959118

Worklist Algorithm

区别于迭代算法,实际的工具不采用迭代算法,worklist可以看做优化

回顾迭代式算法

仅遍历计算in变了的部分

image-20230906112920299

image-20230906113352119

Interprocedural Analysis

过程间分析

Motivation

image-20230906113916346

过程内分析对方法调用进行最保守的假设,可以做任何事情

问题:过于保守,降低了精度

过程间分析需要call graph,调用的目的地址

image-20230906114450105

Call graph

call edge连接call site和callee

image-20230906114617419

image-20230906114641085

主要针对面向对象的语言,给出了4个算法

image-20230906114815381

virtualcall实现多态,难以处理

image-20230906115124716

具体调用的方法在运行时确定,取决于

  • 对象的类型
  • 方法签名(可以唯一确定一个方法

image-20230906115354456

优先当前类有方法体的方法,不能是抽象的,如果没有则去父类找

image-20230906115605922

CHA需要类的继承的信息,根据A的类型来决定对应的call

OO语言的顶会

image-20230906200743561

算法采用分类讨论

image-20230906201056655

static call最简单

image-20230906201244904

B类可能没有foo,因此需要一个Dispatch而不是直接用B.foo()\

私有和构造函数都能用dispatch解决

image-20230906201506211

对于virtual call,包含了所有的子类的方法,因为

image-20230906201707497

例子都属于virtual call

{C.foo()}

{A.foo(), C.foo(), D.foo()}

{A.foo(), C.foo(), D.foo()}

如果B b =new B(), Resolve(b.foo())={A.foo(), C.foo(), D.foo()} 结果不变

这里是一个special call吗?不是因为Java支持动态方法分配,且涉及到了继承关系

因为算法只考虑变量的声明类型

image-20230906211704923

一般用在IDE中

image-20230906211826590

navigate菜单中

image-20230906211956325

reachable是处理过的方法

通过resolve发现新的方法

image-20230907095105736

image-20230907100051983

Interprocedural CFG

ICFG表示的是整个程序的结构

紧跟着call site的就是return site,利用call graph来解决ICFG

image-20230907100501603

image-20230907100605564

为什么还保留一条额外的边

image-20230907100725411

Interprocedural Data Flow Analysis

image-20230907101105920

遇到call node需要kill掉left hand side variable的值

image-20230907103248743

edge transfer就是给形参赋值

保留call to return edge是为了保证本地数据流关系的保留,即函数内部的

image-20230907104117327

如果没有这条边,相当于函数addOne内还需要维护a的值,如下图,效率很低

image-20230907104201277

kill的具体原因,需要用返回值覆盖

image-20230907105040021

image-20230907105101994

如果是过程内分析,会进行最保守的假设,所有调用返回值都是NAC,imprecise

过程间分析更加精确

image-20230907105527714

image-20230907105536788

image-20230907105714714

Pointer Analysis Introduction

Motivation

利用CHA来求目标方法会有多个,不精确

CHA利用对象的类和子类来分析

如果对x进行常量传播,x是NAC

指针分析更精确

image-20230914182323812

Introduction to Pointer Analysis

指针分析回答指针可以指向哪些地址

作为一种may analysis,过近似,给出可能指向的所有地址

image-20230911092021640

OO语言内的指针包括filed和variable

指针分析的输入是一段程序,输出是如右表所示的表格

image-20230911093038934

Alias Analysis别名分析

  • 指针分析:指针可以指向哪些对象

  • 别名分析:两个指针能否指向同一地址

显然,可以利用指针分析实现别名分析

image-20230911093309820

指针分析的应用:

  • 计算调用图
  • 编译优化
  • 漏洞检测 空指针

image-20230911093514885

Key Factors

非常复杂,在精度和效率之间取舍

image-20230911093643312

Heap Abstraction

堆抽象:如何对堆内存建模

因为在动态执行中,堆的对象可能是无穷的,静态分析需要在一定时间内得出结果,堆抽象需要将具体的对象抽象成有限数量的抽象的对象

image-20230911093955437

了解有两大流派,学习allocation sites技术

image-20230911094118770

根据对象的创建点来建模,$O_2$表示创建点

因为程序中创建对象的语句是有限的,显然抽象的对象数量是有限的

Context Sensitivity

上下文:考虑如何对调用点建模

方法可能被调用很多次,对应不同的上下文时,方法内的调用可能不同

  • 上下文敏感可以模拟 区分不同的上下文,上下文不同时,对同一个方法分析多次

  • 上下文不敏感每个方法仅分析一次

image-20230911100457311

上下文敏感可以显著提高精度

学习计划是先学习不敏感,再学习敏感

Flow Sensitivity

指如何对控制流进行建模

  • 控制流敏感:尊重语句的执行顺序
  • 控制流不敏感:忽视控制流的顺序

java的数据类型可以分为值类型和引用类型;

  • 基本类型也称为值类型,分别是字符类型 char,布尔类型 boolean以及数值类型 byte、short、int、long、float、double。
  • 引用类型则包括类、接口、数组、枚举等。

Java 将内存空间分为堆和栈。基本类型直接在栈中存储数值,而引用类型是将引用放在栈中,实际存储的值是放在堆中,通过栈中的引用指向堆中存放的数据。

image-20230911101619604

右边是flow不敏感分析的结果,目前主流是flow insensitive(对精度影响不大)

Analysis Scope

回答应该分析程序中的哪些部分

  • 所有程序
  • 需求驱动的分析:计算量更小;效率差异可能不够明显,仅满足特定需求
    • 如果有多个client的需求,可能会有重叠,不如进行全程序分析效率高

image-20230911104031780

image-20230911104343223

Concerned Statements

只关心影响与指针有关的语句

image-20230911105633949

  • 本地变量:x 数量最多
  • 静态field:C.f 和变量类似,不是重点
  • Instance field:x.f 对象的field
  • 数组元素 Array[i],一般会忽略index,静态分析无法得到,抽象成 只有一个field的对象,所有指都可以能取到,因此和instance field类似了

结论:学会1 3即可(不是

image-20230911110032514

主要是5条语句

image-20230911110354258

image-20230911110406168

image-20230911110735865

Pointer Analysis Foundations 1

image-20230911110905857

Rules

首先分析没有方法调用的程序(前4条语句),再学习如何处理方法调用

image-20230911111820078

规则是推导式的,$pt(p)$指的是p指向的对象

image-20230911113127194

new是将$o_i$加入到$pt(x)$中去

赋值将$y$指向的加入到$x$指向的

image-20230911113140353

image-20230911113613953

image-20230911113800642

image-20230911113809394

image-20230911160527617

How to implement pointer analysis

本质上是将指针信息传播给其他指针,也可以理解为求解包含约束

指针分析的关键是当指针集$pt(x)$变化时,将变化传播给其他相关的指针

利用图来传播

image-20230911161609721

指针流图pointer flow graph

有向图,表示对象如何在图中流动

image-20230911161731273

边的含义是x的变化可能流向y

如何建立PFG的边?根据程序的语句的4条规则

image-20230911162000627

c.f仅是一个指针表达式,不是一个指针,指针必须是对象

image-20230911163008942

实现包括两步

  • 构建指针流图
  • 在PFG上传播指向信息

Algorithm

分别对应4个语句

S是要分析的语句的集合

image-20230911164230546

WL包含了指针和指针集,是后续要分析的对象

简化只有2种语句

集合的减法是为了去重,去掉ptn已经有的指针

image-20230911170359600

image-20230911170411007

image-20230911170430735

已经是union了为什么要去重?不影响正确性,但是可以跳过

image-20230911171405824

另外两条对称的语句

image-20230911172033462

可能有其他同类的不同对象已经连接了实例方法,因此是may引入新的PFG边

执行这个例子

image-20230912162251382

image-20230912162437486

Pointer Analysis Foundations 2

如何处理方法调用

过程间分析,需要call graph

与CHA方法对比,根据指针分析来确定call graph

image-20230912164701071

实际上指针分析和call graph是一起构建的,on the fly

复杂起来了(

  • disptach:根据接受者对象和方法签名去找目标方法m,在做call graph

  • 传receiver对象:$m_{this}$,OO语言很多操作通过this实现

  • 传参:实参传给形参,变量之间连起来
  • 传回返回值

image-20230912165752464

solidity的dispatch只需要函数签名

问题:为什么this不加一个边?

连上会传递错误的信息,this只指向当前对象

image-20230912170440967

实际的操作

image-20230912170522098

从入口方法main函数进行分析,只分析reachable的方法,reachable对效率和精度有帮助

image-20230912172112179

黄色部分是新增的步骤,和call graph相关

image-20230912172223253

reachable方法

  • 入口方法
  • 出现新的调用边

image-20230912173001173

为什么只处理new和assign,因为这两个语句不需要语境

image-20230912184947416

为什么call graph存在$l\to m$就不再执行?实际上是对象的类型来决定目标方法的,虽然oi是新的对象,但是其他同类型的对象oj可能已经连过这一条边

这些判断条件存在的原因:为了实用性,减少不必要的操作

上下文非敏感,每个算法处理一次

算法的输出是每个变量的指针集以及调用图

image-20230912185840030

例子,动笔自己写一写

image-20230912190641848

和CHA的区别:更精确了

image-20230912192345447

image-20230912192951269

image-20230912193211655

Pointer Analysis Context Sentivity

Java指针分析中对精度提升最明显的技术

动态执行时该程序时$i=1$

采用常量传播分析是NAC

image-20230912194827600

需要上下文敏感的指针分析,每次调用id时对实参进行区分

image-20230912195049875

Introduction

上下文不敏感为什么会不准确

  • 动态执行时,一个方法可能在不同的语境下被多次调用
  • 不同调用语境中方法的变量可能指向不同对象
  • 不同语境下的对象 混合传播 到了程序的其他部分

提高上下文敏感分析的效率

image-20230912201100384

最古老和最著名的技术是call-site当做上下文,对调用栈的抽象

image-20230912201119775

下节课介绍其他变种,后续介绍都是call-site

具体关注的是变量的上下文

image-20230912201045606

上下文敏感 堆

  • OO程序会频繁操作对象,heap-intensive
  • 为了提高精度需要对 对象加上下文
    • 粒度更细的抽象

image-20230912201334791

为什么能提高精度?

动态执行时,每次调用都会创建新的对象

同一个语句,不同对象的操作可能不同

image-20230912201515062

例子

动态执行指向n1,堆不敏感的程序分析指向n1 n2

image-20230912202332554

有上下文敏感heap时,右边x.f语句会产生两个不同,意思是方法内对 对象的field也进行区分

如果没有变量上下文敏感,只做堆上下文敏感,相当于没做

image-20230912205913463

都加上下文才能提高精度

Rules

先给出定义域和记号

程序的变量、对象都加上 上下文

image-20230912210139484

策略决定c的内容,可以理解为一系列call-site

注意field没有,具体的实例的field有,因为通过对象来访问

指针也分两类,分别是变量和对象的;因此表示方式是两类的并

具体实现指针分析器需要利用这些规则

image-20230912213823131

具体的理解

对于new语句,语境当中的规则:假设在方法m中,上下文是c,则给对象也加上下文

image-20230912214053341

对于assign语句,比较直观

image-20230912214230647

先分别取出x和y指向的对象,为什么不是同一个上下文c?

因为x和y的上下文相同,但是x和y指向的对象的语境不一定相同,上下文c和c‘可以相同

image-20230912214620756

load和store对称

对于调用的规则,如何决定c

假设调用在某个方法里,当前的语境是c

image-20230912215123422

  • 先取出对象指向的上下文
  • 选择对应方法,与上下文无关,取决于类型
  • 选择上下文:为目标方法$m$选择上下文,根据当前调用点$l$能得到的信息
    • 具体怎么选,请看下集
  • 传receiver object
  • 传返回值

image-20230912215631131

好像是直接用了L?考虑如果在例子外面套个循环,就需要一个方法select进行选择了;除了还有其他的表示方法

$c^t$ 是新的一个上下文

image-20230912220108442

目前Java流敏感分析的效果不够好

Algorithms

算法有两部分,构造PFG,在PFG上传播指针信息

image-20230913152920936

image-20230913153854777

区别在于每个节点表示的都是上下文敏感的变量或者field,节点额外带有上下文,笛卡尔积多了一个维度

image-20230913153130047

连边就根据4条规则

对于call比较复杂,方法dispatch,传参数,this不连边,传返回值

image-20230913154003008

打码之后和上下文不敏感的算法几乎一样

image-20230913154510890

首先看solve算法

image-20230913154601481

下面的集合也带有上下文信息

比如RM foo在ct下可达

CG也是上下文敏感的call-site和callee都有上下文,$c\to c^t$

入口函数的上下文为空

同一个call-site,目标函数内的context是一样的

image-20230913162044882

Addedge和Propagate和CI分析一致

Variants

其他技术

给出select函数的定义

最常用的三种上下文敏感的变量

  • call-site敏感
  • object敏感
  • type敏感

image-20230913162648159

如果是上下文不敏感,可以看做是上下文敏感的特殊情况,select返回为空

image-20230913164121180

每个context包括一系列的call-sites,将call site加入到caller,类似于调用栈,也叫call string,K-CFA(k-Context-Free Analysis)

call site sentivity

image-20230913164034410

怎么得到当前的代码行数呢

递归调用的时候(方法调用自己),会出现无穷多次call-site

image-20230913164548268

因此需要一个深度$k$,限制上下文的长度为$k$,一般$k\leq3$,会合并连续相同的callsite然后取队列末尾的$k$个

image-20230913165010456

上下文层数越多,精度越高,一般是至少2层

image-20230913170125124

分析x.get具体指向的方法

动态的理解:会返回1

静态分析:得到One.get()

image-20230913172604357

利用调用点区分了14和15两个调用,如果是CI分析

image-20230913172709985

object sensitivity

image-20230913193654682

另一种表现形式的select,根据receiver object和heap context来区分

image-20230913195207715

this指的是上下文本身(对象)

和1call site进行对比

image-20230913195721511

换成2 call site能区分

object是否一定比call site好呢

this一样,调用的方法也一样

image-20230913201016340

  • 一般情况下精度是不可比较的
  • 但是对Java这种OO语言,object更准确

image-20230913201700466

type sensitivity

实际上是对object的抽象

image-20230913202205377

InType得到的不是生成的对象的类型,而是语句所在类

精度不如对象敏感技术,牺牲了精度换取速度

image-20230913202510805

image-20230913201401242

image-20230913202953061

Security

抽象什么是安全:在敌手存在时达成某个目标

image-20230913205207631

image-20230913205405562

美国的NVD发现最多的漏洞是injection

injection和leak实际上是一类问题,信息流

Information Flow Security

目标:阻止不必要的信息流

image-20230913205701513

  • Access Control:标准方法,检查是否具有权限来访问特定信息;考虑信息是如何被处理的
    • 得到信息后如何使用?
  • 信息流安全 end2end
    • 跟踪程序如何安全地处理信息
    • 考虑信息如何传播

image-20230913205921749

信息论的定义

image-20230913210049720

给变量分级

不同等级变量之间信息如何流动

image-20230913210226746

最简单分法是2级分法(使用最广泛

image-20230913210241719

可以利用偏序关系(格)来建模

image-20230913210345697

可以有比较复杂的level设置

policy:限制信息如何在不同密级之间流动

image-20230913211342441

  • 高级变量不能影响低级变量
  • 通过观测低级信息无法推测出高级信息

image-20230913211325855

Confidentiality and Integrity

image-20230913211612588

和密码学定义的Integrity不同,更像是真实性,外界信息的真实性

image-20230913211740289

给US air force提出的问题

image-20230913212019260

从完整性角度看,高级流向低级也不安全

扩展完整性的定义,之前的定义有点类似于正确性

image-20230913212158190

数据流和信息流的区别:

数据流可以看做具体的数据

信息流更加抽象,广义,可以将数据流看做是信息流

Explicit Flows and Covert Channels

image-20230913212559603

以上是显式流动

秘密可能作为条件语句的判断条件,称为隐式流

image-20230913212739282

while循环 是一个信息流,但不是数据流

image-20230913213034386

最后一个如果为负数,可能有error

统称上面这种类型为隐藏信道

image-20230913213249693

还有侧信道,观察缓存命中率

总结所有类型的CC非常有挑战性

一般情况下,Cover Channel泄露信息有限

image-20230913213650461

因此后续课程主要采用污点分析分析显式流

  • 感觉后者更有意义

Taint Analysis

使用最广泛的信息流分析工具

数据分类

  • 感兴趣的数据,label(同位素)
  • untainted

污点数据来源于特定方法的返回值

关心污点数据是否会流动到特定的sink,一般是一些比较敏感的方法

是否存在从source到sink的流

image-20230913213911354

应用

  • 保密性: $\text{ secret data} \to \text{method}$
  • 完整性:$\text{input} \to \text{critical command}$

image-20230913214159779

两个性质的对称性

污点分析回答的问题

  • 标记数据是否会流动到某个sink(sink的指针会指向标记的数据吗?)

两者是高度一致的,因此可以借助指针分析进行污点分析

  • 将标记的数据视为特殊的object
  • source是allocation site
  • 利用指针分析进行污点数据传播

image-20230913214528489

首先扩展指针分析的定义域,污点数据是指针分析的子集

image-20230913214946878

输入输出

image-20230913215045186

规则

call:如果dispatch方法来自source,认为可能是需要污点分析的

后续的传播和指针分析一样

image-20230913215415014

image-20230913215406095

检查sink?调用sink方法时,参数是否是tainted

image-20230913215502781

例子

java中都是浅拷贝

x和y是别名

方便debug

image-20230913220135749

image-20230913220115069

对于运算符重载,需要更复杂的机制设计

image-20230913220301552

Datalog-Based Program Analysis

Motivation

命令式语言:

声明式语言:sql

image-20230913221434446

实现一个复杂的指针分析,采用不同语言的区别

回顾指针分析的rules和算法

image-20230913221600990

还需要考虑的细节

image-20230913221610803

如果用声明式语言实现

image-20230913221806951

可读性更强了

Introduction

声明式逻辑编程语言,Prolog的子集

曾经是数据库的查询语言

  • 程序分析
  • 网络协议
  • 吹牛

image-20230913222022073

没有控制流?没有函数

表达能力不够

data/predicate

事实

数据的表

image-20230913222125660

元组属于data,真的,称为fact

谓词由Atom表示

image-20230913222349159

原子可以判定真假

下面这个类型也是原子

image-20230913222547175

Rules/Logic

制定了如何推导fact

image-20230913222737380

是逻辑与

image-20230913222823795

如何理解规则

image-20230913222951872

考虑所有组合,如果一个组合可以让所有子目标为真,head为真,包含所有为真的谓词

交换subgoal不交换结果

image-20230913223252088

image-20230913223410217

问题在于初始数据来源

  • EDB:程序运行前定义好的;不变;

  • IDB:根据Rules定义,程序的输出,head只能是IDB

image-20230913223615033

表示 或

写两条语句或者采用;

优先级低

image-20230913223949083

表示非采用!

image-20230913224015374

否 是搜索所有情况吗

支持递归,能力强大的来源

image-20230913224101296

如果没有递归,只能支持基本的关系代数

image-20230913224230753

需要保证规则是safe,所有的变量是有限的

  • 表是有限的,表取反就是无限的

image-20230913224527154

取反和递归必须分开

image-20230913224943480

程序如何执行?engine

image-20230913225056738

只能产生facts

Pointer Analysis

指针分析的EDB是语法分析可以直接获得到的信息

IDB是指针分析的结果

image-20230914081639719

通过定义域定义4类语句

IDB只有2类,变量指向和fields指向

image-20230914082014217

image-20230914082257853

程序的可读性非常强,代码实现很干净

image-20230914082932296

首先运行New,因为varpoints都是空

将整个New复制到Varpointsto

image-20230914083536305

终止条件:不再能产生新的facts

如何处理函数

引入新的谓词 EDB和IDB

k应该包含参数信息,不然无法处理多态

和之前类似,传4部分信息

image-20230914090327689

增加对入口方法的处理即有了全程序分析

image-20230914090712426

Taint Analysis

在指针分析的基础上,修改EDB和IDB

image-20230914091418518

image-20230914091438076

_是因为不关心当前的下标

优势和劣势

image-20230914095905639

  • 简洁、可读性强
  • engine优化,效率高

缺点

  • 表达性受限,不是图灵完备
    • 如果需要删除facts,无法实现
    • 对于all的逻辑不是很好表达
  • engine是黑盒,无法自行优化效率

image-20230914100142781

CFL-Reachability and IFDS

context free language是IFDS的理论基础

利用图可达进行程序分析表达

image-20230914101547722

放松心态,学懂50%就算成功!

Feasiable and Realizable Paths

存在一些路径是不可达的

希望程序分析尽可能不被这些不可达路径污染,然而静态分析中这个问题是不可判定的

image-20230914101250283

红色路径是静态分析无法避免的错误

绿色路径可以通过上下文敏感避免

image-20230914101854201

image-20230914101908102

realizable path:跨函数调用的返回应该和call匹配

unrealizable一定是不会执行的,如何识别

image-20230914102037213

括号匹配,太复杂就不适用,寻找系统的方法

image-20230914102223380

CFL-reachability

上下文无关文法生成的是上下文无关语言

没学过编译但学过计算理论

image-20230914102916339

编程语言文法一般是CFG

image-20230914103028029

部分 括号匹配

有右括号一定有左括号,反之不一定成立(call了不一定return)

通过call-site进行括号的索引

如何形式化括号匹配的问题?写CFL的语法

image-20230914104300136

从规则来看,没有单独产生右括号的规则

image-20230914104707483

IFDS

image-20230914104809038

可以通过图可达性来表达的图分析算法

不再是迭代式算法,用图的方式(没有传播的过程)

过程间的 有限 可分配的 子集问题

定义域有限 流函数是distributive

image-20230914105259135

具体可以认为是先meet再transfer和调换顺序结果一致

回顾MOP,利用IFDS能够给出MRP

image-20230914105804428

是所有edge上的f的复合函数

MOP是把所有path的结果并起来

MRP只考虑realizaable path(返回边和callsite对应,不能返回到之前已经返回过的边),不再沿着假的边去分析,可能更精准

image-20230914110511798

显然是MOP的子集

构造supergraph,定义flow func

构造explded supergraph

image-20230914111707351

$G^*$由一系列的$G_{main}$和$G_p$组成

image-20230914140129907

每个call site都有3条edge

image-20230914140322154

flow function的设计采用 可能未初始化的变量 的设计

具体的函数形式为lambda表达式

image-20230914141003251

lambda表达式类似于匿名函数,$\lambda e_{param}\cdot e_{body}$

无论输入,输出$x,g$

S是所有没有被初始化的值

$\lambda \ S.{S-x}$

减去g为了提高精度,真实情况不会有这条边,增加这一条边传播了本地变量的信息

image-20230914142144730

有了supergraph之后,建立exploded supergraph,拆分了flow function

D=2

image-20230914142834835

image-20230914144611310

和传统的程序分析的定义区分,之前通过n4的out来判断存在

image-20230914150855265

image-20230914151715271

利用tabulation算法判断可达性

image-20230914151704558

如果d可达就涂成蓝色

image-20230914151857768

这个算法比较复杂,不做详细介绍

image-20230914152005445

E是边的个数,D是domain size

处理exit节点时, 找到对应的call边

额外还有call到return的 summary edge,加速

image-20230914152618402

可分配性的理解

image-20230914153507313

具体问题能够利用IFDS解决需要用可分配性判断

IFDS的flow函数只能处理一个元素

image-20230914153649860

如果需要多个输入事实来判断能否产生正确的输出,不能用IFDS

最后的两个例子可以用IFDS

x,y,x.f指向o,正确吗

image-20230914154323952

缺少别名信息,这个信息同时需要x和y,因此指针分析不能用标准的IFDS

image-20230914154812428

image-20230914154937595

Soundness and Soundiness

程序分析约有50年,soundiness是2015年提出的

前沿的话题

soundness

保守的近似,近似所有可能的程序行为

  • 学术界:分析真实程序语言编写的完整的程序,没有sound
  • 工业界:所有工具都不得不牺牲soundness

image-20230914155709950

每个编程语言存在的难以分析的feature

比如js的eval,c对指针加减

image-20230914155955552

因此现在论文的结果可能声称是sound,对hard one是unsound;

或者忽略

不分析会导致严重的结果吗?Java

image-20230914161155068

soundiness指真实的程序没法分析一些困难的语言的特征

大佬振臂高呼,提soundiness

image-20230914161603588

image-20230914161732880

三类概念的区别

为什么下面的两类很困难

Hard Language Feature: Java Reflection

对java和安卓分析的噩梦,notorious

image-20230914162225436

为什么难分析

在Java编程语言中,反射(Reflection)是指在运行时动态地获取、检查和操作类、对象、方法和属性的能力。它允许程序在运行时通过名称来获取类的信息,调用方法,访问字段,创建对象等,而不需要在编译时明确地引用类或方法。

Java反射提供了一组类和接口,如ClassMethodField等,用于在运行时检查和操作类的结构。通过使用反射,可以实现以下功能:

  1. 获取类的信息:通过反射,可以获取类的名称、父类、实现的接口、构造函数、方法和字段等信息。
  2. 动态创建对象:通过反射,可以在运行时通过类名创建对象的实例,而无需提前知道类的具体类型。
  3. 调用方法:通过反射,可以在运行时调用对象的方法,包括公共方法、私有方法和静态方法。
  4. 访问和修改字段:通过反射,可以在运行时访问和修改对象的字段(即成员变量),包括公共字段和私有字段。
  5. 操作数组:通过反射,可以动态创建、访问和修改数组对象。

image-20230914163513966

反射是运行时行为

为什么需要分析呢(应用在哪里,松耦合,编程更灵活)

image-20230914164026620

右边这个例子可能是错误的

image-20230914164317486

分析反射的技术:字符串分析+指针分析

直观的想法

存在的问题:这些变量可能是从文件中读入的;编码过的

image-20230914164531901

李老师和谭老师的工作绕不过去

类型推理+字符串分析+指针分析

在调用的时候利用参数来推理

image-20230914165357239

image-20230914165556297

目前最新的工作也是他俩做的

第三类方法,利用动态分析的结果,依赖于test case,给出的都是真的

image-20230914165745956

Hard Language Feature: Native Code

image-20230914165932042

native声明指方法由外部语言实现的,如跨语言调用C/C++

JNI

image-20230914170548019

image-20230914171130534

现在的解决方案:

  • 手动建模native code
    • 用java简单模拟一下功能
    • 大概比java实现快一个数量级
  • binary分析

image-20230914171721458

Soundiness Home Page

image-20230914172026836

image-20230914172057149