How AWS’s Automated Reasoning Group helps make AWS and other Amazon products more secure

Data breaches have seemingly become part of everyday digital life. In the past few years many large financial services firms, among others, have been hit with data breaches. In fact, the research firm Risk Based Security reports that in the first nine months of 2019, medical services, retailers, and government agencies suffered 5,183 data breaches, opening 7.9 billion records to theft or other nefarious purposes.

Security is the top priority for AWS, the world’s most comprehensive and broadly adopted cloud platform. In addition to an abundance of security resources and expert guidance, AWS has a (not so) secret weapon that helps protect the company and its customers—automated reasoning. Automated reasoning applications help detect against unauthorized access, improve network security, and ensure software compatibility.

In response to the rapid scale of cloud growth, AWS invested in automated reasoning as a way to provide higher security assurance at scale. Five years ago, Byron Cook, senior principal scientist, established the Automated Reasoning Group (ARG) within AWS. Considered by many as the strongest team in its field, ARG began to create and implement automated reasoning tools to secure AWS’s own infrastructure and services, as well as those of AWS customers.

Automated reasoning is a sub-field of artificial intelligence; it applies mathematical analysis to better understand complex computer systems or large code bases. The technique takes a system and a question you might have about the system—like “is the system memory safe?”—and reformulates the question as a set of mathematical properties.

While AI is very good at sorting unstructured data – picking out photos of cats from thousands of animal photos, for instance – automated reasoning can be used for more abstract and less clearly defined tasks, such as who should or should not have access to a certain set of data.

In software development, automated reasoning replaces laborious and possible flawed testing with a rigorous mathematical proof that the software will function properly and securely, such as ensuring that data structures are correct.

“Automated reasoning is a way to quickly analyze infinite or very large-scale state spaces,” says Cook. “It does so by using high-school algebra to push symbols around.”

In concept, automated reasoning dates to the 19^th century and the work of George Boole, whose work on Boolean Logic – with its variables of true and false – laid the foundation for all modern programming languages.

“Automated reasoning doesn’t look at data, but instead looks for things where we know there is a definite set of rules,” adds Neha Rungta, a senior principal applied scientist and former NASA research scientist. “It asks, ‘Given our specifications, is there a case where something unexpected can happen?’

“It doesn’t need data, or logs, or who has accessed things in the past. It just looks at your configurations [and] your policies. Because of the rules we’ve encoded, it can very quickly tell you who outside your account has access.”

In just a few years, the team’s automated reasoning tools have been applied to a broad range of challenges in networking, access control permissions, automated compliance verification, and analyzing code bases for some of AWS’s most prominent services. Most recently, ARG released a new service capability called IAM Access Analyzer. Access Analyzer is a capability of AWS IAM, and makes it easier for customers to spot holes in their policies that would grant overly broad access to their resources or data. In turn, security teams use these findings to determine whether this introduces unintended risk.

For example, policies may prohibit engineers from accessing a company’s key financial information, or financial people from seeing engineers’ work. IAM Access Analyzer applies logic and mathematical inference to determine all possible access paths allowed by a resource policy. Once the policy is written, IAM Access Analyzer monitors data pathways without human intervention.

Automated reasoning is also under the hood of Amazon S3, providing industry-leading security to Amazon’s popular cloud-storage service.

Says Cook: “Data security is certainly one of the top three pain points for the tech industry – a headline about a data breach in a newspaper is pretty much a daily occurrence. It has been a priority of ours to put features in place to make sure our AWS customers’ resource policies are correctly configured.”

In addition to AWS, automated reasoning is being used across Amazon. Amazon Prime Video, for instance, uses the technology to check software updates to ensure the update doesn’t “break” a user’s device – a challenging task given all the devices now available.

”Our automated code review analyzer, Coastguard, uses automated reasoning to help third-party device manufacturers integrate Prime Video’s app correctly, before their devices hit stores or customer’s homes,” says Jim Christy, software development manager for Prime Video. “Getting the native client code right the first time is mission critical. Coastguard analyzes third-party integration code and detects when it has integrated incorrectly.”

Interest in automated reasoning solutions is increasing, especially now as more businesses transition workloads to the cloud as a result of the coronavirus pandemic.

“Automated reasoning helps our customers maintain security as they scale up,” says Reto Kramer, ARG director. “Lots of our users want to focus on their own business problems, not understanding the nuances of resources policies. With automated reasoning, we can give them cloud security that they’re comfortable with. It has really been a game-changer.”

Since its inception, ARG has invested both in conferences focused on automated reasoning (FMCAD, PLDI, etc.) and specific professors that are pushing the edges of the field. By hiring a diverse class of interns annually, ARG has influenced the makeup of the field and built strong ties across the community. In 2018, ARG launched an initiative called Provable Security, a collective reference to the tools, features, thought leadership and community of experts in the automated reasoning field that had made their way to ARG.

“We have the dream team,” Cook says. “At AWS we have perhaps 50 PhD interns this year alone, with seven different teams doing work. We’ve hired some of the foremost practitioners in the world; individuals with backgrounds at NASA, and similar organizations.”

Adds Rungta: “Automated reasoning has caused a shift in the mindset of our engineers. I get emails every day from engineers asking, ‘Can we use automated reasoning for my project?’ Its power is that you don’t have to test things and hope it works. If you run an automated reasoning tool your task will always be accomplished as specified.”

She predicts automated reasoning will have a huge impact on technology in the years to come, not only in fields such as cloud security, but in machine learning, threat detection, autonomous vehicles or aircraft, the Internet of Things, and much more.

“We’re just at the start of this journey,” says Rungta. “In a hyper-connected world, automated reasoning will be so integral that we won’t even be talking about what it is, just like nobody asks today, ‘What is the internet?’ It will just be part of the system.”

Want to learn more about automated reasoning? Watch this video from AWS re:Invent 2019 where Rungta explains more about how automated reasoning works.