Skip to content

Function contract tutorial

Jump to bottom
Mark Tuttle edited this page Oct 5, 2021 · 81 revisions

This CBMC tutorial will

  • introduce you to function contracts, and
  • give you the chance to write, check, and use function contracts on real code.

We assumes that you have some familiarity with CBMC. We assume that

  • you have run CBMC before, and
  • you have written a simple proof harness to prove the memory safety of a simple function.

Outline:

Introduction

This tutorial shows how to use function contracts instead of function stubs in a proof. We all know that using CBMC to prove the memory safety of a large function can push CBMC to the limit of its capacity. We often stub out out some of the low-level functions used by the large function to simplify the problem for CBMC. If the function interacts with the network, for example, we might stub out the send and receive functions in the network interface: We stub out send to return an arbitrary success or failure return value of the appropriate type, and stub out receive to return an arbitrary network packet of the appropriate type.

Using function stubs in a proof often results in a perfectly acceptable proof. But we must tread carefully if the functions being stubbed out have side effects that can affect memory safety. For example, suppose the send and receive functions manipulate a queue of pending packets. Then the externally observable behavior of the send and receive functions is more than just the return values modeled by the stubs.

This tutorial shows how to replace stubs in a proof with function contracts. A function contract is --- among other things --- a description of a function's externally observable behavior. In particular, it describes how a function can change the memory (outside of the function's local memory) and what values a function can return. We can prove that a function satisfies its contract, and then use the contract in place of the function in the proofs of other functions.

Install the tools

Let's begin by installing the latest versions of cbmc and cbmc-viewer. What follows are instructions taken from our tool installation page.

Install tool dependencies

On MacOS, run

brew install python3 ctags ninja gnuplot graphviz
python3 -m pip install --upgrade jinja2 voluptuous

On Ubuntu, run

sudo apt-get install python3 python3-pip ctags ninja-build gnuplot graphviz
python3 -m pip install --upgrade jinja2 voluptuous

Replace python3 with sudo python3 if you run into permission problems.

Install cbmc

On MacOS, run

brew install cbmc

On Ubuntu, follow the instructions on the CBMC release page or run

UBUNTU=$(lsb_release --short --release)
CBMC_REL="https://api.github.com/repos/diffblue/cbmc/releases/latest"
CBMC_URL=$(curl --silent ${CBMC_REL} | grep browser_download_url | grep ubuntu-${UBUNTU} | sed 's/.*"\(.*\)"/\1/')
curl --silent -LO ${CBMC_URL}
sudo dpkg -i $(basename ${CBMC_URL})

Install cbmc-viewer

Follow the instructions on the CBMC Viewer release page or run

VIEWER_REL="https://api.github.com/repos/awslabs/aws-viewer-for-cbmc/releases/latest"
VIEWER_URL=$(curl --silent ${VIEWER_REL} | grep browser_download_url | sed 's/.*"\(.*\)"/\1/')
curl --silent -LO ${VIEWER_URL}
python3 -m pip install $(basename ${VIEWER_URL})

Replace python3 with sudo python3 if you run into permission problems.

Clone the s2n repository

In this tutorial, we will use the s2n-tls repository for our examples. Clone the repository with

git clone https://github.com/aws/s2n-tls.git
cd s2n-tls
git submodule update --init --checkout --recursive

Understanding the problem

In the s2n-tls repository, the function s2n_stuffer_certificate_from_pem is an example of a large function that calls another function s2n_stuffer_skip_to_char indirectly via other functions. The current memory safety proof for s2n_stuffer_certificate_from_pem is in the directory tests/cbmc/proofs/s2n_stuffer_certificate_from_pem. If we look at the Makefile for this memory safety proof, we notice two things.

First, the proof depends on a bound on the maximum size of the blob containing the certificate:

# From tests/cbmc/proofs/s2n_stuffer_certificate_from_pem/Makefile

MAX_BLOB_SIZE = 10
DEFINES += -DMAX_BLOB_SIZE=$(MAX_BLOB_SIZE)

Second, the proof depends on stubs for several functions including the function s2n_stuffer_skip_to_char:

# From tests/cbmc/proofs/s2n_stuffer_certificate_from_pem/Makefile

PROOF_SOURCES += $(PROOF_STUB)/s2n_stuffer_read_expected_str.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_stuffer_skip_expected_char.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_stuffer_skip_to_char.c

If we look at this stub for s2n_stuffer_skip_to_char

/* From tests/cbmc/stubs/s2n_stuffer_skip_to_char.c */

int s2n_stuffer_skip_to_char(struct s2n_stuffer *stuffer, const char target)
{
    POSIX_PRECONDITION(s2n_stuffer_validate(stuffer));
    return nondet_bool() ? S2N_SUCCESS : S2N_FAILURE;
}

we see that it checks that the stuffer is well-formed and returns arbitrarily either success or failure. You can't get much stubbier than that! If you look at the implementation of s2n_stuffer_skip_to_char

/* From stuffer/s2n_stuffer_text.c */

int s2n_stuffer_skip_to_char(struct s2n_stuffer *stuffer, const char target)
{
    POSIX_PRECONDITION(s2n_stuffer_validate(stuffer));
    while (s2n_stuffer_data_available(stuffer) > 0) {
        if (stuffer->blob.data[stuffer->read_cursor] == target) {
            break;
        }
        stuffer->read_cursor += 1;
    }
    POSIX_POSTCONDITION(s2n_stuffer_validate(stuffer));
    return S2N_SUCCESS;
}

you see that the function checks that the stuffer is well-formed at the top and the bottom, but it also advances the stuffer's read cursor. That's something not modeled by the stub. Let's write a function contract for s2n_stuffer_skip_to_char, and use this function contract in place of the stub in the proof of s2n_stuffer_certificate_from_pem.

Function contracts

A function contract has three components

  • requires clauses that describe preconditions that are required to be true when the function is called (perhaps the function must be called with pointers that are nonnull) written __CPROVER_requires(...),
  • ensures clauses that describe postconditions and are certain to be true when the function returns (perhaps the return value is either NULL or points to a space in a string) written __CPROVER_ensures(...), and
  • assigns clauses the describe the write set that is the set of memory locations the function is allowed to modify (and only memory locations in the write set are modified by the function) written __CPROVER_assigns(...).

When writing ensures clauses, it is convenient to be able to refer to

  • the return value of the function written __CPROVER_return_value, and
  • the old value of a variable x written __CPROVER_old(x), making it easy to refer to the value of the variable immediately before and after the function invocation.

When writing assigns clauses, it is convenient to be able to refer to

  • not just a pointer value ptr but the entire object that ptr points two written __CPROVER_POINTER_OBJECT(ptr)

CBMC will combine multiple requires clauses in a function contract into a single requires clause. The same is true for ensures and assigns clauses. Feel free to break up your requires, ensures, and assigns clauses into small, easy-to-read statements.

CBMC provides a collection of __CPROVER intrinsic functions to refer to these concepts, as mentioned above, but the s2n repository uses its own names for some of them via a set of preprocessor macros and we will use these names in this tutorial.

/* From utils/s2n_ensure.h */

#define CONTRACT_REQUIRES(...)   __CPROVER_requires(__VA_ARGS__)
#define CONTRACT_ENSURES(...)    __CPROVER_ensures(__VA_ARGS__)
#define CONTRACT_ASSIGNS(...)    __CPROVER_assigns(__VA_ARGS__)
#define CONTRACT_RETURN_VALUE   (__CPROVER_return_value)

Writing function contracts

Let's begin by writing a function contract for s2n_stuffer_skip_to_char:

/* From stuffer/s2n_stuffer_text.c */

int s2n_stuffer_skip_to_char(struct s2n_stuffer *stuffer, const char target)
{
    POSIX_PRECONDITION(s2n_stuffer_validate(stuffer));
    while (s2n_stuffer_data_available(stuffer) > 0) {
        if (stuffer->blob.data[stuffer->read_cursor] == target) {
            break;
        }
        stuffer->read_cursor += 1;
    }
    POSIX_POSTCONDITION(s2n_stuffer_validate(stuffer));
    return S2N_SUCCESS;
}

The function checks that the stuffer is valid at the start and end of the function, so validity is a natural thing to check in the function's requires and ensures clauses. The function also advances the stuffer's read cursor, so the read cursor is a natural thing to include in the function's assigns clause. We annotate a function with its function contract by including the contract between the function declaration and the opening brace. Our function contract for this function is

int s2n_stuffer_skip_to_char(struct s2n_stuffer *stuffer, const char target)
  CONTRACT_REQUIRES(s2n_result_is_ok(s2n_stuffer_validate(stuffer)))
  CONTRACT_ENSURES(s2n_result_is_ok(s2n_stuffer_validate(stuffer)))
  CONTRACT_ASSIGNS(stuffer->read_cursor)
{
 ...
}

Notice that we wrap s2n_result_is_ok around the result of s2n_stuffer_validate to interpret the validation result (a struct) as a boolean value.

Let's pause a moment to modify the source code to include this function contract:

For comparison, here is a copy of the modified source file.

Using function contracts

Now lets use the function contract for s2n_stuffer_skip_to_char in the memory safety of s2n_stuffer_certificate_from_pem. That is, let's replace the stub with the function contract in the proof.

The original memory safety proof for s2n_stuffer_certificate_from_pem is in the proof directory tests/cbmc/proofs/s2n_stuffer_certificate_from_pem. In order to use the function contract for s2n_stuffer_skip_to_char, we need to build the goto binary as usual linking together the proof harness and the source code. But we also need to instrument the goto binary to use the function contract in place of the function every time the function is called. From the command line, we instrument the code with

goto-instrument --replace-call-with-contract s2n_stuffer_skip_to_char ...

The starter kit will do this for us, however, if we set a Makefile variable to the list of function contracts to use

USE_FUNCTION_CONTRACTS += s2n_stuffer_skip_to_char

Let's pause a moment to prove memory safety using the function contract:

  • Change directory to the proof directory tests/cbmc/proofs/s2n_stuffer_certificate_from_pem.
  • Edit the Makefile.
    • Comment out the line that pulls in the stub for s2n_stuffer_skip_to_char: 
      PROOF_SOURCES += $(PROOF_STUB)/s2n_stuffer_skip_to_char.c
    • Add the line that pulls in the function contract for s2n_stuffer_skip_to_char: 
      USE_FUNCTION_CONTRACTS += s2n_stuffer_skip_to_char
  • Run make report to check the proof with cbmc.
  • Run open report/html/index.html to see the report produced by cbmc-viewer.

For comparison, here is a copy of the modified Makefile. We have some debugging advice if you encounter problems.

Checking function contracts

Now let's check that s2n_stuffer_skip_to_char satisfies its function contract. To do this, we need to

  • write a proof harness for the function, and
  • write a Makefile for the proof.

The proof harness

The original memory safety proof for s2n_stuffer_skip_to_char is in the proof directory tests/cbmc/proofs/s2n_stuffer_skip_to_char. The original proof harness is s2n_stuffer_skip_to_char_harness.c:

/* From tests/cbmc/proofs/s2n_stuffer_skip_to_char/s2n_stuffer_skip_to_char_harness.c */

void s2n_stuffer_skip_to_char_harness()
{
    /* Non-deterministic inputs. */
    struct s2n_stuffer *stuffer = cbmc_allocate_s2n_stuffer();
    __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(stuffer)));
    __CPROVER_assume(s2n_blob_is_bounded(&stuffer->blob, BLOB_SIZE));
    const char target;

    /* Save previous state from stuffer. */
    struct s2n_stuffer            old_stuffer = *stuffer;
    struct store_byte_from_buffer old_byte_from_stuffer;
    save_byte_from_blob(&stuffer->blob, &old_byte_from_stuffer);

    /* Operation under verification. */
    if (s2n_stuffer_skip_to_char(stuffer, target) == S2N_SUCCESS) {
        assert(S2N_IMPLIES(s2n_stuffer_data_available(&old_stuffer) == 0, 
                           stuffer->read_cursor == old_stuffer.read_cursor));
        if (s2n_stuffer_data_available(stuffer) > 0) {
            assert(stuffer->blob.data[ stuffer->read_cursor ] == target);
            size_t idx;
            __CPROVER_assume(idx >= old_stuffer.read_cursor && idx < stuffer->read_cursor);
            assert(stuffer->blob.data[ idx ] != target);
        }
    }
    assert_stuffer_immutable_fields_after_read(stuffer, &old_stuffer, &old_byte_from_stuffer);
    assert(s2n_result_is_ok(s2n_stuffer_validate(stuffer)));
}

That's a lot to look at, but notice that

  • it begins by allocating a stuffer with unconstrained values, but with blob size bounded by BLOB_SIZE,
  • it assumes the stuffer is valid at the start of the harness just like the function contract,
  • it asserts that the stuffer is valid at the end of the harness just like the function contract,
  • it calls the function, and
  • it defines and checks a lot of other stuff that we can ignore in this proof.

All we want to do is check that s2n_stuffer_skip_to_char satisfies its function contract, so all the proof harness needs to do is allocate the stuffer and call the function:

void s2n_stuffer_skip_to_char_harness()
{
    /* Non-deterministic inputs. */
    struct s2n_stuffer *stuffer = cbmc_allocate_s2n_stuffer();
    const char target;

    /* Assume bound on blob size */
    __CPROVER_assume(
        S2N_IMPLIES(stuffer != NULL, stuffer->blob.size <= MAX_BLOB_SIZE));

    /* Invoke the function */
    s2n_stuffer_skip_to_char(stuffer, target);
}

The Makefile

To prove that the function satisfies its contract, we have to compile our proof harness and the source code into a goto binary as usual, but then we have to instrument the goto binary to check the function contract. From the command line, we instrument the code with

goto-instrument --enforce-contract s2n_stuffer_skip_to_char ...

The starter kit will do this for us, however, if we set a Makefile variable to the list of function contracts to check

CHECK_FUNCTION_CONTRACTS += s2n_stuffer_skip_to_char

One issue is that checking contracts changes the names of loops in the function being checked. You will have to change the loop name from s2n_stuffer_skip_to_char.1 to __CPROVER_contracts_original_s2n_stuffer_skip_to_char.1 in the unwinding statement in the Makefile.

Running cbmc

Let's pause now to check that the function satisfies its contract.

  • Change to the proof directory tests/cbmc/proofs/s2n_stuffer_skip_to_char.
  • Edit the proof harness s2n_stuffer_skip_to_char_harness.c and replace the function s2n_stuffer_skip_to_char_harness there with the short s2n_stuffer_skip_to_char_harness given above.
  • Edit the Makefile to add the line CHECK_FUNCTION_CONTRACTS += s2n_stuffer_skip_to_char anywhere before the final line sourcing Makefile.common.
  • Run make report to check the proof with cbmc
  • Run open report/html/index.html to see the report produced by cbmc-viewer

For comparison, here is a copy of the modified proof harness and modified Makefile. We have some debugging advice if you encounter problems.

Let the hackathon begin

Now you do it!

We have three high level functions all in stuffer/s2n_stuffer_pem.c

that call three low level functions all in stuffer/s2n_stuffer_text.c

What we have done is choose one high-level function and one low-level function and

  • written a function contract for the low-level function,
  • used the contract to prove memory safety of the high-level function, and
  • check that the low level function satisfies the contract.

Now you do it! Choose a different combination of high-level and low-level functions and do the same thing.

If you get stuck, the answers are in the contracts-testing branch of this private repository

Debugging advice

Using the litani report

The report produced by litani (the build system invoked by make report that runs cbmc and cbmc-viewer) is a valuable source of information. When make report is done, you will see a line that looks like

Report was rendered at file:///var/folders/bf/ylpsb9dx7fd59fx48bh2c1h00000gs/T/litani/runs/latest/html/index.html

Open that file in a browser with

open file:///var/folders/bf/ylpsb9dx7fd59fx48bh2c1h00000gs/T/litani/runs/latest/html/index.html

and you can see the report produced by litani. In particular, you will see a line for the proof of s2n_stuffer_certificate_from_pem like Litani status line

  • If you click on the blue bar on the far right under the column marked "Report," you will see a second copy of the report produced by cbmc-viewer.
  • If you click on the blue icon on the far left intended to denote a "pipeline," you can see all of the logs produced by the various stages of running make report. In particular, if you encounter any errors (like some step of building the goto binary fails), you can see the list of pipeline stages like Litani pipeline failure.
    The failing stage is marked with a red "x", and if you click on the name of a failing pipeline stage, you can see the log for the stage and debug what went wrong.

Developing over ssh

If you are doing your work on Ubuntu over ssh from your laptop, you may have difficulty viewing the files mentioned here in a browser. One low-tech solution is to use rsync to copy the files to your laptop and open them in a browser on your laptop:

cd /tmp
rsync -r -L ubuntu:/var/folders/bf/ylpsb9dx7fd59fx48bh2c1h00000gs/T/litani/runs/latest/html .
open html/index.html

Documentation

For more information, see our documentation:

The work on requires, ensures, and assigns clauses are fairly mature. The other work is still a work in progress. Please contact us if you find yourself needing this functionality.

Clone this wiki locally