程序验证工具的研究 中国科学技术大学 陈意云

Presentation on theme: "程序验证工具的研究 中国科学技术大学 陈意云"— Presentation transcript:

1 程序验证工具的研究 中国科学技术大学 陈意云 0551-3607043 yiyun@ustc.edu.cn

2 报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高程序验证能力的思路 一个程序验证系统原型演示
报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 通过一个简单例子了解概念和工作流程 函数前后条件、循环不变式、 Hoare逻辑的赋值公理，最弱前条件演算、验证条件的生成、验证条件的证明 面向实际程序验证需要解决的问题 提高程序验证能力的思路 一个程序验证系统原型演示

3 一类程序验证器的工作原理 例子：用加运算来实现乘运算的函数 function mult(m, n) { x = 0 ; y = 0 ;
while y < n do { x = x + m ; y = y + 1 ; } 例子：用加运算来实现乘运算的函数

4 一类程序验证器的工作原理 由程序员提供 由程序员提供 n  0 - - 前条件 function mult(m, n) { x = 0 ;
y = 0 ; while y < n do { x = x + m ; y = y + 1 ; } } x = m  n - - 后条件 由程序员提供 由程序员提供

5 一类程序验证器的工作原理 也由程序员提供 n  0 function mult(m, n) { x = 0 ; y = 0 ;
while y < n do { (x = my)  (y  n) 循环不变式 x = x + m ; y = y + 1 ; } } x = m  n 也由程序员提供

6 一类程序验证器的工作原理 函数前后条件、循环不变式 都称为断言 它们看上去像编程语言的布 尔表达式 n  0
function mult(m, n) { x = 0 ; y = 0 ; while y < n do { (x = my)  (y  n) 循环不变式 x = x + m ; y = y + 1 ; } } x = m  n 函数前后条件、循环不变式 都称为断言 它们看上去像编程语言的布 尔表达式

7 一类程序验证器的工作原理 Hoare逻辑赋值公理: { Q[E/x] } x = E { Q }
n  0 function mult(m, n) { x = 0 ; y = 0 ; while y < n do { (x = my)  (y  n) x = x + m ; y = y + 1 ; } } x = m  n Hoare逻辑赋值公理: { Q[E/x] } x = E { Q } 例子: { ? } x = x +1 { x > 6 } { x > 5 } x = x +1 { x > 6 } x > 5是  赋值x = x +1, 和  后条件x > 6 的最弱前条件

8 一类程序验证器的工作原理 从后向前进行最弱前条件演算，产生验证条件 n  0 function mult(m, n) { x = 0 ;
y = 0 ; while y < n do { (x = my)  (y  n) x = x + m ; y = y + 1 ; } } x = m  n 从后向前进行最弱前条件演算，产生验证条件

9 一类程序验证器的工作原理 n  0 function mult(m, n) { x = 0 ; y = 0 ;
while y < n do { (x = my)  (y  n) x = x + m ; y = y + 1 ; } ((x = my)  (y  n))  (y < n) // 循环结束程序点的断言 } x = m  n

10 一类程序验证器的工作原理 第1个验证条件 n  0 function mult(m, n) { x = 0 ; y = 0 ;
while y < n do { (x = my)  (y  n) x = x + m ; y = y + 1 ; } ((x = my)  (y  n))  (y < n)  (x = mn) } x = m  n 第1个验证条件

11 一类程序验证器的工作原理 通过最弱前条件演算得到 n  0 function mult(m, n) { x = 0 ; y = 0 ;
while y < n do { (x = my)  (y  n) x = x + m ; (x = m(y+1))  ((y+1)  n) y = y + 1 ; } (x = my)  (y  n) ((x = my)  (y  n))  (y < n)  (x = mn) } x = m  n 通过最弱前条件演算得到

12 一类程序验证器的工作原理 n  0 function mult(m, n) { x = 0 ; y = 0 ;
while y < n do { (x = my)  (y  n) (x+m = m(y+1))  ((y+1)  n) x = x + m ; (x = m(y+1))  ((y+1)  n) y = y + 1 ; } (x = my)  (y  n) ((x = my)  (y  n))  (y < n)  (x = mn) } x = m  n

13 一类程序验证器的工作原理 第2个验证条件 n  0 function mult(m, n) { x = 0 ; y = 0 ;
((x = my)  (y  n))  (y < n)  (x+m = m(y+1))  ((y+1)  n) while y < n do { (x = my)  (y  n) (x+m = m(y+1))  ((y+1)  n) x = x + m ; (x = m(y+1))  ((y+1)  n) y = y + 1 ; } (x = my)  (y  n) ((x = my)  (y  n))  (y < n)  (x = mn) } x = m  n 第2个验证条件

14 一类程序验证器的工作原理 n  0 function mult(m, n) { x = 0 ; (x = m0)  (0  n)
y = 0 ; ((x = my)  (y  n))  (y < n)  (x+m = m(y+1))  ((y+1)  n) while y < n do { (x = my)  (y  n) (x+m = m(y+1))  ((y+1)  n) x = x + m ; (x = m(y+1))  ((y+1)  n) y = y + 1 ; } (x = my)  (y  n) ((x = my)  (y  n))  (y < n)  (x = mn) } x = m  n

15 一类程序验证器的工作原理 n  0 function mult(m, n) { (0 = m0)  (0  n) x = 0 ;
(x = m0)  (0  n) y = 0 ; ((x = my)  (y  n))  (y < n)  (x+m = m(y+1))  ((y+1)  n) while y < n do { (x = my)  (y  n) (x+m = m(y+1))  ((y+1)  n) x = x + m ; (x = m(y+1))  ((y+1)  n) y = y + 1 ; } (x = my)  (y  n) ((x = my)  (y  n))  (y < n)  (x = mn) } x = m  n

16 一类程序验证器的工作原理 第3个验证条件 n  0
function mult(m, n) { ( n  0 )  ((0 = m0)  (0  n)) (0 = m0)  (0  n) x = 0 ; (x = m0)  (0  n) y = 0 ; ((x = my)  (y  n))  (y < n)  (x+m = m(y+1))  ((y+1)  n) while y < n do { (x = my)  (y  n) (x+m = m(y+1))  ((y+1)  n) x = x + m ; (x = m(y+1))  ((y+1)  n) y = y + 1 ; } (x = my)  (y  n) ((x = my)  (y  n))  (y < n)  (x = mn) } x = m  n 第3个验证条件

17 一类程序验证器的工作原理 由自动定理证明器完成验证条件的证明 n  0
function mult(m, n) { ( n  0 )  ((0 = m0)  (0  n)) x = 0 ; y = 0 ; ((x = my)  (y  n))  (y < n)  (x+m = m(y+1))  ((y+1)  n) while y < n do { (x = my)  (y  n) x = x + m ; y = y + 1 ; } ((x = my)  (y  n))  (y < n)  (x = mn) } x = m  n 由自动定理证明器完成验证条件的证明

18 一类程序验证器的工作原理 程序验证器小结 1、程序员 为各函数写函数前后条件 为各循环写循环不变式 2、程序验证器
为各函数产生验证条件（通过从前向后的演算或从后向前的演算） 证明所产生的验证条件（使用自动定理证明器）

19 报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高程序验证能力的思路 一个程序验证系统原型演示
报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高断言语言的表达能力 解决各种数据类型带来的特殊问题 解决非结构化控制结构带来的问题 … … 提高自动定理证明器的能力 提高程序验证能力的思路 一个程序验证系统原型演示 19

20 提高断言语言的表达能力 例1：表达数组a[100]的有序性 例2：表达单链表的有序性 可以在语言布尔表达式语法的基础上引入量词
i: a[i] <= a[i+1] 例2：表达单链表的有序性 用量词的方式 n:Z.i:0..n-2. p(->next)i->data <= p(->next)i+1->data 用归纳谓词的方式 SortedList(p)  p == NULL || p->next == NULL || p->data <= p->next->data && SortedList(p->next) 20

21 提高断言语言的表达能力 例3：表达二叉排序树的有序性 用归纳谓词的方式 Gt(x, p)  p == NULL ||
x > p->data && Gt(x, p->left) && Gt(x, p->right) Lt(x, p)  p == NULL  x < p->data && Lt(x, p->left) && Lt(x, p->right) Bst(p)  p == NULL  Bst(p->left) && Bst(p->right) && Gt(p->data, p->left) && Lt(p->data, p->right) 用量词方式较难定义 21

22 提高断言语言的表达能力 例4：断言语言需要更加复杂扩展的例子 断言语言越复杂，生成的验证条件就复杂，验证条件的自动证明就越困难
程序不会出现内存泄漏 程序不会对dangling指针进行dereference操作 在任何时候，最多只有一个进程处于临界区（安全性） 只要进程请求进入临界区，则最终会被允许进入（活性） 断言语言越复杂，生成的验证条件就复杂，验证条件的自动证明就越困难 22

23 解决各种数据类型带来的特殊问题 以指针类型为例 指针别名 先前提到的无内存泄漏等 最终也导致对自动定理证明器有较高期望
{ A } x = 5 { x + y == 10 } 按Hoare逻辑的赋值公理 A = (x + y == 10) [5/x] = 5 + y == 10 = y == 5 实际上最弱前条件A应该是：x == y || y == 5 先前提到的无内存泄漏等 最终也导致对自动定理证明器有较高期望 23

24 解决非结构化控制结构带来的问题 Hoare逻辑对结构化语句的推理规则 循环体中的break语句和continue语句
推理规则不会像上述规则这样简洁 {P} S1 {R} {R} S2 {Q} {P} S1; S2 {Q} {PE} S {P} {P} while E do S {PE} {PE} S1 {Q} {PE} S2 {Q} {P} if E then S1 else S2 {Q} 24

25 报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高程序验证能力的思路 一个程序验证系统原型演示
报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高断言语言的表达能力 解决各种数据类型带来的特殊问题 解决非结构化控制结构带来的问题 … … 提高自动定理证明器的能力 提高程序验证能力的思路 一个程序验证系统原型演示 25

26 报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高程序验证能力的思路 一个程序验证系统原型演示
报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高程序验证能力的思路 程序员提供对验证有帮助的提示 提高合法程序的门槛 用程序分析获得的信息来支持程序验证 … … 一个程序验证系统原型演示 26

27 程序员提供对验证有帮助的提示 方式1：程序员声明数据结构的形状 给程序员带来好处
typedef struct node{Node* : LIST next; int data;} Node; typedef struct node{Node*:TREE left; Node* :TREE right; int data;}Node; 给程序员带来好处 免除提供有关数据结构形状的函数前后条件 免除提供有关形状的循环不变式 帮助检查引起内存泄漏的操作 帮助检查对NULL指针和dangling指针的dereference操作 27

28 程序员提供对验证有帮助的提示 方式2：提供数据结构的性质定理 删除二叉排序树根节点的函数
通过循环，找到左子树的最右叶节点，取它的数据作为根节点数据，删除该最右叶节点 函数的前条件是 p!=NULL  Bst(p) 函数的后条件式是 Bst(p) 从Bst(p)等谓词定义, 基于演绎推理, 推不出性质：绿色节点是左子树上最大 但又小于根的节点 … … … p 28

29 程序员提供对验证有帮助的提示 方式2：提供数据结构的性质定理 好处：减轻了自动定理证明器的负担 那是一个需要归纳证明的性质
Gt(x, p)  p == NULL || x > p->data && Gt(x, p->left) && Gt(x, p->right) Lt(x, p)  p == NULL  x < p->data && Lt(x, p->left) && Lt(x, p->right) Bst(p)  p == NULL  Bst(p->left) && Gt(p->data, p->left) && Bst(p->right) && Lt(p->data, p->right) 那是一个需要归纳证明的性质 程序员在给出Bst等谓词定义时， 还需要给出程序用到的性质定理 好处：减轻了自动定理证明器的负担 … … … p 29

30 提高合法程序的门槛 方法1：给编程语言设计一个形状系统 排除不符合形状系统规定的程序，类似于类型检查 单链表指针h作为函数的实参
 nxt . . . m个节点, m>=0 允许作为实参 指向它的是NULL指针 30

31 提高合法程序的门槛 方法1：给编程语言设计一个形状系统 排除不符合形状系统规定的程序，类似于类型检查 单链表指针h作为函数的实参
 nxt . . . m个节点, m>=0 允许作为实参 h D nxt . . . m个节点, m>=0 不允许作为实参 指向它的是dangling指针 31

32 提高合法程序的门槛 方法1：给编程语言设计一个形状系统 排除不符合形状系统规定的程序，类似于类型检查 单链表指针h作为函数的实参
 nxt . . . m个节点, m>=0 允许作为实参 h D nxt . . . m个节点, m>=0 不允许作为实参 h不允许作为实参 p允许作为实参 h  nxt . . . m个节点, m > 0 p n个节点, n >0 32

33 提高合法程序的门槛 方法1：给编程语言设计一个形状系统 排除不符合形状系统规定的程序，类似于类型检查 一个双向链表
h  r . . . l 一个双向链表 循环迭代依次把域l都赋值为NULL，然后当单链表用 h  r . . . l 形状系统拒绝这个程序，因为它偏离了声明的形状 33

34 提高合法程序的门槛 方法1：给编程语言设计一个形状系统 好处： 其他方法，例如 有助于自动推断有关形状的循环不变式 减轻自动定理证明器的负担
对有些类型的运算加以限制：有控制地使用指针算术运算和类型强制等 减少非结构化的控制流 34

35 用程序分析来支持程序验证 方法：先程序分析，后程序验证 用特定程序分析获取的信息来支持随后的程序验证 例如
{ p->data == 10 } p1->nxt->data = p->data + 5 { ? } 取决于p1->nxt是否等于p。若不知道，则需要考 虑两种情况，因而后条件是: p1->nxt != p  (p->data == 10  p1->nxt->data == 15)  p1->nxt == p  p->data == 15 若先指针分析，得到指针相等信息，则大大简化 35

36 用程序分析来支持程序验证 方法：先程序分析，后程序验证 用特定程序分析获取的信息来支持随后的程序验证 例如
{ p->data == 10 } p1->nxt->data = p->data + 5 { ? } h  nxt . . . m个节点, m>=0 p1 p n个节点, n>=0 36

37 用程序分析来支持程序验证 方法：先程序分析，后程序验证 用特定程序分析获取的信息来支持随后的程序验证 例如
{ p->data == 10 } p->data = p->data + 5 { ? } h  nxt . . . m个节点, m>=0 p1 p n个节点, n>=0 37

38 用程序分析来支持程序验证 方法：先程序分析，后程序验证 用特定程序分析获取的信息来支持随后的程序验证 例如
{ p->data == 10 } p->data = p->data + 5 {p->data == 15 } h  nxt . . . m个节点, m>=0 p1 p n个节点, n>=0 38

39 报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高程序验证能力的思路 一个程序验证系统原型演示
报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高程序验证能力的思路 程序员提供对验证有帮助的提示 提高合法程序的门槛 用程序分析获得的信息来支持程序验证 … … 一个程序验证系统原型演示 39

40 报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高程序验证能力的思路 一个程序验证系统原型演示
报 告 提 纲 一类基于逻辑推理的程序验证器的工作原理 面向实际程序验证需要解决的问题 提高程序验证能力的思路 一个程序验证系统原型演示 40

41 一个程序验证系统原型演示 特点 已经能验证 研究指针程序验证的一个成果，还在扩展完善中
为操作易变数据结构的指针程序设计了一种专用的形状图逻辑，设计了形状系统 先形状分析，后程序验证 已经能验证 演示：快速排序程序（数组程序）、二叉排序树的插入函数（递归），二叉排序树的删除函数（循环）和树堆(treap) 还有：伸展树(splay tree)，平衡树(AVL tree) 和 AA tree等 41

42 谢 谢 ！