Reasoning About Exceptional Behavior At the Level of Java Bytecode

TL;DR

This paper introduces Vimp, a high-level bytecode representation, and an extension of ByteBack, to improve formal verification of Java programs' exceptional behavior across multiple JVM languages.

Contribution

It presents Vimp as an intermediate layer for bytecode verification, enabling accurate reasoning about exceptions in Java, Scala, and Kotlin programs.

Findings

ByteBack can verify Java programs with exceptions across all Java versions.

Vimp enhances verification flexibility and adaptability.

The approach extends to Scala and Kotlin JVM languages.

Abstract

A program's exceptional behavior can substantially complicate its control flow, and hence accurately reasoning about the program's correctness. On the other hand, formally verifying realistic programs is likely to involve exceptions -- a ubiquitous feature in modern programming languages. In this paper, we present a novel approach to verify the exceptional behavior of Java programs, which extends our previous work on ByteBack. ByteBack works on a program's bytecode, while providing means to specify the intended behavior at the source-code level; this approach sets ByteBack apart from most state-of-the-art verifiers that target source code. To explicitly model a program's exceptional behavior in a way that is amenable to formal reasoning, we introduce Vimp: a high-level bytecode representation that extends the Soot framework's Grimp with verification-oriented features, thus serving as an intermediate layer between bytecode and the Boogie intermediate verification language. Working on bytecode through this intermediate layer brings flexibility and adaptability to new language versions and variants: as our experiments demonstrate, ByteBack can verify programs involving exceptional behavior in all versions of Java, as well as in Scala and Kotlin (two other popular JVM languages).