Proofs as Relational Invariants of Synthesized Execution Grammars

TL;DR

This paper introduces LTTP, an automatic safety verifier for low-level data structure programs that synthesizes relational invariants and control path grammars to prove program safety without manual input.

Contribution

The paper presents LTTP, a novel automatic verifier that synthesizes control path grammars with relational invariants for verifying safety of complex low-level data structure programs.

Findings

Successfully verified JVM bytecode benchmarks

Outperformed previous verifiers on complex data structures

Automated synthesis of control path invariants

Abstract

The automatic verification of programs that maintain unbounded low-level data structures is a critical and open problem. Analyzers and verifiers developed in previous work can synthesize invariants that only describe data structures of heavily restricted forms, or require an analyst to provide predicates over program data and structure that are used in a synthesized proof of correctness. In this work, we introduce a novel automatic safety verifier of programs that maintain low-level data structures, named LTTP. LTTP synthesizes proofs of program safety represented as a grammar of a given program's control paths, annotated with invariants that relate program state at distinct points within its path of execution. LTTP synthesizes such proofs completely automatically, using a novel inductive-synthesis algorithm. We have implemented LTTP as a verifier for JVM bytecode and applied it to verify the safety of a collection of verification benchmarks. Our results demonstrate that LTTP can be applied to automatically verify the safety of programs that are beyond the scope of previously-developed verifiers.