FMOℤ 2022

Program

Abstracts

Rob van Glabeek

Mutual exclusion: impossibility results and faulty protocols

A mutual exclusion protocol needs to satisfy 2 main requirements, and a few implicit ones.
Safety: It shouldn’t allow two process to be in the critical section simultaneously.
Liveness: Each process that wants to enter the critical section will eventually get there.
Whether a given protocol satisfies these requirement also depends on whether it is speed-independent, and on the hardware of shared registers: can a write action be postponed by an ongoing read action?

I present the impossibility result that there exists no correct mutual exclusion protocol satisfying both safety and liveness when assuming speed-independence, and that a write be postponed by a read. If we give up on any of these assumptions, mutual exclusion is unproblematic.

An alternative for the assumption that a write can be postponed by an ongoing read is that multiple reads and writes can happen simultaneously. But when two writes occur simultaneously, anything may end up the memory, and when a read overlaps a write, any value may be read. Under those assumptions, many mutual exclusion protocols from the literature turn out to be incorrect, even those that set out to address exactly this problem, such as Szymansky’s protocol. Making a correct protocol is very tricky, and its verification calls for tools such as mCRL2.

Athanasios Evangelou-Oost

Modelling distributed specifications with simplicial sets

We discuss an algebraic model for distributed specifications. In this model, systems are defined as simplicial presheaves, which we think of as sets of traces of observable behaviours closed under ’stuttering’ and ’mumbling’ and parametrised over a space that represents physical extent. We define basic operations on these systems such as nondeterministic sum, parallel product and sequential product. We then explain how subsystems of a fixed system form a ’refinement algebra’, i.e., a lattice with monoidal operators whose ordering represents implementability of specifications. We conclude by suggesting directions for future work.

Rajeev Gore

CEGAR-Tableaux: improved modal satisfiability via modal clause-learning and SAT

We present CEGAR-Tableaux, a tableaux-like method for propositional modal logics utilising SAT-solvers, modal clause-learning and multiple optimisations from modal and description logic tableaux calculi. We use the standard Counter-example Guided Abstract Refinement (CEGAR) strategy for SAT-solvers to mimic a tableau-like search strategy that explores a rooted tree-model with the classical propositional logic part of each Kripke world evaluated using a SAT-solver. Unlike modal encodings into SAT-solvers and modal resolution methods, we do not explicitly represent the accessibility relation but track it implicitly via recursion. By using “satisfiability under unit assumptions”, we can iterate rather than “backtrack” over the satisfiable diamonds at the same modal level (context) of the tree model with one SAT-solver. By keeping modal contexts separate from one another, we add further refinements for reflexivity and transitivity which manipulate modal contexts once only. Our solver CEGARBox is, overall, the best for modal logics K, KT and S4 over the standard benchmarks, sometimes by orders of magnitude. It can now also handle all of the 15 logics in the modal cube as well as multimodal tense logic Kt(n) (AKA description logic ALCI). We believe that in the future, all tableaux calculi implementations will use CEGAR-Tableaux.

Nicholas Coughlin

Rely/guarantee reasoning for weak memory models

Rely/guarantee reasoning provides a compositional approach to the verification of concurrent programs. However, such reasoning traditionally assumes a sequentially consistent memory model. Therefore, its application is unsound when considering the weak memory models widely implemented by modern hardware. To address this, we present rely/guarantee-based approaches capable of capturing the behaviours enabled by two classes of weak memory models. The first considers architectures that can be modelled via a notion of thread local instruction reordering. We exploit this property to identify conditions under which instruction reordering will not invalidate rely/guarantee reasoning on an assumed sequentially consistent memory model. The second approach considers non-multicopy atomic architectures, in which stores are not simultaneously propagated throughout the system and, hence, may be observed by threads at different times. We leverage the abstractions provided by rely/guarantee specifications to argue for the valid composition of any two threads despite the possibility of differences in their observed stores.

Brae Webb

Verifying Expression Graph Optimizations in GraalVM

Compiler optimization passes have been shown to be prone to subtle implementation bugs. Almost all software relies on the faithful translation performed by compilers, thus implementation bugs pose a substantial problem. Our work focuses on addressing this problem by verifying the optimization passes of a state-of-the-art polyglot compiler, GraalVM.

The GraalVM optimizing compiler represents expressions using a graph structure in SSA form. We present our efforts to verify the correctness of expression optimizations performed by the compiler. Proof infrastructure has been developed to aid the lifting of machine word theories in Isabelle/HOL to the compiler’s graph structure. Optimization rules are specified via a domain specific language from which proof obligations and supporting lemmas are generated. This enables optimization verification by non-expert users.

Michael Norrish

Kalas: a verified, end-to-end compiler for a choreographic language

Choreographies are an abstraction for globally describing deadlock-free communicating systems. A choreography can be compiled into multiple endpoints preserving the global behaviour, providing a path for concrete system implementations. Of course, the soundness of this approach hinges on the correctness of the compilation function. In this talk, I will describe a verified compiler for Kalas, a choreographic language. Its machine-checked end-to-end proof of correctness ensures all generated endpoints adhere to the system description, preserving the top-level communication guarantees. We use the verified CakeML compiler and HOL4, giving concrete executable implementations and statements of correctness at the machine code level for multiple architectures.

Franck Cassez

Deductive Verification of Smart Contracts with Dafny

We present a domain specific language (DSL) written on top of Dafny, to develop and formally reason about smart contracts.

Mark Utting

Verified Ethereum Bytecode Generation

We describe an approach to verifying the correctness of Ethereum smart contracts that goes all the way from high-level financial properties down to the correctness of the low-level blockchain bytecode that implements the smart contract. The verification process uses the VALE language to specify smart contracts and the semantics of Ethereum bytecode instructions. These are translated into F* programs whose correctness can be verified using the Z3 SMT solver. The verified Ethereum bytecode can be generated directly by a translator from the VALE specification.

Ian Hayes

Handling localisation in rely/guarantee concurrency: An algebraic approach

The rely/guarantee approach of Jones extends Hoare logic with rely and guarantee conditions in order to allow compositional reasoning about shared-variable concurrent programs. This talk focuses on localisation in the context of rely/guarantee concurrency in order to support local variables. Because we allow the body of a local variable block to contain component processes that run in parallel, the approach allows variables local to a block to become shared variables of its component parallel processes. Localisation is also required to support call-by-value parameters and data refinement. To support the mechanisation of the rely/guarantee approach we have developed a synchronous concurrent refinement algebra that consists of a hierarchy of algebras. Its foundation consists of a small set of primitive commands plus a small set of primitive operators from which all remaining constructs are defined. To support local variables we add primitive localisation operators based on Tarski’s cylindric algebra, the algebra of predicate calculus (i.e. exists and for-all quantifiers), but generalised to commands, rather than predicates. From this we can prove properties of localisation, including its interaction with rely and guarantee conditions.

Scott Heiner

Compositional feasibility for hybrid systems using an output-localisation operator

Hybrid systems use discrete actions in conjunction with real-time continuous dynamics, and are present in safety-critical settings such as transport, health and security. Given a specification of a hybrid system, we would like an effective and adaptive way of proving its feasibility. In this talk we focus on a compositional definition for this feasibility which leverages the structure of a hybrid implementation of a synchronous concurrent refinement algebra. This implementation adapts the stream-processing functions of Müller and Broy to an interval-based trace model, and uses weak conjunction as its primary synchronisation operator. Variables are internally defined for this model, where a program’s meaning is interpreted with respect to a set of output variables. To prove feasibility in a compositional way, we liberate a program of its output during execution, extend it to remove timing constraints, and show that it is a refinement of the set of all infinite traces. To liberate the program of its output, we define an output-localisation operator, based on the cylindric operators used in Hayes and Meinicke’s work to define local variables.

Nisansala Yatapanage

Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols

Rely/guarantee reasoning helps to draw out the underlying assumptions in security protocols, which are often obscured by other techniques. This talk describes an attempt at modelling the Needham-Schroeder protocol using rely/guarantee reasoning.

Chenyi Zhang

Taint Trace Analysis For Java Web Applications

Taint analysis is concerned about whether a value in a program can be influenced, or tainted, by user input. Existing works on taint analysis focus on tracking the propagation of taint flows between variables in a program, and a security risk is reported whenever a taint source (user input) flows to a taint sink (resource that requires protection). However, a reported bug may have its taint source and taint sink located in different software components, which complicates the bug tracking and bug confirmation for developers. This work proposes Taint Trace Analysis (TTA), which extracts traces of taint flows across program contexts and field accesses in the Doop framework. The output of TTA can be visualized as a set of traces which illustrate the inter-procedural taint propagation from taint sources to their corresponding sinks. As a consequence, TTA provides more useful information for developers and users after a vulnerability is reported. Our implementation of TTA in Doop adds only a small run-time overhead on top of the (amended) P/Taint for a range of analyses on Securibench Micro.

Yi Lu

Nontransitive Information Flow Control

Modern information-flow control (IFC) security models follow Denning’s classical lattice approach and allow a developer to specify and track security labels at the granularity of program variables using a transitive flow relation. In this talk, we first discuss the recent work on nontransitive IFC that assumes no transitivity of the underlying flow relation of labels and fits naturally for coarse-grained security policies where labels are specified at the modules or components. Then, we explore a dual-labelled security model that combines both fine-grained and coarse-grained labels to capture information-based security intents in programs that are composed of mutually untrusted components.