SaTC: CORE: Small: Automating the End-to-End Verification of Security Protocol Implementations

The world critically depends on a wide variety of security protocols for properties such as authentication, secure communication, commerce, anonymity, and group messaging. Although widely deployed, these protocols are brittle, with regular, high-profile vulnerabilities discovered each year. When the complexities of high performance implementation meet the complexities of cryptographic protocol reasoning, such vulnerabilities seem inevitable.

However, this project's foundational work on developing provably secure protocol implementations will help secure basic infrastructure that is used ubiquitously in all sectors, including industry, education, and national security. Results from this research will also be incorporated into graduate and undergraduate security and verification courses taught by the researchers, and they will develop various outreach programs to educate K-12 students and teachers, as well as the general public, about online security.

In more detail, this project will create a protocol-verification framework that achieves end-to-end verification results in a largely automated fashion. Unlike prior monolithic tools for verifying security protocols, the framework will be inherently modular. Since modular proofs are built upon abstractions of protocols, this will enable non-experts to securely iterate on protocols without needing to grasp all lower-level details below the abstraction.

By lowering the barrier to entry for developing secure protocols, the framework will enable more proofs of protocols from a wider community of developers. Second, the framework will be the first tool to prove the security of protocols in the computational model (the cryptographic "gold standard") using information-flow typing for a wide range of cryptographic mechanisms.

Finally, the project will also develop automation that takes in a protocol description and synthesizes a verifiably secure protocol implementation

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.