Reading Time: 3 minutes

Can anyone ssh into an instance in this VPC via a route other than our bastion?

Are any of our objects stored in S3 publicly readable? Writable?

Helping customers answer these questions in the general case and preventing bad configurations from making it into the wild is one of the main themes at AWS’ inaugural Security conference, re:Inforce.

AWS has a Provable Security program that matches what you would expect if you’re familiar with the field:

Using automated reasoning technology, the application of mathematical logic to help answer critical questions about your infrastructure, AWS is able to detect entire classes of misconfigurations that could potentially expose vulnerable data. We call this provable security-absolute assurance in security of the cloud and in the cloud.

AWS Provable Security

What this boils down to is:

  1. (hard) AWS models the states that services and resources can be in along with the actions that people can take
  2. Read the current state of resource configuration from AWS APIs
  3. Use an SMT Solver to ask and answer questions about whether the current configuration would, e.g. permit traffic on port 22 to reach a given instance from a set of traffic sources

Automated reasoning uses math and logic to answer questions as opposed to the standard technique of testing a few scenarios to see if an action is possible. I don’t use the word ‘few’ to diminish the effort of empirically testing 10s, 100s, or even 1000s of conditions. But empirical testing is intractable for a ‘simple’ question when the state space routinely offers, e.g. 9 Billion combinations.

The Provable Security team presented a primer on the field and how all this works at AWS yesterday in ‘The Evolution of Automated Reasoning Technology at AWS (SEP201)‘ (video). I highly recommend that talk for everyone interested in Cloud security as well as the GRC301 talk for a deeper dive.

AWS built a cool tool named Tiros, which is currently internal, but you can harness its power today with:

  • The new S3 features where you can deny public read or write access to data in s3 buckets at an account level
  • The ‘Network Reachability’ rule for AWS Inspector which can answer the first question about ssh access
  • AWS Config rules (8) that can help you detect unwanted configurations or behavior such as:
    • not encrypting access to S3
    • bucket policies adhere to a model s3 bucket policy that you provide
    • lambda functions that are publicly executable

Based on a discussion after one of the Provable Security talks, you can hook into the Tiros automated reasoning engine by creating custom rules that define IAM policies that detect whatever undesirable configuration you’re after. I plan to explore that soon and share what I find.