区块链 2022-07-04 00:32 作者:baidu    浏览:145    

大纲1

二静态程序分析概述

2.1静态分析的应用

2.2静态分析是近似结果,莱斯定理

3.1 TIP语言实例

3.2 TIP语法

3.3范式

程序优化分析:优化编译器以生成有效代码。

程序正确性分析:为检测程序错误而设计

程序开发分析:举个例子,第117行可能调用哪个函数? 或者相反,函数f可能从哪里调用? 函数内联和其他重构依赖于这些信息。

一句话,“程序测试可以用来指示错误的存在,但决不能指示它们的存在”。 本节的标题,简言之是静态分析和莱斯定理的关系,

具体来说,可以看到熊英飞老师关于这一部分的说明。

也就是说,莱斯利定理描述了由图灵机创建的程序的某些属性是不可确定的,通过分析安全漏洞的程序转换为静态分析的目的,可以确定程序或属性是否“有缺陷” (另外,莱斯定理仅限于图灵机编写的程序,如果不是图灵机就无法适用。 请大家自己调查什么是图灵机)

但根据莱斯利定理,无法确定该程序是否具有缺陷,只能通过静态分析或理想分析器找到近似判断。 这个判断可以说是无限接近理想的分析。

例如,要找出程序中所有缓冲区的漏洞,需要生成导致该漏洞的所有测试用例,可以吗? 你能找到引起这个漏洞的所有用例吗? 答案是否定的。

这就是我们一节所说的“静态分析是近似的结果”。 因此,静态分析就是尽可能地朝着理想值进行分析,在安全领域找到尽可能多的漏洞。 但是,我们找不到这个程序的漏洞。

如果还不理解,可以看到下面两条横线中的这个例子。

近似的答案有助于发现程序中的错误,可能被认为是程序验证的薄弱形式。 例如,使用C语言指针编程到处都是危险的,包括取消引用空指针悬空内存泄漏和意外别名。 普通编译器对指针错误几乎没有保护作用。 考虑可能发生以下错误的小程序:

标准编译器工具不会检测到此程序的错误。 如果在软件测试中找到错误,则可能会忽略该错误。 除非有测试用例碰巧使用42个参数运行程序,否则该程序不会发生错误。 但是,如果对空值指针目标和分支阈值的问题有近似的答案,则可以静态捕获上述许多错误,而无需实际运行程序。

这种个性化的语言表达对静态分析工作具有启发作用。 原书先讲语法再讲例子,这里先讲例子再讲语法。

原文中给出了三种常见的函数程序,可以看出基本上和c语言没有太大的区别。 除了一些自定义语法外,“alloc”是为指针分配内存。

循环程序:

递归程序:

超复杂的程序:

TIP是一个

介绍一下TIP吧

参数表示:

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

对于表达式Exp :

以上文本表示exp是表达式,“|”是或。 这意味着exp是Int整数Id参数或多个表达式之间的运算或输入。 这意味着最后一行input可以从输入流中读取整数。

TIP的编写与大多数编程语言的编写几乎相同,但相当于简化的规则。 陈述也可以输出一个表达,如Id=Exp,即a=a b。

图中的问号和大括号表示可选择的分支。

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

函数调用是附加的表达式:

太抽象了,举个例子: Exp-a a,b b

作为值调用的函数

函数也可以用作一级值。 函数的名称可以用作引用函数的变量。 您也可以将此类函数的值指派给常规变量,并将其作为参数传递给函数,然后从函数返回。

与简单的函数调用不同,被调用的函数现在是计算为函数值的表达式。 通过函数值,可以说明面向对象语言方法和函数语言的高阶函数面临的主要挑战。

在main函数中,inc函数作为参数传递给twice函数,并调用两次指定的函数。

指针

? 下图:

第一个表达式将新单元格分配给用给定表达式的值初始化的堆,并生成指向该单元格的指针。 具体例子如下:

第一行分配了一个初始值为null的单元格,第二行中的y指向变量x,然后第三行中的值42分配给第一行中的分配单元格,第四行通过两个指针引用读取该单元格的新值。 也就是说,Stm行的指针操作对应于z的操作。

记录

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

例如,第一行将创建包含两个字段的记录。 一个名称为f,值为1,另一个名称为g,值为2。 第二行读取f字段的值:

从第五节可以看出,这是对面向对象语言的语法描述。

像几种常见的编程语言一样,对字段的赋值操作可能如下所示:

具体例子如下。

程序

TIP语言的定义程序只是函数的集合:

对于完整程序,main函数是开始执行的函数。 的参数从输入流的开头开始依次提供,返回的值附加到输出流中。

以上,语法介绍结束了。

编写程序时,使用丰富的灵活语法可能会很有用,但在编写和实现静态分析时,使用语法更简单的语言通常更方便。 因此,在静态分析中,有时会通过将程序变换为等价但句法更简单的程序来将程序正规化。 一个特别有用的规范化是展平嵌套指针表达式。 这样,指针的解引用将始终采用*Id格式,而不是更常见的*Exp格式。 同样,函数调用也始终是格式Id而不是Exp。 也可用于平展开演公式直接调用的参数分支阈值和返回公式。

举个例子:

归一化后如下所示

上图的定律是,一个陈述只包含一个操作。


 
打赏