Skip to content

SYSTEM Cited by 2 sources

AWS policy interpreter (IAM / Cedar)

What it is

AWS's authorization engine — the component that evaluates whether a given principal is allowed to take a given action on a given resource under a given set of policies. Publicly it surfaces as IAM and Cedar (the open-source policy language AWS extracted from internal work); Cook's references to the "AWS policy interpreter" cover the full family of internal and public tooling across a decade of work.

Ten years of proof over AWS's most critical building blocks for security (e.g., the AWS policy interpreter, our cryptography, our networking protocols, etc.) now allows us to use agentic development tools with higher confidence by being able to prove correctness. — Byron Cook (Source: sources/2026-02-17-allthingsdistributed-byron-cook-automated-reasoning-trust-ai)

Why it's on this wiki

The policy interpreter is Cook's headline example of an AWS building block that has been the subject of automated-reasoning proof for a decade. Every primitive with a durable proof scaffolding compounds in value as new tooling — especially agent-generated code — arrives: the proofs get reused against every future change.

It is simultaneously a case study in scaling automated reasoning into a production-critical control plane and a meta-point about investment in formal methods paying off on long time horizons.

The decade-long arc

  • Early 2010s. Automated reasoning applied to IAM policy analysis at AWS.
  • Zelkova-era (public footprint, ~2018). SMT-backed policy analysis exposed to customers (e.g., IAM Access Analyzer).
  • Cedar (2023, public). Open-source policy language specifically designed for analyzability — the product crystallization of AWS's internal policy-semantics work.
  • 2026. Proofs over the policy interpreter now extend to reasoning about agentic-tool-generated policy changes, per Cook.

The public surface (IAM, Access Analyzer, Cedar) is the tip; the internal tooling that "predates and underlies it" is what Cook is referring to when he says "AWS policy interpreter." Cedar is the most visible instance of concepts/specification-driven-development applied to authorization.

Methodological parallel: from spec-surfacing to contradiction-surfacing

Cook highlights an instructive non-technical point about the decade of policy work:

Complex rules and laws often have subtle contradictions that can go unnoticed until someone tries to reach consensus on their interpretation. We've seen that within Amazon trying to nail down the details of AWS's policy semantics, or the details of virtual networks.

Formalizing policy surfaced disagreement inside Amazon about what the policies were supposed to mean. This is not a bug — it's the whole point of concepts/specification-driven-development. Spec-authoring forces latent interpretations into explicit text.

Relation to other AWS automated-reasoning portfolio

The policy interpreter is one of several primitives Cook lists as having been proven over a decade:

  • Cryptography — implementations vs reference procedures.
  • Networking protocols — routing / reachability / property correctness.
  • Virtualization layer — Nitro-era isolation proofs.
  • Per-service data flow (2025, CISO Amy Herzog) — "data at rest is encrypted", "credentials are never logged" invariants.
  • Storage (ShardStore via patterns/executable-specification).

Together these form the scaffolding Cook argues is AWS's moat when agentic tools begin modifying AWS-internal primitives.

Caveats

  • "AWS policy interpreter" is not a single public product. It references a family of internal tooling whose public footprint includes IAM, IAM Access Analyzer, Cedar, and associated analyzers. The exact internal architecture is not detailed in this source.
  • Cedar is the most direct public artifact for anyone wanting to see the engineering shape of policy-semantics-as-formal-spec; it is an intentional public extraction of internal practice.

Seen in

Last updated · 200 distilled / 1,178 read