I am very happy to announce that from September 2018 I will be a Marie-Curie Fellow at Imperial College. My project “Verification through Security and Progress Abstractions” (VeSPA) was awarded a Marie-Curie Individual Fellowship for 2 years. I will be working with Philippa Gardner to explore new ways to effectively prove Progress (aka liveness) and Security (eg. secrecy) of concurrent programs.
I will be posting updates on the project here, so watch this space!
With the growing number of sensitive tasks that we delegate to algorithms, the development of methods to certify their trustworthiness is of paramount importance. The VeSPA project is grounded in formal methods: the challenge is to certify correctness criteria with a mathematically rigorous—and, ideally, automatically produced—proof. Modern technology is characterised by a shift of paradigm: the view of computation as carried out by a single agent as a sequence of steps transforming some input into some output—aka sequential computation—is not a satisfactory model of real-world systems anymore. Instead, we are increasingly relying on software that is organised as a decentralised collection of interacting components: our mobile phones, web servers, even our watches. Computation/services carried out by a dynamic network of interacting components is what we call concurrent computation. Our trust in these systems relies on a range of interdependent properties:
- Safety: nothing bad can ever happen. Can the system crash?
- Progress: something good eventually happens. Will the system be reactive to requests?
- Security: no secret is ever leaked. Does the system protect sensitive information from intruders?
Analysing these properties is vastly more complicated for concurrent software: the decentralised interaction between processes introduces much more subtle behaviour than what is found in sequential centralised computation. This superior complexity is reflected by the level of formal methods adoption by the industry. Success stories such as Facebook’s Infer and Microsoft SLAM typically focus on safety of essentially sequential programs. Concurrency-related aspects are either grossly over-approximated, ignored, or handled by informal arguments. The main reason for this disconnect is what I call the analysis scalability problem. A proof certifying safety of a concurrent system needs to take into consideration all possible executions, sometimes in an open environment. The space of all possible interactions and interferences is so large and complex that we lack proper tools to reason about it, both manually and automatically. In other words, our understanding of concurrency does not scale, yet.
Concurrent software is difficult: difficult to design, to understand, and to formally analyse. Software engineers have developed a number of patterns, strategies, practices to help designing concurrent software. Two invaluable principles used to tame the complexity of design are:
Locality & Composition
Software should be the composition of loosely-coupled components interacting in a local way. More concretely, a component should affect and be affected by a well-identified set of resources and processes; thus avoiding global effects, which give rise to unmanageable monolithic systems. The behaviour of a composite system should be a simple composition of the behaviour of the individual components.
I call this a compositional design.
Software is built on top of other software. The functionality of a component should be packaged into an external interface which hides the specific internal implementation choices. The software component thus becomes reusable.
I call this a modular design.
The VeSPA approach is to promote these principles from guides to the design, to strategies for proving correctness, of systems. Specifically, a proof for a software component should be as compositional as the design of the system. It should also be as reusable as the software component. By making proofs compositional and modular, we can solve the analysis scalability problem: proving a system correct has the same complexity as designing it. Proving the interaction of loosely-coupled components correct would be done by composing loosely-coupled proofs. Reusing a software component would allow its correctness proof to be reused. Thanks to abstraction, re-implementations of a software component which satisfy the same external interface would only require to re-prove correctness of the component, but not of the component that use its external interface.
To realise this vision, VeSPA attacks the analysis scalability problem for Progress and Security of concurrent software, from the point of view of Verified Specification. A specification is a formalisation of the intended behaviour of a software component. A specification is verified against a component, when there is formal proof that the component indeed has the behaviour described by the specification. The design of specifications is crucial in supporting Locality&Composition and Abstraction. Current specification formats for concurrent systems fundamentally lack these characteristics, especially if one considers Progress and Security. VeSPA’s line of attack is based on a synergy between insights gained in my previous work and Gardner’s.
For more on the project watch this space!