程序验证技术——霍尔逻辑

赶在四月的最后一天,发篇有点营养的文章。

如何确保程序的正确性?这是一个很难的问题,答案是暂时没有。

在本站的很多篇文章中,我都说过测试并不可靠。因为测试的目标就是尽可能找出错误,测试用例越完善,覆盖度越高,能够找出的错误就越多。但问题就在于,一般情况下,测试用例的覆盖度根本达不到100%。

造成这个问题的主要原因是测试的粒度不够细,起码是函数级的,当然这里并不排除很多路径本身就是没有意义的。从粒度考虑,更加完美的方式是语句级,出于对并发验证的考虑,这里的语句应该是原子语句,即不被打断。这种方式就是所谓的形式化验证技术,对代码进行验证,这种做法的粒度能够达到语句级,如果前后断言编写得当,验证工具自身没有bug,并且你相信数学是可靠的,那么便能证明程序的正确性。虽说有坚实的理论基础,但是要真正做成产品并广泛应用恐怕还有很长一段路要走。

本文讲述的就是形式化验证,这也是我所在实验室的研究方向,该领域属于PL,即Programming Language领域的研究方向之一。谨以此文作为知识回顾和巩固,不排除存在错误,如果各位觉得有不妥之处,欢迎留言指正。

0x00 本文的目标

作为程序验证的第一篇,本文并不会过度深入。本文的目标语言是C,并且不会涉及指针操作,即不包含任何数据结构。

并不是说不能做,只是就目前来看,霍尔逻辑并没有办法处理,等以后写分离逻辑了,再进行扩展。

0x01 C语言基本结构

我们以C语言为研究目标,理由是它相对简单,并且常用于安全攸关的领域,

专业一点的方式是使用BNF来进行阐述,但我并不专业,并且估计大家未必乐意看,索性就大概描述下吧。

C语言主要结构:

  • Seq: C1;C2 // 可以继续对C展开
  • Ass: id = expr;
  • Func: fun(args ...) { stats }
  • While: while(expr) { stats } // for和while差不多
  • If: if(expr) { stats } else { stats }

如下将就各个结构进行描述。

0x02 验证的形式

在C语言基本结构一节中,我们已经介绍了本文将会涉及的结构,那么如我们以何种形式进行验证呢?

答案是前后断言,大概形式如下:

Assertion: P
C
Assertion: Q

这里的P和Q即前断言和后断言,而<P, C, Q>三元组即所谓的霍尔三元组。

霍尔三元组具体有2类:

  1. {P}C{Q}
  2. [P]C[Q]

这里我们假设有一个函数,能够对断言进行计算,假定这个函数就是eval。

{P}C{Q}表达的含义是在P成立的前提下,即eval(P)=true,要么C永远不结束;要么C结束,并且符合后断言Q。

[P]C[Q]表达的含义是在P成立的前提下,即eval(P)=true,C一定结束,且符合后断言Q。

两者的具体区别即为是否要求C一定结束,如果结束,则都有P->Q,即P蕴含Q。

根据蕴含的定义,想要P->Q成立,即eval(P->Q)=true,只有两种情况:

  1. eval(P)=false
  2. eval(P)=true && eval(Q)=true

情况1即为命题天然成立,具体的语义是:我们并不想对相应的代码段进行验证,这么做的风险是很可能会丢失相关知识,导致下文的验证无法通过。

还有一种特殊的情况需要指明一下,{P}C{false},如果eval(P)=true,那么这种情况不一定为false,可以思考一下C不终止的情况。

对于霍尔逻辑的断言,这里有两种推导方式,分别是正向推导和逆向推导。

0x03 赋值语句的断言规则

对于如下语句和断言:

{x + 1 > 0}
x = x + 1;
{x > 0}

对于正向推导,我们可以根据赋值语句,将断言中的x + 1替换为x,记作[x/x+1]。如此我们便可得到新的断言{x > 0},而{x > 0} ==> {x > 0},即蕴含关系成立。

对于逆向推导,我们可以根据复制语句,讲断言中的x替换为x + 1,记作[x+1/x]。如此我们便可得到新的断言{x + 1 > 0},而{x + 1 > 0} ==> {x + 1 > 0},即蕴含关系成立。

由于正向推导和逆向推导大同小异,以下我们以正向推导为例。

0x04 选择语句

对于如下语句和断言:

{true}
if(x > 0)
  x = x + 1;
else
  x = 1 - x;
{x > 0}

对于if-else的2条分支,我们需要对执行路径进行分离,在第一步简单的推导后,我们会将符合2条分支的分支条件加入到断言中,新的断言将会变成如下2种形式:

{true /\ x > 0}
x = x + 1;
{x > 0}
{true /\ x <= 0}
x = 1 - x;
{x > 0}

继续推导,我们将会得到如下2条蕴含式:

{true /\ x > 1} ==> {x > 0} //显然,这是成立的
{true /\ x >= 1} ==> {x > 0} //显然,这也是成立的

0x05 循环语句

循环语句和条件语句类似,只不过它会反复执行罢了,作为验证,我们肯定是不能模拟执行的,我们需要一些特殊的断言,使得验证器可以在扫过一遍循环体后,就确定是否符合断言。

这个特殊的断言就是loop invariant,即循环不变式,所谓循环不变式,就是从循环开始执行起,到循环结束为止,一直成立的断言,对于复杂的循环,尤其是带有嵌套的循环,给出一个恰当的循环不变式,是一件极其困难的事情,需要经过一定的训练才能完成。

我们可以先给出抽象描述,如下:

{P} while B { C } {Q}

它可以展开成如下2条:

  1. {i /\ B} C {i}
  2. {i} while B { C } {i /\ !B}

我们只需要证明{P} ==> {i}并且{i /\ !B} ==> {Q}即可,至于这么做的理论依据和证明,请看相关论文,这不属于本文范畴。

下面我们给出一个例子:

sum = 0;
i = 6;
{sum == 0 /\ i == 6}
while(i > 0) {
  sum += i;
  --i;
}
{sum == 21}

这里的循环不变式为{sum + i*(i+1)/2 == 21}。

我们可以看看如下证明过程:

sum = 0;
i = 6;
{sum == 0 /\ i == 6} ==>
{sum + i*(i+1)/2 == 21}
while(i > 0) {
  {sum + i*(i+1)/2 == 21 /\ i > 0}
  sum += i;
  {sum + (i-1+1)*(i-1)/2 == 21 /\ i > 0}
  --i;
  {sum + i*(i+1)/2 == 21 /\ i > 0} ==>
  {sum + i*(i+1)/2 == 21}
}
{sum == 21} ==>
{sum + i*(i+1)/2 == 21 /\ i == 0}

0x06 序列语句

序列语句相对简单,它本身就是其它语句的整合。如下:

{true}
x = 0;
{x == 0}
x++;
{x == 1} ==>
{x == 1}

对于其它语句序列,也是类似。

0x07 函数调用语句

函数调用也有前后断言,函数内部其实就是序列语句,可以用归纳定义来解决这一切。

只不过在添加函数的前后断言时,有点不同,它是添加在函数声明处的,例如有如下名为foo的函数声明:

{Pfoo}
int foo(int c) {...}
{Qfoo}

在实际调用处,需要证明{P} ==> {Pfoo}和{Qfoo} ==> {Q}。这个并没有什么特别之处,这里不在赘述。

0xFF 总结

假设我们已经解决了指针的问题,易变数据结构的问题,形式化验证技术还是很有可行性的。

阅读完本文后,大家应该也能感觉到,形式化验证和传统的测试是不太一样的,具体体现在它的逻辑性更加强,要求更加严格,甚至到了死板的地步,但想要让机器证明,死板只是前提罢了,越是死板严格,就越有说服力。除此之外,我们完全不需要通过执行程序来完成验证。

当然,凡事都有两面性,验证技术的学习成本很高,这一点从循环不变式的编写就能看出,需要一定的技巧。

已有 3 条评论
  1. binks binks

    您好,我是一名大四学生,研究生的方向也是PL。我现在处于基础知识的学习阶段,但发现Hoare逻辑和分离逻辑的相关资料都较少。我想向您请教一下这方面的资料,您方便与我联系一下吗?

    1. binks binks

      邮箱是615902477@qq.com

      1. Software Foundation,以及相关论文

说两句: