The formal verification of entire software systems is one of the grand challenges of computer science. Recently, researchers from Prof. David Basin’s and Prof. Peter Müller’s groups have made significant progress on this challenge.
In a paper at this year’s Object-Oriented Programming, Systems, Languages & Applications conference (OOPSLA’20), they propose a new approach, dubbed Igloo, which soundly links protocol verification with software verification. The Igloo methodology provides strong end-to-end guarantees, meaning that pro
perties proven for abstract models also hold for the implemented systems.
The leading researcher, Dr. Christoph Sprenger, says:
“The main novelty of our approach is that it establishes a sound link between protocol verification based on labeled transition systems and code verification based on separation logics. This enables the combination of state-of-the-art tools from each area: interactive theorem proving in higher-order logic for protocol verification and code verification using modern separation logics, which support advanced programming language features needed for efficient and maintainable code such as heap data structures and concurrency. So far, we support Nagini (for Python) and VeriFast (for Java), but code verifiers for other languages can be integrated with only minimal requirements. Our case studies include distributed algorithms, fault-tolerant systems, and security protocols, where the different components are written in different languages and some employ local concurrency to improve efficiency. Our work contributes towards the formal verification of realistic distributed systems.”
Igloo is expressive, versatile and supports modeling of a wide range of distributed systems using state-of-the-art verification tools. The researchers show the feasibility of the Igloo methodology in several case studies. All results are formalized in a theorem prover. This foundational approach yields strong soundness guarantees.
The full paper as well as the artifact are available online. The presentation introducing Igloo will be available on Youtube following the OOPSLA conference on Nov 21st, 2020.