A verified implementation of a small subset of the C standard library
C Shell
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
include/verlibc
src/string
.gitattributes
.gitignore
NOTICE
README.markdown
build.bat

README.markdown

This project is a proof-of-concept, machine-verified implementation of a subset of the C standard library. The idea is to annotate standard C library functions with VCC annotations which allow VCC to verify not only implementations of functions, but that standard library functions are used correctly in programs as well.

For example, consider the declaration of the strlen function in verlibc:

_(pure) size_t strlen(const char *str _(ghost size_t nul_lim))
    _(requires \thread_local_array(str, nul_lim + 1))
    _(requires \exists size_t i; i <= nul_lim && str[i] == '\0')
    _(reads \array_range(str, nul_lim + 1))
    _(ensures \result <= nul_lim)
    _(ensures str[\result] == '\0' && \forall size_t j; j < \result ==> str[j] != '\0')
    ;

requires annotations are preconditions that must be true in order for the function to be used. ensures annotations are post-conditions concerning the result. Here, the strlen preconditions require that there must exist an offset in str of a NUL character and that all characters from *str through *(str + nul_lim) must be valid to access. The postconditions ensure that the result is less than or equal to nul_lim, str[\result] is a NUL character, and none of the preceding characters are NUL characters.

Using verlibc, VCC is able to verify the assertion in this code and that strlen is used correctly:

const char str[13] = { 'h', 'e', 'l', 'l', 'o', '\0', 'w', 'o', 'r', 'l', 'd', '!', '\0' };
size_t len = strlen(str _(ghost 12));

_(assert len == 5)

Project Goals

The principal goal of this project is to add a consistent set of VCC annotations to C standard library functions. In pursuit of this goal, annotated C functions are given implementations and are tested with simple "unit tests".

The purpose of implementations is to make sure that the model of a standard library function (as specified by the annotations) is neither too strong nor too weak, and that the annotations are correctly specified. verlibc implementations thus tend to be simple rather than optimal because it is easier to check not only the current set of annotations, but proposed changes as well.

The purpose of the "unit tests" is to make sure that the annotations are actually usable in verifying functions that call the corresponding standard library functions. They aren't unit tests in the traditional sense because the implementations are verified by VCC, so there is no need to exhaustively check every case for errors.

Contributing

There are several ways to contribute! Here is a list of ideas:

  1. Annotate a C standard library function.

  2. Check the annotations for errors or omitted pre- or postconditions.

  3. Simplify existing annotations.

  4. Use VCC and verlibc annotations to verify C software that utilizes the standard library.

  5. Download a source distribution of an open source implementation of the C standard library, replace its implementations of standard library functions with verlibc's implementations, and run the project's unit test suite. This helps to verify that VCC itself is correct.

  6. Write "non-technical", natural language descriptions of the lengthier mathematical assertions. For example, _(ensures \forall size_t k; k < n && (\forall size_t j; j < k ==> str[j] != '\0') ==> (\forall size_t j; \old(strlen(b, b_nul_pos)) <= j && j <= \old(strlen(b, b_nul_pos)) + k ==> b[j] == str[j - \old(strlen(b, b_nul_pos))])) roughly means "k is a number less than n such that each of the first k characters of the string pointed to by str is non-NUL. For each such k, the first k + 1 bytes of str were appended to the end of b".

  7. Look for "TODO" in comments.

Please use GitHub's pull request system (preferred) or send patches generated with git format-patch to dtrebbien@gmail.com.

Note that unless you specify otherwise, Contributions are licensed under the terms and conditions of the Apache License, Version 2.0, without any additional terms or conditions. See Section 5, Submission of Contributions, of the Apache License, Version 2.0.

License

verlibc code is licensed under the terms of the Apache License, Version 2.0.