|
Abstract:
Non-interference is a formalisation of the property that a program does not "leak" secret information. In this talk we show how to define such a notion of non-interference for an abstract version of Java Card bytecode programs where the main technical challenge is to handle the dynamic allocation of objects. Furthermore we define and discuss an information flow analysis that can be used to statically verify that a given program has the non-interference property. The analysis is shown to be formally correct with respect to the semantics.
|