Integrated Java Bytecode Verification

Andreas Gal, Christian Probst, Michael Franz

    Research output: Contribution to journalJournal articleResearchpeer-review

    141 Downloads (Pure)

    Abstract

    Existing Java verifiers perform an iterative data-flow analysis to discover the unambiguous type of values stored on the stack or in registers. Our novel verification algorithm uses abstract interpretation to obtain definition/use information for each register and stack location in the program, which in turn is used to transform the program into Static Single Assignment form. In SSA, verification is reduced to simple type compatibility checking between the definition type of each SSA variable and the type of each of its uses. Inter-adjacent transitions of a value through stack and registers are no longer verified explicitly. This integrated approach is more efficient than traditional bytecode verification but still as safe as strict verification, as overall program correctness can be induced once the data flow from each definition to all associated uses is known to be type-safe.
    Original languageEnglish
    JournalElectronic Notes in Theoretical Computer Science
    Volume131
    Pages (from-to)27-38
    ISSN1571-0661
    Publication statusPublished - 2005

    Cite this