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 imm...

Full description

Saved in:
Bibliographic Details
Main Authors: Calvagna, Andrea, Tramontana, Emiliano
Format: Conference Proceeding
Language:English
Subjects:
byte code verification
Law
Load modeling
Optimized production technology
Registers
Software engineering
software testing
Testing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1524-4547
2641-8169
DOI:10.1109/WETICE.2013.35