Non-Interference and Simple Erasure Policies for Java Card Bytecode |
Rene Rydhof Hansen
|
| Abstract | In 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. |
| Keywords | java card static analysis information flow erasure policies |
| Type | Conference paper [Without referee] |
| Conference | Programming Language Interference and Dependence 2005 |
| Year | 2005 Month September |
| Address | London, England |
| Publication link | http://www.dcs.kcl.ac.uk/events/past/2005/PLID05/ |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |