Asphalion is an extension of Velisarios, also implemented in Coq, that supports the verification of hybrid fault-tolerant systems, i.e., systems that combine components that can fail arbitrarily and components that can only crash on failure. To reason about such systems, Asphalion provides a sound knowledge sequent calculus that features both non-trusted and trusted knowledge operators. Using Asphalion we have verified one of the main safety property of the MinBFT landmark protocol. This is joint work with Ivana Vukotic and Paulo Verissimo
Funded Projects
This project comes with funding for the following positions (don't hesitate to contact me for more information):
- an up to 3 years fully-funded postdoctoral position
- a fully-funded PhD position
Design of BFT protocols. We propose to develop novel BFT techniques that are less costly (less replicas and less exchanged messages) than state-of-the-art solutions by relying on trusted components (e.g., secure hardware components such as Intel SGX), and to apply these techniques to develop more efficient and reliable blockchain systems. Moreover, we also propose to developed techniques to turn state-of-the-art BFT protocols into protocols that achieve timeliness guarantees, allowing their integration in real-time applications. A couple of relevant publications: Eurosys 2022; TPDS 2021.
Formal verification of BFT protocols. One way to provide strong correctness guarantees is to use formal verification methods, such as theorem provers to automatically or interactively prove that a piece of software or hardware behaves as intended. Many theorem provers have been developed and improved over the years allowing to do just that, such as Agda, Coq, Isabelle, etc. We propose to make use of the highly expressive Coq or Agda provers to ensure the correctness of these protocols. More precisely, we propose to develop within those provers, support to implement BFT protocols, models to capture the environments in which those protocols execute, as well as proof techniques to guarantee their correctness. A couple of relevant publications: OOPSLA 2019; ESOP 2018.
Other Recent Projects
Velisarios is an extension of EventML, implemented in Coq, that supports the verification of Byzantine fault-tolerant systems, and reasoning about distributed epistemic knowledge. Using Velisarios we have verified the standard agreement safety property of the PBFT landmark protocol. Check out our implementation for details. In the future, we want to support proving properties such as liveness and timeliness, and we want to connect Velisarios with the Verified Software Toolchain (VST) in order to verify the correctness of programs written in C. This is joint work with Ivana Vukotic, Marcus Volp, and Paulo Verissimo
Allen's Partial Equivalence Relation (PER) semantics provides a semantics for Nuprl's type theory that allows one to prove that Nuprl's inference rules are valid, and therefore that Nuprl is consistent. Until our ITP 2014 paper, these proofs were done by hand. In order to formally prove that these rules are correct (and therefore that Nuprl is consistent), we have implemented this PER semantics using the Coq proof assistant. This implementation (1) provides a bridge between Nuprl and Coq, and (2) is the basis for developing certified versions of Nuprl. This is joint work with Abhishek Anand and Mark Bickford.
KeYmaera X is a theorem prover for cyber-physical systems (modeled as hybrid systems) that implements a logic called Differential Dynamic Logic (dL for short). KeYmaera X has a small core thanks a uniform substitution based proof calculus. We have implemented and verified this core in Coq. Check out our implementation for details. This was joint work with Brandon Bohrer and Andre Platzer from CMU, who have implemented and verified KeYmaera's core in Isabelle.
Using our formalization of Nuprl in Coq, we are turning Nuprl into an intuitionistic type theory, i.e., we have proved that some versions of Brouwer's continuity and bar induction principles are valid w.r.t. Nuprl's PER semantics. In order to prove the validity of such continuity principles we have turned Nuprl into a nominal type theory. It remains open whether stronger continuity and bar induction rules are also valid. Moreover, we have also implemented a version of Brouwer's concept of choice sequences on top of Nuprl's underlying digital library of facts and definitions. In addition, the library can now also contain sequences of choices that can be filled over time. We validated standard axioms about choice sequences by turning Nuprl's semantics into a Beth model. This is joint work with Liron Cohen, Mark Bickford, and Robert L. Constable.
EventML is a ML-like constructive specification language that implements a paradigm for verified programming. It gives precedence to the programming task, and also allows programmers to cooperate with a proof assistant in order to structure arguments of correctness. It is designed specifically to cooperate with the Nuprl proof assistant in order to develop correct-by-construction asynchronous protocols. This is joint work with Mark Bickford and Robert L. Constable.
Using EventML, we have specified, synthesized, and verified safety properties of the Multi-Paxos protocol. To do so, we have automated some patterns of reasoning; and to get efficient code, we have built a process optimizer in Nuprl. We are reusing this methodology to develop other provably correct protocols, striving towards more resilient and trustworthy systems. One of our current goal is to verify Byzantine fault tolerant protocols written in C using, among other things, the Verified Software Toolchain (VST). This is joint work with Mark Bickford, Robert L. Constable, Ivana Vukotic, Marcus Volp, and Paulo Verissimo
Programming languages such as SML have sophisticated, flexible and safe type systems. Unfortunately, the type error messages for incorrect programs are confusing. Skalpel implements a promising approach to making type errors easier to understand and fix called type error slicing, in which slices (program points) containing all and only the information needed by the programmer to understand and fix a type error are identified and exhibited. Check out the web page of our project, from which you can download packages for Debian and Red-Hat-based systems as well as a web demo.
Past Projects
Intersection types introduce type polymorphism in a finitary way. Expansion was introduced to recover the principal typing property in such systems. The study of realisability semantics for such systems with expansion might help casting some light on the expansion mechanism.
Reducibility is a method based on realisability semantics where the idea is to interpret types by sets of λ-terms closed under some properties. This method seems promising in generalising diverse properties' proofs of the (typed or untyped) λ-calculus.