南京大学《软件分析》李越, 谭添—

南京大学《软件分析》李越, 谭添——1. 导论

导论

主要概念:

sound
complete
PL领域概述

动手学习

本节无

文章目录

导论
- 1. PL(Programming Language) 程序设计语言
- - 1.1 程序设计语言的三大研究方向
  - 1.2 与静态分析相关方向的介绍与对比
  - - 静态程序分析
    - 动态软件测试
    - 形式化(formal)语义验证(verification)
- 2. 静态分析:
- - 2.1莱斯定理(Rice‘s Theorem):
  - 2.2 perfect,sound(ness), complete(ness)
  - 2.3 静态分析的目标
- 3. 静态分析的应用与前景
- 4. 静态分析的步骤

1. PL(Programming Language) 程序设计语言

1.1 程序设计语言的三大研究方向

理论: 语言怎么设计, 形式(Formal)逻辑是什么

环境: 语言要运行起来, 就要环境

应用: 保证运行起来要快, 要安全, 要可靠

拓展–语言的分类:

命令式(imperative)编程语言JAVA, C, CPP…
函数式(functional)Haskell…
逻辑式/声明式

语言没变, 环境变了, 软件越来越大越复杂

拓展阅读:

在命令式语言中，指令一个一个给出，用条件、循环等来控制逻辑（指令执行的顺序），同时这些逻辑通过程序变量不断修改程序状态，最终计算出结果。我觉得，尽管 IP 现在都是高级语言了，但是本质上并没有脱离那种“类似汇编的，通过读取、写入等指令操作内存数据”的编程方式（我后面会提及，这是源于图灵机以及后续冯诺依曼体系结构一脉的历史选择）。国内高等教育中接触的绝大多数编程语言都是 IP 的，比如 Java、C、C++等。
在函数式语言中，逻辑（用函数来表达）可以像数据一样抽象起来，复杂的逻辑（高阶函数）可以通过操纵（传递、调用、返回）简单的逻辑（低阶函数）和数据来表达，没有了时序与状态，隐藏了计算的很多细节。不同的逻辑因为没有被时序和状态耦合在一起，程序本身模块化更强，也更利于不同逻辑被并行的处理，同时避免因并行或并发处理可能带来的程序故障隐患，这也说明了为什么 FP 语言如 Haskell 在金融等领域（高并发且需要避免程序并发错误）受到瞩目。
逻辑式/声明式语言抽象的能力就更强了，计算细节干脆不见了。把你想表达的逻辑直观表达出来就好了。如今，在数据驱动计算日益增加的背景下，LP 中的声明式语言（Declarative programming language，如 Datalog）作为代表开始崭露头角，在诸多专家领域开拓应用市场。

1.2 与静态分析相关方向的介绍与对比

静态程序分析

优点：在选定的精度下能够保证没有bug。这在教程中会详细介绍。
缺点：
1. 学术门槛相对高。目前已知国内高校公开的课程资料只有北京大学，南京大学，国防科大，吉林大学的，且通俗易懂的教材稀少（详细课程及教材链接见本文末尾）。作为一门计算机专业的高年级选修课，入门和提高都较困难。
2. You tell me.

动态软件测试

优点：在工程中被广泛应用，并且有效。实现简单，便于自动化。
缺点：
1. 无法保证没有bug。 这是无法遍历所有可能的程序输入的必然结果。
2. 在当今的由多核与网络应用带来的并发环境下作用有限。 某个bug可能只在特定情况下发生，因而难以稳定地复现。如果你对并发程序的动态测试细节感兴趣，可以参考《拧龙头法测试并发程序》。（截图来自南京大学《形式化语义》课程资料）

外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传

形式化(formal)语义验证(verification)

优点：由于用数学的方法对程序做了抽象，能够保证没有bug。
缺点：
1. 学术门槛较高，学习者必须有良好的数学基础才能入门。
2. 验证代价较高，一般来说非常重要的项目会使用这一方式保证程序质量。甚至在操作系统这样重要的软件中，也并不一定会使用。(截图来自鸿蒙OS直播发布会)

2. 静态分析:

粗略定义: 在程序运行之前就通过分析行为完成一些检验, 无需编译运行

可能的检验: 有无信息泄密, 有无空指针解引用, 有无死代码…

2.1莱斯定理(Rice‘s Theorem):

原话: Any non-trivial property of the behavior of programs in a r.e. language is undecidable
概念解释:
- r.e.(recursively enumerable递归可枚举): 就是计算机可以识别的语言也就是我们能见到的所有语言
- non-trivial: 简单理解就是与程序运行时行为有关的性质
人话: 一个正常你见过的编程语言, 没有方法能让你确切知道程序是否有某个和运行时行为相关的性质: 比如对c语言程序来说, 不存在一个方法能确切的告诉你程序里有没有空指针

简单来说, 就是不存在完美(perfect)的静态分析方法

perfect/truth = sound + complete

2.2 perfect,sound(ness), complete(ness)

Sound: 误报, 能够找全, 但是找的不一定对

Complete: 漏报, 找的全对, 但是不一定找全

一般静态分析追求sound

为什么追求sound而不是complete举例:

抓贼做类比, sound就是先抓嫌疑人, complete就是抓看一眼就是贼的

sound可以保证缩小排查范围, 保证贼就在嫌疑人里, 在嫌疑人中排查, complete做不到, 因为没抓全的贼还是要在全中国的人里排查, 还不如一开始就在全中国一个个排查谁是贼

举例: 一个程序里真实情况是有a, b, c三个地方有空指针

perfect就是报告真实情况: a, b, c三个地方有空指针

Sound就是报告a, b, c, d四个地方有空指针(d不是空指针也就是报错了, 但至少abc报全了)

Complete就是报告a, b两个地方有空指针(虽然ab都报对了, 但是c没有报到, 就是没有报全)

外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传

2.3 静态分析的目标

正确性——保证sound

怎样的程序分析是对的:

if input: x = 1
else: x = 0

想要分析x = ?

x = 1 or 0: sound&complete 正确
x = 1 or 0 or 2 or 3: sound 正确
x = 1 or -1: 啥也不是错误
x = 1: complete 错误

精确性

能提供更多的信息

当inputTrue, x = 1; 当inputFalse, x = 0: precise精确的
x = 1 or 0: imprecise不精确

目标: 保证sound的前提下, 让分析的精确度和速度尽可能高

动态特性: JAVA反射本地代码可能会影响Sound很难真正的sound

帮助提高程序可靠性, 防止空指针内存泄漏

帮助提高安全性, 防止信息泄密, 注入攻击

编译优化, 死代码消除, 代码移动(code motion)

程序理解, 类型提示

3. 静态分析的应用与前景

人才非常少

学术界: 程序设计语言, 软件工程, 系统, 安全…等任何需要编程的方向,
工业界: 每个公司都有专门的软件分析的团队, 去分析本公司的代码质量, 还有专门做分析的公司: GrammarTech, Semmle, Sourcebrella

更具体的比如智能合约安全, 区块链安全, 智能漏洞检测等

程序分析的用途概览：

**程序可靠性（Program Reliability）**想必你应该经历过程序崩溃后报错信息中显示的空指针异常吧，是的，像这种影响程序可靠性的诸多 bug，很多都可以被程序分析在静态时检测出来，包括那些可能会导致程序不响应的程序缺陷，如内存泄漏。
**程序安全性（Program Security）**程序分析几乎是软件安全必学的内容之一。
**编译优化（Compiler Optimization）**源码中的许多操作在编译时可以转换成更加高效的方式。此外，dead code elimination 可以避免永远执行不到的代码编译进程序； code motion 可以将某些表达式移动到其他位置，减少重复计算的冗余。
**程序理解（Program Understanding）**程序理解和 IDE 设计非常相关，例如调用关系、继承关系、声明类型等信息都需要通过程序分析的方法获取。程序的调试有时也需要程序分析技术的辅助。