Project Offers

Background

With the growth in complexity of algorithms and designs, the importance of formal verification - proving or disproving a set of correctness properties underlying a system - has been raised. Formal verification of correctness properties becomes even more paramount when concurrent and distributed systems are considered. Correctness properties are usually partitioned into safety properties - something bad will not occur - and liveness - something good will eventually happen.

While the verification of safety properties is theoretically well established and ready to be deployed at large scale (e.g. [GHE15]), the ensurance of liveness properties is far less understood though it is as crucial as safety when it comes to the analysis of distributed systems. Researchers from the Australian National University (ANU) and from Data61, CSIRO have formulated an assumption called justness that is claimed to be exactly right for proving a large class of liveness properties [vGH19]. The idea behind justness is that independent parallel components should not block each other from executing enabled actions. Since justness seems to always hold in real-life implementations, it is considered as a warranted replacement of classical fairness assumptions.

Research Questions and Tasks

To promote justness as the fundamental assumption for verifying liveness properties and to provide a scale-able verification framework, the following two problems need to be addressed.

To support our research, the internship aims at the development of a proof theory in the proof assistant Isabelle/HOL [NPW02] for justness-preserving semantic equivalences."requirements: "knowledge of the proof assistant Isabelle/HOL is an advantage, but not a prerequisite; however knowledge in (computational) logic and discrete mathematics is required

References

Contact: P. Höfner peter.hoefner AT anu.edu.au

Background

Formal reasoning for concurrent systems - for example using rely guarantee style reasoning - is complicated as all possible interleavings of the programs running in parallel need to be considered. Concurrent Data Structures (CDSs) are significantly more difficult to design and to verify than their sequential counterparts. The situation becomes even more problematic and verification more intricate (and hence even more indispensable) when the effects of both hardware (e.g. x86-TSO, ARMv8) and software (e.g. C11) weak memory models are considered.

Linearizability-style specification is a standard approach among algorithm designers for deducing correctness when considering weak memory models. However, it has been shown that linearizability does not suffice for this purpose [RDRLV19]. The alternative, called strong linearizability, has its own limitations as not all algorithms satisfy this criterion [RHW11]. We plan to follow the seminal paper [5] and study CDSs structures under weak memory consistency (WMC).

Research Questions and Tasks

The aim of the project is to verify basic concurrent data structures, in particular locks. This could include locks, such as ticket lock, spin lock or the CLH lock. As all locks have identical specifications regarding safety properties, but obviously different implementations, the use of Rely-Guarantee reasoning techniques in combination with a Refinement calculus (RGR) will reveal where the implementations differ. RGR usually guarantees safety (functional correctness), but not liveness properties. These include progress properties and avoidance of starvation, which are of equal importance for CDSs.

To guarantee correctnes and to support proof mechanization, the verification tasks should be carried out in an Isabelle-framework. To guarantee compositionality - an indispensable feature for verifying concurrent systems - a combination of rely-guarantee refinement proofs should be used."reference_dl: "[RDRLV19]<:>Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, Viktor Vafeiadis: On Library Correctness under Weak Memory Consistency. POPL 2019: 68:1-68:31<:>[RHW11]<:>Wojciech Golab, Lisa Higham, Philipp Woelfel: Linearizable Implementations Do Not Suffice for Randomized Distributed Computation. STOCS 2011: 373–382

Requirements: knowledge in the area of interactive theorems proving (e.g. Coq, HOL4 or Isabelle/HOL) is an advantage

Contact: P. Höfner peter.hoefner AT anu.edu.au

Background

Predicate transformer semantics were introduced by Dijkstra [Dij75]. They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two predicates on the state space of the statement. In this sense, predicate transformer semantics are a kind of denotational semantics. Predicate transformer semantics are a reformulation of Floyd–Hoare logic [Flo67,Hoa69]. Whereas Floyd-Hoare logic is presented as a deductive system, predicate transformer semantics (either by weakest-preconditions or by strongest-postconditions) are complete strategies to build valid deductions of Floyd-Hoare logic. In other words, they provide an effective algorithm to reduce the problem of verifying a Hoare triple to the problem of proving a first-order formula.

Predicate transformers have been carried over to cope with concurrent systems [Lam90]

Research Questions and Tasks

Usually predicate transformers are used to prove (partial and total) correctness of programs, i.e. a program yields the desired final result. In a concurrent setting, this assumes that every components 'plays according to the rules'.

The project aims at looking at the possibility of using the same techniques (predicate transformers) to reveal possible attack strategies. That means, given a 'undesired state' - a state an attacker would like to reach - can we calculate a strategy/program for an attacker to achieve this state. Ideally, a theoretical approach should be underlined by concrete examples.

References

Requirements: knowledge in the area of formal verification, e.g. Hoare logic

Contact: P. Höfner peter.hoefner AT anu.edu.au

Background

Relations are among the most ubiquitous concepts in mathematics and computing. Relational calculi have their origin in the late nineteenth century and their initial development was strongly influenced, but then overshadowed, by the advancement of mathematical logic. Around 1940, Alfred Tarski revived the subject by formalising the calculus of binary relations alternatively within the three-variable fragment of first-order logic and as an abstract relation algebra within first-order equational logic Today, relation algebras form an estab- lished field of mathematics with numerous textbooks and research publications.

The relevance of relational calculi in computing has been realised since the early beginnings. Relational approaches had considerable impact on program semantics, refinement and verification through the work of Dijkstra, Hoare, Scott, de Bakker, Back and others. Formal methods like Alloy, B and Z, or Bird and de Moor’s algebraic approach to functional program development are strongly relational. Further applications of relations in computing include data bases, graphs, preference modelling, modal reasoning, linguistics, hardware verification and the design of algorithms. Here, our main motivation is program development and verification.

Research Questions and Tasks

Algorithmic Graph Theory —as taught in many university courses— focuses on the notions of acyclicity and strongly connected components of a graph and the related search algorithms. Our aim is about combining mathematical precision and concision in the context of algorithmic graph theory. Specifically, we use point-free reasoningg about paths in graphs (as opposed to pointwise reasoning about paths between nodes in graphs), resorting to pointwise reasoning only where this is unavoidable.

The aim is to use relation algebra as the basis of a machine-supported formal verification of graph algorithms in order to assess the current state of automated verification systems.

References

Requirements: interest in logic and algebraic reasoning, some experience with interactive theorem provers such as Isabelle/HOL, Coq or HOL is of advantage.

Contact: P. Höfner peter.hoefner AT anu.edu.au

Background

The milli Common Representation Language (mCRL2) [GM14] is a formal specification language (process algebra) with an associated collection of tools offering support for model checking, simulation, state-space generation, as well as for the optimisation and analysis of specifications [CGKSVWW13]. The toolset has been used in countless case studies, including the analysis software for the CERN's Large Hadron Collider, and the IEEE 1394 link layer [Lut97].

While the set of tools for mCRL2 is impressive, the tools fail short when it comes to proof mechanisation. By proof mechanisation we mean support by interactive proof assistants, such as Isabelle/HOL [NPW02].

Mechanising process calculi and process-algebraic models in proof assistants can almost be considered routine. However, a lot of this work focuses on process calculi themselves; little work has been done on mechanising the application of such calculi to the practical verification of network protocols.

Research Questions and Tasks

The aim of this research project is to develop a framework for the process algebra mCRL2 in Isabelle/HOL. This will include the following tasks.

The development should follow modern techniques and guidelines for Isabelle/HOL, e.g. [NK14] Ideally, the project will be submitted to the Archive of Formal Proofs (https://www.isa-afp.org) after successful completion.

References

Requirements: Process algebra, some experience with interactive theorem provers such as Isabelle/HOL, Coq or HOL is of advantage.

Contact: P. Höfner peter.hoefner AT anu.edu.au

Background

Wireless Mesh Networks (WMNs) are a promising technology that is currently being used in a wide range of application areas, including Public Safety, Transportation, Mining, etc. Typically, these networks do not have a central component (router), but each node in the network acts as an independent router, regardless of whether it is connected to another node or not. They allow reconfiguration around broken or blocked paths by ``hopping'' from node to node until the destination is reached. Unfortunately, the performance of current systems often does not live up to the expectations of end users in terms of performance and reliability, as well as ease of deployment and management.

We explore and develop adaptive network protocols and mechanisms for WMNs that can overcome the major performance and reliability limitations of current systems. To support the development of these new protocols, the project also aims at new Formal Methods based techniques, which can provide powerful new tools for the design and evaluation of protocols and can provide critical assurance about protocol correctness and performance.

Research Questions and Tasks

Routing protocol specifications are usually written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. Moreover no formal guarantees can be given based on such a description. The use of Formal Methods such as process algebra avoids these problems, leading not only to a precise description of protocols, but also allowing formal reasoning. The project's work will be in this area; it can include

Requirements: The concrete requirements depend on the chosen topic and the applicant's interests and strengths. An interest in formal methods is a must, though.

Contact: P. Höfner peter.hoefner AT anu.edu.au