Formal Verification of Distributed Components – PiCoq

The ubiquitous role played by software makes it necessary to analyse its
properties in a rigourous manner, to state and prove guarantees about its
behaviour. However, an important part of modern software often consists in
large distributed systems, with mobility or reconfiguration capabilities. By
essence, such systems are almost impossible to analyse in a direct and global
way: proofs on paper are not tractable, and automatic model-checking
techniques are not expressive enough, or reach their limits because of state
explosion.

Research in concurrency theory and process algebras has developed formal
models for the description of many aspects of distributed programming.
Abstract primitives have been proposed to model, at a foundational level,
phenomena like distribution, higher-order communication, mobility, or
component update. To some extent, behavioural theories have been built in
order to state and prove properties of such systems, but work is needed to
develop these into a corpus of powerful and actually usable proof techniques.

Moreover, the need for rigourous guarantees justifies the use of formal
methods, to certify the behaviour of a given system. While writing
computer-certified proofs has long been considered as an exercise involving
"academic-size" proofs, recent work has confirmed that theorem provers are now
mature enough to deal with large proofs, be it proofs of complex results in
mathematics or proofs about programming language semantics (Gonthier and
Werner's proof of the 4 colour theorem, which required the development of
sophisticated prover technology, or the certified compiler developed in the
ANR project Compcert). While the state of the art is rather advanced for
sequential languages, tools for mechanical reasoning within a theorem prover
about concurrent and distributed systems are currently missing.

We propose in PiCoq to improve this situation by developing an environment for
the formal verification of properties of distributed, component-based
programs. Our approach lies at the interface between two research areas:
concurrency theory and proof assistants.

Achieving our goal relies on three scientific advances.

1. Find mathematical frameworks that ease modular reasoning about concurrent
and distributed systems: due to their large size and complex interactions,
distributed systems cannot be analysed in a global way. They have to be
decomposed into modular components, whose individual behaviour can be
understood.

2. Improve existing proof techniques for distributed/modular systems: while
behavioural theories of first-order concurrent languages are well understood,
this is not the case for higher-order ones. We also need to generalise
well-known modular techniques that have been developed for first-order
languages to facilitate formalisation in a proof assistant, where source code
redundancies should be avoided.

3. Define core calculi that both reflect concrete practice in distributed
component programming and enjoy nice properties w.r.t. behavioural
equivalences. This is closely related to point 2, as the proof techniques
available for a given language strongly depend on the interaction of its
primitives with behavioural equivalences.

Beyond these theoretical advances, we expect the development of the proof
environment itself to be quite challenging, as it will require several
sophisticated proof-engineering techniques such as the handling of binders,
implementation of tactics to solve automatically decidable statements, or
smart usage of modules to make the code readable and reusable.

Finally, we will validate the developed tools by certifying some proofs about
distributed component systems. Our validation will be threefold: formalise
classic and recent articles about distributed systems, give a formal
specification of a calculus that closely reflects a component model, and prove
the correctness of a distributed abstract machine.