Semi-automatic verification of instruction sets
View the Project on GitHub https://github.com/katamaran-project
An instruction set architecture (ISA) is an abstract specification of the syntax and semantics of machine code. It defines an envelope of allowed behaviour for CPU designers and a set of assumptions that software designers can rely on.
We are interested in critical safety guarantees of ISAs and more specifically the security guarantees of features such as trusted execution environments , virtual memory, or capability machines. Our long-term goal is to verify with machine checked proofs that security guarantees are upheld by the semantics of all instructions. Moreover, we want to verify these properties in a form that can be used to reason about programs, as a way to ultimately verify security properties of full systems, i.e. hardware combined with software.
Scaling up ISA property proofs raises important proof engineering challenges. For the verification effort to scale reasonably in terms of the size and complexity of the specification and for making it robust to changes, proof automation is a necessity. To this end, we are developing Katamaran, a semi-automated separation logic verifier for the Sail specification language.
Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
Sander Huyghebaert, Steven Keuchel, Coen De Roover and Dominique Devriese
Manuscript, under submission
[pdf]
Verified Symbolic Execution with Kripke Specification Monads (and no Meta-Programming)
Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov and Dominique Devriese
In ICFP 2022: ACM SIGPLAN International Conference on Functional Programming
[pdf]
[doi]
[artifact]
Semi-automatic verification of ISA security guarantees in the form of universal contracts
Sander Huyghebaert, Steven Keuchel and Dominique Devriese
Short paper presented at the workshop on the Security of Software / Hardware Interfaces, SILM’21
[pdf] [slides]
Katamaran: semi-automated verification of ISA specifications
Steven Keuchel, Georgy Lukyanov and Dominique Devriese
Extended abstract REMS-DeepSpec 2020 workshop.
[pdf] [slides]