Automated abstract certification of non-interference with object aliasing in rewriting logic

Non-interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from high to low security levels. In this paper, we extend a certification technique for confidentiality of Java classes regarding non-interference, in order to consider objects and object aliasing. The technique is based on rewriting logic, which is efficiently implemented in the high-level programming language Maude. Starting from a previous Java abstract semantics specification written in Maude, we develop an information flow sensitive Java semantics that allows us to observe global non-interference properties, with object aliasing. In order to achieve a finite state transition system, we develop an abstract Java semantics that we use for secure and effective confidentiality analysis. We have implemented our methodology and developed some experiments that demonstrate the feasibility of our approach.