前言


发现现在网上的笔记都不怎么适合阅读,就自己做一下

简介


程序语言 (Programming Languages)

国内研究PL的不多,人才很少
活跃度很高
在这里插入图片描述
在理论部分,考虑的是如何设计一个语言的语法和语义,如何设计语言的类型系统等等问题;有了语言的语法、语义和类型系统之后,我们需要支撑语言的运行。因此,在环境部分,需要考虑如何为运行中的程序提供运行时环境——如何设计编译器,在运行时需要怎样的支持(如内存的分配管理)等等;应用部分则关注如何保证语言所写出程序的效率、安全性和可靠性,主要考虑如何对程序进行分析,验证和合成(如何自动合成一个程序)。
静态程序分析属于应用下的一块。

《静态程序分析》对谁有用?

学生,开发者,研究者……几乎所有当代生活者都能从中受益。

学习方向与程序有关的学生。

计算机方向的学生可以通过深入学习这一领域知识而为自己建立独特的学术和就业优势,也能加深对编程的理解以降低自己写出bug的频率。

其他方向的学生既然已经开始阅读这一页面,想必对计算机方向的内容有一定兴趣。你可以通过了解这一技术,了解静态分析软件(包括其内置于编译器,集成开发环境的部分)能够为你提供怎样的功能和便利,以及如何更好地使用这些软件,以此保证你所关心的程序质量。

工作内容与程序有关的开发者。

无论你希望更好地理解Wiki上众多的开源或是闭源的静态程序分析技术,还是希望自己开发一个适用于眼下工作内容的静态程序分析器以保证程序质量,了解静态程序分析都会有所帮助。

研究领域与程序相关的研究者。 或许你希望微调研究方向,却因没有合适的入门材料而苦恼;或许你希望了解计算机领域的相关知识以期获得启发……这一教程可以作为你的入门材料或是闲暇读物。

生活与程序相关的每个人

软件质量是信息化时代的重要议题之一,在这个时代生活与工作,你一定会遇到相关的问题。

在大多数学校和企业中,没有开设该领域的课程。

什么是静态程序分析?

静态程序分析在计算机科学领域中的定位

编程语言的分类
当今的计算机世界,面对这样一个问题:

Background: In the last decade, the language cores had few changes, but the programs became significantly larger and more complicated.
Challenge: How to ensure the reliability, security and other promises of large-scale and complex programs?
数十年来语言的核心没有变化,但软件的规模和复杂性增长迅速,如何保证程序的可靠性?

尽管新的语言和特性层出不穷,但现在编程语言无非三大类:

  • 命令式(C、C++、JAVA)
  • 函数式(Scala、Haskell)
  • 逻辑式(Prolog)

静态程序分析的应用

静态程序分析可以处理以下问题(以下概念只需要了解,重要的应用在后面课程中会详细讲解。

提高程序可靠性

  • Null pointer dereference, memory leak, etc.
  • 空指针引用与内存泄漏等:几乎每个程序编写者都被这两个问题所困扰过

提高程序安全性

  • Private information leak, injection attack, etc.

  • 隐私信息泄漏:这一问题在移动应用中较为普遍

  • ​注入攻击:这是网络安全中非常常见的议题。不熟悉的读者可以查看W3School或Wiki上关于SQL注入攻击的例子。

为编译优化提供基础技术

  • Dead code elimination, code motion, etc.

  • ​死代码消除:在编译器的机器无关优化环节,将不会对程序执行结果产生影响的代码(即死代码)删除。

  • ​循环不变量的代码移动:在编译器的机器无关优化环节,在保证不影响程序执行结果的情况下,将循环中的特定语句移动到循环外,使得程序运行时执行的语句数减少。

有助于程序理解

  • IDE call hierarchy, type indication, etc.

  • 为集成开发环境的功能提供帮助:当你使用VS/Idea/Clion/Eclipse/Android Studio等等IDE时,将鼠标悬停在代码上,IDE能够动态地分析并提示你所悬停对象的相关信息,背后使用的技术就是静态程序分析。

  • 此外,静态程序分析技术也可以分析多线程程序,这是一个有难度的研究领域。主要困难在于处理多线程间的interleaving。本书定位入门,不会涉及相关内容。

静态程序分析的市场

在学术界,静态程序分析技术几乎可以应用于所有关于程序的研究方向。

在工业界,国外的Google,IBM等大企业已经初步建立了自己的静态程序分析团队。国内的华为和阿里等企业也正在积极寻找静态程序分析方面的人才。

无论你将来想在学术界还是工业界深入发展,学习这一领域的知识都能为你建立独特的优势。

静态程序分析与类似技术的对比

Testing shows the presence, not the absence of bugs. --Edsger W.
Dijkstra

动态的软件测试和形式化语义的验证的作用与静态程序分析类似,这一部分对这三个细分方向做简单的对比。

静态程序分析

优点:在选定的精度下能够保证没有bug。这在教程中会详细介绍。

缺点:

学术门槛相对高。目前已知国内高校公开的课程资料只有北京大学,南京大学,国防科大,吉林大学的,且通俗易懂的教材稀少。作为一门计算机专业的高年级选修课,入门和提高都较困难。

动态软件测试
优点:在工程中被广泛应用,并且有效。实现简单,便于自动化。

缺点:

  • 无法保证没有bug。 这是无法遍历所有可能的程序输入的必然结果。

  • 在当今的由多核与网络应用带来的并发环境下作用有限。 某个bug可能只在特定情况下发生,因而难以稳定地复现。如果你对并发程序的动态测试细节感兴趣,可以参考《拧龙头法测试并发程序》。(截图来自南京大学《形式化语义》课程资料)

形式化语义验证
优点:由于用数学的方法对程序做了抽象,能够保证没有bug。

缺点:

  • 学术门槛较高,学习者必须有良好的数学基础才能入门。

  • 验证代价较高,一般来说非常重要的项目会使用这一方式保证程序质量。甚至在操作系统这样重要的软件中,也并不一定会使用。

莱斯定理

递归可枚举语言的所有非平凡(nontrival)性质都是不可判定的。
咋证明没看明白。

Sound and Complete

首先我们要回答什么是sound,什么是complete。
在这里插入图片描述
Sound表示是安全的,也就是说,程序分析覆盖了所有的问题(大于等于Truth),这样我们不会缺漏内容,比如静态分析程序的错误。此时我们可以认为是过拟合的。

Complete不是表示Truth完全的,而是说所覆盖的内容完全是我们所需的,也就是说,不会误报,但可能会导致漏报。此时我们可以认为是欠拟合的。

人类对于程序分析的终极目标是:Sound and Complete,也就是图中完美的Truth。但莱斯定理告诉我们,不可能既sound又complete(AI也可以用这个)。所以我们得做个妥协。

大多数时候,我们不希望有错误是没有被发现的,我们可以接受误报,但不能接受漏报,误报的范围是可定的,漏报则意味着有野生的问题,成本开销太高了。所以我们一般都是在尽量保证sound的情况下追求complete。也就是在不漏报的情况下减少误报的情况,这也是符合我们的一般认知的。比如说我们在没有漏报的情况下多了一个误报,这是符合莱斯定理的,也几乎不会影响我们的开发,这就是一个不错的理想情况。

真、假、假阴性、假阳性

这四个其实我一直不是很能绕得明白,就放在这里记录一下。

True/False Positive/Negative

这个A B结构中,B是我们判断的结论,A则是这个结论文正确与否。
所以False Positive就是假阳性,即我们认为他是阳性的,但我们的判断其实是错的。
在这里插入图片描述
比如,False Positive就是,虽然不是Truth,但我们认为是Truth。

虽然在之前我们说保证sound,但也不能为了sound而无限牺牲complete,过多的误报会让报告失去意义,就像全文都是重点就等于没画重点。过多的误报会让人忽略其中有真正的错误报告。

更多推荐