FMOℤ 2018

Program

Abstracts

Rajeev Gore

Well-Founded Unions
(joint work with Jeremy Dawson and Nachum Dershowitz)

Given two or more well-founded (terminating) binary relations, when can one be sure that their union is likewise well-founded? We suggest new conditions for an arbitrary number of relations, generalising known conditions for two relations. We also provide counterexamples to several potential weakenings. All proofs have been machine checked.

Ian Hayes

Challenges of specifying concurrent program components

The purpose of this talk is to review some of the challenges of formally specifying components of shared-memory concurrent programs. The focus is to provide an abstract specification of a component that is suitable for use both by clients of the component and as a starting point for refinement to an implementation of the component. We present some approaches to devising specifications, investigating different forms of specification suitable for different contexts. We examine handling atomicity of access to data structures, blocking operations and progress properties, and transactional operations that may fail and need to be retried.

Sergiy Bogomolov

Time-Triggered Conversion of Guards for Reachability
Analysis of Hybrid Automata

A promising technique for the formal verification of embedded and cyber-physical systems is flow-pipe construction, which creates a sequence of regions covering all reachable states over time. Flow-pipe construction methods can check whether specifications are met for all states, rather than just testing using a finite and incomplete set of simulation traces. A fundamental challenge when using flow-pipe construction on high-dimensional systems is the cost of geometric operations, such as intersection and convex hull. In this talk, we address this challenge by showing that it is often possible to remove the need to perform high-dimensional geometric operations by combining two model transformations, direct time-triggered conversion and dynamics scaling. Further, we discuss how to make the overapproximation error in the conversion arbitrarily small. Finally, we show that our transformation-based approach enables the analysis of a drivetrain system with up to 51 dimensions.

Nicholas Coughlin

Verified Value Numbering in CakeML

CakeML is a functional programming language with a proven correct compiler and runtime, implemented and verified in HOL4 logic. The compilation process features several intermediary languages, particularly an imperative style, SSA-like language operating over machine words named WordLang. Construction of this IL consists of a lowering from a high level IL into corresponding WordLang snippets, often resulting in a suboptimal representation. To improve the quality of the generated code, a value numbering analysis and a series of optimisations have been added as a single pass over WordLang, along with corresponding proofs for the preservation of semantics across these transformations and limited validation of optimising behaviours. The pass is fully implemented in HOL4 logic and translatable into CakeML using the project’s existing proof producing translator, to enable in-logic bootstrapping.

The value numbering implementation consists of a directed acyclic graph encoding of deterministic expressions, with vertices and edges representing operations and operands respectively, as well as several maps to enable quick value number lookups. Optimisations include common subexpression elimination, limited code motion, constant folding and copy propagation. The majority of these are restricted to operating over extended basic blocks, with only a subset of value numbering information being held globally.

The value numbering analysis retains several invariants, such as well-formedness properties of its graph structure, as well as equivalence between the evaluation semantics of its DAG representation and the original program. Optimisations then demonstrate equivalence between evaluation semantics of the DAG and the optimised program. These are composed to demonstrate the preservation of semantics across the pass.

The pass has proven to be effective in eliminating repeated memory address calculations and accesses. However, limitations due to the opaqueness of garbage collector behaviour in WordLang’s semantics prevent future improvement here. Instead, future work will likely be directed towards similar passes at more abstract ILs.

Jim McCarthy

Questioning Formal Methods in Defence Science and Technology

Defence is rife with critical systems which must satisfy safety, security, and mission-suitability properties. They can be large-scale, require through-life maintenance and adjustment, and operate in uncertain environments. Here we consider the proposed and actual use of formal methods when accrediting these systems as fit for deployment. We suggest that current formal methods tools are inadequate for such systems in general, and outline some projects we are pursuing at DST Group with the aim of informing the development of the next generation of tools.

Hira Syeda

Program Verification in the Presence of Cached Address
Translation

Operating system (OS) kernels achieve isolation between user-level processes using multi-level page tables and translation lookaside buffers (TLBs). Controlling the TLB correctly is a fundamental security property — yet all large-scale formal OS verification projects leave correct functionality of the TLB as an assumption. We present a logic for reasoning about low-level programs in the presence of TLB address translation. We extract invariants and necessary conditions for correct TLB operation that mirror the informal reasoning of OS engineers. Our program logic reduces to a standard logic for user-level reasoning, reduces to side-condition checks for kernel-level reasoning, and can handle typical OS kernel tasks such as context switching and page table manipulations.

Robert Colvin

A wide-spectrum language for verification of programs on weak
memory models
(joint work with Graeme Smith)

Modern processors deploy a variety of weak memory models, which for efficiency reasons may (appear to) execute instructions in an order different to that specified by the program text. The consequences of instruction reordering can be complex and subtle, and can impact on ensuring correctness. Previous work on the semantics of weak memory models has focussed on the behaviour of assembler-level programs. In this paper we utilise that work to extract some general principles underlying instruction reordering, and apply those principles to a wide-spectrum language encompassing abstract data types as well as low-level assembler code . The goal is to support reasoning about implementations of data structures for modern processors with respect to an abstract specification.

Specifically, we encode a weak memory model in a pair-wise reordering relation on instructions. Some architectures require an additional definition of the behaviour of the global storage system if it does not provide multi-copy atomicity. In this paper we use the reordering relation in an operational semantics. We derive some properties of program refinement under weak memory models, and encode the semantics in the rewriting engine Maude as a model-checking tool. The tool is used to validate the semantics against the behaviour of a set of litmus tests (small assembler programs) run on hardware, and also to model check implementations of data structures from the literature against their abstract specifications.

Colin Fidge

Low-Level Network Behaviour Analysis using Model Checking
(joint work with Doug Brown)

Understanding the emergent behaviours of computer communications networks is challenging. Here we show how model checking can be used to search for design flaws in standard low-level communications protocols, through appropriate modelling and abstraction. Protocols were modelled at the physical, data link and logical OSI layers and the subsequent automated analysis exposed some potential design weaknesses and security threats.

Peter Höfner

Using Process Algebra to Design Better Protocols

Protocol design, development and standardisation still follow the lines of rough consensus and running code. This approach yields fast and impressive results in a sense that protocols are actually implemented and shipped, but comes at a price: protocol specifications, which are mainly written in natural languages without presenting a formal specification, are (excessively) long, ambiguous, underspecified and erroneous. These shortcomings are neither new nor surprising, and well documented. It is the purpose of this talk to provide further evidence that formal methods in general and process algebras in particular can overcome these problems. They provide powerful tools that help to analyse and evaluate protocols, already during the design phase. To illustrate this claim, I report how a combination of pen-and-paper analysis, model checking and interactive theorem proving has helped to perform a formal analysis of the Ad hoc On-Demand Vector (AODV) routing protocol.

Dirk Pattinson

Modular Formalisation and Verification of STV Algorithms
(joint work with Milad K. Ghale, Rajeev Gore and Mukesh Tiwari)

We introduce a formal, modular framework that captures a large number of different instances of the Single Transferable Vote (STV) counting scheme in a uniform way. The framework requires that each instance defines the precise mechanism of counting and transferring ballots, electing and eliminating candidates. From formal proofs of basic sanity condition for each mechanism inside the Coq theorem prover, we then synthesise code that implements the given scheme in a provably correct way and produces a universally verifiable certificate of the count. We have applied this to various variations of STV, including several used in Australian parliamentary elections and demonstrate the feasibility of our approach by means of real-world case studies.

Patrick Meiring

Type Labels: An Approach for Capability-Based
Access Control in Java

This paper explores the use of a type system for controlling indirect access to resources in Java. We propose a labelling system which is based on restricting the propagation of references to capabilities. Through the use of our labelling system, we are able to provide static guarantees on the use of resources by an application. Although coarse-grained, these guarantees are in many respects stronger than those of the current Java security model. Key challenges addressed by our work are how to control the ambient authority provided by static fields and methods in a language like Java, and how to track the delegation of capabilities in programs incorporating rich type hierarchies.

Xi Wu

Type Capabilities for Object-Oriented Programming Languages

Capabilities are used to restrict access to resources. However, without further control on the propagation of capabilities, they may be potentially obtained by unauthorised code. In this paper, we present a type system to enforce the proper use of capabilities by type checking at compile time, providing desired security guarantees (e.g., restricting capabilities only to authorised code) statically. Capabilities are regarded as types and granted to code based on user-defined policy files. In order to provide a finer-grained access to resources, we introduce parameterized capability types by adding string parameters into capabilities to illustrate on which targets these capabilities can be used, and we also apply this model on the case study of Java file access.

Rob van Glabbeek

Is speed-independent mutual exclusion implementable?

A mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker’s, Peterson’s and Lamport’s bakery are meant to be speed independent.

In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending on how we believe reading and writing to a memory location is really carried out. It can be implemented on electrical circuits, however.

This builds on previous work showing that mutual exclusion cannot be accurately modelled in standard process algebras.