This is the development for Tagged C

Tagged C is a variant of C that implements a Tag-based Reference Monitor to protect a program with arbitrary security policies. That means that its semantics treats every value as a pair of a value and a metadata tag that describes some relevant context or history. Metadata might be information like "I belong to Bob," or "I am a valid pointer to object x." At key points in the language semantics, tags are updated according to user-defined rules. The rules collectively form a policy.

The Policy module type is defined in common/Tags.v.

Policy instantiations are kept in policies/

The formal semantics are in cfrontend/CSem.v.

The reference interpreter is in cfrontend/CExec.v.

For an interactive exploration of Tagged C, visit our github pages site.

First, configure Tagged C. Use the Linux amd64 architecture regardless of your actual architecture: there is no code gen, but other arches could behave unpredictably. Then run make.

./configure x86_64-linux

make

make proof

To execute the interpreter, run:

./ccomp -interp -p [POLICY] [NAME.C]

The Tagged C development is based on CompCert, under the non-commercial license found in the file LICENSE. This development may be used for evaluation, research, educational and personal purposes, and shared or modified consistent with the original license.