Skip to content
/ SeLoC Public

Strong non-interference for fine-grained concurrent programs

License

Notifications You must be signed in to change notification settings

co-dan/SeLoC

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

SeLoC: Relational separation logic for non-interference

This is the Coq development for SeLoC: a relational separation logic for proving non-interference of concurrent stateful programs.

See the paper for more details.

Installation instructions

This version is known to compile with:

If you use opam, then you can install all the dependencies by running the following commands from the root directory:

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam update
opam install .

Otherwise you can manually install all the dependencies and run make && make install.

Directory structure

All the Coq modules are in the subfolders of the theories folder:

  • program_logic: the definition of double weakest preconditions and the core logic rules, as well as the soundness proof.
  • proofmode: tactics that ease symbolic execution proofs.
  • logrel: the type system and its interpretation.
  • examples: examples studied in the paper.
  • heap_lang: operational semantics for HeapLang with deterministic allocation and its adequacy result (see more on that below).

Material from the paper

There are some additional examples that did not make the paper. See, in particular, examples/calendar.v for an example of how to handle delimited information release.

Differences with the paper

There are some differences between the Coq formalization and the presentation in the paper.

First of all, to be compatible with the existing version of HeapLang in Iris, we define double weakest preconditions on top of a language with non-deterministic allocation semantics. However, to have well-defined probabilistic semantics of thread-pools, we require the allocation to be deterministic. We formalize HeapLang with deterministic allocation in heap_lang/lang_det.v (the language is parameterized by an allocation oracle). We prove the following adequacy statement: if we have a double weakest precondition for a program under the standard non-deterministic semantics, we can also have adouble weakest precondition for the same program under the deterministic semantics with an allocator.

Secondly, our type system (and its interpretation) is parameterized by an attacker level ξ, and you can see that throughout the code. In our type system we also have an option type for integers. It is denoted as toption il l where il is the sensitivity label of the underlying integer, and l is the label for the option type (whether it is SOME or NONE); thus it roughly corresponds to option^l (int^il). In the future work we would like to extend the typing rules to arbitrary sum types.

Lastly, In Coq, we do not use the AWP proposition for atomic weakest preconditions we used in the paper. Rather, in the rule dwp-awp (in the formalization: dwp_atomic_lift_wp) we require the expressions e1 and e2 to be atomic and produce no forked off threads. Then, we fall back onto the total weakest precondition from Iris. This allows us to reuse a lot of lemmas and tactics about total weakest preconditions from Iris.