Non-Interference and Erasure Policies for Java Card Bytecode.

René Rydhof Hansen, Christian W. Probst

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    234 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publication6th International Workshop on Issues in the Theory of Security (WITS '06)
    Publication date2006
    Publication statusPublished - 2006
    Event6th International Workshop on Issues in the Theory of Security (WITS '06) -
    Duration: 1 Jan 2006 → …

    Conference

    Conference6th International Workshop on Issues in the Theory of Security (WITS '06)
    Period01/01/2006 → …

    Cite this

    Hansen, R. R., & Probst, C. W. (2006). Non-Interference and Erasure Policies for Java Card Bytecode. In 6th International Workshop on Issues in the Theory of Security (WITS '06) http://www2.imm.dtu.dk/pubdb/p.php?4742