Specification Language

This page describes the specification language we use for the verification of C product lines. For Java, we are using the AspectJ compiler and specifications defined as aspects. The AspectJ compiler compiles the systems to verify and weaves the aspects into resulting byte-code. Then, the byte-code is verified with the model-checking tool JavaPathfinder.

AutoFeature is the automata language we use to express temporal safety properties of features. We use the e-mail client case study as a running example. Specifications written in AutoFeature can be used to detect feature interactions using software model checking. AutoFeature automata are stored beside the feature’s source code in containment hierarchies. Automata may possess infinite states by using automata variables and can embed C language constructs.

As an example, the following automaton defines that only readable e-mails may be forwarded:

/* Forward/ForwardReadable.spec */

#include "Client.h"
#include "Email.h"

automaton ForwardReadable {

    before void forward(_:struct client*, msg:struct email*) {
        if (!isReadable(msg)) {
            fail;
        }
    }
}

The automaton is associated with feature Forward (it is dependent on the presence of the forward function, which is introduced by feature Forward). For purposes of verification, it adds additional statements at the beginning of function forward, which forwards messages to a set of predefined users. An automaton declaration may contain multiple before and after events to inject code into the functions it affects. This code —called event actions— can consist of valid C constructs and the additionally available fail statement, which is used to signal a violation of the specification. Event actions may access values passed as arguments to a function. In the example above, the second argument of function forward is available within the event action as msg of type struct email*. All parameter types of a function must be specified; argument values named _ are not made available in the event action scope.

The following example of a specification documents the usage of the after event and shows how automata can be used to add global declarations to the code base and how members can be added to structures.

/* Forward/ForwardPrivate.spec */

#include "Client.h"
#include "Email.h"

automaton ForwardPrivate {

    introduction {
        //add code to toplevel
        int myint;

        //add a member to the email structure
        shadow struct email {
            int received_encrypted;
        }
    }

    after struct email* msg = createEmail() {
        msg->received_encrypted = 0;
    }

    before void incoming(_:struct client*, msg:struct email*) {
        msg->received_encrypted = msg->isEncrypted;
    }

    before void forward(_:struct client*, msg:struct email*) {
        if (!msg->received_encrypted && msg->isEncrypted) {
            fail;
        }
    }
}

This specification can be used to verify that no e-mails that have been encrypted are ever forwarded in plain text to protect sensitive information from leaking. Therefore, the specification adds a field to e-mail messages using a shadow declaration. Introduction blocks can also contain global variables to be used in event actions. After the field is introduced, the sensitivity of a message needs to be tracked. Therefore, the automaton binds an action before function incoming that initializes the field with the sensitivity of the e-mail. If an e-mail is created manually, the field is also initialized properly. This example does not cope with the cloning of messages, which could be achieved by adding an additional action.

Weaving Process

AutoFeature builds on the AspeCt-oriented C Compiler ACC (http://aspectc.net) for weaving specifications onto specific variants or variability-encoded product lines. To this end, AutoFeature transforms the specifications to ACC aspects.

Fig.: Specification weaving