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.