?

本系列文章为，基于奥尔胡斯大学的Anders M?ller 和 Michael I. Schwartzbach两位教授于2022年2月1日所出版的《static program analysis》，的读书笔记

关注微信公众号 信安科研人，发送“静态分析1”获取书籍英文原版pdf
 

?

编辑

---

目录

一  大纲

 ?编辑

 二 静态程序分析简介

2.1 静态分析的应用

2.2 静态分析是一种近似的结果，莱斯定理

三 TIP语言 tiny imperative programming language

3.1 TIP语言实例

3.2 TIP的语法

3.3 范式

---

一  大纲

 ?编辑

 关注公众号信安科研人，发送“静态分析思维导图”获取导图

 二 静态程序分析简介

2.1 静态分析的应用

1. 程序优化分析：优化编译器（包括解释器中的即时编译器），以便生成有效的代码。
2. 程序正确性分析：设计用于检测程序错误（或验证是否存在错误）
3. 程序开发分析：举个例子，第117行可能调用哪些函数，或者相反，函数f可能从何处调用？函数内联和其他重构依赖于这些信息。

2.2 静态分析是一种近似的结果，莱斯定理

        一言以蔽之：“程序测试可以用来显示错误的存在，但永远不能显示它们的不存在”。这一节的标题，说白了就是静态分析与莱斯定理之间的关系，莱斯定理对静态分析的限制。

?编辑

        具体的可以看熊英飞老师对这部分的讲解： 如何理解莱斯定理对程序静态分析的限制？ - 知乎 (zhihu.com)

        就是说，莱斯定理描述了由图灵机造出的程序的某种属性是不可确定的，那么，转换到以分析安全漏洞的程序静态分析的目的，就是确定程序或者属性是否是“具备缺陷的”。（注意，莱斯定理限定为图灵机做出的程序，非图灵机是不适用的，什么是图灵机大家可以自行查阅）

        然而，按照莱斯定理，我们无法判断这个程序是否一定是具备缺陷的，使用静态分析或理想的分析器，只能找到一个近似的判断。这种判断可以说是无限接近于理想分析。

例如，我要找到一个程序的所有缓冲区漏洞，这需要构建恰好所有符合触发这个漏洞的测试用例，这可能吗？我能找到所有触发这个漏洞的用例吗？答案是不能。

        这就是我们这一节所谓的“静态分析是一种近似的结果”，因此静态分析就是尽可能的向着理想值去分析，对于安全领域就是尽可能找到更多的漏洞，但是我找不尽这个程序的漏洞。

        如果还没有理解，可以看下面俩横线中的这个例子：

---

        近似答案可能有助于发现程序中的错误，视为程序验证的一种弱形式。例如，使用C语言中的指针进行编程到处都是危险，例如空的取消引用、指针悬空、内存泄露和意外别名。普通编译器对指针错误几乎没有保护作用。考虑以下可能执行各种错误的小程序：

?

编辑

?

编辑

         标准编译器工具（如GCC-wall）不会检测到此程序中的错误。通过软件测试查找错误可能会遗漏错误（对于此程序，除非我们碰巧有一个正好使用42个参数运行程序的测试用例，否则不会遇到错误）。然而，如果对有关空值、指针目标和分支条件的问题有近似的答案，那么上述许多错误都可以静态地捕获，而无需实际运行程序。

---

三 TIP语言 tiny imperative programming language

        在接下来的章节中，该书使用一种称为 T(iny) I(mperative) P(rogramming) 的小型命令式编程语言。该语言具有最小型的语法，但包含使静态分析变得有趣和具有挑战性的所有指令结构。

        这种自定义的语言表述对静态分析工作有着启示作用。原书是先说语法再讲例子，这里我先讲例子再讲语法。

3.1 TIP语言实例

         原文给出了三种常见的函数程序，可以看到，基本上和C语言差不太多。除了几个自定义的语法如“var”是定义参数，“alloc”是给指针分配内存。

循环程序：

?

编辑

 递归程序：

?

编辑

 超级复杂的程序：

?

编辑

3.2 TIP的语法

        TIP是一个上下文无关语法。上下文无关文法重要的原因在于它们拥有足够强的表达力来表示大多数程序设计语言的语法；实际上，几乎所有程序设计语言都是通过上下文无关文法来定义的。另一方面，上下文无关文法又足够简单，使得我们可以构造有效的分析算法来检验一个给定字符串是否是由某个上下文无关文法产生的。例子可以参见LR分析器和LL分析器。

        下面来介绍一下TIP

---

    （1）参数表达：

?

编辑

        定义Int表示所有整数，Id表示所有的变量。

        对于表达式Exp：

        ?编辑

?

编辑

         上面些文字所想表达的是：exp为表达式，“|”为或，那么意思就是，Exp可以为Int整数、Id参数、或者多个表达式之间的运算、或者是输入（就是最后一行的input，可以从输入流中读取一个整数）。

（2）陈述 statement

?

编辑

         可以看到TIP中的陈述与大部分编程语言的陈述基本相同，但是相当于是一种简化的规则。陈述可以为 Id =Exp，也就是类似 a = a+b这种，也可以输出一个表达，等等。

        图中那个问号以及中括号，代表可选择的分支。

（3）函数 functions

?编辑

         函数声明 F 包含函数名称、参数列表、局部变量声明、主体语句和返回表达式，其中，函数名称和参数是标识符，就像变量一样。var 块声明了一组未初始化的局部变量。

        函数调用是一种额外的表达式:

?

编辑

         太抽象了，举个例子: Exp->a+a,b+b | X(a+a,b+b,...)

        

(4) 作为值进行调用的函数

        函数还可以作为一级值：函数的名称可以用作一种引用函数的变量，并且可以将此类函数值分配给普通变量，作为参数传递给函数，并从函数返回。

?

编辑

        与简单的函数调用不同，被调用的函数现在是一个计算为函数值的表达式。函数值使我们能够说明面向对象语言中的方法和函数语言中的高阶函数所面临的主要挑战。 

?

编辑

         在main函数中，inc函数作为参数传递给twice函数，该函数两次调用给定函数（inc函数）。

（5）指针

???????               如下图：

?

编辑

?

编辑

        第一个表达式在使用给定表达式的值初始化的堆中分配一个新单元，并产生一个指向该单元的指针。具体的例子如下：

?

编辑

         第一行分配一个初始值为null的单元格，在第二行y指向变量x后，第三行将值42分配给第一行中分配的单元格（从而覆盖null值），第四行通过两个指针解引用读取该单元格的新值（也就是Stm 那一行的指针操作对应的就是z的操作）。

（6）记录

         记录是字段的集合，每个字段都有一个名称和一个值。创建记录和读取字段值的语法如下:

?

编辑

         举个例子，第一行创建一个包含两个字段的记录：一个名称为 f，值为 1，另一个名称为 g，值为 2。第二行读取 f 字段的值：

?

编辑

        可以看到，从第5小节开始，就是针对面向对象类语言的语法描述。

        类似常见的几种编程语言，对字段的赋值操作如下：

?

编辑

         具体例子如下：

?

编辑

（7） 程序

       TIP语言定义，程序只是一个个函数的集合：（也就是说一个函数或语句也能作为程序）

?

编辑

      对于一个完整的程序，名为 main 的函数是启动执行的函数。它的参数从输入流的开头按顺序提供，它返回的值被附加到输出流中。

       以上，语法介绍完毕。

---

3.3 范式

        编写程序时，丰富灵活的语法或许很有用，但在描述和实现静态分析时，使用语法更简单的语言通常更方便。因此，静态分析有时通过将程序转换为等价但语法更简单的程序来规范化程序。一个特别有用的规范化是展平嵌套的指针表达式，这样指针解引用总是采用*Id的形式而不是更一般的*Exp，类似地，函数调用总是采用形式 Id（Id，…，Id）而不是Exp（Exp，…，Exp）。它还可以用于展平算术表达式、直接调用的参数、分支条件和返回表达式。

        举个例子：

?

编辑

         范式化后变成：

?

编辑

         上图的规律就是：一个陈述只包含一个操作。

?