AWS re:Invent 2016: Automated Formal Reasoning About AWS Systems (SEC401)

Опубликовано 1 декабря 2016, 22:04

Automatic and semiautomatic mechanical theorem provers are now being used within AWS to find proofs in mathematical logic that establish desired properties of key AWS components. In this session, we outline these efforts and discuss how mechanical theorem provers are used to replay found proofs of desired properties when software artifacts or networks are modified, thus helping provide security throughout the lifetime of the AWS system. We consider these use cases:

*Using constraint solving to show that VPCs have desired safety properties, and maintaining this continuously at each change to the VPC

*Using automatic mechanical theorem provers to prove that s2n’s HMAC is correct and maintaining this continuously at each change to the s2n source code

*Using semi-automatic mechanical theorem provers to prove desired safety properties of protocols and code