Frama-C predicates

06 Mar 2020 - tsp

As I’ve encountered that many of my friends who also use Frama-C for formal verification of their ANSI C programs really do not know or understand the concept of predicate this is just a short summary. Basically one could imagine a predicate to be a summary of various logical statements that can either hold true or false, i.e. it’s a boolean valued mathematical function that maps to $P : X \to { true, false }$. One can use these predicates to modularize ACSL specifications. They work somewhat like functions with the addition of labels. The most basic predicate is just a collection of simple boolean statements.

Note that this blog post only contains a really basic description of predecates that should be sufficient for most usecases.

For a longer description about Frama-C’s role in formal verification one can look at my previous articles that demonstrated how to do basic verification for simple C programs using the GUI as well as verification of AVR microcontroller code. Predicates are of course also of use in this context.

For a more in-depth introduction one might refer to many other sources like the following:

Simple example

Let’s say we have a structure that wraps an arbitrary number of integer values and we want to define a predicate that specified if this structure is valid or not:

struct bagOfIntegers {
    unsigned long int dwIntegerCount;
    unsigned long int values[];
};

Then one can specify the following predicate to verify that a reference to a bagOfIntegers is valid:

/*@
    predicate bagOfIntegersValid(struct bagOfIntegers *bag) =
        \valid(bag)
        && \valid(&(bag->dwIntegerCount))
        && (bag->dwIntegerCount > 0)
        && \valid(&(bag->values[0..bag->dwIntegerCount-1]));
*/

Now one can annotate set and get functions for this bag using the predicate:

/*@
    requires bagOfIntegersValid(bag) || (bag == \null);
    requires dwIndex >= 0;

    behavior invalidBag:
        assumes (bag == \null);

        assigns \nothing;

        ensures \result == -1;

    behavior invalidIndex:
        assumes bagOfIntegersValid(bag);
        assumes (dwIndex >= bag->dwIntegerCount);

        assigns \nothing;

        ensures bagOfIntegersValid(bag);
        ensures \result == -2;

    behavior validIndex:
        assumes bagOfIntegersValid(bag);
        assumes (dwIndex < bag->dwIntegerCount);

        assigns bag->values[dwIndex];

        ensures bag->values[dwIndex] == value;
        ensures bagOfIntegersValid(bag);
        ensures \result == 0;
*/
int bagOfIntegers_SetEntry(
    struct bagOfIntegers* bag,
    unsigned long int dwIndex,
    unsigned long int value
) {
    if(bag == NULL) {
        return -1;
    }

    if(dwIndex >= bag->dwIntegerCount) {
        return -2;
    }

    bag->values[dwIndex] = value;
    return 0;
}

One might also use such predicates to specify the result of an function, for example an sort function might also specify the sorted predicate:

/*@
    predicate bagOfIntegersSortedASC(struct bagOfIntegers *bag) =
        bagOfIntegersValid(bag)
        && (
            \forall int m; 0 <= m < bag->dwIntegerCount-1
            ==> bag->values[m] < bag->values[m+1]
        ) || (bag->dwIntegerCount < 2);
*/

Labels

Labels are capable of referencing certain positions inside one’s code. They can be used to track memory state. One can specify labels in front of predicate parameters. For example when one wants to specify that variables are swapped after a given set of statements:

/*@
    predicate swappedIntData{L1,L2}(int* data, int len, int i, int j) =
        (i >= 0) && (j >= 0)
        && (i < len) && (j < len)
        && (\at(data[i], L1) == \at(data[j], L2))
        && (\at(data[j], L1) == \at(data[i], L2))
        && (
            \forall int k; (0 <= k < len) && (k != i) && (k != j)
            ==> \at(data[k], L1) == \at(data[k], L2)
        );
*/

One can simply annotate an integer array swapping function:

/*@
    requires \valid(lpData);
    requires (arraySize >= 0);
    requires \valid(&lpData[0..arraySize]);
    requires (i >= 0) && (j >= 0);
    requires (i < arraySize) && (j < arraySize);

    ensures swappedIntData{Old, Here}(lpData, arraySize, i, j);
*/
void intSwap(int* lpData, int arraySize, int i, int j) {
    int temp;

    temp = lpData[i];
    lpData[i] = lpData[j];
    lpData[j] = temp;
}

As usual any label that’s declared in the code (using the usual C labelname: syntax as known as from goto and switch targets) can be used instead of special labels like:

This article is tagged: Programming, Math, Formal, Security, Frama C


Dipl.-Ing. Thomas Spielauer, Wien (webcomplains389t48957@tspi.at)

This webpage is also available via TOR at http://jugujbrirx3irwyx.onion/

Valid HTML 4.01 Strict Powered by FreeBSD IPv6 support