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