Efficient Logic-Based Information Flow Analysis of Object-Oriented Programs

In this thesis, the JavaDL logic is amended by a new modality for the verification of termination-insensitive, object-sensitive, flow-sensitive noninterference of memory locations in object-oriented programs, that is local variables and heap object fields. Noninterference is a security model applied in information flow analysis and the amended JavaDL logic improves the information flow analysis of Java Card programs using the JavaDL sequent calculus. JavaDL formulae are a superset of first-order logic formulae and the logic additionally contains dynamic logic modalities as well as a concept called updates for the transition and evaluation of Java Card program states. Noninterference of memory locations is a property of programs and the respective pairs of start and end states of their executions.
The satisfaction of the property implies that a particular set of memory locations does not interfere with the memory locations not included in this set. A set of memory locations does not interfere with another set if the evaluations of the included memory locations in the end state of any execution are independent of the evaluations of the memory locations included in the other set.
... mehr
Noninterference in Java Card programs has already been formulated and verified in JavaDL by a concept called self-composition which compares the end states of two independent executions of the same program with respect to a particular set of memory locations. This investigation is realisable with the means provided by JavaDL, in particular the dynamic logic modalities. However, in many cases the double execution poses unnecessary proof overhead and the new modality defined in this thesis aims at reducing this overhead. The new calculus reaches this goal by partially interpreting the verified program on a single execution path. As soon as this execution path branches the calculus must return to self-composition or the analysis loses precision.