Combinatorial Validation Testing of Java Card Byte Code Verifiers

We present a technique to fully automate validation of a byte code verifier (BCV) implementation by testing. The technique is based on the use of a finite state machine model of the JVM specifications to systematically explore the set of legal JVM states from which one or more illegal states are immediately reachable. All possible sequences of instructions bringing to illegal states reachable from each legal state are combinatorially enumerated to generate a suite of tests, consisting of valid Java programs. For tests to stress the BCV type inference algorithm, each test program has been purposely designed with a large number of intertwined execution flows. The illegal state in the instruction sequence is hidden inside one of those paths.