-
Leapfrog: Certified Equivalence for Protocol Parsers
Authors:
Ryan Doenges,
Tobias Kappé,
John Sarracino,
Nate Foster,
Greg Morrisett
Abstract:
We present Leapfrog, a Coq-based framework for verifying equivalence of network protocol parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for symbolically computing a compact representation of a bisimulation, using "leaps." Proofs are powered by a certified compilation chain from first-order entailments to low-level bitvector verification conditions, which are di…
▽ More
We present Leapfrog, a Coq-based framework for verifying equivalence of network protocol parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for symbolically computing a compact representation of a bisimulation, using "leaps." Proofs are powered by a certified compilation chain from first-order entailments to low-level bitvector verification conditions, which are discharged using off-the-shelf SMT solvers. As a result, parser equivalence proofs in Leapfrog are fully automatic and push-button.
We mechanically prove the core metatheory that underpins our approach, including the key transformations and several optimizations. We evaluate Leapfrog on a range of practical case studies, all of which require minimal configuration and no manual proof. Our largest case study uses Leapfrog to perform translation validation for a third-party compiler from automata to hardware pipelines. Overall, Leapfrog represents a step towards a world where all parsers for critical network infrastructure are verified. It also suggests directions for follow-on efforts, such as verifying relational properties involving security.
△ Less
Submitted 18 May, 2022;
originally announced May 2022.
-
Targeted Synthesis for Programming with Data Invariants
Authors:
John Sarracino,
Shraddha Barke,
Hila Peleg,
Sorin Lerner,
Nadia Polikarpova
Abstract:
Programmers frequently maintain implicit data invariants, which are relations between different data structures in a program. Traditionally, such invariants are manually enforced and checked by programmers. This ad-hoc practice is difficult because the programmer must manually account for all the locations and configurations that break an invariant. Moreover, implicit invariants are brittle under…
▽ More
Programmers frequently maintain implicit data invariants, which are relations between different data structures in a program. Traditionally, such invariants are manually enforced and checked by programmers. This ad-hoc practice is difficult because the programmer must manually account for all the locations and configurations that break an invariant. Moreover, implicit invariants are brittle under code-evolution: when the invariants and data structures change, the programmer must repeat the process of manually repairing all of the code locations where invariants are violated.
A much better approach is to introduce data invariants as a language feature and rely on language support to maintain invariants. To handle this challenge, we introduce Targeted Synthesis, a technique for integrating data invariants with invariant-agnostic imperative code at compile-time. This technique is nontrivial due to the complex structure of both invariant specifications, as well as general imperative code.
The key insight is to take a language co-design approach involving both the language of data invariants, as well as the imperative language. We leverage this insight to produce two high-level results: first, we support a language with iterators without requiring general quantified reasoning, and second, we infer complicated invariant-preserving patches. We evaluate these claims through a language termed Spyder, a core calculus of data invariants over imperative iterator programs. We evaluate the expressiveness and performance of Spyder on a variety of programs inspired by web applications, and we find that Spyder efficiently compiles and maintains data invariants.
△ Less
Submitted 25 October, 2019; v1 submitted 30 April, 2019;
originally announced April 2019.
-
JSAI: Designing a Sound, Configurable, and Efficient Static Analyzer for JavaScript
Authors:
Vineeth Kashyap,
Kyle Dewey,
Ethan A. Kuefner,
John Wagner,
Kevin Gibbons,
John Sarracino,
Ben Wiedermann,
Ben Hardekopf
Abstract:
We describe JSAI, an abstract interpreter for JavaScript. JSAI uses novel abstract domains to compute a reduced product of type inference, pointer analysis, string analysis, integer and boolean constant propagation, and control-flow analysis. In addition, JSAI allows for analysis control-flow sensitivity (i.e., context-, path-, and heap-sensitivity) to be modularly configured without requiring any…
▽ More
We describe JSAI, an abstract interpreter for JavaScript. JSAI uses novel abstract domains to compute a reduced product of type inference, pointer analysis, string analysis, integer and boolean constant propagation, and control-flow analysis. In addition, JSAI allows for analysis control-flow sensitivity (i.e., context-, path-, and heap-sensitivity) to be modularly configured without requiring any changes to the analysis implementation. JSAI is designed to be provably sound with respect to a specific concrete semantics for JavaScript, which has been extensively tested against existing production-quality JavaScript implementations.
We provide a comprehensive evaluation of JSAI's performance and precision using an extensive benchmark suite. This benchmark suite includes real-world JavaScript applications, machine-generated JavaScript code via Emscripten, and browser addons. We use JSAI's configurability to evaluate a large number of analysis sensitivities (some well-known, some novel) and observe some surprising results. We believe that JSAI's configurability and its formal specifications position it as a useful research platform to experiment on novel sensitivities, abstract domains, and client analyses for JavaScript.
△ Less
Submitted 17 March, 2014;
originally announced March 2014.
