Reasoning About Exceptional Behavior At the Level of Java Bytecode

TL;DR

This paper tackles the challenge of formally verifying exceptional behavior in Java programs by shifting verification to the bytecode level. It extends ByteBack with Vimp, a high-level intermediate representation built on Grimp to express logic, specifications, and exceptional control flow, ultimately lowering to Boogie for verification. The approach uses BBlib to annotate exceptional and normal behavior, supporting features like explicit exception handling, multi-catch, and try-with-resources, and demonstrates robustness to evolving language features while enabling cross-language JVM verification (Java, Scala, Kotlin). Experimental results show the framework verifies diverse programs with modest encoding and verification times, underscoring its practical viability. Overall, the work provides a flexible, bytecode-centered verification pipeline that complements source-level verifiers and broadens applicability to current and future JVM languages and features.

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

Figures (6)

• Figure 1: An overview of [0.5]Byte-Back's verification workflow.
• Figure 2: Annotated Java method and class , which demonstrate some pitfalls of specifying and reasoning about exceptional behavior.
• Figure 3: Examples of exceptional postconditions in BBlib.
• Figure 4: A loop in Java (left), its unstructured representation in Vimp (middle), and the transformation $\mathcal{V}\IfNoValueF{loop}{_{\mathsf{loop}}}$ of its invariant into assertions and assumptions (right).
• Figure 5: A try-catch block in Java (left), its unstructured representation as a trap in Grimp (middle, empty lines are for readability), and its transformation $\mathcal{V}\IfNoValueF{exc}{_{\mathsf{exc}}}$ in Vimp with explicit exceptional control flow (right).