Treffer: Abstract

Java Bytecode Verification ensures that bytecode can be trusted to avoid various dynamic runtime errors, but it requires an analysis which is currently unrealistic to implement on systems with very sparse resources such as Sun’s Java Cards featuring a reduced Java virtual machine embedded on a smartcard (credit card with an integrated microprocessor). Commonly it is assumed that verification has to be performed off-card and shipped by means of cryptographic protection techniques, e.g., digital signatures, to ensure that the bytecode is not tampered with after it has been verified. These techniques, however, create a single point of failure trust because of their dependence on a secret (private) key. This is particularly serious when dealing with embedded systems with a very wide distribution such as Java Cards. This paper proposes an alternative solution by splitting the verification process in two parts: an off-card part, where sufficient verification information is constructed as a verification certificate to be sent together with the bytecode, and an on-card part, where the remaining verification is performed as a check of the code and the certificate, the lightweight verification, which has the advantage of running in a reasonable almost constant space (and almost linear time). We give a formal specification of the two components for a subset of Sun’s Java Card Language, sufficiently strong to write nontrivial down-loadable applets. We prove that the technique is tamper-proof by showing it both sound and complete with respect to standard bytecode verification. Finally we argue that our approach is safer than usual bytecode verification because it isolates a non-complex safety-critical component, the bytecode checker.