12月12, 2020

基于源代码的饿静态漏洞挖掘

软件漏洞的挖掘。

1,静态分析方法,挖掘源代码中的有用信息

2,借助深度学习等技术辅助漏洞挖掘

DARPA CGC大晒,自动化攻防。

1,传统分类中,静态和动态挖掘漏洞的技术:

静态漏洞挖掘是在不运行目标程序的前提下对目标程序进行分析,针对源代码以及针对二进制进行分析,其词法,语法,语义等,并通过相关工具获得其AST, CFG, DDG, PDG, CPG等进行辅助分析,用来挖掘漏洞。

1.1 AST: abstract syntax tree, 源代码语法结构的一种抽象表示。 以树的形式表现出变成语言的语法结构,树上的每个节点都表示源代码中的一种结构。

1.2 CFG: control flow graph, 程序执行过程的抽象表示,用在编译器中的一个抽象数据结构,代表一个程序执行过程中会遍历到的所有路径,用图的形式表示一个过程内的所有基本块执行的可能流向,反正执行过程。

CFI: control flow integrity 控制流完整技术,抵御控制流劫持而提出,早期攻击采用代码注入的方式,通过部署一段shellcode,将控制流转向这段代码执行。

为了阻止这类攻击,开发DEP:data execution prevention机制来限制内存也不能同时具备同时写和执行的权限。

攻击者为了突破DEP,发明了基于代码重用攻击的技术,利用被攻击程序中的代码片段进行拼接形成攻击逻辑,ROP, Ret2libc,JOP等,图灵完备的。

一系列操作数据的规则(指令集,编程语言,细胞自动机)用来模拟任何图灵机。

原先在shellcode在跳转执行的技术可以做到的一切攻击,ROP都能做到。

1.3 DDG: Data flow dependency graph, 以最简单的形式表示各个指令之间的数据依赖关系,图中每一个节点代表一条指令,原子节点,将他们之间具有简单的def-use依赖关系的某些原子节点组合为包含多指令的较大节点。

1.4 CPG: code property graph, 由 shiftleft提出来,

为每个应用唯一的代码版本提供可扩展的和多层的逻辑表示,包括控制图,调用图,程序依赖图,目录结构。

创建了代码多层三维表示,具有很强的洞察力,可充分了解应用程序每个版本执行的内容及可能带来的风险。

2 静态分析针对源代码的研究。

针对源代码的漏洞挖掘主要分为2类, 基于 中间表示和基于逻辑推理。

2.1 基于中间表示的分析技术主要包括:数据流分析,控制流分析,污点分析,符号执行。同时应用在工作中。

2.11 数据流分析是一项编译时使用的技术,它能从中收集程序的语义信息,并通过代数的方法在编译时确定变量的定义和使用。

通过数据流分析,可以不必实际运行程序能够发现程序运行时的行为。

是针对程序中数据的使用,定义及其之间的依赖关系等各个方面信息进行收集。

2.12 控制流分析目的是得到 程序的一个控制流图 contro flow graph.

是对程序执行可能经过的所有路径的图形化。

通过根据不同语句之间的关系,考虑由 条件转移,循环 引入的分支关系。 对过程内的一些语句进行合并,得到程序结构。

有向图,图中的结点对应程序中经过合并的基本块,图中的边对应可能的分支方向,条件转移,循环,这些都是分析程序行为的重要信息。

2.13 污点分析是一种跟踪并分析污点信息在程序中流动的技术,分析对象是污点信息流。 污点指的受到污染的信息,在程序分析中,将来自程序之外并且进入程序的信息当做污点信息。

根据分析的需要,程序内部使用的数据也可作为污点信息,并分析其对应的信息的流向。

根据污点分析时,是否需要运行程序,分为静态污点分析和动态污点分析。

污点分析过程:识别污点信息在程序中的产生点并对污点信息进行标记,利用特定的规则跟踪分析污点信息在程序中的传播过程,在一些关键的程序点检查关键的操作是否会受到污点信息的影响。

污点信息的产生点称为source点,污点信息的检查点称为 sink点。

2.14 符号执行,用符号值代替数字值执行程序的技术,符号是表示一个取值集合的记号。 使用符号执行分析程序时,对于某个表示程序输入的变量,通常使用一个符号表示它的取值,这个符号可以表示程序在此处接收的所有可能的输入。

那些不易或者无法确定取值的变量,也使用符号表示的方式进行分析。

1,将程序中需要关注的变量不能直接确定其取值的变量用符号表示。 2,逐步分析程序可能的执行流程,将变量表示为符合和常量的计算表达式。

程序的正常执行和符号执行的区别是:

1,正常执行中变量可以看做是被赋值了具体的值,而符号执行中可以是具体值也可以是符号和常量的运算表达式。

符号执行可以 把 判断路径调剂是否满足的问题 转换为判断符号取值的约束是否可满足的问题。 使用约束求解的方法,SMT 约束求解器,将符号取值约束的求解问题转为SMT问题,一阶逻辑可以满足性判断问题。

2.2 基于逻辑推理的漏洞检测方法 将源代码进行形式化描述,利用数学推理,证明等方法。 验证形式化描述的一些性质,从而判断程序是否含有某种类型的漏洞,数学推理为基础。但对于较大规模的程序,将代码形式化本身是一件非常困难的事,所以实际上研究价值相对来说并不大。

3 相关工作

3.1基于中间表示

3.2基于逻辑推理 将要验证的程序分析建模为下推式自动机,将安全属性表示为有限状态自动机,并使用模型检查来确定程序中是否可以达到违反预期安全目标的任何状态。

1.https://juejin.im/post/5cc51b096fb9a03218555972

2.http://www.jos.org.cn/html/2017/10/5317.htm

3.https://llvm.org/docs/DependenceGraphs/index.html

4.https://zhuanlan.zhihu.com/p/94611033

5.https://cs.nju.edu.cn/chenlin/pages/sat/dataflow.pdf

6.http://www.jsjkx.com/CN/article/openArticlePDF.jsp?id=10342

7.http://staff.ustc.edu.cn/~yuzhang/compiler/2017f/lectures/optimize-6in1.pdf

8.https://www.52pojie.cn/thread-861992-1-1.html

9.https://www.youtube.com/watch?v=1uLKA7Ux8hg

10.https://www.ndss-symposium.org/wp-content/uploads/2018/02/ndss2018_05A-1_Gens_paper.pdf

11.https://www.danielesgandurra.com/research/blast2008-slides.pdf

12.https://people.eecs.berkeley.edu/~daw/mops/

13.http://people.eecs.berkeley.edu/~daw/papers/mops-ccs02.pdf

https://zhuanlan.zhihu.com/p/203219161

本文链接:https://harry.ren/post/staticanlaysisofsourcecode.html

-- EOF --

Comments