Group of Software Security In Progress

GoSSIP @ LoCCS.Shanghai Jiao Tong University

A Path-Sensitively Sliced Control Flow Graph

论文下载

Intro

  • 目标: path sensitively sliced CFG (PSS-CFG)
    • From:
if(c) p = 1; else p = 0;
x = 0;
if(p > 0) x = 1;
if(x == 0) z = 1;
TARGET: {z}
  • To:
if (!c) z = 1;
  • 方法:
    • path-sensitivity:
  • from:
if (c) p = 1; else p = 0;
S;
  • to:
if (c) { p = 1; S;} 
else { p = 0; S; }
  • 每个分支分别做slicing,就都有可能简化,然后,就变成最终的结果

Basic Idea

  • 给了一个例子,目前已有的考虑了 path sensitivity 的 Frama-C和别的东西也不能切分成我们这么好的效果,因为这个例子中的每一条语句都至少在一条路径上会影响target
  • 例子:

Fig

  • 从左到又依次是源代码,Symbolic execution tree, 简化的SE Tree,最后切分出来的代码
  • 图中尖括号的内容是Redundant State Detection for Dynamic Symbolic Execution这篇文章中提到过的在能够覆盖接下来的路径的约束条件以及依赖集(能够影响target的变量集合),在符号执行每次结束后生成
  • Slice 方法:
    1. 如果一条赋值语句之后的状态的依赖集中没有该变量,这条语句就可以删掉(一般Slice使用的方法)。
    2. 如果if语句之后某个分支的约束无解,则可以将该分支删除。
    3. 如果一个if的两个分支中的语句都被删掉了,把整个if语句去除。

其他细节

  • 生成SE Tree的时候,所有的循环最多展开K次
  • 符号执行过程中循环执行结束之后可能产生很多不同的分支,我们把约束放松一些,用循环的结束条件做约束。。
  • Redundant State Detection文章中是说约束条件是子集就可以状态合并,我们要求约束条件完全相同才能合并。因为,更强的约束条件可能其下的分支减少,我们就是要发现这种情况。。

实验

  • 证明了它生成的切分后的代码和通常的方法相比,生成的代码量增长不多(2倍左右)
  • 但是对PSS-CFG做符号执行要比对普通的切分方法且分出来的CFG做符号执行快(平局3.1)
  • 对PSS-CFG做Program Verification比一般要快2倍。。