Link-Time Bytecode Quickening for Java Card Virtual Machines Without Method-Component Expansion: A Formal and Analytical Study

Java Card virtual machines execute from non-volatile memory in secure elements, where repeated reference indirection adds latency to frequently executed instructions. This paper proposes link-time bytecode quickening for the statically resolvable invocation and static-field instructions: after the ordinary installation-time validation and symbolic resolution, the linker rewrites each selected three-byte instruction in place into an implementation-private direct-address form of the same length, an aligned opcode family carrying the three most significant bits, and the two operand bytes carrying the remaining sixteen bits of a 19-bit logical byte address, which covers 512 KiB above a platform constant. The eight opcode families are verified as available on four editions of the Java Card Virtual Machine Specification and are implemented in our Java Card operating system. A small-step operational semantics presents the standard and the quickened form of each instruction as two rules sharing one effect function, so that correctness reduces to address round-trip, address agreement at link time and per-family refinement obligations; single-step and execution equivalence are proved under explicit linker-correctness, address-stability, address-range and opcode-separation assumptions, and Method-component length and control-flow offsets are preserved. A parametric execution-cost model, instantiated on measured instruction profiles of two EMV applets, Visa VSDC 2.9.2 and the Mastercard M/Chip Advance applet, gives a modeled interpreter-time reduction of 7 to 11 percent relative to the standard implementation in the field. CAP-file input and application source code are preserved; a modified linker and interpreter are required, and invokevirtual and invokeinterface are excluded, since their targets are selected at execution time and cannot be bound by the linker.