zoukankan      html  css  js  c++  java
  • CBMC使用注意事项


    最近在使用CBMC来分析一系列的C文件,在使用过程中碰到很多微妙的问题,参数选取的好坏直接影响了最终分析结果的完整性和准确性。下面讲解一下个人的使用经验,仅供参考。

    我们先考虑单文件的情况

    下面做的所有实验是针对我自己编写的一个简单的充满BugC程序来进行的。该文件内容如下:

    #include <string.h>

    int singleFunc(int j)

    {

    int i;

    int a[5]={1,2,3,4,5};

    for(i=0;i<j;i++)

    {

    a[i]=0; //Upper Bound overflow

    }

    }

    void twoSeparate(int j,int k)

    {

    short i=-32765;

    short m=32765;

    short low=i-j; //Arithmetic overflow when j>=2

    short upper=m+k; //Arithmetic overflow when j>=2

    }

    void twoSeparateString()

    {

    int i=0;

    char a[5],b[3];

    char *c=a;

    char *d=b;

    //int s=-257330;

    //int low=s-i;

    twoSeparate(3,100);

    strcpy(d,c); //Deference error

    //strcpy(b,a);

    }

    void mainSubfunc(int i)

    {

    int j=100;

    int k=10;

    j=j/i; //Divison by zero,But won't happen since input i will never be zero

    int m=0;

    k=k/m; //Division by zero

    }

    void main()

    {

    int i=0,j=0;

    int a[2]={1,2};

    while(1)

    {

    a[i]=3; //Upper Bound Overflow

    i++;

    }

    mainSubfunc(j+1);

    }

    该文件中共包含了5个函数,包括1个独立函数singleFunc2个与main不相关但彼此间存在调用关系的函数twoSeparatetwoSeparateString,以及main和它所调用的一个函数mainSubfunc构成。

    下面是实验流程:

    一、

    1cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c –show-claims

    将产生15个声明,并且对twoSeparateString 不会存在任何声明,。

    2cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c --show-claims --function twoSeparateString 将产生额外7个与twoSeparateString相关的声明。

    3cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c --show-claims --function mainSubfunc

    将产生15个声明,并且对twoSeparateString 不会存在任何声明

    4)在函数twoSeparateString中添加额外的一段可疑代码,如

    int s=-257330;

    int low=s-i;

    再运行cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c –show-claims 将产生 14个声明,其中多的两个是在twoSeparateString中,并是与low=s-i相关的算术溢出声明。

    综上可得,--function的指定一般不会影响可疑声明的生成,但如果函数中存在strcpy等库函数操作的时候,这些函数中是不会生成与strcpy等操作相关的可疑声明的,而不影响该函数中其他可疑声明的生成。

    1cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c --function twoSeparate 会在函数twoSeparatelow=i-j这一行检测出下溢出错误,并停止。所以需要使用claim来指定,使其能检测多个错误。

    2cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c --function twoSeparate –claim twoSeparate.4 指定为twoSeparate.2可以检测出low=i-j的下溢出(其实是伪错误,因为函数twoSeparate是由twoSeparateString调用的,传入的j值不会使low下溢出。当将twoSeparateString作为入口函数的话,即cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c --function twoSeparateString –claim twoSeparate.2 –unwind 20会排除这个错误),指定为twoSeparate.4可以检测出upper=m+k;的上溢出。

    3cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c --function twoSeparate --claim main.

    2 不会验证main中的声明,因为twoSeparate中没直接或间接调用main

    综上可得,CBMC只会检验—function指定的函数,及该函数直接或间接调用的函数中的相关声明

    三、

    1cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c --unwind 20

    循环展开20次,会检测到maina[i]的数组越界错误。

    2cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c --unwind 20 --claim mainSubfunc.2

    不会检测到任何错误,而实际上mainSubfunc.2指明了一个除0错误。

    3cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.c --function mainSubfunc

    会检测到除0错误

    综上可得,如果所检测的函数中包含while等循环,必须指定unwind次数,否则不会终止。而且对于那些位于while循环之后的那些声明是不会被检测到的。

    四、

    cbmc --bounds-check --pointer-check --overflow-check --div-by-zero-check --nan-check usageTest.gb --function mainSubfunc --unwind 20 --claim mainSubfunc.2

    如果先用goto-cc将文件进行处理,生成.gb文件。那么--function等参数会失效,也就是说系统会将main设为入口函数并且不可改变,所以它也就只能检验到main以及被main所直接和间接调用的函数中存在的声明。这会导致很大一部分声明都检测不到,所以尽量不要使用goto-cc进行预先处理。

    下面我们先考虑多文件的情况

    我采用了下面两个文件

    unwind.c

    void main()

    {

    int i=0;

    int a[2]={1,2};

    subfunc(i+1); //Location ditermines different results

    while(1)

    {

    a[i]=3;

    i++;

    }

    }

    subfunc.c

    void subfunc(int i)

    {

    int j=100;

    int k=10;

    j=j/i;

    int m=0;

    k=k/m;

    }

    下面进行实验,先用goto-cc编译成一个文件做法是可以的,不过正如上面所说这样做会导致一部分声明检验不到。当然针对上面的代码是都可以检测到的,但如果将subfunc(i+1)放到while循环之后就检测不到subfunc中的声明了,正如上面的步骤三中说的。

    正如前面所讲最好还是使用源文件作为输入,其实只要将所有相关的检测文件列到参数中就可以了

    cbmc --bounds-check --div-by-zero-check unwind.c subfunc.c --unwind 20 --claim subfunc.2

    cbmc --bounds-check --div-by-zero-check unwind.c subfunc.c --claim main.2 --unwind 20

  • 相关阅读:
    python同时继承多个类且方法相同
    django扩展用户继承AbstractUser
    python中单下划线和双下划线
    django扩展用户一对一关联
    django拓展用户proxy代理
    django 内置User对象基本使用
    selenium+pthon之二----了解浏览器的相关操作方法
    最近很燥,决心沉下心来学习!
    selenium+pthon之一----环境搭建与脚本实例
    Fiddler入门三
  • 原文地址:https://www.cnblogs.com/zztian/p/2397460.html
Copyright © 2011-2022 走看看