Read on Twitter
@Werner talked about the significant investments AWS is making in automated reasoning tools "that make it easy for customers to help detect security gaps" in his re:invent keynote.
1/n “IAM Access Analyzer validates that your IAM policies only allow what you intended” @AWSIdentity. Available at no cost, turn it on now to validate there is no unintended access to your S3 buckets and other resources:
2/n IAM Access Analyzer is powered by Zelkova. “Zelkova translates policies into precise mathematical language and then uses automated reasoning tools to check their properties.” How Zelkova works: https://d1.awsstatic.com/Security/pdfs/Semantic_Based_Automated_Reasoning_for_AWS_Access_Policies_Using_SMT.pdf
3/n “Zelkova makes broad statements about all resource requests because its based on mathematics and proves instead of using heuristics”. Powers S3 Block Public Access, AWS Config Managed Rules, AWS Trusted Advisor, Amazon Macie, Amazon GuardDuty, IoT Device Defender, and more.
4/n “S3 Block Public Access allows you to configure bucket permissions as long as they don’t provide unrestricted access to the internet”. Turn on S3 Block Public Access - https://aws.amazon.com/blogs/aws/amazon-s3-block-public-access-another-layer-of-protection-for-your-accounts-and-buckets/
5/n @AndrewGacek describes the automated reasoning technique driving S3 Block Public Access,
6/n "Amazon VPC Reachability Analyzer uses automated reasoning processes to look at your AWS configuration without sending a single packet it can tell if the system is doing what you want it to do." Use it now https://aws.amazon.com/blogs/aws/new-vpc-insights-analyzes-reachability-and-visibility-in-vpcs/
7/n Whats the secret sauce? Its how we transform AWS into Math. Nerd out with this talk on the recipe for the secret sauce
8/n Security Detectors in Amazon CodeGuru use automated reasoning to help you detect security issues - give it a whirl https://aws.amazon.com/blogs/devops/tightening-application-security-with-amazon-codeguru/
9/n How are we using automated reasoning internally? Read about the machine-checked proof of security for AWS Key Management service: https://dl.acm.org/doi/10.1145/3319535.3354228
10/10 To view the journey of taking automated reasoning from an academic curiosity to something that applies at AWS scale watch @byroncook
