2018-02-14 17:33:01 +01:00
|
|
|
Formalisation of ["Noninterference, Transitivity, and Channel-Control Security Policies"](http://www.csl.sri.com/papers/csl-92-2/) by John Rushby.
|
|
|
|
|
|
|
|
|
|
Requires [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp).
|
|
|
|
|
|
2019-06-14 19:52:10 +02:00
|
|
|
The proofs are in `Rushby.v` and one instantiation is in `ArrayMachine.v`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
BEWARE!!! I wrote this formalization when I started my PhD, and I
|
|
|
|
|
didn't know much about (idiomatic) Coq back then. As a result, the
|
|
|
|
|
code is quite shitty.
|
