Zappa for Correctly Implementing CPSA Analyzed Protocols

ABSTRACT

The Cryptographic Protocol Shapes Analyzer CPSA determines if a cryptographic protocol achieves authentication and secrecy goals.  It can be difficult to ensure that an implementation of a protocol matches up with what CPSA analyzed, and therefore be sure the implementation achieves the security goals determined by CPSA.

Zappac is a compiler that translates a role in a protocol into a Rust procedure, and when it is compiled and linked with a Zappa runtime system, produces a program that achieves the security goals determined by CPSA.  We describe Zappa and how it implements advanced features of CPSA such as mutable state.

The entire Zappa system is implemented in Rust.  Besides providing memory safety via Rust's type system, the use of Rust allowed us to factor the code so that implementors of runtime systems have a great amount of flexibility.  The compiler produces instructions that are defined by a trait, and so runtime systems get to choose how to implement them.  In fact, the Zappa system has two very different libraries for constructing runtime systems.  These libraries support message wire formats based on ASN.1 and canonical S-Expressions.

Formal methods have not been used to verify the Zappa system. However, there are several reasons we believe Zappa-generated role implementations deserve more trust than implementations produced by hand.  (1) The algorithm used by the Zappa compiler is based on the formally verified Roletran compiler that is included in a CPSA distribution.  (2) The implementation of the instructions produced by the compiler is fairly straightforward.  Thus we believe the use of the Zappa system greatly improves confidence in the implementation of protocol roles analyzed by CPSA.

This talk is aimed at the Protocol Verification topic, specifically on the verification of implementations (verifying that the code correctly implements the specification).

Author

Dr. John D. Ramsdell is a Principal Cybersecurity Engineer at the MITRE Corporation.  He was educated at Cornell and Harvard Universities.  He has made contributions on such diverse subjects such as graph theory for numerical analysis, instant messaging, verification of implementations of programming languages, remote attestation, information flow, and cryptographic protocol analysis. Dr. Ramsdell has authored or co-authored about 25 academic publications.