Verification-based test case generation for information-flow properties.

Digital systems accumulate ever more personal data, and the potential of privacy breaches leading to gross privacy violations continuously increases. Information flow security deals with the problem of how certain program outputs are influenced by certain inputs. This paper handles the problem of testing information flow properties of object oriented programs. We present a symbolic-execution-based approach to automatic test case generation for four variations of the noninterference property. We also extend existing test coverage criteria and discuss their suitability for information flow test suites. We have implemented our approach using the KeY verification system, and have evaluated the implementation.