静态分析系列1-南大软件分析1.0 导论学习笔记

Posted 区块链市场观察家

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了静态分析系列1-南大软件分析1.0 导论学习笔记相关的知识,希望对你有一定的参考价值。

文章目录

印象回顾

昨天看了南大《软件分析》的第一节导论,回忆一下还记得哪些重要内容,此部分回顾不打算纠正。

静态分析概念:在软件运行之前的代码分析,也许可以理解为编译阶段。

Rice Theory: 对于编程语言来说,不存在完全精确的或者说完美的静态代码分析。

系统指标及其取舍: Sounds 是漏洞 Truth 的超集,包含所有漏洞的同时会存在误报。Compelete 是漏洞 Truth 的子集,准确报告漏洞的同时会存在漏报。

实际应用中,对于一套系统来说,宁愿存在误报,也不愿意存在漏报。因为误报可以人工核查,但漏报可能会带来致命危险。所以一般静态分析,都是 Sounds 类型。

系统性能的平衡: 从漏洞产出的角度分析,静态分析的精确度远远比速度重要,但谁会愿意使用静态分析需要6小时甚至更多时间的工具呢?如果从精确度来讲,指针可能都无法分析全面。所以一个良好的静态分析工具,一定是精确度和速度的良好平衡。

抽象和 over-xx: 记忆淡忘

重要启发: 李樾老师提到一个观点,我的个人理解是,研究的兴趣更重要,基本不存在没有产出的点。如果用心去做,在这个过程中自然而然就会发现创新点,如果不用心去做,当然大概率会半途而废。

领导提点过我,容易想太多,实际情况也确实常常如此。去年7月份了解学习过两周的静态代码审计,但后面纠结于产出无望而停止探索。目前在学习中也遇到了很长时间的瓶颈,难以深入,一部分原因是个人兴趣,更重要的是纠结产出。很多时候,我们都太缺乏死磕到底的精神,甚至最近几天也在考虑静态分析能不能、要不要持久地学习下去,诚实地讲感到惭愧。

当然,也是随着这一年的成长,接触到一些身边师傅做的静态分析项目,另外南大分析的课程很早以前就有师傅在群里推荐,以及公司提供了最大的契机,这些东西都增强了我对静态分析的信心。没有这些平台,估计也就没有这些契机,这件事情我也不会去学习研究。只能说平台对个人的成长至关重要吧。

还有至关重要的一点:Don’t Compare.

二刷复习

主要内容

快速回顾查漏补缺,主要对上一节的回顾内容进行补充。

Static Analysis:在运行之前了解程序相关的所有行为,及其性质是否能够得以满足。
简单来说,在运行程序之前,在静态时刻和编译时刻,就知道关于程序行为的一些特征和性质。

Rice’s Theorem(大米定理):对于递归可枚举语言 / 编程语言,对于程序的性质想要给出准确答案是不可能的。

通过符号分析示例了解静态分析的抽象和近似:

变量值的符号抽象: 变量值可以抽象为 +、-、0、Top/Unknown、Undefined。

Over-approximation(过近似): Transfer Functions,转换函数或转换方法。在抽象之后需要近似,Transfer Function 实际上是给每一条语句的抽象值做 转换规则

根据什么制定转换规则呢?根据分析目标和不同程序语句的语义。

运算语句的转换规则: 拿符号分析举例来说,目前通过抽象获得了变量的抽象值,想要分析变量值的正负等信息,就需要定义规则如不同的抽象值 + - * / 不同的抽象值 = 某种抽象值。通过这些 运算语句的转换规则,获得变量值运算结果/最终变量值的符号。

Control Flows 的转换规则: 近似还需要有 Control Flows/控制流 来制定转换规则,或者说程序执行的流,可以理解为通过上下文信息判断变量值的符号信息。

通过示例说明,变量值没有经过运算,而是通过 if 条件来定义变量的值,此时就需要识别该 Control Flows 来判断变量值的符号。如何识别呢?我们需要抽象 Control Flows,然后制定 Control Flows的转换规则 来获取变量值的符号信息。

控制流的合并 flow merging: 控制流会有不同的执行路径分支,在不同分支执行后的的所有变量值汇聚点,我们需要对两个分支内的变量值进行一个合并。

原因是,由于难以枚举程序的所有执行路径,所以把 flow merging 作为 Control Flows 抽象的方式,它是静态分析默认采取的一种近似方式。

课程说明

前半部分课程主要大纲:

  • 中间表示(Intermediate Representation)
  • 数据流分析的应用和基础(三节)
  • 内部优化分析
  • CFL-Reachability and IFDS(Context Free Language 上下文无关技术的可达性)(Interprocedural,Finite,Distributive,Subset Problem,是一种基于图可达性的程序分析框架)
  • Soundness and Soundiness

后半部分课程主要大纲:

  • 指针分析的基础和上下文敏感度(三节)
  • 当代指针分析
  • 安全领域的静态分析
  • Datalog-Based Analysis(Datalog是一种数据查询语言)
  • 抽象解释

五个课程实验:

  • Constant Propagation(CP,常数传播,作用是编译优化)
  • Dead Code Elimination(DCE,死码消除)
  • Class Hierarchy Analysis(CHA,类层次分析,从该部分开始可以进行整个系统的分析)
  • Pointer Analysis(PTA,指针分析)
  • Context-Sensitive Pointer Analysis(CSPTA,上下文敏感的指针分析)

本节划重点

1)What are the differences between static analysis and (dynamic)testing?

2)Understand soundness, completeness, false negatives(漏报), and false positives(误报).

3)Why soundness is usually required by static analysis?

4) How to understand abstraction and over-approximation?

个人理解重点和扩展

理解并记忆内容

对个人来说,记住如下三点内容,以及一个启发即可。不要觉得简单,这只是导论,而且才接触了过近似的皮毛。

  • Rice’s Theorem.

  • Soundness 和 completeness

  • Abstraction 和 over-approximation

扩展信息:南大硕士招生信息

李樾老师,南京大学计算机科学与技术系,程序设计语言与静态分析研究组。

学院招生信息,参考 南京大学2022年硕士研究生统考拟录取名单公示

学院位置始于录取名单文件第61页,录取专业和录取人数如下。再找相关的老师和学长学姐咨询下细节。

  • 学硕-计算机科学与技术,共计9人
  • 专硕-电子信息,共计40人

以上是关于静态分析系列1-南大软件分析1.0 导论学习笔记的主要内容,如果未能解决你的问题,请参考以下文章

静态分析系列1-南大软件分析2.1 认识Java的Soot静态分析框架(待补充)

学习笔记网络图数据分析导论(solid)

学习笔记网络图数据分析导论(solid)

南大算法设计与分析课程复习笔记L3 - Recursion

南大算法设计与分析课程复习笔记

《需求工程--软件建模与分析》阅读笔记01