The formal methods work on CHERI coming out of the REMS project has been amazing. Peter Sewell’s team has done a fantastic job of producing proofs that are actually useful. The first step was forcing us to properly define the claims that we were making. What does it mean for capabilities to never increase in rights? Sealing and unsealing are a counter-example to the naive interpretation (an unsealed capability, by design, has more rights than the sealed one, but not more rights than the capability that was used to construct the sealed one). Similarly, when we say that reachable memory is defined by the transitive closure of memory reachable from the capabilities in your register file, there are some exceptions when you consider the entire machine model: when you take an exception, you transition to privileged mode, which has access to some other registers and so the reachable memory increases (again, by design - privileged mode should have access to more memory).
They’ve built a model of various ISAs that can run as an interpreter (working as a golden model - the official RISC-V spec is based on this work) and can be exported to various theorem provers to allow proofs on properties of both individual instructions and on sequences of instructions. The more complex security proofs are all built on this.
Going from a spec of the architecture to a proof that an implementation corresponds to the architecture is a lot more work but hopefully they’ll get funding to start addressing that gap. Even without that, using the gold model for tandem verification (run the same sequence of instructions through it and a simulation of the HDL and looking for places where they diverge) is great, especially when driven by fuzzing over the instruction set. They did some quite neat work here on spec-coverage-directed fuzzing, ensuring that every branch in the code in the specification is covered by the test suite. That doesn’t guarantee correctness (two inputs that do the same in the spec may diverge in the implementation and not be caught) but it does give quite a lot of confidence.
I don’t work on the formal side of the project at all. I believe Sail exports to Isabelle, HOL4 and Coq. Sail also integrates with Z3 and so simple proofs can be done with just the SMT solver. Robert Norton-Wright, on my team, has used this to validate some properties of the capability encoding. For simple stand-alone things you can write them directly in Sail and have Z3 check them.
The formal methods work on CHERI coming out of the REMS project has been amazing. Peter Sewell’s team has done a fantastic job of producing proofs that are actually useful. The first step was forcing us to properly define the claims that we were making. What does it mean for capabilities to never increase in rights? Sealing and unsealing are a counter-example to the naive interpretation (an unsealed capability, by design, has more rights than the sealed one, but not more rights than the capability that was used to construct the sealed one). Similarly, when we say that reachable memory is defined by the transitive closure of memory reachable from the capabilities in your register file, there are some exceptions when you consider the entire machine model: when you take an exception, you transition to privileged mode, which has access to some other registers and so the reachable memory increases (again, by design - privileged mode should have access to more memory).
They’ve built a model of various ISAs that can run as an interpreter (working as a golden model - the official RISC-V spec is based on this work) and can be exported to various theorem provers to allow proofs on properties of both individual instructions and on sequences of instructions. The more complex security proofs are all built on this.
Going from a spec of the architecture to a proof that an implementation corresponds to the architecture is a lot more work but hopefully they’ll get funding to start addressing that gap. Even without that, using the gold model for tandem verification (run the same sequence of instructions through it and a simulation of the HDL and looking for places where they diverge) is great, especially when driven by fuzzing over the instruction set. They did some quite neat work here on spec-coverage-directed fuzzing, ensuring that every branch in the code in the specification is covered by the test suite. That doesn’t guarantee correctness (two inputs that do the same in the spec may diverge in the implementation and not be caught) but it does give quite a lot of confidence.
Do you work in anything related to CHERI?
Edit: I note from your profile you do.
What theorem provers do you use? I saw some slides that referred to Isabelle and Coq.
Do program analysis or model checking have any role in the project?
I don’t work on the formal side of the project at all. I believe Sail exports to Isabelle, HOL4 and Coq. Sail also integrates with Z3 and so simple proofs can be done with just the SMT solver. Robert Norton-Wright, on my team, has used this to validate some properties of the capability encoding. For simple stand-alone things you can write them directly in Sail and have Z3 check them.