Verifying Functional Correctness Properties At the Level of Java Bytecode

TL;DR

ByteBack is a verification technique that operates on Java bytecode, enabling the verification of functional correctness properties across different Java versions and features, thus decoupling verification from source language changes.

Contribution

It introduces ByteBack, a novel bytecode-based verification method that reconstructs necessary information for correctness proofs, supporting modern Java features and multiple versions.

Findings

Successfully verifies bytecode from various Java versions

Supports modern Java features beyond current verifiers

Demonstrates robustness across language evolution

Abstract

The breakneck evolution of modern programming languages aggravates the development of deductive verification tools, which struggle to timely and fully support all new language features. To address this challenge, we present ByteBack: a verification technique that works on Java bytecode. Compared to high-level languages, intermediate representations such as bytecode offer a much more limited and stable set of features; hence, they may help decouple the verification process from changes in the source-level language. ByteBack offers a library to specify functional correctness properties at the level of the source code, so that the bytecode is only used as an intermediate representation that the end user does not need to work with. Then, ByteBack reconstructs some of the information about types and expressions that is erased during compilation into bytecode but is necessary to correctly perform verification. Our experiments with an implementation of ByteBack demonstrate that it can successfully verify bytecode compiled from different versions of Java, and including several modern language features that even state-of-the-art Java verifiers (such as KeY and OpenJML) do not directly support$\unicode{x2013}$thus revealing how ByteBack's approach can help keep up verification technology with language evolution.