@CONFERENCE\{IMM2006-04742,
    author       = "R. R. Hansen and C. W. Probst",
    title        = "Non-Interference and Erasure Policies for Java Card Bytecode.",
    year         = "2006",
    booktitle    = "6th International Workshop on Issues in the Theory of Security ({WITS} '06)",
    volume       = "",
    series       = "",
    editor       = "",
    publisher    = "",
    organization = "",
    address      = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/4742-full.html",
    abstract     = "Non-interference is the property of a program not to leak any secret information. In this paper we propose a notion of non-interference for an abstract version of the Java Card bytecode language. Furthermore an information-flow analysis for verifying non-interference is developed and proved sound and correct with respect to the formal semantics of the language. The information-flow analysis can automatically verify the absence of leaks in a program, thus proving non-interference. Based on the definition of non-interference we propose a notion of simple erasure policies. These allow to statically check that confidential information is unavailable after a certain point---and that this unavailability is enforced by the system. This is a crucial requirement for systems like e-commerce or e-voting."
}