Neha Rungta's 2022 CAV keynote

A billion SMT queries a day

CAV keynote lecture by the director of applied science for AWS Identity explains how AWS is making the power of automated reasoning available to all customers.

At this year’s Computer-Aided Verification (CAV) conference — a leading automated-reasoning conference collocated with the Federated Logic Conferences (FLoC) — Amazon’s Neha Rungta delivered a keynote talk in which she suggested that innovations at Amazon have “ushered in the golden age of automated reasoning”. 

Amazon scientists and engineers are using automated reasoning to prove the correctness of critical internal systems and to help customers prove the security of their cloud infrastructures. Many of these innovations are being driven by powerful reasoning engines called SMT solvers.  

Satisfiability problems, or SAT, ask whether it’s possible to assign variables true/false values that satisfy a set of constraints. SMT, or satisfiability modulo theories, is a generalization of SAT to involve integers, real numbers, strings, or functions. It is a mainstay of formal methods — the use of automated reasoning to prove that a computer program will behave the way it’s supposed to.

The following is a condensed and edited version of Rungta’s talk. You can also read the accompanying invited paper.

Zelkova

At Amazon, we use automated reasoning to prove the correctness of internal systems and to provide services that allow customers to prove the correctness of their cloud systems. Today I am going to focus on a single but critical part of that work. I am going to show you how we help customers get their access controls right using an automated-reasoning engine called Zelkova. I want to show you the balancing act we do between science and engineering to make automated reasoning work at scale.

Related content
SOSP paper describes lightweight formal methods for validating new S3 data storage service.

Zelkova takes as input an access control policy and a question about access control and returns a correct answer to the question. That sounds too good to be true: what’s the catch, you may ask?

The correctness of the answer depends on asking the right question. Our key innovation here is that, rather than require customers to ask the right questions, the way previous approaches did, we have AWS services ask Zelkova questions on behalf of customers.

For example, Amazon S3 Block Public Access asks Zelkova, “Does this S3 bucket policy grant public access?” AWS Identity and Access Management (IAM) Access Analyzer asks Zelkova, “Does this KMS key grant cross-account access?” It is easy for customers to determine the security of cloud resources by looking at the answers. This model — having AWS services ask the questions — allows us to democratize automated reasoning and make it usable by all AWS customers.

Under the hood, Zelkova translates the policy and question into an SMT query and calls a portfolio solver to get an answer, as in the figure below. A portfolio solver invokes multiple solvers in the backend — here, they include Z3, CVC4, cvc5, and a custom automaton solver — and returns the results from the solver that comes backs with an answer first, in a winner-take-all strategy. Leveraging the diversity of SMT solvers enables Zelkova to solve queries quickly — within a couple hundred milliseconds to tens of seconds.

Zelkova design.png
Zelkova is an automated-reasoning engine that helps customers make universal statements such as “There is no public access to my AWS resources”. It uses a "portfolio solver", which invokes multiple solvers in the backend — Z3, CVC4, cvc5, and so on — and returns the first answer to come back.

SMT solvers use clever algorithms and heuristics to solve problems that are computationally hard. The time it takes to solve a query depends on a wide variety of factors, including the solver configuration, the random seed picked during analysis, and the heuristics being used. The result is that two queries with small syntactic differences can have wildly different run times. Similarly, seemingly minor implementation changes in the solvers can lead to a large run-time variance.

Related content
Meet Amazon Science’s newest research area.

We turned to engineering best practices to even out the lack of predictability and monotonicity in the performance of SMT solvers. Before deploying a new version of the solver for Zelkova, we perform extensive offline testing and benchmarking.

SMT solving at cloud scale

We experienced some unexpected bumps when we wanted to upgrade CVC4 with its newer version, cvc5 (version 0.0.4). In the graph comparing the two solvers, we have approximately 15,000 SMT queries generated by Zelkova. We select a distribution of queries whose solution times range from 0.01 second to 30 seconds; after 30 seconds, the solver process is killed and a timeout reported.

Some queries that are not solved by CVC4 within the time bound are now being solved by cvc5, as is seen from the points aligned vertically at the right side of the graph. However, cvc5 times out on some queries that are solved by CVC4, as is seen from the points aligned horizontally at the top of the graph.

cvc5 0.0.4.png
Comparing the run times of queries solved by CVC4 and cvc5 (version 0.0.4).

The change in run times for SMT queries can have an impact on the customer experience. For example, in Amazon S3 Block Public Access, when analyzing a bucket policy, if the solver times out, it classifies the bucket as “public”.

Suppose that, with the previous solver version, there was a bucket marked “not public” based on the results of a query. Further suppose that, with the current solver version, if the same query times out, then the bucket is marked as “public”. This will lock down the bucket, and the intended users will not be able to access it. This is unexpected for the user, who made no configuration changes. Hence, we need to ensure that all queries that were previously getting solved within the max time bound are still getting solved.

cvc5 0.0.7.png
Comparing the run times of queries solved by CVC4 and cvc5 (version 0.0.7).

We dug into the root causes of the discrepancy, and it turned out that a rewrite rule had been disabled in cvc5. We worked with the cvc5 developers to get it re-enabled (in version 0.0.7), but the story doesn’t end there. It turns out that even with the fix, CVC4 was twice as fast as cvc5 on many easier problems, solving them in one second instead of two.

Run-time comparison.png
Run-time data that led us to add cvc5 to the Zelkova portfolio solver.

This slowdown was significant because Zelkova is called in the request path of security controls such as Amazon S3 Block Public Access. When a user attempts to attach a new access control policy to an S3 bucket or to update an existing one, a synchronous call is made to Zelkova and the corresponding portfolio solver to determine if the policy grants unrestricted public access or not. The bulk of the analysis time is spent on the SMT solvers, so doubling the analysis time for queries can potentially degrade the user experience. This is why we decided to add cvc5 to the Zelkova portfolio solver rather than replace CVC4 with it.

Democratizing automated reasoning

What does this mean for our customers? Instead of focusing on the technology, they can think about its value to them. We tell customers they can make universal statements about the security of their cloud infrastructure. A universal statement holds over the entire universe of possibilities, not just what we’ve tested or fuzzed or observed or thought about. Services such as Amazon S3 Block Public Access, IAM Access Analyzer, Amazon VPC Network Access Analyzer, and Amazon Inspector allow customers to make universal statements such as “there is no public access to my S3 bucket”.

High assurance with provable security
Neha Rungta and Andrew Gacek's talk at the AWS re:Inforce security conference.

I believe that these services would be useful to all our customers. To learn how to use them, watch the talk on high assurance with provable security that my colleague Andrew Gacek and I gave earlier this summer at the AWS re:Inforce security conference. Automated reasoning is transforming the landscape of cloud security, and its power is available to all AWS customers through a few clicks.

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
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.
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, 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 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
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
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.
US, WA, Seattle
The Search Supply & Experiences team, within Sponsored Products, is seeking an Applied Scientist to solve challenging problems in natural language understanding, personalization, and other areas using the latest techniques in machine learning. In our team, you will have the opportunity to create new ads experiences that elevate the shopping experience for our hundreds of millions customers worldwide. As an Applied Scientist, you will partner with other talented scientists and engineers to design, train, test, and deploy machine learning models. You will be responsible for translating business and engineering requirements into deliverables, and performing detailed experiment analysis to determine how shoppers and advertisers are responding to your changes. We are looking for candidates who thrive in an exciting, fast-paced environment and who have a strong personal interest in learning, researching, and creating new technologies with high customer impact. Key job responsibilities As an Applied Scientist on the Search Supply & Experiences team you will: - Perform hands-on analysis and modeling of enormous datasets to develop insights that increase traffic monetization and merchandise sales, without compromising the shopper experience. - Drive end-to-end machine learning projects that have a high degree of ambiguity, scale, and complexity. - Build machine learning models, perform proof-of-concept, experiment, optimize, and deploy your models into production; work closely with software engineers to assist in productionizing your ML models. - Design and run experiments, gather data, and perform statistical analysis. - Establish scalable, efficient, automated processes for large-scale data analysis, machine-learning model development, model validation and serving. - Stay up to date on the latest advances in machine learning. About the team We are a customer-obsessed team of engineers, technologists, product leaders, and scientists. We are focused on continuous exploration of contexts and creatives where advertising delivers value to shoppers and advertisers. We specifically work on new ads experiences globally with the goal of helping shoppers make the most informed purchase decision. We obsess about our customers and we are continuously innovating on their behalf to enrich their shopping experience on Amazon
US, WA, Seattle
Amazon.com strives to be Earth's most customer-centric company where customers can shop in our stores to find and discover anything they want to buy. We hire the world's brightest minds, offering them a fast paced, technologically sophisticated and friendly work environment. Economists at Amazon partner closely with senior management, business stakeholders, scientist and engineers, and economist leadership to solve key business problems ranging from Amazon Web Services, Kindle, Prime, inventory planning, international retail, third party merchants, search, pricing, labor and employment planning, effective benefits (health, retirement, etc.) and beyond. Amazon Economists build econometric models using our world class data systems and apply approaches from a variety of skillsets – applied macro/time series, applied micro, econometric theory, empirical IO, empirical health, labor, public economics and related fields are all highly valued skillsets at Amazon. You will work in a fast moving environment to solve business problems as a member of either a cross-functional team embedded within a business unit or a central science and economics organization. You will be expected to develop techniques that apply econometrics to large data sets, address quantitative problems, and contribute to the design of automated systems around the company. About the team The International Seller Services (ISS) Economics team is a dynamic group at the forefront of shaping Amazon's global seller ecosystem. As part of ISS, we drive innovation and growth through sophisticated economic analysis and data-driven insights. Our mission is critical: we're transforming how Amazon empowers millions of international sellers to succeed in the digital marketplace. Our team stands at the intersection of innovative technology and practical business solutions. We're leading Amazon's transformation in seller services through work with Large Language Models (LLMs) and generative AI, while tackling fundamental questions about seller growth, marketplace dynamics, and operational efficiency. What sets us apart is our unique blend of rigorous economic methodology and practical business impact. We're not just analyzing data – we're building the frameworks and measurement systems that will define the future of Amazon's seller services. Whether we're optimizing the seller journey, evaluating new technologies, or designing innovative service models, our team transforms complex economic challenges into actionable insights that drive real-world results. Join us in shaping how millions of businesses worldwide succeed on Amazon's marketplace, while working on problems that combine economic theory, advanced analytics, and innovative technology.