Research Project: Guidelines and Deliverables

This page outlines the goals of the project part of the module, discusses their assessment and lists some high-level ideas. The projects are meant to be completed in teams of one or two.

This part of the is open-ended: you are encouraged to explore your own ideas in the space of specification and verification of systems and algorithms.

The most important part for the project is to be interesting, related to specification and verification of algorithms/systems, and to be developed to a certain level of maturity. For instance, if you are specifying a real-world system in TLA+, you may wish to break it to multiple components and work on them separately to have some of them fully specified and model-checked at the end, while the others being sketched enough to be convincing. When you pick your specification/verification target, make sure that there is no available formalisations on the internet. In your report you will have to focus on the simplifications/assumptions you’ve made to encode your model in a formal framework.

You are not required to use one of the tools covered in the module (TLA+/Z3/Dafny): projects developed using other frameworks for formal reasoning, such as Coq, Isabelle, Ivy, F*, Alloy, etc will be considered given that they satisfy the grading criteria outlined below.

Grading

The research project amounts to 40% of your grade. This score is combined from:

  • Initial project proposal: 5% (why the problem is interesting, why feasible)

  • Code quality: 5% (well-documented, corresponds to the text in the report)

  • Written report: 10% (evaluated based on structure, clarity)

  • Presentation: 10% (you should be able to explain your design choices)

  • Self- and peer evaluation: 10% (based on the peer feedback in case of teams of two)

The deliverables of your projects should be submitted on Canvas. Presentations of the projects will take place some time on or after Sem 2 Week 13 (April 10, 2023).

On Incomplete Deliverables

If your project turned out to be a larger undertaking than you were planning, it is acceptable to have it not fully completed. That said, your final artefact should still present some amount of non-trivial effort, possibly packaged with instructions on how one could build on it; your report should clearly list the obstacles that prevented you from finishing your initially planned agenda.

Some Ideas for Projects

More ideas might be added to the list below.

High-Level System Specifications in TLA+

You can use TLA+ (or a similar framework) for specifying and model-checking a system involving some complex interaction between multiple parties at a certain level of abstractions. Examples include distributed systems, network protocols, financial transactions, DeFi smart contracts, etc. For instance, you can specify and verify the safety and liveness of some variant of Paxos. Relatively easy examples include: Mencius, Egalitarian Paxos, Disk Paxos, or Fast Paxos. Harder examples include BFT, or Stellar.

At the time of this writing the following published distributed systems did not have a machine-checked formalisation (google for the title to find the corresponding paper):

  • Spanner: Google’s Globally Distributed Database

  • Building Consistent Transactions with Inconsistent Replication

  • Chain Replication for Supporting High Throughput and Availability

  • The Chubby Lock Service for Loosely-Coupled Distributed Systems

  • Don’t settle for Eventual: Scalable Causal Consistency for Wide-Area Storage with COPS

  • Making Geo-Replicated Systems Fast as Possible, Consistent when Necessary

  • Dynamo: Amazon’s Highly Available Key-Value Store

  • Byzantine Ordered Consensus without Byzantine Oligarchy

Implementing Custom Problem Solvers using SMT

SMT provides a rich landscape for implementation of custom tools for solving complex contraint-based problems and implementing verification tools. Here are some ideas:

  • A program synthesiser for bit hacks

  • An exploit generator for a simple version of ROP

  • Using Z3 for solving CTF challenges

Specifying and Verifying Algorithms in Dafny

A typical case study in Dafny would be an “interesting” verified data structure with a number of methods/functions along with their non-trivial specifications. The list of such data structures includes (but is not limited to):

A good source of data structures to specify and verify can be found in the literature on databases.

As an alternative to that, you may want to pick a “hard” problem from LeetCode, implement it in Dafny and verify its solution with regard to logical specification paraphrasing its description given in plain English.