VERIFY on Tuesday, July 20th

08:50‑10:00 Welcome by the Chairs. Session 1
Location: IF 4.31+4.33
08:50 Invited Talk
09:00 Cliff Jones (Newcastle University, UK)
Abstractions Before Proofs

Proving that programs satisfy their specifications can benefit enormously from tool support but theorem proving tools can also constrain a user's thinking. This talk argues that, for large or complex programs, it is layers of abstraction that make or break the comprehensibility of developments. However powerful a theorem proving tool is, it will make little long-term contribution to the understanding of programs if the user is forced to bend their steps of development to fit the tool. Abstraction is essential to achieve separation of issues and to help in the understanding of complex systems. The formalism chosen governs the difficulty of completing detailed proofs that can be verified with mechanically checkable rules. This talk will emphasize abstractions and techniques for reasoning about the development of concurrent programs. In conclusion, the argument will turn to positive recommendations for tool developers.

10:30‑12:30 Session 2: Verification in Various Domains
Location: IF 4.31+4.33
10:30 Angelo Brillout, Daniel Kroening, Philipp Ruemmer and Thomas Wahl
Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays

Craig interpolation has become a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. In this paper, we present a novel interpolation procedure for the theory of arrays, extending an interpolating calculus for the full theory of quantifier-free Presburger arithmetic, which will be presented at IJCAR this year. We investigate the use of this procedure in a software model checker for C programs. A distinguishing feature of the model checker is its ability to faithfully model machine arithmetic with an encoding into Presburger arithmetic with uninterpreted predicates. The interpolation procedure allows the synthesis of quantified invariants about arrays. This paper presents work in progress; we include initial experiments to demonstrate the potential of our method.

11:10 Shuling Wang and Xu Wang
Proving Four-Slot Algorithm Using Ownership Transfer

Simpson's four-slot algorithm has been an instructive example in studying various assertional proof methods/logics geared towards shared variable concurrency. Previously, techniques like rely-guarantee, data refinement and resource separation have been applied to simplify the construction of its correctness proof. Still, an elegant, concise and insightful proof is elusive.

Recently with the new generation of logics coming of age which are, for the first time, equipped with ownership transfer, it becomes imperative to ask to what extent can ownership transfer facilitate a nice proof of the algorithm. Ownership transfer is especially promising here because the conflict resolution mechanism in the four-slot algorithm can be easily recast as an implementation based on ownership transfer.

11:50 Michael von Tessin
Towards High-Assurance Multiprocessor Virtualisation

Virtualisation is increasingly being used in security-critical systems to provide isolation between system components. Being the foundation of any virtualised system, hypervisors need to provide a high degree of assurance with regards to correctness and isolation. seL4 is a high-performance microkernel that can be used as a hypervisor. Functional correctness of its C implementation has been formally verified. seL4 is a uniprocessor microkernel and the verification framework only allows to reason about sequential programs. However, we want to be able to use the full power of multiprocessor/multicore systems, and at the same time, leverage the high assurance seL4 already gives us for uniprocessors.

This work-in-progress paper explores possible multiprocessor designs of seL4 and their amenability to verification. It presents a formal multiprocessor execution model in Isabelle/HOL, connects it to an abstract specification of seL4's new multiprocessor code, formulates the desired isolation properties, outlines the proofs done and the ones in progress, and establishes a formal connection to seL4's uniprocessor model to enable an overall proof.

14:00‑15:00 Session 3: Invited Talk
Location: IF 4.31+4.33
14:00 VĂ©ronique Cortier (LORIA INRIA-Lorraine, France)
Verification of Security Protocols

Security protocols are short programs aiming at securing communications over a network. They are widely used in our everyday life. Their verification using symbolic models has shown its interest for detecting attacks and proving security properties. In particular, several automatic tools have been developed and are used to efficiently detect flaws. In this talk, we will first review results and techniques that allow automatic analysis of security protocols. In a second part, we will present recent results that demonstrate that formal abstract models used for verification are actually sound with respect to much richer models that considers issues of complexity and probability. As a consequence, it is possible to derive strong, clear security guarantees still keeping the simplicity of reasoning in symbolic models.

15:30‑16:50 Session 4: Verification of IT-Security
Location: IF 4.31+4.33
15:30 Mark Bickford
Automated Proof of Authentication Protocols in a Logic of Events

Using the language of event orderings and event classes, and using a type of atoms to represent nonces, keys, signatures, and ciphertexts, we give an axiomatization of a theory in which authentication protocols can be formally defined and strong authentication properties proven. This theory is inspired by \PCL, the protocol composition logic defined by Datta, Derek, Mitchell, and Roy.

We developed a general purpose \emph{tactic} (in the \Nup theorem prover), and applied it to automatically prove that several protocols satisfy a strong authentication property. Several unexpected subtleties exposed in this development are addressed with new concepts---\emph{legal protocols}, and a \emph{fresh signature criterion}---and reasoning that makes use of a well-founded causal ordering on events.

This work shows that proofs in a logic like \PCL can be automated, provides a new and possibly simpler axiomatization for a theory of authentication, and addresses some issues raised in a critique of \PCL.

16:10 Bernhard Beckert, Daniel Bruns and Sarah Grebing
Mind the Gap: Formal Verification and the Common Criteria

It is a common belief that the rise of standardized software certification schemes like the Common Criteria~(CC) would give a boost to formal verification, and that software certification may be a killer application for program verification. However, while formal models are indeed used throughout high-assurance certification, verification of the actual implementation is not required by the CC and largely neglected in certification practice - despite the great advances in program verification over the last decade.

In this paper we discuss the gap between program verification and CC software certification, and we point out possible uses of code-level program verification in the CC certification process.