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

Amazon scientists are on the cutting edge of using math-based logic to provide better network security, access management, and greater reliability.

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.

Byron Cook
Byron Cook, ARG senior principal scientist

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.

Data security is certainly one of the top three pain points for the tech industry...It has been a priority of ours to put features in place to make sure our AWS customers’ resource policies are correctly configured.
Byron Cook, ARG senior principal scientist

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 19th 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?’

Neha Rungta
Neha Rungta works on formal verification techniques for cloud security within the Amazon Web Services Automated Reasoning Group.

“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.”

Jim Christy
Jim Christy, software development manager, Prime Video

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.”

Reto Kramer
Reto Kramer, ARG director

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.

Related content

US, MA, Boston
The Artificial General Intelligence (AGI) team is looking for a passionate, talented, and inventive Applied Scientist with a strong deep learning background, to build industry-leading technology with Large Language Models (LLMs) and multi-modal systems. You will support projects that work on technologies including multi-modal model alignment, moderation systems and evaluation. Key job responsibilities As an Applied Scientist with the AGI team, you will support the development of novel algorithms and modeling techniques, to advance the state of the art with LLMs. Your work will directly impact our customers in the form of products and services that make use of speech and language technology. You will leverage Amazon’s heterogeneous data sources and large-scale computing resources to accelerate advances in generative artificial intelligence (GenAI). You are also expected to publish in top tier conferences. About the team The AGI team has a mission to push the envelope in LLMs and multimodal systems. Specifically, we focus on model alignment with an aim to maintain safety while not denting utility, in order to provide the best-possible experience for our customers.
IN, HR, Gurugram
We're on a journey to build something new a green field project! Come join our team and build new discovery and shopping products that connect customers with their vehicle of choice. We're looking for a talented Senior Applied Scientist to join our team of product managers, designers, and engineers to design, and build innovative automotive-shopping experiences for our customers. This is a great opportunity for an experienced engineer to design and implement the technology for a new Amazon business. We are looking for a Applied Scientist to design, implement and deliver end-to-end solutions. We are seeking passionate, hands-on, experienced and seasoned Senior Applied Scientist who will be deep in code and algorithms; who are technically strong in building scalable computer vision machine learning systems across item understanding, pose estimation, class imbalanced classifiers, identification and segmentation.. You will drive ideas to products using paradigms such as deep learning, semi supervised learning and dynamic learning. As a Senior Applied Scientist, you will also help lead and mentor our team of applied scientists and engineers. You will take on complex customer problems, distill customer requirements, and then deliver solutions that either leverage existing academic and industrial research or utilize your own out-of-the-box but pragmatic thinking. In addition to coming up with novel solutions and prototypes, you will directly contribute to implementation while you lead. A successful candidate has excellent technical depth, scientific vision, project management skills, great communication skills, and a drive to achieve results in a unified team environment. You should enjoy the process of solving real-world problems that, quite frankly, haven’t been solved at scale anywhere before. Along the way, we guarantee you’ll get opportunities to be a bold disruptor, prolific innovator, and a reputed problem solver—someone who truly enables AI and robotics to significantly impact the lives of millions of consumers. Key job responsibilities Architect, design, and implement Machine Learning models for vision systems on robotic platforms Optimize, deploy, and support at scale ML models on the edge. Influence the team's strategy and contribute to long-term vision and roadmap. Work with stakeholders across , science, and operations teams to iterate on design and implementation. Maintain high standards by participating in reviews, designing for fault tolerance and operational excellence, and creating mechanisms for continuous improvement. Prototype and test concepts or features, both through simulation and emulators and with live robotic equipment Work directly with customers and partners to test prototypes and incorporate feedback Mentor other engineer team members. A day in the life - 6+ years of building machine learning models for retail application experience - PhD, or Master's degree and 6+ years of applied research experience - Experience programming in Java, C++, Python or related language - Experience with neural deep learning methods and machine learning - Demonstrated expertise in computer vision and machine learning techniques.
US, WA, Seattle
Prime Video is a first-stop entertainment destination offering customers a vast collection of premium programming in one app available across thousands of devices. Prime members can customize their viewing experience and find their favorite movies, series, documentaries, and live sports – including Amazon MGM Studios-produced series and movies; licensed fan favorites; and programming from Prime Video add-on subscriptions such as Apple TV+, Max, Crunchyroll and MGM+. All customers, regardless of whether they have a Prime membership or not, can rent or buy titles via the Prime Video Store, and can enjoy even more content for free with ads. Are you interested in shaping the future of entertainment? Prime Video's technology teams are creating best-in-class digital video experience. As a Prime Video team member, you’ll have end-to-end ownership of the product, user experience, design, and technology required to deliver state-of-the-art experiences for our customers. You’ll get to work on projects that are fast-paced, challenging, and varied. You’ll also be able to experiment with new possibilities, take risks, and collaborate with remarkable people. We’ll look for you to bring your diverse perspectives, ideas, and skill-sets to make Prime Video even better for our customers. With global opportunities for talented technologists, you can decide where a career Prime Video Tech takes you! Key job responsibilities As an Applied Scientist in the Content Understanding Team, you will lead the end-to-end research and deployment of video and multi-modal models applied to a variety of downstream applications. More specifically, you will: - Work backwards from customer problems to research and design scientific approaches for solving them - Work closely with other scientists, engineers and product managers to expand the depth of our product insights with data, create a variety of experiments to determine the high impact projects to include in planning roadmaps - Stay up-to-date with advancements and the latest modeling techniques in the field - Publish your research findings in top conferences and journals About the team Our Prime Video Content Understanding team builds holistic media representations (e.g. descriptions of scenes, semantic embeddings) and apply them to new customer experiences supply chain problems. Our technology spans the entire Prime Video catalogue globally, and we enable instant recaps, skip intro timing, ad placement, search, and content moderation.
IN, HR, Gurugram
Our customers have immense faith in our ability to deliver packages timely and as expected. A well planned network seamlessly scales to handle millions of package movements a day. It has monitoring mechanisms that detect failures before they even happen (such as predicting network congestion, operations breakdown), and perform proactive corrective actions. When failures do happen, it has inbuilt redundancies to mitigate impact (such as determine other routes or service providers that can handle the extra load), and avoids relying on single points of failure (service provider, node, or arc). Finally, it is cost optimal, so that customers can be passed the benefit from an efficiently set up network. Amazon Shipping is hiring Applied Scientists to help improve our ability to plan and execute package movements. As an Applied Scientist in Amazon Shipping, you will work on multiple challenging machine learning problems spread across a wide spectrum of business problems. You will build ML models to help our transportation cost auditing platforms effectively audit off-manifest (discrepancies between planned and actual shipping cost). You will build models to improve the quality of financial and planning data by accurately predicting ship cost at a package level. Your models will help forecast the packages required to be pick from shipper warehouses to reduce First Mile shipping cost. Using signals from within the transportation network (such as network load, and velocity of movements derived from package scan events) and outside (such as weather signals), you will build models that predict delivery delay for every package. These models will help improve buyer experience by triggering early corrective actions, and generating proactive customer notifications. Your role will require you to demonstrate Think Big and Invent and Simplify, by refining and translating Transportation domain-related business problems into one or more Machine Learning problems. You will use techniques from a wide array of machine learning paradigms, such as supervised, unsupervised, semi-supervised and reinforcement learning. Your model choices will include, but not be limited to, linear/logistic models, tree based models, deep learning models, ensemble models, and Q-learning models. You will use techniques such as LIME and SHAP to make your models interpretable for your customers. You will employ a family of reusable modelling solutions to ensure that your ML solution scales across multiple regions (such as North America, Europe, Asia) and package movement types (such as small parcel movements and truck movements). You will partner with Applied Scientists and Research Scientists from other teams in US and India working on related business domains. Your models are expected to be of production quality, and will be directly used in production services. You will work as part of a diverse data science and engineering team comprising of other Applied Scientists, Software Development Engineers and Business Intelligence Engineers. You will participate in the Amazon ML community by authoring scientific papers and submitting them to Machine Learning conferences. You will mentor Applied Scientists and Software Development Engineers having a strong interest in ML. You will also be called upon to provide ML consultation outside your team for other problem statements. If you are excited by this charter, come join us!
US, WA, Seattle
Do you want to re-invent how millions of people consume video content on their TVs, Tablets and Alexa? We are building a free to watch streaming service called Fire TV Channels (https://techcrunch.com/2023/08/21/amazon-launches-fire-tv-channels-app-400-fast-channels/). Our goal is to provide customers with a delightful and personalized experience for consuming content across News, Sports, Cooking, Gaming, Entertainment, Lifestyle and more. You will work closely with engineering and product stakeholders to realize our ambitious product vision. You will get to work with Generative AI and other state of the art technologies to help build personalization and recommendation solutions from the ground up. You will be in the driver's seat to present customers with content they will love. Using Amazon’s large-scale computing resources, you will ask research questions about customer behavior, build state-of-the-art models to generate recommendations and run these models to enhance the customer experience. You will participate in the Amazon ML community and mentor Applied Scientists and Software Engineers with a strong interest in and knowledge of ML. Your work will directly benefit customers and you will measure the impact using scientific tools.
US, MA, Boston
The Artificial General Intelligence (AGI) team is looking for a passionate, talented, and inventive Senior Applied Scientist with a strong deep learning background, to build industry-leading technology with Large Language Models (LLMs) and multimodal systems. Key job responsibilities As a Senior Applied Scientist with the AGI team, you will work with talented peers to lead the development of novel algorithms and modeling techniques, to advance the state of the art with LLMs. Your work will directly impact our customers in the form of products and services that make use of speech and language technology. You will leverage Amazon’s heterogeneous data sources and large-scale computing resources to accelerate advances in generative artificial intelligence (GenAI). About the team The AGI team has a mission to push the envelope in LLMs and multimodal systems, in order to provide the best-possible experience for our customers.
IN, KA, Bengaluru
The Amazon Alexa AI team in India is seeking a talented, self-driven Applied Scientist to work on prototyping, optimizing, and deploying ML algorithms within the realm of Generative AI. Key responsibilities include: - Research, experiment and build Proof Of Concepts advancing the state of the art in AI & ML for GenAI. - Collaborate with cross-functional teams to architect and execute technically rigorous AI projects. - Thrive in dynamic environments, adapting quickly to evolving technical requirements and deadlines. - Engage in effective technical communication (written & spoken) with coordination across teams. - Conduct thorough documentation of algorithms, methodologies, and findings for transparency and reproducibility. - Publish research papers in internal and external venues of repute - Support on-call activities for critical issues Basic Qualifications: - Master’s or PhD in computer science, statistics or a related field - 2-7 years experience in deep learning, machine learning, and data science. - Proficiency in coding and software development, with a strong focus on machine learning frameworks. - Experience in Python, or another language; command line usage; familiarity with Linux and AWS ecosystems. - Understanding of relevant statistical measures such as confidence intervals, significance of error measurements, development and evaluation data sets, etc. - Excellent communication skills (written & spoken) and ability to collaborate effectively in a distributed, cross-functional team setting. - Papers published in AI/ML venues of repute Preferred Qualifications: - Track record of diving into data to discover hidden patterns and conducting error/deviation analysis - Ability to develop experimental and analytic plans for data modeling processes, use of strong baselines, ability to accurately determine cause and effect relations - The motivation to achieve results in a fast-paced environment. - Exceptional level of organization and strong attention to detail - Comfortable working in a fast paced, highly collaborative, dynamic work environment
IN, KA, Bengaluru
The Amazon Alexa AI team in India is seeking a talented, self-driven Applied Scientist to work on prototyping, optimizing, and deploying ML algorithms within the realm of Generative AI. Key responsibilities include: - Research, experiment and build Proof Of Concepts advancing the state of the art in AI & ML for GenAI. - Collaborate with cross-functional teams to architect and execute technically rigorous AI projects. - Thrive in dynamic environments, adapting quickly to evolving technical requirements and deadlines. - Engage in effective technical communication (written & spoken) with coordination across teams. - Conduct thorough documentation of algorithms, methodologies, and findings for transparency and reproducibility. - Publish research papers in internal and external venues of repute - Support on-call activities for critical issues Basic Qualifications: - Master’s or PhD in computer science, statistics or a related field or relevant science experience (publications/scientific prototypes) in lieu of Masters - Experience in deep learning, machine learning, and data science. - Proficiency in coding and software development, with a strong focus on machine learning frameworks. - Experience in Python, or another language; command line usage; familiarity with Linux and AWS ecosystems. - Understanding of relevant statistical measures such as confidence intervals, significance of error measurements, development and evaluation data sets, etc. - Excellent communication skills (written & spoken) and ability to collaborate effectively in a distributed, cross-functional team setting. Preferred Qualifications: - Track record of diving into data to discover hidden patterns and conducting error/deviation analysis - Ability to develop experimental and analytic plans for data modeling processes, use of strong baselines, ability to accurately determine cause and effect relations - The motivation to achieve results in a fast-paced environment. - Exceptional level of organization and strong attention to detail - Comfortable working in a fast paced, highly collaborative, dynamic work environment - Papers published in AI/ML venues of repute
US, WA, Bellevue
Our mission is to provide consistent, accurate, and relevant delivery information to every single page on every Amazon-owned site. MILLIONS of customers will be impacted by your contributions: The changes we make directly impact the customer experience on every Amazon site. This is a great position for someone who likes to leverage Machine learning technologies to solve the real customer problems, and also wants to see and measure their direct impact on customers. We are a cross-functional team that owns the ENTIRE delivery experience for customers: From the business requirements to the technical systems that allow us to directly affect the on-site experience from a central service, business and technical team members are integrated so everyone is involved through the entire development process. You will have a chance to develop the state-of-art machine learning, including deep learning and reinforcement learning models, to build targeting, recommendation, and optimization services to impact millions of Amazon customers. Do you want to join an innovative team of scientists and engineers who use machine learning and statistical techniques to deliver the best delivery experience on every Amazon-owned site? Are you excited by the prospect of analyzing and modeling terabytes of data on the cloud and create state-of-art algorithms to solve real world problems? Do you like to own end-to-end business problems/metrics and directly impact the profitability of the company? Do you like to innovate and simplify? If yes, then you may be a great fit to join the DEX AI team. Key job responsibilities - Research and implement machine learning techniques to create scalable and effective models in Delivery Experience (DEX) systems - Solve business problems and identify business opportunities to provide the best delivery experience on all Amazon-owned sites. - Design and develop highly innovative machine learning and deep learning models for big data. - Build state-of-art ranking and recommendations models and apply to Amazon search engine. - Analyze and understand large amounts of Amazon’s historical business data to detect patterns, to analyze trends and to identify correlations and causalities - Establish scalable, efficient, automated processes for large scale data analyses, model development, model validation and model implementation
IN, KA, Bengaluru
Amazon is investing heavily in building a world class advertising business and we are responsible for defining and delivering a collection of self-service performance advertising products that drive discovery and sales. Our products are strategically important to our Retail and Marketplace businesses driving long term growth. We deliver billions of ad impressions and millions of clicks daily and are breaking fresh ground to create world-class products. We are highly motivated, collaborative and fun-loving with an entrepreneurial spirit and bias for action. With a broad mandate to experiment and innovate, we are growing at an unprecedented rate with a seemingly endless range of new opportunities. The ATT team, based in Bangalore, is responsible for ensuring that ads are relevant and is of good quality, leading to higher conversion for the sellers and providing a great experience for the customers. We deal with one of the world’s largest product catalog, handle billions of requests a day with plans to grow it by order of magnitude and use automated systems to validate tens of millions of offers submitted by thousands of merchants in multiple countries and languages. In this role, you will build and develop ML models to address content understanding problems in Ads. These models will rely on a variety of visual and textual features requiring expertise in both domains. These models need to scale to multiple languages and countries. You will collaborate with engineers and other scientists to build, train and deploy these models. As part of these activities, you will develop production level code that enables moderation of millions of ads submitted each day.