Verification of the implementation for the F-PKI Protocol
Background
F-PKI is an enhancement to the HTTPS public-key infrastructure (or web PKI) that gives trust flexibility to both clients and domain owners, and enables certificate authorities (CAs) to enforce stronger security measures. With F-PKI, each domain owner can define a domain policy (specifying, for example, which CAs are authorized to issue certificates for their domain name) and each client can set or choose a validation policy based on trust levels. This enables a property that is sorely needed in today’s Internet: trust heterogeneity. Different parties can express different trust preferences while still being able to verify all certificates.
Goals
F-PKI has been implemented as a external page server written in Go and a external page client browser extension written in JavaScript and Go which is compiled to WebAssembly. The goal of this project is the verify the Go portions of the client extension, which are responsible for the logic of validating certificates, using the Gobra verifier.
In particular, we plan to solve the following problems:
- Verify memory safety for the core components, i.e., show that there are no null-pointer dereferences or data races.
- Formalize and verify the security and correctness goals of the protocol as program specifications
- Find precise specifications for the library calls.
Opportunities
- Contribute to a large, long-term research project at the external page Center for Cyber Trust working with the groups of Adrian Perrig and Peter Müller
- Contribute to a technical solution that helps improve the flexibility of modern networking
- Gain experience in using a state-of-the-art program verifier for a mainstream programming language
Prerequisites
Experience in the following fields would be beneficial:
- The programming language Go
- Program verification (e.g. through the course of the same name)
- HTTP protocols and PKI infrastructure
Contact
Nicolas Klose (Programming Methodology Group)