Using dependence graphs to assist verification and testing of information-flow properties

Abstract

Information-flow control (IFC) techniques assist in avoiding information leakage of sensitive data to an observable output. Unfortunately, the various IFC approaches are either imprecise, thus producing many false positive alerts, or they do not scale. Using system dependence graphs (SDGs) to model the syntactic dependencies between different program parts is a highly scalable approach that enables to check whether the observable output depends on the sensitive input. While this approach is sound, security violations that it reports can be false alarms. We present a technique to overcome these problems by combining two existing approaches in a novel way. We show how each security violation reported by an SDG-based approach can be used to create a simplified program that can then be handled with a second approach to prove or disprove the reported violation. As the second approach we use deductive verification and test case generation. We show that our approach is sound, and demonstrate its benefits by means of examples. We discuss the challenges of implementing the approach using JOANA and KeY.