Fifth Summer School on Formal Techniques

Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the fifth in the series, will focus on the principles and practice of formal techniques, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in developing and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school will have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions.

Lecturers

• Natarajan Shankar (SRI CSL):
  Speaking Logic
  (PVS, PVS Course, Speaking Logic )
  Abstract: Formal logic has become the lingua franca of computing. It is used for specifying digital systems, annotating programs with assertions, defining the semantics of programming languages, and proving or refuting claims about software or hardware systems. Familiarity with the language and methods of logic is a foundation for research into formal aspects of computing. This course covers the basics of logic focusing on the use of logic as a medium for formalization and proof.
• Arie Gurfinkel (SEI CMU, USA):
  Building Program Verifiers from Compilers and Theorem Provers
  (Materials)
  Abstract: Developing an automated program verifier is an extremely difficult task. By its very nature, a verifier shares many of the complexities of an optimizing compiler and of an efficient automated theorem prover. From the compiler perspective, the issues include idiomatic syntax, parsing, intermediate representation, static analysis, and equivalence preserving program transformations. From the theorem proving perspective, the issues include verification logic, verification condition generation, synthesizes of sufficient inductive invariants, deciding satisfiability, interpolation, and consequence generation. Luckily, the cores of both compilers and theorem provers are well understood, well-defined, and readily available. In these lectures, we examine how to build a state-of-the-art program verifier by re-using much of existing compilers and SMT-solvers. The lectures are based on the SeaHorn verification framework developed at CMU.
• Cathy Meadows (NRL, USA):
  Cryptographic Protocol Analysis Modulo Equational Theories: the Maude-NRL Protocol Analyzer
  (Slides 1, Slides 2)
  Abstract: In this course we give an overview of the Maude-NPA Protocol Analyzer. Maude-NPA is a tool for the symbolic analysis for cryptographic protocols. It searches for ways in which an active attacker could subvert the protocols' goals, such as authentication or secrecy. Maude-NPA is designed to take account of the algebraic properties of the crypto systems involved, in order to give a more complete representation of both the protocol and the attacker's capabilities. We give a presentation of the theory and principles under which Maude-NPA operates, and also give the students the opportunity to gain hands-on experience with the tool.
• Bart Jacobs (KU Leuven, Belgium):
  VeriFast: Modular verification of sequential and concurrent C and Java programs using separation logic (Reading materials)
  Abstract: VeriFast is a tool that takes as input a C or Java program module annotated with preconditions, postconditions, loop invariants, data structure descriptions and proof hints written in a variant of separation logic, and, without further user interaction and usually in a matter of seconds, returns either "0 errors found", or a failed symbolic execution path. If the tool reports "0 errors found" for all modules of a program, this means no execution of the program accesses unallocated memory, performs a data race, or violates any of the user-specified assertions. The tool operates by symbolically executing each function/method, using a separation logic formula to represent the state of memory, and using an SMT solver to decide proof obligations about data values.

  In these lectures, you will learn how to use VeriFast to modularly verify sequential and concurrent C and Java programs, and you will also learn how VeriFast operates internally, and why, if it reports "0 errors found", the program does indeed satisfy the specified properties.

• Kim Guldstrand Larsen (Aalborg University, Denmark):
  From Timed Automata to Stochastic Hybrid Games -- Model Checking, Performance Evaluation and Synthesis
  (Lecture material)
  Abstract: Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. During the last 20 years the real-time model checker UPPAAL has been developed allowing for efficient verification of hard timing constraints of timed automata. Moreover a number of significant branches exists, e.g. UPPAAL CORA providing efficient support for optimization, and UPPAAL TIGA allowing for automatic synthesis of strategies for given safety and liveness objectives. Most recently, the branch UPPAAL SMC, a highly scalable new engine has been released supporting (distributed) statistical model checking (and synthesis) of stochastic hybrid automata (and games).

  The lecture will review the various branches of UPPAAL and their concerted applications to a range of real-time and cyber-physical examples including schedulability and performance evaluation of mixed criticality systems, modeling and analysis of biological systems, energy-aware wireless sensor networks, smart grids and energy aware buildings and battery scheduling. Also, we shall see how other branches of UPPAAL may benefit from the new scalable engine of UPPAAL SMC in order to improve their performance as well as scope in terms of the models that they are supporting. This includes application of UPPAAL SMC to counter example generation, refinement checking, controller synthesis, and optimization.

  The lab sessions will be based on exercises requiring hands-on experience with UPPAAL, UPPAAL TIGA and UPPAAL SMC (all down-loadable from www.uppaal.org).

• John Harrison, Intel (Portland, USA):
  HOL Light --- from foundations to applications
  (HOL Light)
  Abstract: The HOL Light theorem prover is a real-world theorem proving program with an unusually simple logical kernel. It has been used both for applications in formal verification, especially of floating-point algorithms, and pure mathematics including the Flyspeck project's formal proof of the Kepler conjecture. We will describe how the system is built up from its low-level foundations and how it can be applied in various areas. In the lab exercises we will try to show not only how to perform basic formal proofs, but how conceptually simple it is to add new "correct by construction" derived rules of inference.

Invited Speakers

• Temesghen Kahsai:
  Trusting outsourced components in flight critical software (Slides)
  Abstract: A common practice in the development of complex component-based flight critical software systems is to outsource the implementation of some of the components to external contractors or assemble them from commercial off-the-shelf (COTS) systems. Those components are delivered as black-box systems, although they may have been first prototyped in-house by the system integrator. In this talk, I will illustrate a work in progress approach to formally analyze flight critical software that has been assembled from COTS or outsourced for implementation. Such approach is based on contract-based compositional verification, which consists of two stages: a pre- and a post-delivery verification stages. In the first stage, verification focuses on generating contracts, a widely used method for organizing the integration of component-based systems, for the outsourced component. Contracts specify the precise information needed to reason about a component's interaction with other parts of the system as well as system-level properties. In the second stage, outsourced components or COTS must be checked for conformance to the pre-specified formal contract.
• Dana Scott:
  λ-Calculus Then and Now
  (Scott Bio, λ-Calculus: Then and Now, Timeline, λ-Calculus: Enumeration Operators and Types,
  λ-Calculus: Enumeration Operators and Types, Bibliography) and
  A Stochastic λ-Calculus
  (Extended Abstract, Stochastic λ-Calculus, Stochastic λ-Calculus)
  Abstract:
• Mariana Raykova:
  Secure Two-Party Computation in Sublinear (Amortized) Time
  Abstract: Traditional approaches to generic secure computation begin by representing the function f being computed as a circuit. If f depends on each of its input bits, this implies a protocol with complexity at least linear in the input size. In fact, linear running time is inherent for non-trivial functions since each party must “touch” every bit of their input lest information about the other party’s input be leaked. This seems to rule out many applications of secure computation (e.g., database search) in scenarios where inputs are huge.
  Adapting and extending an idea of Ostrovsky and Shoup, we present an approach to secure two-party computation that yields protocols running in sublinear time, in an amortized sense, for functions that can be computed in sublinear time on a random-access machine (RAM). Moreover, each party is required to maintain state that is only (essentially) linear in its own input size. Our protocol applies generic secure two-party computation on top of oblivious RAM (ORAM). We present an optimized version of our protocol using Yao’s garbled-circuit approach and a recent ORAM construction of Shi et al.
  We describe an implementation of this protocol, and evaluate its performance for the task of obliviously searching a database with over 1 million entries. Because of the cost of our basic steps, our solution is slower than Yao on small inputs. However, our implementation outperforms Yao already on DB sizes of 218 entries (a quite small DB by today’s standards).