Conference Proceedings

Verifying that a compiler preserves concurrent value-dependent information-flow security

R Sison, T Murray

Leibniz International Proceedings in Informatics, LIPIcs | Schloss Dagstuhl | Published : 2019

Abstract

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