Cryptographic Protocol Verification in AWS
Presented as part of the 2020 HCSS conference.
|
In this talk, I will describe how Amazon Web Services verifies the cryptographic protocols that are used to secure its cloud platform. This verification is accomplished through the mechanization of cryptographic security proofs in the computational model. In some cases, we mechanize proofs in existing tools, such as EasyCrypt. In order to reason about complex protocols, we developed Quivela, which is capable of proving asymptotic indistinguishability between real and ideal functionalities in a universally composable setting. Verified protocols include the domain management protocol used by the AWS Key Management Service, and the compromise-resilient signature protocol that authenticates all AWS requests. |
Protocol verification is a useful component of design/architecture verification at AWS, and it allows us to identify issues in existing designs, and explore alternatives in new designs. By producing verified protocol models, we also get closer to the eventual goal of a fully verified design and implementation, in which the model serves as a functional specification for the implementation.
Adam Petcher is an applied scientist at Amazon Web Services who specializes in cryptography and formal verification. His current work is in the area of machine-checked cryptographic proofs and the formal verification of cryptographic implementations. Prior to AWS, Adam worked on applied cryptography at Oracle and MIT Lincoln Laboratory.