AWS has thousands of customers who expect continuous deployments and face millions of attack vectors.
Over a million request configurations are sent daily to their policy analysis engine called Zelkova.
This system can detect if a given configuration is too lenient (meaning your system is going to get creamed). It stops incorrect configurations from reaching production.
The problem is simple, but the solution isn't easy.
AWS Configurations have varying actors, resources, and conditions. They may even be defined using variables! This makes the problem of judging a configuration "safe" or "unsafe" very difficult.
So AWS relies on two major improvements over state-of-the-art solvers:
- Caching configurations heavily.
- Guessing if a configuration is safe.
The second point is tricky. Since rules can have IP addresses, strings, and even regex wildcards, AWS uses multiple methods to guess if a config is correct.
AWS Zelkova first transforms configurations into "logically equivalent" rulesets. These are simplified versions of the original configurations.
The simplified versions are easy to test. Zelkova uses a fleet of Satisfiability Modulo Theories (SMT) Solvers to check for correctness.
If the transformed logical versions pass, we assume that the config is good.
Else, the config is marked as dangerous and not allowed.
It may seem like overkill, but at AWS scale, this system is called over a million times daily. That's a lot of systems kept secure!
I read about Google Zanzibar and Vanadium recently. AWS Zelkova is, in contrast, a more generic system.
The language is much richer than what most systems offer, and we as a community should thank their engineering team for publishing relevant whitepapers.
To learn more about system design and distributed systems security, head to InterviewReady.