A Dafny-based approach to thread-local information flow analysis
The Dafny program verifier supports proofs of functional correctness of single-threaded programs written in an imperative, object-based or functional style. In this paper, we show how Dafny can also be used to support proofs of information flow security in multi-threaded programs. For generality, information flow is analysed with respect to a user-defined lattice of security values, and the security classifications of program variables are value-dependent, i.e., they are not fixed but depend on the current program state. For scalability, our multi-threaded analysis is carried out thread locally using rely/guarantee reasoning. The required well formedness properties of our security lattices and rely and guarantee conditions are proven using Dafny lemmas.
Mon 15 MayDisplayed time zone: Hobart change
11:00 - 12:30
|A Dafny-based approach to thread-local information flow analysis|
Graeme Smith The University of Queensland
|Transparent Actor Model|
|Using cylindric algebra to support local variables in rely/guarantee concurrency|