> For the complete documentation index, see [llms.txt](https://ranger-nju.gitbook.io/static-program-analysis-book/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://ranger-nju.gitbook.io/static-program-analysis-book/ch4/04-02-datalog-based-pa.md). # 实现——声明式指针分析 ## Datalog-Based Program Analysis Datalog是一种声明式（Declarative）的编程语言。 主要内容如下： 1. Motivation 2. Introduction to Datalog 3. Pointer Analysis via Datalog 4. Taint Analysis via Datalog ## Motivation 如果用Imperative的编程方式做指针分析，很麻烦。 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-1afb6e87ab12f383b61651ca765c60ce38eb0ef9%2Fimage-20201223184349163.png?alt=media) 而如果用Declarative的方式做编程分析，能够极大地简化实现。 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-393847f7ddc6fb501fcc387c1e266292a08789bb%2Fimage-20201223184415502.png?alt=media) ## Introduction to Datalog 接下来学习一个船新的语言——Datalog，它实际上是大名鼎鼎的Prolog的一个子集。 `Datalog=Data+Logic(and,or,not)` * 没有副作用 * 没有控制流 * 没有函数 * 不是图灵完备的 ### Data #### Predicates 谓词(Predicates)是datalog中的一个主要组成部分，可以看作是数据所组成的一个表(table of data)，每一行都代表一个事实(fact)。例如： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-cef32ee85d67debf1b44176bb46085af1bf0db63%2Fimage-20201223185015690.png?alt=media) #### Atoms 原子(Atoms)是Datalog中的基本元素，组成和例子如下： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-7a7ebcaa351e590558a21e9683bf8d34971a918f%2Fimage-20201223185231533.png?alt=media) Atoms可以分成两类 * Relational Atoms ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-cc25d0fd96e7ee50a1b2384b9252b8bac9a973f9%2Fimage-20201223185504296.png?alt=media) * Arithmetic Atoms * 如`age >= 18` ### Logic #### Datalog Rules & Logic And Datalog使用规则来进行推导(inference)，其定义如下： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-35ee998cf6c5d1bdb5e12ecc7c3d93bfc1654036%2Fimage-20201223185750701.png?alt=media) 当Body中的所有表达式都为True时，Head才为True，如： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-70b907da7b1a7b9594030ef82b6e435c6cc04d51%2Fimage-20201223185957740.png?alt=media) 求解过程(Interpretation of Datalog Rules)——枚举Body中所有关系表达式的可能取值组合，进而得到新的predicate/table。例如： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-47d4c215ef22044c4c64b6cc850b33ba4de618ff%2Fimage-20201223190539380.png?alt=media) ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-3bfa6afb53308dac04d58e2d9fc19c158048e1c0%2Fimage-20201223190710495.png?alt=media) 谓词分为两类：EDB & IDB。 * EDB (extensional database) * 在程序运行前，这些数据已经给定 * IDB (intensional database) * 这一类数据仅由规则推导得来 例如： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-28926be05e41d2e71531fa23292d8619af537720%2Fimage-20201223190916420.png?alt=media) #### Logic Or 以上例子实际上是逻辑与，而逻辑或则有两种实现方式： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-648c581ec5a8bc8e1bc13e2d860052476ac07e4c%2Fimage-20201223191303096.png?alt=media) 此外还需要考虑运算优先级的问题，建议在书写程序时用括号明确地标识期望的运算优先级：`H<-A,(B;C)`。 #### Logic Not/Negation ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-9a00ff975db2ca718e74ed7b1f31cca887dfd1d8%2Fimage-20201223191451507.png?alt=media) #### Recursion ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-55f5bea6d21e4b2d39c4486b9899d45e5ba76844%2Fimage-20201223191716873.png?alt=media) ### Rule Satety 讲到这里，停下来思考一下，这两条Rules看起来有什么问题吗？ * `A(x) <- B(y), x > y.` * `A(x) <- B(y), !C(x,y).` ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-29b8ebec186a69b194c133bc933c7bb11bb1e48a%2Fimage-20201223192111827.png?alt=media) ~~第一次学看不出问题也没问题的~~ 由于x有无限的取值能满足规则，所以**生成的A是一个无限大的关系**。因此上述两条规则是不安全的。在Datalog中，只接受安全的规则。 这里我们需要记住一个判定的准则：**如果规则中的每个变量至少在一个non-nageted relational atom中出现一次，那么这个规则是安全的**。 *这实际上是借助已有的predicates（它们必定是有限的）来限制变量的取值范围。* *** 类似地，还有这样的规则： `A(x) <- B(x), !A(x)` ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-817d41af90e171bb76f1b4534f441e559d839632%2Fimage-20201223193351919.png?alt=media) 对应地有第二个准则：**不要把recursion和negation写在同一条规则里**，*即避免写出非A推导出A这样的规则*。 ### Execution of Datalog Program ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-79681345777d1ffeb70f2e246db4a5c5d7a5ec66%2Fimage-20201223193808413.png?alt=media) Datalog的两大重要特性： * 单调性。因为事实（facts）不会被删除的。 * 必然终止。 * 事实的数量是**单调**的。 * 由Rule Safety，所能得到的IDB的大小也是**有限**的。 ## Pointer Analysis via Datalog 了解了Datalog的基本语法和性质，我们就可以用它来实现声明式的指针分析算法。其中三个重要的部分对应如下： * EDB：从程序的语义分析中能得到的与指针相关的信息 * IDB：指针分析的结果 * Rules：指针分析的规则 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-f3a135a29298348c07617e764857615feb07ed06%2Fimage-20201223194245876.png?alt=media) 和之前一样，我们把Call放到最后处理。 ### Datalog Model-EDB\&IDB 我们首先需要对前四条语句建模。输入的EDB代表了4个存储相应类型语句的table，输出为Variable和Field的指向关系。 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-5a459565c7201615f2cd92280a2cf46a35b0e7a0%2Fimage-20201223194326258.png?alt=media) 一个关于EDB的例子如下： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-2dfab9ca8c52c604138c00b53f772a72392be333%2Fimage-20201223194559347.png?alt=media) ### Datalog Rules Body按照红线所示代表前提，Head按照蓝线所示代表结论。 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-069d954817490082725f0e5e7a67dfcb30a55261%2Fimage-20201223195004344.png?alt=media) ### Example 利用刚刚讲解的算法和Datalog的执行规则，分析这一段代码，给出推导结束后的IDB。 ```java b = new C(); a = b; c = new C(); c.f = a; d = c; c.f = d; e = d.f; ``` 结果如下： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-255fc077031fde0cd63c3f98ff88865adad7229f%2Fimage-20201223195501180.png?alt=media) ### PA with Calls 回顾指针分析中Call的规则： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-8bf2af96550b2e8030a3a5f555c7191a29273faa%2Fimage-20201223200506410.png?alt=media) #### This 首先，我们需要引入新的EDB和IDB： （VCall即Virtual Call，ThisVar即This Variable） ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-b8236a487a993295f5c4ecbe753146cec4065a64%2Fimage-20201223200243589.png?alt=media) 我们能够同时知道三个信息： 1. this指向对象o 2. 方法m是可达的 3. 方法m可达是因为在l行处存在对方法m的调用 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-9868eefdda4a56786a7b64581f6d2cfd0ab4f91b%2Fimage-20201223200617134.png?alt=media) #### Parameters 接下来要处理参数的传递，与之前类似，引入EDB标识Argument(调用语句行号，参数标号和参数本身)和Parameter(被调用方法，参数标号和参数本身)： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-a2858ca05c891a0c2777803aba8b292db26bd06e%2Fimage-20201223200945544.png?alt=media) 而对应用Datalog书写的规则如果用自然语言描述，就是处理行号l处对m的调用时，根据形参和实参的信息，将实参已经有的指向关系传递给形参数。 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-cfbd3a09fbc45ff4d3e8849f0bddc67a15bce91f%2Fimage-20201223201109543.png?alt=media) #### Return Value 引入EDB： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-6dc8f0d2c5ba283bbb9c4e7efb35abea88e9ff7f%2Fimage-20201223201354991.png?alt=media) 对应的Datalog Rule，处理返回值的指向关系： ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-9246b6a30abe2e85441a59a34322e1bdcabef632%2Fimage-20201223201428109.png?alt=media) #### Sum up 以上三个部分总结起来，就能得到以下的Datalog Rules。 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-97a935c2b21792e2aa1832196d6adc3747cdc725%2Fimage-20201223201612811.png?alt=media) 进而能得到全程序的分析算法如下。值得一提的是，在VarPointsTo规则中，添加Reachable(m)跳过不可达方法中的对象。而其他规则不需要加这一条件，则是因为它们都有VarPointsTo规则作为Body的一部分。 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-815156160a7cb6849fcdf569e0f0dbaa4f833f75%2Fimage-20201223201746117.png?alt=media) ## Taint Analysis via Datalog ### Datalog Model 同样需要用户提供Source和Sink。输出被标记的数据可能流到的Sink方法。 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-d5886a74a7a04e7f24c0211f076fddb0dee0686c%2Fimage-20201223201956852.png?alt=media) ### Datalog Rules 说明：这里参数列表中用`—`表示通配符，即不关心枚举时这个位置取什么值。 ![](https://4182415683-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MJC1RRYQ991XoNX219t%2Fuploads%2Fgit-blob-db97a44802fcbb694e6834ed9e2f1ab9c12e7449%2Fimage-20201223202140289.png?alt=media) ## Key Points * Pros * **Succinct** and **readable** * **Easy** to implement * **Benefit from off-the-shelf optimized Datalog engines** * Cons * **Restricted expressiveness**, i.e., it is impossible or inconvenient to express some logics * Cannot fully control **performance** * Overall Review * **Datalog** language * How to implement **pointer analysis via Datalog** * How to implement **taint analysis via Datalog**