Run-Time Verification for Observational Determinism Using Dynamic Program Slicing

Abstract

Information flow security states that secret information should not affect what is publicly observable. Such a requirement is usually expressed as a noninterference policy, which in general stipulates that the executions of a program must be indistinguishable to public observers when the program runs on inputs that differ only in secret values. When applied to multithreaded programs, an appropriate noninterference policy should specifically care about the nondeterministic behavior of programs resulting from the fact that the underlying scheduler is not known a priori. Observational determinism is such a policy that we aim to enforce in multithreaded programs. To do so, we first elaborate on how the inputs that are equivalent to public observers may lead to different public outputs. This, in turn, helps us propose a run-time verification mechanism based on threaded program dependence graphs and dynamic program slicing to prevent what causes the policy to be violated. The proposed mechanism is provably sound and is more permissive than analogous static mechanisms. It is also shown that the mechanism prevents illegal information flows when programs run in environments with different thread schedulers.