Non-Interference and Simple Erasure Policies for Java Card Bytecode

Rene Rydhof Hansen

AbstractIn this paper we propose a notion of non-interference for an
abstract version of the Java Card bytecode language. Programs that
have the non-interference property are guaranteed to not leak any
secret information. 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 be implemented and used to automatically
verify the absence of leaks in a program.

Based on the definition of non-interference we propose a notion of
simple erasure policies that are useful in applications where
confidential information must be made temporarily available to
untrusted parties, e.g., in e-commerce or e-voting.
Keywordsjava card static analysis information flow erasure policies
TypeConference paper [Without referee]
ConferenceProgramming Language Interference and Dependence 2005
Year2005    Month September
AddressLondon, England
Publication linkhttp://www.dcs.kcl.ac.uk/events/past/2005/PLID05/
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering