On improvements of low-deterministic security

Abstract

Low-security observable determinism (LSOD), as introduced by Roscoe and Zdancewic [18, 24], is the simplest criterion which guarantees probabilistic noninterference for concurrent programs. But LSOD prohibits any, even secure low-nondeterminism. Giffhorn developed an improvement, named RLSOD, which allows some secure low-nondeterminism, and can handle full Java with high precision [5]. In this paper, we describe a new generalization of RLSOD. By applying aggressive program analysis, in particular dominators for multithreaded programs, precision can be boosted and false alarms minimized. We explain details of the new algorithm, and provide a soundness proof. The improved RLSOD is integrated into the JOANA tool; a case study is described. We thus demonstrate that low-deterministic security is a highly precise and practically mature software security analysis method.