静态分析：datalog

2024-05-16

Motivation

  • 命令式语言：每一步都写命令，告诉计算机怎么做，如 C++
  • 声明式语言：告诉计算机要做什么，更加精炼，简单，如 SQL 语言
  • 如果要以命令式语言来书写指针分析，需要考虑非常多细节，容易出错
  • 但是以声明式语言来书写指针分析就很简洁，易读

Introduction to Datalog

基本信息

  • Datalog 是一种声明性逻辑编程语言，是 Prolog 的一个子集。开始是一门数据库语言
  • Datalog = Data + Logic（and or not）
    • 没有副作用（给变量赋值，修改变量的值）
    • 没有控制流
    • 没有函数
    • 不是图灵完备的

在 Datalog 中，谓词（predicate）是一组语句，本质上是一张数据表

一个事实断言：一个特定的元组(一行)属于一个关系(一个表)，则它表示一个谓词对于一个特定的值组合为真简单说：谓词可以判断语句的真假，依据就是这个语句在不在谓词所表示的表中

image-20240120133759310

基本单位

  • 关系原子：P（X1，X2，…，Xn） P 是谓词的名字，Xi 是谓词的项，可以是变量或者常量，例如 Age(“Alan”，16) is true
  • 算术原子：以关系表达式表达 如 age >= 18

逻辑运算规则

逻辑与：H <- B1，B2，…，Bn. H 是一个原子，Bi 也是一个原子
  • 表示所有 Bi 为真，H 为真
  • 考虑子目标中变量值的所有可能组合
  • 如果一个组合使所有子目标为真，那么头部原子(具有相应的值)也为真
  • 头谓词由所有真原子组成
  • image-20240120134559989
  • image-20240120134611181
逻辑或：（优先级比逻辑与低，要先运算或就要添加括号）

要么直接书写多条规则

  • SportFan(person) <- Hobby(person, “jogging”).
  • SportFan(person) <- Hobby(person,“swimming”).
  • 表示满足 jogging 或者 swimming

要么使用;来连接谓词

SportFan(person) <-Hobby(person,“jogging”) ; Hobby(person,“swimming”).

逻辑非：H(X1,X2) <- B1(X1,X3), !B2(X2,X4), … ,Bn(Xm).
递归：datalog 真正强大的原因
  • Datalog 支持递归规则，这允许 IDB 谓词从自身(直接/间接)推导出自身
  • Reach(from, to) <- Edge(from, to).
  • Reach(from, to) <-Reach(from, node) , Edge(node, to).
  • 其中 Edge(a,b)表示图中有一条从节点 a 到节点 b 的边，Reach(a,b)表示从 a 可以到达 b。

EDB 和 IDB 谓词

EDB（extensional database）

  • 可以看出 datalog 程序的输入
  • 先验定义的谓词（提前给好）
  • 是不可变的

IDB（intensional database）

  • 由规则建立的谓词
  • 可以视为输出

image-20240120134834748

规则安全性

原则：

  • 如果每个变量至少出现在一个非否定的关系原子中，则该规则是安全的。
  • 在 Datalog 中，一个原子的递归和否定必须分开。否则，规则可能包含矛盾，推理不能收敛。

例子：

  • A(x) <- B(y) , x > y. x 可以有无限多个值来满足这个规则，不安全
  • A(x) <- B(y) , !C(x,y). 只要 y 为假，那么 x 无论取什么，C(x,y)为假，这样 x 也有无限多个值
  • A(x) <- B(x), !A(x). 这条规则自相矛盾，毫无意义

整体运行逻辑

image-20240120135727761

  • 单调性:数据是单调的，事实不能被删除
  • Datalog 程序总是会终止：Datalog 是单调的 且 IDB 谓词的可能值是有限的(规则安全)
  • 优点：简洁易读 + 易于实现 + 受益于现成的优化 Datalog 引擎
  • 缺点：表现力受限（无法或不方便表达某些逻辑） + 无法完全控制性能

Pointer Analysis via Datalog

  • EDB：可以从程序中直接提取的指针分析的信息
  • IDB：指针分析结果
  • rules：指针分析规则

数据模型（求解 EDB）

image-20240120140017035

运算规则（推导 IDB）

image-20240120140209982

涉及方法调用时

image-20240120140401310

其中

  • VCall(l:S, x:V, k:M) Dispatch(o:O, k:M, m:M) ThisVar(m:M, this:V) 传方法与 this 指针
  • Argument(l:S, i:N, ai:V) Parameter(m:M, i:N, pi:V) 传递参数
  • CallReturn(l:S, r:V) MethodReturn(m:M, ret:V) 传递返回值
  • 是 EDB
  • Reachable(m:M) CallGraph(l:S, m:M)是 IDB

全程序分析代码

image-20240120140829596

  • main 函数先执行，进行 reachable.
  • 只要在标红处限定方法 m 即可，因为其他规则都依赖于 VarPointsTo 这个方法，如果方法不可达，那么这个方法中的变量的 VarPointsTo 必为空，就不会有其他影响了

Taint Analysis via Datalog

数据模型

EDB 谓词

  • Source(m: M) // source methods
  • Sink(m: M, i: N) // sink methods
  • Taint(l: S, t: T) // associates each call site to the tainted data from the call site

IDB 谓词：TaintFlow(sr: S, sn: S, i: N) 表示污点数据可能从 sr 方法产生，通过 sn 的第 i 个参数传递到 sink 方法 sn。

规则

image-20240120141259995