An Operational Semantics of the Java Card Firewall

This paper presents an operational semantics for a subset of Java Card bytecode, focussing on aspects of the Java Card firewall, method invocation, field access, variable access, shareable objects and contexts. The goal is to provide a precise description of the Java Card firewall using standard tools from operational semantics. Such a description is necessary for formally arguing the correctness of tools for validating the security of Java Card applications.

• Type: Conference
• Year: 2001
• Where: ESMART
• Authors: Marc Éluard, Thomas P. Jensen, Ewen Denney
• Keywords: ESMART 2001, Java Card, Java Card Applications, Operational Semantics, Security Privacy