Model-Checking Secure Information Flow for Multi-Threaded Programs
This paper describes a practical exercise in using the self-composition approach to model check secure information flow for multithreaded programs. Concretely, the authors show how eager trace invariance, proposed by Roscoe, and observational determinism, in the version of Terauchi, can be characterised as temporal logic formulae and encoded in the Concurrency WorkBench. The encoding can be used to check security of several simple example programs, including examples that would be rejected by a type checker. As future work, they plan to make the approach scale. For this, they need to improve the modelling of the program model, without an explicit encoding of the data domain.