FMOℤ 2024

Program

Abstracts

Carroll Morgan (UNSW)

Getting the message across

We are all here because we advocate, practise, research and teach Formal Methods... which began > 50 years ago. Yet -most- undergraduate students who graduate from Computer-Science courses world-wide do not know what Formal Methods is — and certainly don’t use it. The rest of us are paying the price for that, every day.

This talk describes some aspects of an in-the-lecture actual teaching style for Formal Methods, one that has had some success at UNSW: the style is intended to get the FM message across to that majority of students who will otherwise never encounter it and –if possible– even to excite them. The associated course concerned is called "(In-) Formal Methods", and a textbook "Formal Methods, Informally" for it will be published by CUP (soon).

But the aim of the talk here is not advertising, because this audience does not need it — rather it is to encourage discussion among us on similar teaching styles developed by "others of the Faithful", those here at this meeting, and to exchange ideas (or perhaps create new ones) of how we can go further.

An earlier talk, on how one might -assess- students in such a course, can be found at https://panopto.abo.fi/Panopto/Pages/Viewer.aspx?id=1688654f-9933-4053-83bd-b12600b7e091

Zhe Hou (Griffith University)

Compositionally Automating Separation Logic for Foundational Verification by Algebraic Transformation of Data Refinement

Foundational verification considers the functional correctness of real programming languages with formalised semantics and uses proof assistants (e.g., Coq, Isabelle) to certify proofs. The need for verifying real languages compels it to involve expressive Separation Logics (SLs) that exceed the scopes of well-studied automated proof theories, e.g., symbolic heap. Consequently, foundational verification relies heavily on ad-hoc heuristics that lack a systematic meta-theory for automation. We aim to mitigate the gap by proposing a generic automation method that

1. unifies data refinement with separation logic to lift concrete data structures to abstract models; 2) is based on axiomatised algebraic properties to generically automate verification on any data structures that satisfy the axioms. The properties capture high-level semantics of data structures, boosting the automation by such high-level knowledge. As a result, we present the first generic and scalable theory of SL automation for foundational verification. Case studies on formalised C semantics show our theory instantiates reasoning procedures for 10 widely-used data structures automatically, including an AVL tree and a bucket hash map. For example, our framework can automate the verification of programs like quicksort in Isabelle/HOL with only 10 lines of annotations and manual proofs, significantly reducing the manual effort compared to existing methods (90 lines of proofs).

Rajeev Gore and Anthony Peigne (ANU)

Verified Tableaux: from modal to modal fixpoint logics

I will first give a simple example of how to automatically extract an OCaml program for adding two natural numbers using Coq’s extraction facility. To do so, we need to encode a logic program "add n m r" which encodes "n + m = r" and convince Coq that "for all n and m, there is a terminating algorithm to compute r such that add n m r holds". Constructively.

I will then explain how we used Coq to extract a formally verified OCaml program for deciding LTL-satisfiability where LTL is the linear temporal logic of "next" and "until" over the natural number line.

I will first introduce the syntax and semantics of LTL. Then explain the tableaux rules for LTL. Then explain how we encoded these rules in Coq and the theorems that we proved. Finally, I will show some performance figures comparing our OCaml implementation versus the one of Florian Widmann (an ex-phd student of mine).

It’s all supposed to be introductory!

All the hard work was done by Anthony but he cannot attend.

Aaron Bryce (ANU)

A Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments

Gentzen’s 1936 proof of the consistency of Peano Arithmetic was a significant result in the foundations of mathematics. We provide here a modified version of the proof, based on Gödel’s reformulation, and including additional details and minor corrections which are necessary to definitively prove the well-foundedness of the cut-elimination argument in a constructive environment. All results have been verified using the Coq theorem prover.

Alicia Michael (DSTG)

BASIL: Binary Analysis for Secure Information Flow Logics on Concurrent Code

Information flow logics for detecting security leaks in programs have reached a high level of maturity, supporting value-dependent security classifications of program variables, i.e., security classifications which evolve as the program executes, and thread-local reasoning over concurrent code. To put these logics into practice, however, requires further considerations. Firstly, it is well known that compiler optimisations can violate security guarantees established on source code, and hence analysis must take place on binaries. Secondly, for scalability the logics must be supported by automated tools and these tools need to be at least trusted, if not provably sound. In this paper, we present BASIL, a tool for applying information flow logics to lifted AArch64 binaries using the Boogie automated program verifier. A high level of trust is provided by the wide user base of Boogie, which has been employed as a back-end for many other tools over almost two decades. The lifter we use has also been derived from Arm’s AArch64 machine-readable formal semantics.

Pengbo Yan (University of Melbourne)

Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms

We consider the problem of how to verify the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a number of complexities that feature in the semantics and invariant needed to verify the security of many practical probabilistic oblivious algorithms. We propose an approach based on reasoning over perfectly oblivious approximations, using a program logic that combines both classical Hoare logic reasoning and probabilistic independence reasoning to support all the needed features. We formalise and prove our new logic sound in Isabelle/HOL and apply our approach to formally verify the security of several challenging case studies beyond the reach of prior methods for proving obliviousness.

Daniel Cumming (Runtime Verification)

KMIR: Concrete and Symbolic Execution of Rust MIR Through K

Rust is a nascent systems language, continually rising in popularity. Recently, many projects have approached providing formal methods solutions for program analysis. However many of these tools have restrictions on subset of Rust they target, or a challenging user interface for developers inexperienced in formal methods to adopt. We aim to provide deductive verification and symbolic execution for the Rust MIR (Middle Intermediate Representation) by encoding the operational semantics of MIR in K, and leveraging the tools automatically produced through the K ecosystem. Furthermore, we plan to implement a property verification framework to allow Rust developers the simplest user interaction possible for transitioning from testing to verification.

Micah Brown (DSTG)

Ironbark: A Formally Verifiable Processor

This presentation will discuss the approach taken to try and work towards being able to deploy a useful system which can be shown and verified to be secure from any remote attack. It focuses on the secure processor, named “Ironbark” which provides a foundation for this aim. It will cover some of the key considerations, the formal engineering required, and some of the key results achieved so far.

Toby Murray (University of Melbourne)

Assume but Verify:
Deductive Verification of Leaked Information in Concurrent Applications

We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the problem into (a) proving that the program only leaks information it has declassified via assume annotations already widely used in deductive program verification; and (b) auditing the declassifications against a declarative security policy. We show how condition (a) can be enforced by an extension of the existing program logic SecCSL, and how (b) can be checked by proving a set of simple entailments. Part of the challenge is to define respective semantic soundness criteria and to formally connect these to the logic rules and policy audit. We support our methodology in an auto-active program verifier, which we apply to verify the implementations of various case study programs against a range of declassification policies.

Gernot Heiser (UNSW)

Lions OS – towards a verified operating system

The seL4 microkernel is arguably the most highly assured operating system (OS) kernel, featuring a complete proof chain from high-level security properties to the functional specification of its operation to the implementation and ultimately the executable binary. This proof chain is complete for the 32-bit Arm and 64-bit RISC-V architectures, while the functional correctness proof exists for the 64-bit Arm and x86 architectures.

However, the microkernel itself provides little more than mechanisms for secure multiplexing of hardware, everything else is left to usermode components. Unfortunately, our experience has shown that using seL4 well to build practical secure systems is hard, it requires deep OS expertise. We have now embarked on designing, implementing and verifying Lions OS, a complete seL4-based OS aimed at the embedded/IoT/cyberphsical space, which is where most seL4 deployments happen these days. Lions OS is based on the seL4 Microkit, an abstraction layer that drastically simplifies the programming model (by specialising to static system architectures, which match the requirements of the target domain).

In the talk I will first provide a refresher on seL4, its verification story, and then discuss on-going work on the kernel itself, which includes Time Protection, the principled prevention of microarchitectural timing channels. It will then the give an overview of the Microkit, followed by the core ideas behind Lions OS, and a description of its present state. This will set the scene for the related UNSW talks: Rob Sison will discuss on-going work on proving time protection, as well as the use of SMT solvers for verifying Lions OS components and how to connect this to the seL4 proofs. Johannes Åman Pohjola will present the Pancake programming language we will be using to implement and verify (parts of) Lions OS.

Rob Sison (UNSW)

Two new frontiers for seL4’s refinement proofs:
Time protection and OS service verification

This talk will give a brief overview on the status of ongoing and planned research and development at Trustworthy Systems to expand the scope of the seL4 kernel’s refinement proofs in two directions: (1) refinement (downwards) to prove seL4 implements time protection correctly at the C specification level and lower, and (2) abstraction (refinement’s dual, upwards) of the kernel’s functional specification to a form suitable for SMT-based automated verification of the user-level seL4 Microkit and Lions OS service components built on top it. Here I will lay out the research and engineering challenges facing us on both these fronts and the planned subprojects for which we are seeking talented PhD students, postdocs and engineers to tackle them.

Johannes Åman Pohjola (UNSW)

Pancake: a language for verification-friendly systems programming

We introduce Pancake, an in-development language for verifiable, low-level systems programming, especially device drivers. Pancake features a very simple type system that makes it attractive to systems programmers, while at the same time aiming to ease the formal verification of code. Pancake has a well-defined semantics which the compiler is proven to preserve, meaning that each generated binary code preserves the semantics of its original program. We will discuss the design of the language, how we believe it eases verification, and how exactly we plan to verify Pancake programs. There will be device registers, there will be coalgebras—there’s something for everybody!

Gabriel Nunes (Macquarie University)

The Privacy-Utility Trade-off in the Topics API

Third-party cookies have been a privacy concern since cookies were first developed in the mid 1990s, but more strict cookie policies were only introduced by Internet browser vendors in the early 2010s. More recently, due to regulatory changes, browser vendors have started to completely block third-party cookies, with both Firefox and Safari already compliant.

The Topics API is being proposed by Google as an additional and less intrusive source of information for interest-based advertising (IBA), following the upcoming deprecation of third-party cookies. Initial results published by Google estimate the probability of a correct re-identification of a random individual would be below 3% while still supporting IBA.

We analyze the re-identification risk for individual Internet users introduced by the Topics API from the perspective of Quantitative Information Flow (QIF), an information- and decision-theoretic framework. Our model allows a theoretical analysis of both privacy and utility aspects of the API and their trade-off, and we show that the Topics API does have better privacy than third-party cookies while providing high utility to IBA companies.

Luigi D. C. Soares (Macquarie University)

Privacy Risk Assessment for Open Banking

The term “open banking” describes a series of global initiatives to allow the sharing of customer data between financial companies to facilitate competition within their sector. In this project, we formalise in the rigorous framework of quantitative information flow (QIF) relevant privacy risks in a concrete open-banking scenario, namely: (i) customer re-identification and transaction-history recovery and (ii) collateral attribute-inferences using external correlations. We provide extensive analyses of these risks in real-world data from open banking, supplied by a fintech in Australia. We show that the open-banking system studied presents considerable privacy risks with respect to transactions, both in the presence and in the absence of demographic data. Finally, we exemplify potential real-world collateral attribute-inference attacks, in which we show how an attacker might leverage scientific correlations to infer individuals’ level of neuroticism and self-control from their transaction history. We hope that this work may: (i) help financial customers in Australia make better-informed decisions about what kind of information, and how much of it, to share via open banking; (ii) raise awareness about the potential privacy risks of open banking in other countries; and (iii) foster the development of privacy regulation in digital finance and the open data economy.

Zhongkui Ma (UQ)

ReLU Hull Approximation

Neural networks have offered distinct advantages over traditional techniques. However, the opaque neural networks render their performance vulnerable, in the presence of adversarial samples. This underscores the imperative of formal verification of neural networks, especially in the safety-critical domain. Deep neural networks are composed of multiple hidden layers with neurons, where mathematical operations stack linear and nonlinear (activation functions) operations. Using linear inequalities plays a crucial role in constraining and deducing the ranges of results from nonlinear operations. Considering correlations among input variables of multiple neurons leads to constraints known as multi-neuron constraints, posing a non-trivial high-dimensional challenge in computing the convex hull of functions. Our work is dedicated to designing methods for computing multi-neuron constraints for the ReLU function to serve the robustness verification of neural networks. We have introduced a novel approach WRALU (Wrapping ReLU) for computing the convex hull of a ReLU function (published in POPL’24). This method significantly reduces computation time and complexity, constructing fewer constraints to achieve more precise approximations while handling higher dimensions.

James Tobler (University of Melbourne/DSTG)

Formally Verifying Robustness Certification for Neural Networks in Dafny

Neural networks are often susceptible to minor perturbations in input that can cause them to misclassify. A prominent solution to this problem is the use of globally-robust neural networks, which employ a certification function to check whether the classification of a given output cannot be altered by such a perturbation. Outputs that pass this test are called “certified robust” and are considered safe to return. However, these certification functions have not yet been verified at the implementation level, and they often rely on approximation-based algorithms that do not guarantee soundness. To provide assurance that a given output is robust, we implemented and verified a certification function for globally-robust neural networks in Dafny. This presentation describes an overview of the program, the specifications verified, the important design decisions taken for the implementation, and an evaluation of its performance and completeness.