Class-level Non-Interference
The Information-Flow property of Non-Interference was recently relaxed into Abstract Non-Interference (ANI), a weakened version where attackers can only observe properties of data, rather than their exact value. ANI was originally defined on integers, where a property models the set of numbers satisfying it. The present work proposes an Object-Oriented, Java-based formulation of an instance of ANI where data take the form of objects, and the observed property comes to be their type. The execution of a program is taken to be the invocation of some method by an external user: a class is secure if, for all its (non-private) methods, the type of their low-security data after the execution does not depend on the initial type of its high-security data (i.e., there are no illicit flows). The relation to ANI theory (in its abstract version) can be seen in the representation of abstract domains in terms of class hierarchies: an upper closure operator map an object into the smallest class it is an instance of. An analyzer for a non-trivial subset of Java is illustrated. A sketch of a soundness proof is provided: a program is never misclassified as secure, i.e., it is rejected whenever the absence of illicit ows cannot be guaranteed.
non-interference information flow language-based security abstract interpretation object-oriented programming languages