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
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.:
SecC should build by simply typing make in the top-level directory of the repository.
This should produce a shell script secc for running SecC.
For https://www.docker.com/ fans:
gidonernst/secc:latestSimply run secc, supplying a list of files to analyse as command line arguments.
In the following example, two threads access a shared record record, protected by the lock mutex.
Run with
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);
}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: