SATABS Homepage Predicate Abstaction with SAT for ANSI-C

Loop Detection for SATABS

Conventional predicate abstraction suffers from the fact that it requires one predicate for each iteration of a loop construct in the program. In contrast to that, SATABS can extract looping counterexamples from the abstract model, and parameterizes the simulation instance in the number of loop iterations.

 

Example: Buffer Overflow in AEON 0.2a

  • aeon-0.2a.tar.gz
    This file contains the original sources of Aeon 0.2a, a simple SMTP mail delivery program, which was developed by Piotr Benetkiewicz.
  • aeon_satabs.tgz
    This file contains stubs and a patch for the original Aeon sources.

 

Requirements

SATABS needs BOPPO for detecting loops.

 

Instructions

Note that a detailed description of this example is provided in the SATABS user manual. If you encounter problems when following the brief instructions in this section please refer to the manual.
  1. Download the tarballs (see above) and unpack the files.
  2. The file aeon_satabs.tgz contains a patch (aeon.diff) which has to be applied to the original Aeon sources in aeon-0.2a.tar.gz. Call

    patch -p0 < aeon.diff

    in the parent directory of aeon-0.2a/.

    Alternatively, if the patch tool is not installed on your computer, change #define MAX_LEN 512 in aeon-0.2a/aeon.h to #define MAX_LEN 50.

    This is a limitation due to a performance issue of the SATABS simulator and will be removed soon.
  3. We assume you have unpacked the original Aeon sources to the directory aeon-0.2a/, the include files to include/ and stub.c to the directory stubs/.
  4. Run

    satabs --show-claims --model-checker boppo --loop-detection -I include/ aeon-0.2a/aeon.c aeon-0.2a/base64.c aeon-0.2a/lib_aeon.c stubs/stubs.c

    Ignore the warnings that the bodies of several functions are missing. All relevant function bodies are supplied in stubs.c.
  5. Inspect following claim:
    Claim 5:
    file stubs/stubs.c line 8 column 10 function c::strcpy
    dereference failure: array `home' upper bound
    !(dest == &home[0]) || !(i >= 50)
    This claim refers to the call

    strcpy(home, getenv("HOME")); /* get home path */

    in the function getConfig in lib_aeon.c (line 19). This function is called at the beginning of the main function of Aeon. The claim states that the upper bound of the array home (which is of size MAX_LEN) must not be violated.
  6. Try to verify the claim by calling

    satabs --claim 5 --model-checker boppo --loop-detection -I include/ aeon-0.2a/aeon.c aeon-0.2a/base64.c aeon-0.2a/lib_aeon.c stubs/stubs.c

    After a while, SATABS will provide a counterexample trace that illustrates how the call to strcpy in combination with getenv can result in a buffer overflow. This buffer overflow is also listed by NIST/US-CERT (Vulnerability Summary CVE-2005-1019).
The implementation of getenv in stubs.c demonstrates how (potentially malific) external input can be modeled using non-determinism (refer to the manual for a detailed explanation).