Conference Proceedings

Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security

R Sison, T Murray

Proceedings of the 10th International Conference on Interactive Theorem Proving | Schloss Dagstuhl | Published : 2019


It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties (in which classification of locations can vary depending on values in other locations) and complicated further when programs exploit shared-variable concurrency. Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typ..

View full abstract