Combinatorial Interaction Testing of a Java Card Static Verifier

We present a combinatorial interaction testing approach to perform validation testing of a fundamental component for the security of Java Cards: the byte code verifier. Combinatorial testing of all states of the Java Card virtual machine has been adopted as the coverage criteria. We developed a formal model of the Java Card byte code syntax to enable the combinatorial enumeration of well-formed states, and a formal model of the byte code semantic rules to be able to distinguish between well-typed and ill-typed ones, and to derive actual test programs from them. A complete framework has been implemented, enabling fully automated application and evaluation of the conformance tests to any verifier implementation.