Add “Formal reasoning about the security of Amazon Web Services”

[ghost]

Formal reasoning about the security of Amazon Web Services Byron Cook http://www0.cs.ucl.ac.uk/staff/b.cook/CAV18_invited.pdf

It mention a long list of tools:

External tools that we use include Boogie [1], Coq [4], CBMC [2], CVC4 [5], Dafny [6], HOL-light [8], Infer [9], OpenJML [10], SAW [13], SMACK [14], Souffle [37], TLA+ [15], VCC [16], > and Z3 [17].

I'm not sure what's the best format to include the information so I didn't create a pull request. I'll leave it for @ligurio to decide :)

[ligurio]

Yep, it's worth to add. Thanks! @fracting could you create a PR?

[ghost]

Sorry, I'm not sure what's the best format.

Do you prefer:

TLA+ How Amazon Web Services Uses Formal Methods, Use of Formal Methods at Amazon Web Services CBMC Model Checking Boot Code from AWS Data Centers Various other toolsFormal reasoning about the security of Amazon Web Services

Or do you prefer a long list of tools in details, like:

TLA+ How Amazon Web Services Uses Formal Methods, Use of Formal Methods at Amazon Web Services CBMC Model Checking Boot Code from AWS Data Centers Boogie, Coq, CBMC, CVC4, Dafny, HOL-light, Infer, OpenJML, SAW, SMACK, Souffle, TLA+, VCC, Z3Formal reasoning about the security of Amazon Web Services

Or any other better solution?

[ghost]

I think it's nice to have https://aws.amazon.com/security/provable-security/ in the table as well. I'm just not sure how to organize the information.