Modeling and Verification of Distributed Systems
Distributed systems, including secure networking, security protocols, distributed database systems, and replication algorithms, are interesting targets for formal modeling and verification.
Using several stepwise refinement, we can derive models of such systems that are correct by construction from abstract, often centralized, specifications. Such a development may involve several steps until we get to a sufficiently detailed model that can serve as the basis for an implementation. Global properties proven for any of these models are preserved through further refinements. We have embedded a theory of refinement in the interactive theorem prover Isabelle/HOL to support this process.
We have recently proposed a methodology, called Igloo, which allows us to decompose a sufficiently detailed model into different component models, which we then further transform into program specifications (formulated in separation logic, which is a form of Hoare logic suitable for reasoning about heap data structures). We can then implement each component and verify it against its program specification using a code verification tool. The Igloo theory ensures that the global properties proved for the models are preserved to the implementation level.
Possible projects
- Formal modeling and verification of consensus protocols or other distributed algorithms
- Formal modeling and verification of concurrency control protocols for distributed database transactions (see also related student project topic)
- Extending the theory of refinement
- Improve Igloo's usability by adding new features and automated tools using Isabelle/ML programming
Desirable Prerequisites for Student Projects
- strong skills in functional programming (e.g. from the FMFP course)
- some familiarity with Isabelle/HOL (e.g. from self-study)
Previous Theses
- Cedric Gebistorf, BSc thesis, Igloo Component Model Transformation in Isabelle/ML
- Sven Wiesner, MSc thesis, Automated Translation of Tamarin Theories into I/O Specifications for Igloo
- Noah Delius, MSc thesis, Automatic Generation of I/O Specifications from Component Event Systems in Igloo
- Giuseppe Arcuti, MSc thesis, Automatic Decomposition of Interface Models
- Roman Niggli, BSc thesis, Modeling and Verification of the Raft Consensus Protocol
- Shabnam Ghasemirad, semester project, Modular Reasoning in Igloo
Further Information
Please contact Christoph Sprenger or see the related project page.