Professor Brijesh Dongol

The rise of persistent memory is disrupting computing to its core. Our work aims to help programmers navigate this brave new world by providing a program logic for reasoning about x86 code that uses low-level operations such as memory accesses and fences, as well as persistency primitives such as flushes. Our logic, Pierogi, benefits from a simple underlying operational semantics based on views, is able to handle optimised flush operations, and is mechanised in the Isabelle/HOL proof assistant. We detail the proof rules of Pierogi and prove them sound. We also show how Pierogi can be used to reason about a range of challenging single- and multi-threaded persistent programs.

Weak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style memory models, our previous work has shown that it is possible to extend Hoare logic and Owicki-Gries reasoning to verify correctness of weak memory programs. The technique introduces a set of high-level assertions over C11 states together with a set of basic Hoare-style axioms over atomic weak memory statements (e.g. reads/writes), but retains all other standard proof obligations for compound statements. This paper takes this line of work further by introducing the first deductive verification environment in Isabelle/HOL for C11-like weak memory programs. This verification environment is built on the Nipkow and Nieto's encoding of Owicki-Gries in the Isabelle theorem prover. We exemplify our techniques over several litmus tests from the literature and two non-trivial examples: Peterson's algorithm and a read-copy-update algorithm adapted for C11. For the examples we consider, the proof outlines can be automatically discharged using the existing Isabelle tactics developed by Nipkow and Nieto. The benefit here is that programs can be written using a familiar pseudocode syntax with assertions embedded directly into the program.

Swarm attestation protocols extend remote attestation by allowing a verifier to efficiently measure the integrity of software code running on a collection of heterogeneous devices across a network. Many swarm attestation protocols have been proposed for a variety of system configurations. However, these protocols are currently missing explicit specifications of the properties guaranteed by the protocol and formal proofs of correctness. In this paper, we address this gap in the context of list swarm attestation protocols, a category of swarm attestation protocols that allow a verifier to identify the set of healthy provers in a swarm. We describe the security requirements of swarm attestation protocols. We focus our work on the SIMPLE+ protocol, which we model and verify using the tamarin prover. Our proofs enable us to identify two variations of SIMPLE+: (1) we remove one of the keys used by SIMPLE+ without compromising security, and (2) we develop a more robust design that increases the resilience of the swarm to device compromise. Using tamarin, we demonstrate that both modifications preserve the desired security properties.

This paper explores the use of ownership as a key auxiliary variable within Owicki-Gries framework. We explore this idea in the context of a ring buffer, developed by Amazon, which is a partial library that only provides methods for reserving (acquiring) and releasing addresses within the buffer. A client is required to implement additional functionality (including an additional shared queue) to enable full synchronisation between a writer and a reader. We verify correctness of the Amazon ring buffer (ARB) and show that the ARB satisfies both safety and progress. Our proofs are fully mechanised within the Isabelle/HOL proof assistant.

This book constitutes the refereed proceedings of the workshops which complemented the 23rd Symposium on Formal Methods, FM 2019, held in Porto, Portugal, in October 2019. This volume presents the papers that have been accepted for the following workshops: Third Workshop on Practical Formal Verification for Software Dependability, AFFORD 2019; 8th International Symposium From Data to Models and Back, DataMod 2019; First Formal Methods for Autonomous Systems Workshop, FMAS 2019; First Workshop on Formal Methods for Blockchains, FMBC 2019; 8th International Workshop on Formal Methods for Interactive Systems, FMIS 2019; First History of Formal Methods Workshop, HFM 2019; 8th International Workshop on Numerical and Symbolic Abstract Domains, NSAD 2019; 9th International Workshop on Open Community Approaches to Education, Research and Technology, OpenCERT 2019; 17th Overture Workshop, Overture 2019; 19th Refinement Workshop, Refine 2019; First International Workshop on Reversibility in Programming, Languages, and Automata, RPLA 2019; 10th International Workshop on Static Analysis and Systems Biology, SASB 2019; and the 10th Workshop on Tools for Automatic Program Analysis, TAPAS 2019.

Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory preserving its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of persistent concurrent data structures, together with associated notions of correctness. In this paper, we present the first formal proof technique for durable linearizability, which is a correctness criterion that extends linearizability to handle crashes and recovery in the context of NVM. Our proofs are based on refinement of IO-automata representations of concurrent data structures. To this end, we develop a generic procedure for transforming any standard sequential data structure into a durable specification. Since the durable specification only exhibits durably linearizable behaviours, it serves as the abstract specification in our refinement proof. We exemplify our technique on a recently proposed persistent memory queue that builds on Michael and Scott’s lock-free queue.

Cylindric algebras have been developed as an algebraisation of equational first order logic. We adapt them to cylindric Kleene lattices and their variants and present relational and relational fault models for these. This allows us to encode frames and local variable blocks, and to derive Morgan's refinement calculus as well as an algebraic Hoare logic for while programs with assignment laws. Our approach thus opens the door for algebraic calculations with program and logical variables instead of domain-specific reasoning over concrete models of the program store. A refinement proof for a small program is presented as an example.

Modern processors such as ARMv8 and RISC-V allow executions in which independent instructions within a process may be reordered. To cope with such phenomena, so called promising semantics have been developed, which permit threads to read values that have not yet been written. Each promise is a speculative update that is later validated (fulfilled) by an actual write. Promising semantics are operational , providing a pathway for developing proof calculi. In this paper, we develop an incorrectness-style logic, resulting in a framework for reasoning about state reachability. Like incorrectness logic, our assertions are underapproximating, since the set of all valid promises are not known at the start of execution. Our logic uses event structures as assertions to compactly represent the ordering among events such as promised and fulfilled writes. We prove soundness and completeness of our proof calculus and demonstrate its applicability by proving reachability properties of standard weak memory litmus tests.

Security-critical applications often rely on memory isolation mechanisms to ensure integrity of critical data (e.g., keys) and program instructions (e.g., implementing an attestation protocol). These include software-based security microvisor (SµV) or hardware-based (e.g., TrustLite or SMART). Here, we must guarantee that none of the assembly-level instructions corresponding to a program violate the imposed memory access restrictions. We demonstrate our approach on two architectures (SµV and TrustLite) on which remote at-testation protocols are implemented. We extend an approach based on the Binary Analysis Platform (BAP) to generate compiled assembly for a given C program, which is translated to an assembly intermediate language (BIL) and ultimately to Isabelle/HOL theories. In our extension, we develop an adversary model and define conformance predicates imposed by an architecture. We generate a set of programs covering all possible cases in which an assembly-level instruction attempts to violate at least one of the conformance predicates. This shows that the memory access restriction of both SµV and TrustLite are dynamically maintained. Moreover, we introduce conformance predicates for assembly-level instructions that can change the control flow, which improve TrustLite's memory protection unit.

The properties of a blockchain such as immutability, provenance, and peer-executed smart contracts could bring a new level of security, trust, and transparency to e-learning. In this paper, we introduce our proof-of-concept blockchain-based e-learning platform developed to increase transparency in assessments and facilitate curriculum personalisation in a higher education context. Most notably, our platform could automate assessments and issue credentials. We designed it to be pedagogically neutral and content-neutral in order to showcase the benefits of a blockchain back-end to end users such as students and teaching staff. Our evaluation suggests that our platform could increase trust in online education providers, assessment procedures, education history and credentials.

Correctness conditions like linearizability and opacity describe some form of atomicity imposed on concurrent objects. In this paper, we propose a correctness condition (called causal atomicity) for concurrent objects executing in a weak memory model, where the histories of the objects in question are partially ordered. We establish compositionality and abstraction results for causal atomicity and develop an associated refinement-based proof technique.

In the interleaving model of concurrency, where events are totally ordered, linearizability is compositional: the composition of two linearizable objects is guaranteed to be linearizable. However, linearizability is not compositional when events are only partially ordered, as in the weak-memory models that describe multicore memory systems. In this paper, we present a generalisation of linearizability for concurrent objects implemented in weak-memory models. We abstract from the details of specific memory models by defining our condition using Lamport's execution structures. We apply our condition to the C11 memory model, providing a correctness condition for C11 objects. We develop a proof method for verifying objects implemented in C11 and related models. Our method is an adaptation of simulation-based methods, but in contrast to other such methods, it does not require that the implementation totally orders its events. We apply our proof technique and show correctness of the Treiber stack that blocks on empty, annotated with C11 release-acquire synchronisation.

We define local transactional race freedom (LTRF), which provides a programmer model for software transactional memory. LTRF programs satisfy the SC-LTRF property, thus allowing the programmer to focus on sequential executions in which transactions execute atomically. Unlike previous results, SCLTRF does not require global race freedom.We also provide a lower-level implementation model to reason about quiescence fences and validate numerous compiler optimizations.

Deductive verification techniques for C11 programs have advanced significantly in recent years with the development of operational semantics and associated logics for increasingly large fragments of C11. However, these semantics and logics have been developed in a restricted setting to avoid the thin-air-read problem. In this paper, we propose an operational semantics that leverages an intra-thread partial order (called semantic dependencies) induced by a recently developed denotational event-structure-based semantics. We prove that our operational semantics is sound and complete with respect to the denotational semantics. We present an associated logic that generalises a recent Owicki-Gries framework for RC11 (repaired C11), and demonstrate the use of this logic over several example proofs.

Secure speculation is an information flow security hyperproperty that prevents transient execution attacks such as Spectre, Meltdown and Foreshadow. Generic compiler mitigations for secure speculation are known to be insufficient for eliminating vulnerabilities. Moreover, these mitigation techniques often overprescribe speculative fences, causing the performance of the programs to suffer. Recently Cheang et al. have developed an operational semantics of program execution capable of characterising speculative executions as well as a new class of information flow hyperproperties named TPOD that ensure secure speculation. This paper presents a framework for verifying TPOD using the Isabelle/HOL proof assistant by encoding the operational semantics of Cheang et al. We provide translation tools for automatically generating the required Isabelle/HOL theory templates from a C-like program syntax, which speeds up verification. Our framework is capable of proving the existence of vulnerabilities and correctness of secure speculation. We exemplify our framework by proving the existence of secure speculation bugs in 15 victim functions for the MSVC compiler as well as correctness of some proposed fixes.

This paper develops an operational semantics for a release-acquire fragment of the C11 memory model with relaxed accesses. We show that the semantics is both sound and complete with respect to the axiomatic model of Batty et al. The semantics relies on a per-thread notion of observability, which allows one to reason about a weak memory C11 program in program order. On top of this, we develop a proof calculus for invariant-based reasoning, which we use to verify the release-acquire version of Peterson’s mutual exclusion algorithm.

Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference freedom rule for concurrency. In this paper, we develop a new proof calculus for the C11 RAR memory model (a fragment of C11 with both relaxed and release-acquire accesses) that allows all Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. Our proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. We demonstrate the utility of our proof calculus by verifying a number of standard C11 litmus tests and Peterson’s algorithm adapted for C11. Our proof calculus and its application to program verification have been fully mechanised in the theorem prover

Teleo-Reactive (TR) robotic agent programs comprise sequences of guarded action rules clustered into named parameterised procedures. Their ancestry goes back to the first cognitive robot, Shakey. Like Shakey, a TR programmed robotic agent has a deductive Belief Store comprising constantly changing predicate logic percept facts, and knowledge facts and rules for querying the percepts. In this paper we introduce TR programming using a simple example expressed in the teleo-reactive programming language TeleoR, which is a syntactic extension of QuLog, a typed logic programming language used for the agent’s Belief Store. We give a formal definition of the regression property that rules of TeleoR procedures should satisfy, and an informal operational semantics of the evaluation of a TeleoR procedure call. We then formally express key features of the evaluation in LTL. Finally we show how this LTL formalisation can be used to prove that a procedure’s rules satisfy the regression property by proving it holds for one rule of the example TeleoR program. The proof requires us: to formally link a TeleoR agent’s percept beliefs with sensed configurations of the external environment; to link the agent’s robotic device action intentions with actual robot actions; to specify the eventual physical effects of the robot’s actions on the environment state.

This book constitutes the refereed proceedings of the Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 2019. The 14 full papers presented together with 3 abstract papers were carefully reviewed and selected from 22 submissions. The papers are organized in topical sections named: Tutorial lectures; Teaching Program Verification; Teaching Program Development; and Effective Teaching Techniques.

Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency. So far, this has lead to the design of a number of persistent concurrent data structures, built to satisfy an associated notion of correctness: durable linearizability.

This paper introduces a technique for modelling and verifying weak memory C11 programs in the Event-B framework. We build on a recently developed operational semantics for the RAR fragment of C11, which we use as a top-level abstraction. In our technique, a concrete C11 program can be modelled by refining this abstract model of the semantics. Program structures and individual operations are then introduced in the refined machine and can be checked and verified using available Event-B provers and model checkers. The paper also discusses how ProB model checker can be used to validate the Event-B model of C11 programs. We applied our technique to the C11 implementation of Peterson’s algorithm, where we discovered that the standard invariant used to characterise mutual exclusion is inadaquate. We therefore propose and verify new invariants necessary for characterising mutual exclusion in a weak memory setting.