Ninth 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 ninth in the series, will focus on the principles and practices of formal techniques, with a strong emphasis on the hands-on use and development of these technologies. It primarily targets graduate students and young researchers who are interested in studying and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school can expect to have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions.

Lecturers

• Modular Program Verification
  Peter Müller (ETH Zurich) (Slides, Viper Project page, Viper Tutorial, Assignments)
  Abstract: Modular program verification constructs a correctness proof for each program component in isolation, without considering its clients or the implementations of the components it builds on. Modularity makes verification scalable, allows one to give correctness guarantees for individual components such as libraries, and reduces the re-verification effort required by program changes.
  Modular verification is especially difficult for heap-manipulating programs, where components may interact in subtle ways through shared memory, and for concurrent programs, where thread interleavings complicate reasoning.
  In this series of lectures, I will present a verification approach that addresses these challenges using a notion of access permissions for memory locations. I will introduce a permission-based program logic (similar to separation logic) and explain how to automate verification in this logic using standard SMT solvers. In particular, I will present the Viper verification infrastructure, which allows one to express verification problems in an intermediate language and provides several back-ends that automate the verification effort.
• A principled approach to software design
  Daniel Jackson (CSAIL MIT) (Slides)
  Abstract: Design is about shaping things to fulfill a purpose; engineering is about making them efficient and robust. Software engineering (aka programming) has advanced in large part because we found principles that make good outcomes more likely. For example, if you apply the principles of representation independence, small interfaces and information hiding, you’ll be able to contain modifications more effectively and thus get more maintainable software.
  Software design — which, if the word has its standard meaning, is about shaping the behavior of software so that it meets its intended purpose—hasn’t yet reached this stage. Today, it’s done mostly by trial and error, and the principles that exist are primarily for user interfaces. In these lectures, I’ll present a new way to think about software design based on a structure that I call a concept, and will show how a collection of simple principles can explain a variety of design failures in familiar software products.
• Model Checking and its Applications
  Orna Grumberg (Technion Israel) (Lecture 1, Lecture 2, Lecture 2 updated)
  Abstract: Model checking is a successful automated verification technology that obtains a system model and a specification and returns `yes’ if the system satisfies the specification and `no’ otherwise.

  As the size and complexity of systems and specifications continuously grow, new tools and technologies are developed to cope with the new challenges. As a result, we are capable of handling new problems in new application areas.

  In this series of talks we will present two application areas that benefit from the new technologies. One is program differencing, which identifies the semantic difference between program versions. The other is program repair, which automatically proposes repairs of buggy programs.

• Introduction to Static Analysis from an Abstract Interpretation Perspective
  Kwangkeun Yi (Seoul National University) (Slides, Supplementary Note)
  Abstract: Static analysis aims at discovering semantic properties of programs without running them. Static analysis plays an important role in all phases of program development, including the verification of specifications, the verification of programs, the synthesis of optimized code, and also the refactoring and maintenance of software applications. It is commonly used in order to certify critical software. It also makes it possible to improve the quality of general purpose software and enables aggressive code optimizations. In this lecture I will give an introduction to static analysis and cover the basics of both theoretical foundations and practical implementations of scalable static analysis tools. Firstly I will cover general frameworks for designing correct static analyses. Then I will cover techniques for scalable implementations of the designs. Lastly I will cover some specialized frameworks for designing static analysis, which are simpler than the general frameworks yet powerful enough for specific cases in hand.
• An overview of Easycrypt and how to prove concrete security of cryptographic primitives
  Benjamin Gregoire (INRIA France) (Slides1, Slides2, Lab1)
  Abstract: EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs. EasyCrypt is used to prove the security of complex cryptographic constructions.
  The lectures will present
  1. The code-based game-playing approach to computer-aided cryptographic proofs and the connection to program verification; and the foundations of EasyCrypt: probabilistic relational Hoare logic;
  2. We will present our language Jasmin and how EasyCrypt can be used to prove functional correctness of Jasmin program, but also relational properties like side channel resistance.
  The EasyCrypt exercise sessions involved proving
  1. Security against chosen plaintext attacks (IND-CPA) for the Bellare and Rogaway 1993 and the Hashed ElGammal encryption schemes;
  2. Functional correctness of Jasmin implementation (using EasyCrypt)

Speaking Logic: Background Course

• Natarajan Shankar and Stéphane Graham-Lengrand (SRI CSL):
  Speaking Logic
  (Speaking Logic, PVS Tutorial)
  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.

Invited Speakers

The school also includes several distinguished invited talks.

• Michael Beeson (SJSU):
  Formalizing Geometry
  (Slides)

  Abstract: Geometry has been an important testbed of the axiomatic method, logic, and formalization, for over two millennia. This talk will review the history, the axiomatics, and the use of computer-assisted proof-finding and proof-checking in geometry.

• Peter Neumann and Prashant Mundkur (SRI):
  CHERI: an ISA-oriented approach for secure systems
  (CHERI, Sail, RISC-V, and CHERI-RISC-V)

  Abstract: This talk discusses one approach of how we might design and implement highly trustworthy hardware-software systems. We discuss problems that must be overcome, some lessons from the past, and recent efforts to apply formal methods systemically. We consider ongoing efforts relating to the CHERI (Capability Hardware Enhanced RISC Instructions) hardware instruction-set architecture (ISA), its underlying security principles, emerging formal proofs of the satisfaction of critical ISA security properties, and what CHERI hardware could do to enable better total-system security.

• Maria Paola Bonacina (Università degli Studi di Verona):
  Overview of automated reasoning and ordering-based strategies
  (Slides)
• Stéphane Graham-Lengrand (SRI CSL):
  Type Theory at SSFT
  (Slides and Exercises)
• Elaine (Runting) Shi (Cornell and IC3):
  Rethinking Large-Scale Consensus
  (Slides1, Slides2)

  Abstract: Although distributed consensus has been studied for three decades, they were not deployed at a large scale until decentralized cryptocurrencies like Bitcoin. In this talk, I will explain why the classical theoretical foundation for distributed systems is insufficient for capturing the robustness and game theoretic properties we care about for new decentralized environments. Specifically, I will demonstrate why almost all classical "synchronous" consensus protocols are underspecified and thus unimplementable in practice. I will then describe a new model called "best-possible partition tolerance" that allows us to achieve honest-majority consensus while providing resilience to network partitions (the combination of which was classically deemed impossible due to a well-known lower bound by Dwork, Lynch, and Stockmeyer).

Schedule

Previous Summer Schools on Formal Techniques

Information about previous Summer Schools on Formal Techniques can be found at

• SSFT18
• SSFT17
• SSFT16
• SSFT15
• SSFT14
• SSFT13
• SSFT12
• SSFT11

Jay Bosamiya of CMU has blogged about the 2018 Summer School at https://www.jaybosamiya.com/blog/2018/05/31/ssft/

Registration

Registration for SSFT19 is now closed - check back next year