Logical Methods for Safety and Security of Software Systems

Lectures

Gilles Barthe:
Relational Verification for Differential Privacy and Cryptography

Many privacy and security properties are relational, in the sense that
they relate two executions of a system, or the execution of an ideal
system, which is secure by assumption, and a real system, for which
security is sought. As a consequence, relational properties are an
important target for program verification.
The course will introduce probabilistic couplings, which are used in
probability theory for analyzing Markov chains, and demonstrate that
many relational properties of probabilistic programs are modelled by
(generalized) probabilistic couplings. Then, it will present program
logics for proving the existence of probabilistic couplings, and show
applications to differential privacy and cryptography.

Markov chains (MC) and Markov decision processes (MDP) are widely
used as operational models for the quantitative system analysis. They can be
understood as transition systems augmented with distributions for the states
(in MC) or state-action pairs (in MDPs) to specify the probabilities for the
successor states. Additionally one might add weight functions for modeling
accumulated costs or rewards earned along path fragments to represent e.g.
the energy consumption, the penality to be paid for missed deadlines, the
gain for completing tasks successfully or the degree of the achieved utility.

The tutorial will introduce the main features of discrete-time, finite-state
Markovian models (MC and MDP) and their quantitative analysis against
temporal logic specifications. The first part will present the basic principles
of the automata-based approach for linear temporal logic (LTL) and
probabilistic computation tree logic (PCTL), including a summary of techniques that have been proposed
to tackle the state-explosion problem. The
second part of the tutorial will present algorithms for dealing with fairness
assumptions and computing conditional probabilities and quantiles.

Many program verification, analysis, testing and synthesis queries
reduce to solving satisfiability of logical formulas.
Yet, there are several applications where satisfiability,
and even a model or a proof, is insufficient.
Examples of useful additional information include
interpolants, models that satisfy optimality criteria,
generating strategies for solving quantified formulas,
enumerating and counting solutions. The lectures describe
logical services from the point of view of the Satisfiability
Modulo Theories solver Z3. We cover their foundations, algorithmics
and ways to put these features to use.

F* is a verification-oriented programming language equipped with dependent
types, programmable monadic effects, and a weakest precondition calculus. These
features allow us to express precise and compact specifications for programs.
The F* type-checker then tries to prove that programs meet their specifications
using a combination of SMT solving and manual proofs. Programs written in F* can
be compiled to OCaml, F#, and (more recently) to C for execution.

The main ongoing use case of F* is to build a verified, efficient, drop-in
replacement for the HTTPS stack. So far, this includes implementations of the
TLS Internet Standard and of its underlying cryptographic algorithms and
constructions.

In these lectures, I will give an overview of programming & verification in F*
based on security examples, ranging from functional correctness for optimized
implementations of cryptographic algorithms to cryptographic proofs of security
for (fragments of) TLS 1.3.

In the process of software production and maintenance, much effort and
many resources are invested in order to ensure that the product is as bug free as
possible. Manual bug repair is time-consuming and requires close acquaintance
with the checked program. Therefore, there is a great need for tools performing
automated program repair.

Many works are aimed at developing program repair tools which enable auto-
matic repair of real-world bugs found in large-scale software projects. As a result,
they are targeted for the type of bugs found in deployed real-world software.

Our repair algorithm, on the other hand, is designed for assisting the
developer in early stages of developments. Our goal is to have a fast, easy-to-use
program repair tool, which programmers can run routinely. Ideally, programmers
will run the tool immediately after making changes to the program, before any
manual effort was invested in debugging at all.

We use a bounded notion of correctness. We say that a program is repaired if
whenever a bounded computation reaches an assertion, the assertion is evaluated
to true. Our repair method is sound, meaning that, every returned program is
repaired. Just like Bounded Model Checking, this increases our confidence in the
returned program.

Our programs are repaired using a predefined set of mutations, applied to
expressions in conditionals and assignments (e.g. replacing a + operator by a
−). We impose no assumptions on the number of mutations needed to repair
the program and are able to produce repairs involving multiple buggy locations,
possibly co-dependent.

To make sure that our suggested repairs are as close to the original program as
possible, the repaired programs are examined and returned in increasing number
of mutations. In addition, only minimal sets of mutations are taken into account.
Our method is complete in the sense of returning all minimal sets of mutations
that create a repaired program.

The choice to use mutations for repair makes the search space small enough
to enable completeness at an affordable cost, yet it is expressive enough to repair
meaningful bugs (especially those present in earlier stages of development).

Our algorithm is based on the translation of the program into a set of SMT
constraints which is satisfiable iff the program contains an assertion violation.
This was originally done for the purpose of Bounded Model Checking in [2].Thus,
searching the space of mutated programs is reduced to searching unsatisfiable
sets of constraints. We show how to perform the latter efficiently using a sophis-
ticated cooperation between SAT and SMT solvers.

Probabilistic programming is en vogue. It is used to
describe complex Bayesian networks, quantum programs, security protocols
and biological systems. Programming languages like C, C#, Java, Prolog,
Scala, etc. all have their probabilistic version. Key features are
random sampling and means to adjust distributions based on obtained
information from system observations. We show some semantic intricacies, argue that termination is more involved than the
halting problem, and discuss recursion and run-time analysis.

We first give a brief overview of program analysis methods, with an
emphasis on the relative strengths and weaknesses of dynamic and static
analyses, and under- vs. over-approximative methods. We then explain how
low-level exploits are orchestrated, and illustrate this with a few
practical examples. We then discuss how program analysis methods can be
applied to automate the search for functional exploits, and attempt a
scientific approach towards evaluating alternative analysis techniques.
We will discuss bounded model checking, path-based symbolic simulation,
and abstraction techniques.

In automated synthesis, we transform a specification into a system that is
guaranteed to satisfy the specification against all environments. The short
course introduces the synthesis problem for specifications given by
linear-temporal logic (LTL) formulas, algorithms for solving it, its complexity,
and recent ideas in making synthesis useful in practice. The course assumes no
previous knowledge. We will define LTL, automata on infinite words, two-player
games, and transducers, and will learn how they serve as a basis for the formal
definition and solutions of the synthesis problem.

This series of four lectures will provide an introduction to compiler
verification for ML-like functional programming languages. In
particular, the lectures will cover topics such as: (1) how to setup a
compiler verification proof, i.e. the semantics of programming
languages and the theorem statements; (2) how to verify the
compilation of the data abstraction that functional languages provide;
(3) how to implement and verify compilation of (curried) closure
applications; (4) and finally how a verified compiler can be
bootstrapped in the logic of an interactive theorem prover. Many of
the examples will be based on the CakeMLcompiler which has
been verified and bootstrapped in the HOL theorem prover.

This series of lectures is concerned with data structures for functional
programming languages and with the formal verification of their functional
correctness and their complexity. A number of more and less well known data
structures will be examined and it will be shown that a theorem prover (here:
Isabelle) is a suitable environment for proving not just functional
correctness but also for analyzing the (amortized) complexity of algorithms.
The focus will be on search trees and priority queues.

Formal verification technology is widely deployed, different proof technologies occupying largely separate spheres. SMT solvers combine linear arithmetic and other decision procedures with simple logic, while interactive theorem provers allow the editing of large specifications and resolution theorem provers solve hard problems in pure first-order logic. However, real world problems require a combination of verification technologies.

Hybrid systems have a digital control but continuous behaviour. For example, a thermostat switches on or off according to the current temperature, which will then rise or fall continuously. Other applications may involve acceleration or the opening of valves; in each case the continuous behaviour is described by a differential equation and approximated by a formula involving the special functions sin, cos, exp, ln, etc.

MetiTarski is an automatic theorem prover for verifying inequalities involving such functions. It combines classical resolution, decision procedures for polynomial problems and axiomatic information about special functions. In addition, MetiTarski contains specialised code to put formulas into a canonical form, and a modified term ordering; these cooperate to create a search space in which occurrences of special functions are successively eliminated.

The lectures will examine this architecture in detail, with the aim of suggesting new ways of combining resolution with decision procedures. They will cover classical resolution and in particular ordered resolution (or superposition), which uses an ordering to constrain the search by selecting a particular literal. They will describe a method of integrating decision procedure calls with resolution at a low level. They will examine refinements specific to MetiTarski, such the Knuth-Bendix term ordering and necessary modifications to it. Applications of MetiTarski to hybrid systems will also be covered. Finally, we can ask how to integrate such techniques with other verification tools.

Dynamic logic has been introduced for understanding programs, but its real
calling are dynamical systems. Dynamic logic excels at providing simple and
elegant logical foundations for the dynamical systems arising in cyber-physical
systems. Since these CPSs combine cyber aspects such as communication and
computer control with physical aspects such as movement in space, their
dynamical system models also combine discrete dynamics with continuous dynamics.
Differential dynamic logic provides a programming language for these models and
comes with a compositional axiomatization. Its implementation in the
KeYmaera X
theorem prover has been instrumental in verifying applications such as the
Airborne Collision Avoidance System ACAS X and ground robot navigation. This
series of lectures will additionally consider
differential game logic for hybrid games ,
which add an adversarial element to the dynamics.