Abstract Viper is a verification infrastructure that facilitates the development of automated verifiers based on separation logic. Viper consists of the Viper intermediate language and two backend verifiers based on symbolic execution and verification condition generation, respectively. It has been used to build over a dozen program verifiers that translate verification problems in Go, Java, Python, Rust, and many others, into the Viper language and automate verification using the Viper backends. In this paper, we describe the original design goals for Viper’s language, verification logic, and tool architecture, summarize our experiences, and explain our principles for evolving the system.

Abstract Most automated program verifiers for separation logic use either symbolic execution or verification condition generation to extract proof obligations, which are then handed over to an SMT solver. Existing verification algorithms are designed to be sound, but differ in performance and completeness. These characteristics may also depend on the programs and properties to be verified. Consequently, developers and users of program verifiers have to select a verification algorithm carefully for their application domain. Taking an informed decision requires a systematic comparison of the performance and completeness characteristics of the verification algorithms used by modern separation logic verifiers, but such a comparison does not exist. This paper describes five verification algorithms for separation logic, three that are used in existing tools and two novel algorithms that combine characteristics of existing symbolic execution and verification condition generation algorithms. A detailed evaluation of implementations of these five algorithms in the Viper infrastructure assesses their performance and completeness for different classes of input programs. Based on the experimental results, we identify candidate portfolios of algorithms that maximize completeness and performance.

Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, important to prove the absence of such flaws through formal verification. Much existing work focuses on the verification of protocol models, which is not sufficient to show that their implementations are actually secure. Verification techniques for protocol implementations (e.g., via code generation or model extraction) typically impose severe restrictions on the used programming language and code design, which may lead to sub-optimal implementations. In this paper, we present a methodology for the modular verification of strong security properties directly on the level of the protocol implementations. Our methodology leverages state-of-the-art verification logics and tools to support a wide range of implementations and programming languages. We demonstrate its effectiveness by verifying memory safety and security of Go implementations of the Needham-Schroeder-Lowe, Diffie-Hellman key exchange, and WireGuard protocols, including forward secrecy and injective agreement for WireGuard. We also show that our methodology is agnostic to a particular language or program verifier with a prototype implementation for C.

Abstract Modern separation logics allow one to prove rich properties of intricate code, e.g., functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand, automation with dedicated verifiers typically requires sophisticated proof search algorithms that are specific to the given program logic, resulting in limited tool support that makes it difficult to experiment with program logics, e.g., when learning, improving, or comparing them. Proof outline checkers fill this gap. Their input is a program annotated with the most essential proof steps, just like the proof outlines typically presented in papers. The tool then checks automatically that this outline represents a valid proof in the program logic. In this paper, we systematically develop a proof outline checker for the TaDA logic, which reduces the checking to a simpler verification problem, for which automated tools exist. Our approach leads to proof outline checkers that provide substantially more automation than interactive provers, but are much simpler to develop than custom automatic verifiers.

Permission-based verification logics such as separation logic have led to the development of many practical verification tools over the last decade. Verifiers employ the separating conjunction A*B to elegantly handle aliasing problems, framing, race conditions, etc. Introduced along with the separating conjunction, the magic wand connective, written A -* B, can describe hypothetical modifications of the current state, and provide guarantees about the results. Its formal semantics involves quantifying over states: as such, the connective is typically not supported in automatic verification tools. Nonetheless, the magic wand has been shown to be useful in by-hand and mechanised proofs, for example, for specifying loop invariants and partial data structures. In this paper, we show how to integrate support for the magic wand into an automatic verifier, requiring low specification overhead from the tool user, due to a novel approach for choosing footprints for magic wand formulas automatically. We show how to extend this technique to interact elegantly with common specification features such as recursive predicates. Our solution is designed to be compatible with a variety of logics and underlying implementation techniques. We have implemented our approach, and a prototype verifier is available to download, along with a collection of examples.

The concept of controlling access to mutable shared data via permissions is at the heart of permission logics such as separation logic and implicit dynamic frames, and is also used in type systems, for instance, to give a semantics to "read-only" annotations. Existing permission models have different strengths in terms of expressiveness. Fractional permissions, for example, enable unbounded (recursive) splitting, whereas counting permissions enable unbounded subtraction of the same permission amount. Combining these strengths in a single permission model appeared to increase the complexity for the user and tools. In this paper we extend our previous work on abstract read permissions by providing them with a novel constraint semantics, which retains the use of the domain of rational numbers but enables unbounded subtraction of identical amounts. Thus we can keep an intuitive model conducive to SMT solvers while enabling "counting."