Customers often ask me how AWS maintains security at scale as we continue to grow so rapidly. They want to make sure that their data is secure in the AWS Cloud, and they want to understand how to better secure themselves as they grow.

We have a Shared Responsibility Model at AWS, in which we are responsible for security of the cloud, and you are responsible for security in the cloud. This enables you to focus on strategic efforts while AWS oversees operational tasks.

AWS has millions of active users, each with varying degrees of proficiency in IT security. Many users want to focus on their own customers, rather than understanding the semantic nuances of things like virtual private clouds (VPCs) or resource policies. Luckily, in addition to an abundance of security resources and expert guidance, AWS has a (not so) secret weapon that helps protect us and our customers—automated reasoning.

Automated reasoning is a class of algorithmic techniques that search for mathematical proofs of correctness for complex systems. For example, automated reasoning tools can analyze policies and network architecture configurations and prove the absence of unintended configurations that could potentially expose vulnerable data. We call this provable security. It provides the highest level of assurance possible for critical security characteristics of the cloud, such as access control policies or network exposure of Amazon Elastic Compute Cloud (Amazon EC2) instances. I spoke about automating security at the AWS Santa Clara Summit, and now I want to dive deeper on one way to approach this.

In this post, I will share more about the provable security initiative and its various automated-reasoning-backed technologies, such as Zelkova and Tiros. We apply provable security to our own infrastructure so that we can achieve the highest levels of security while our services rapidly grow. Now, we're bringing this same capability of assurance to you.

Automated reasoning technology

Our Automated Reasoning Group (ARG) applies formal verification techniques in innovative ways to cloud security and compliance for our customers and for our own AWS developers. The group includes experts in automated reasoning who saw this as an opportunity to pioneer the application of their work to the cloud.

Automated reasoning is used to provide higher levels of security assurance for core AWS code used by our internal teams, as well as in tools that are customer accessible across a variety of AWS security services. Let's take a closer look at two of these tools, Zelkova and Tiros.

Zelkova

Zelkova is a technology that provides customers with continuous insight into their access control permissions, alerting them anytime there is a violation of security best practices.

Zelkova does this by using automated reasoning to analyze policies, such as those used for AWS Identity and Access Management (IAM) and Amazon Simple Storage Service (Amazon S3). These define permissions and dictate what each user can (or can't) do. Zelkova translates policies into precise mathematical language and then uses automated reasoning tools to check their properties.

These tools include automated reasoners called Satisfiability Modulo Theories (SMT) solvers, which automatically prove or disprove formulas over constants, strings, regular expressions, dates, and IP addresses from the policies. Zelkova can make broad statements about all resource requests because it's based on mathematics and proofs instead of heuristics, pattern matching, or simulation.

Zelkova can help customers meet their security and compliance responsibilities. For example, Amazon S3 uses Zelkova to check each bucket policy and warns customers if an unauthorized user is able to read or write to their bucket. When a bucket is "public," that means there are some public requests that are allowed to access the bucket. If a bucket is "not public," all public requests are denied. This allows you to easily identify potential access management issues.

As another example, Zelkova powers the Amazon S3 Block Public Access feature. Block Public Access disables public access control lists (ACLs) on buckets and objects in Amazon S3. It also prevents bucket policies that would allow public access. For existing policies that allow public access, the feature disallows access from outside of the bucket's account.

Zelkova is also used in:

• AWS Config, a service that enables users to assess, audit, and evaluate the configurations of their AWS resources. AWS Config continuously audits AWS resource configurations and now includes Zelkova-based managed rules, such as:
  • s3-bucket-public-read-prohibited
  • s3-bucket-public-write-prohibited
  • s3-bucket-server-side-encryption-enabled
  • s3-bucket-ssl-requests-only
  • lambda-function-public-access-prohibited
• AWS Trusted Advisor, an online tool that provides users real-time guidance to help them provision their resources following AWS best practices. AWS Trusted Advisor helps improve the security of a customer's AWS environment, including analyzing resource policies.
• Amazon Macie, a security service that uses machine learning to automatically discover, classify, and protect sensitive data in AWS.
• Amazon GuardDuty, a threat detection service that continuously monitors for malicious activity and unauthorized behavior to help protect your AWS accounts and workloads.
• AWS IoT Device Defender, a service that helps customers secure their fleet of IoT devices. AWS IoT Device Defender continuously audits a customer's IoT configurations to make sure that they aren't deviating from security best practices.

Tiros

Tiros is another tool built with automated reasoning technology. Tiros maps the connections between network mechanisms, including accessibility from the open internet.

For a large company, it's critical to ensure that sensitive data is secure, but confirming all possible data paths and associated controls manually can take months or even years. Tiros can check all network pathways and data permission levels in milliseconds. In addition to using Tiros to help secure our own infrastructure, Tiros is also used in products available to you, such as Amazon Inspector.

One of the most important benefits of Zelkova and Tiros is that users can leverage these tools to help identify gaps in the design phase before any data is exposed. Furthermore, this technology is automated, removing manual human intervention to help provide greater scalability. Finally, it's provable—by converting the problem into a logic-based mathematical equation, it can be proven with mathematical certainty.

Looking ahead

Automated reasoning is now helping AWS customers protect their environments worldwide—and it's just the beginning for this technology. The AWS ARG team is always looking to the future and has plans for more projects that will advance cloud security further, such as automating compliance verification.

For example, a mathematical proof can be used to prove that there's no instance of a weak key being used anywhere in the entire system. That's a much higher bar than just having a "reasonable assurance" of no weak keys, which is the objective that auditors traditionally use.

With previous tools, auditors could not evaluate all of the code in all possible configurations, nor could they evaluate instances where keys were being used. With automated reasoning, customers can use a proof to examine the entire system for a certain value to gain insight into their environments. This creates a higher standard for security beyond today's advanced control measures, such as automated controls, preventive controls, or detective controls.

We (and our auditors) are really excited about this possibility. Systems are becoming immensely complex and it's getting harder to test environments using traditional methods—now mathematical proofs can do it for us.

Summary

Understanding how to scale security in the cloud is just one of the IT security challenges organizations are tackling today. Cloud security continues to evolve with each innovation, such as automated reasoning applications. It's critical that our community of builders understand these changes and what it means for the security of your respective organizations.

That's why AWS has created a new annual conference focused on cloud security: AWS re:Inforce. Taking place June 25-26 at the Boston Convention and Exhibition Center, attendees of AWS re:Inforce can expect two full days of security, identity, and compliance learning and community building.

For anyone interested in learning more about automated reasoning and provable security, this is a great opportunity to get the latest updates from our experts. Chad Woolf, AWS VP of Security Assurance, and Byron Cook, Director of the AWS ARG, will sit down with a representative from Coalfire, one of AWS' independent security assessors. Their session will cover how the Provable Security initiative is creating new, higher-assurance models for auditors and customers. Byron will also be giving a session that dives deeper into the fundamentals of how logic is used in provable security technologies. Finally, ARG Principal Engineer, Neha Rungta, will be speaking with Distinguished Security Engineer Eric Brandwine about how provable security started and quickly grew at AWS.

Check out our web site for more information on provable security.

We hope to see you at AWS re:Inforce this year!