SecC: Verified Correctness and Information Flow for C

SecC is a program verifier for a subset of C based on Security Concurrent Separation Logic SecCSL, described in our CAV’19 paper. It permits one to reason about complex information flow with value-dependent and conditional security classifications (see the example below). SecCSL integrates such specifications neatly into standard concurrent separation logic. Moreover, the logic is proven sound in Isabelle/HOL.

Contact: Gidon Ernst, Toby Murray

Repositories:

Content

Installation

Manual installation

First check that Java 8 is installed. Run java -version and look for a version number that begins with 1.8.

SecC has been tested with Scala 2.12.8, which can be downloaded here: https://downloads.lightbend.com/scala/2.12.8/scala-2.12.8.tgz.
Unpack the .tgz archive somewhere appropriate, and set the SCALA_HOME environment variable to wherever the archive was unpacked, e.g.:

tar -xzf scala-2.12.8.tgz
export SCALA_HOME=$PWD/scala-2.12.8

SecC should build by simply typing make in the top-level directory of the repository.

git clone https://bitbucket.org/covern/secc.git
cd secc
make

This should produce a shell script secc for running SecC.

Eclipse Plugin

Docker

For https://www.docker.com/ fans:

Running SecC

Simply run secc, supplying a list of files to analyse as command line arguments.

./secc file1.c file2.c ...

Example

In the following example, two threads access a shared record record, protected by the lock mutex.

Run with

./secc examples/example.c

Output

examples/example.c
  thread1 ... success ❤ (time: 15ms, paths: 2)
  thread2 ... success ❤ (time:  5ms, paths: 1)

The is_classified field of the record identifies the confidentiality of the record’s data: when is_classified is true, the value stored in the data field is confidential, and otherwise it is safe to release publicly. This is expressed inside an invariant attached to the lock mutex (modeled here as post- resp. precondition of the functions lock and unlock).

The first thread outputs the data in the record whenever it is public by writing to the (memory mapped) output device register pointer OUTPUT_REG (here also protected by mutex). The second thread updates the record, ensuring its contents is not confidential, here by clearing its data.

struct mutex;
struct mutex *mutex;

struct record { int is_classified; int data; };
struct record *record;
int *OUTPUT_REG;

void lock(struct mutex *m);
    _(ensures exists int v. OUTPUT_REG |->[low()] v)
    _(ensures exists int c, int d.
        &record->is_classified |->[low()] c &&
        &record->data |->d && d :: (c ? high() : low()))

    void unlock(struct mutex *m);
    _(requires exists int v. OUTPUT_REG |->[low()] v)
    _(requires exists int c, int d.
        &record->is_classified |->[low()] c &&
        &record->data |->d && d :: (c ? high() : low()))

    void thread1() {
        while(1) {
            lock(mutex);
            if(!record->is_classified)
                *OUTPUT_REG = record->data;
            unlock(mutex);
        } 
    }

void thread2() {
    lock(mutex);
    record->is_classified = 0;
    record->data = 0;
    unlock(mutex);
}

Isabelle Theories

The logic SecCSL has been formalized in Isabelle/HOL 2018, which you can download here: http://isabelle.in.tum.de/website-Isabelle2018/. Assuming the isabelle command is in your path, the proofs can be re-checked as follows:

git clone https://bitbucket.org/covern/seccsl.git
cd seccsl
isabelle build -c -d . -v SecCSL