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 language | English |
|---|---|
| Title of host publication | 6th International Workshop on Issues in the Theory of Security (WITS '06) |
| Publication date | 2006 |
| Publication status | Published - 2006 |
| Event | 6th International IFIP WG 1.7 Workshop on Issues in the Theory of Security - Vienna, Austria Duration: 25 Mar 2006 → 26 Mar 2006 |
Conference
| Conference | 6th International IFIP WG 1.7 Workshop on Issues in the Theory of Security |
|---|---|
| Country/Territory | Austria |
| City | Vienna |
| Period | 25/03/2006 → 26/03/2006 |