Note: [1] A preliminary version of parts of this work appeared in Proc. Principles of Security and Trust (POST ’16) [4]. This work was partially supported by DFG grants Sn11/12-1/2/3 in the scope of the priority program “Reliably Secure Software Systems”.
Abstract: We present a new algorithm, together with a full soundness proof, which guarantees probabilistic noninterference (PN) for concurrent programs. The algorithm follows the “low-deterministic security” (LSOD) approach, but for the first time allows general low-nondeterminism as long as PN is not violated. The algorithm is based on the earlier observation by Giffhorn and Snelting that low-nondeterminism is secure as long as it is not influenced by high events [International Journal of Information Security 14 (2015) 263–287]. It uses a new system of classification flow equations in multi-threaded programs, together with inter-thread/interprocedural dominators. Compared to LSOD, precision is boosted and false alarms are minimized. We explain details of the new algorithm and its soundness proof. The algorithm is integrated into the JOANA software security tool, and can handle full Java with arbitrary threads. We apply JOANA to a multi-threaded e-voting system, and show how the algorithm eliminates false alarms. We thus demonstrate that low-deterministic security is a highly precise and practically mature software security analysis method.
Keywords: Software security, information flow control, probabilistic noninterference, program analysis
