Byron Cook, who founded and leads the Automated Reasoning Group at Amazon Web Services (AWS) Security, gave a powerful talk at the Federated Logic Conference in July about how Amazon uses formal methods for ensuring the security of parts of AWS infrastructure. In the past four years, this group of 20+ has progressively hired well-known formal methods experts to face the growing demand inside AWS to develop tools based on formal verification for reasoning about cloud security.

Cook summarizes very succinctly the challenge his team is addressing at 17:25 in the recording: "How does AWS continues to scale quickly and securely?"

A message that Cook hammers out numerous times in his talk is that "soundness is key". See at 25:05 as he explains that some customers value so much the security guarantees that AWS can offer with formal verification that it justified their move to AWS.

Even closer to what we do with SPARK, he talks at 26:42 about source code verification, and has this amaz(on)ing quote: "Proof is an accelerator for adoption. People are moving orders of magnitude workload more because they're like 'in my own data center I don't have proof' but there they have proofs."

In the companion article that was published at the conference, Cook gives more details about what the team has achieved and where they are heading now:

In  2017  alone  the  security  team  used  deductive  theorem provers or model checking tools to reason about cryptographic protocols/systems, hypervisors, boot-loaders/BIOS/firmware, garbage collectors, and network designs.

In many cases we use formal verification tools continuously to ensure that security is implemented as designed. In this scenario, whenever changes and  updates  to  the  service/feature  are  developed,  the  verification  tool is  reexecuted automatically prior to the deployment of the new version.

The customer reaction to features based on formal reasoning tools has been overwhelmingly  positive,  both  anecdotally  as  well  as  quantitatively.  Calls by AWS services to the automated reasoning tools increased by four orders of magnitude in 2017. With the formal verification tools providing the semantic foundation, customers can make stronger universal statements about their policies and networks and be confident that their assumptions are not violated.

While AWS certainly has unique security challenges that justify a strong investment in security, it's not unique in depending on complex software for its operations. What is unique so far is the level of investment at AWS in formal verification as a means to radically eliminate some security problems, both for them and for their customers.

This is certainly an approach we're eager to support with our own investment in the SPARK technology.