User Tools

Site Tools

A Proof Technique for Noninterference In Open Systems

Enrico Scapin

Kuesters, Truderung, and Graf proposed a framework allowing tools that can check noninterference properties but a priori cannot deal with cryptography (probabilities and polynomially bounded adversaries) to establish cryptographic indistinguishability properties, such as privacy properties, for Java programs. As for checking noninterference, many program analysis tools can only deal with closed Java programs. The systems to be analyzed are, however, often open: they interact with a network or use some libraries which are not necessarily trusted and, hence, are not part of the code to be analyzed. Therefore, as part of the framework, a proof technique was proposed to reduce the problem of checking noninterference in an open system to checking noninterference for a single (almost) closed system. In this work, we extend the syntax and semantics of Jinja+, the language the framework is stated for, with java-interfaces, abstract classes, and strings. Consequently, we show that, except for the proof technique for noninterference in open systems, all definitions and results of the framework carry out easily to the extended language. Nonetheless, regarding the proof technique, non-trivial modifications have been required in order to model the exchange of data between the system and the environment, when also strings are involved.