alt Hacker NewsAnd what teams use these methods exactly?
Replies
jmccarthy • last Tuesday at 11:23 PM
https://aws.amazon.com/verified-permissions/ (AVP) is a team and product which uses the formally verified Cedar language. https://arxiv.org/abs/2403.04651
And what teams use these methods exactly?
https://aws.amazon.com/verified-permissions/ (AVP) is a team and product which uses the formally verified Cedar language. https://arxiv.org/abs/2403.04651
The article directly mentions several.
> Teams across AWS that build some of its flagship products—from storage (e.g., Amazon S3, EBS), to databases (e.g., Amazon DynamoDB, MemoryDB, Aurora), to compute (e.g., EC2, IoT)—have been using P to reason about the correctness of their system designs.
Later it more specifically mentions these (I probably missed a few):
S3 index, S3 ShardStore, Firecracker VMM, Aurora DB engine commit protocol, The RSA implementation on Graviton2
(EDIT: formatting)