aws-agentcore-cedar-policy

Extract — Why AgentCore Policy chose Cedar (AWS Security Blog)

• URL: https://aws.amazon.com/blogs/security/why-policy-in-amazon-bedrock-agentcore-chose-cedar-for-securing-agentic-workflows/
• Fetched: 2026-09-27 ~19:33 CST · defuddle parse —md
• Related: Cedar Analysis OSS blog; cedar-policy/cedar-spec Lean CLI; cedar-for-agents MCP schema generator

Core claims

• Treat the LLM as untrusted: non-deterministic, prompt-injectable, no robust cmd/data split. Hard-coded workflows kill agency; HITL alone → approval fatigue. Controls must sit outside the LLM, at the orchestrator/tool boundary.
• AgentCore Gateway + Policy: default-deny on tool traffic; Cedar policies selectively permit tool invocations + argument constraints. Applies to all MCP tool traffic through Gateway.
• Why Cedar: purpose-built authz; human-readable; analyzable via automated reasoning (symbolic encoder); no loops/stateful ops → O(n) eval; default-deny, forbid-wins, no-ordering → deterministic.
• Neuro-symbolic authoring: NL → LLM → Cedar; (1) MCP tool descs → Cedar schema → validate policies; (2) Cedar Analysis encodes policies as formulas — detect always-permit, always-deny, contradictions, conflicts, redundancy. Holistic analysis on attach to Gateway.
• Partial evaluation: on list tools, omit actions that would always be denied — LLM never sees forbidden tools (reduces attempt surface).
• JWT/principal tags (e.g. customer_tier) vs LLM-produced tool args: policies constrain both; principal claims can’t be hallucinated.

Numbers / concrete checks (examples, not large benches)

• Blog is architectural + worked examples, not a pass-rate paper.
• Analysis examples: contradictory Gold&&Platinum; tautological qty>=100 || qty<100; permit/forbid conflict on refunds (forbid wins → Gold refunds all blocked); policy-diff table showing “more permissive” after narrowing an unless (counterintuitive).
• Cedar Analysis available as OSS CLI (Lean symbolic compiler path cited via cedar-spec / cedar-lean-cli).

DIY-relevant patterns

• Separate policy gate from agent brain — central authz outside tools/agent code; auditable single checkpoint.
• NL→policy only if paired with formal analysis feedback loop (otherwise same hallucination risk).
• Schema from tool catalog (MCP) as first gate before Analysis.
• Partial eval / capability filtering before the LLM plans.
• Adopt for Herdr/orchestrators: Cedar (or equivalent analyzable policy) on tool invoke; default-deny; Analysis in CI before deploy; JWT-style trusted attrs for principal. Skip: encoding authz in system prompts; scattering if-checks across tools.
• Complements code-level FV (BMC/Verus/Lean): this is runtime authorization envelope, not functional correctness of generated code.

Gaps / confidence

• AWS product framing; little independent eval metrics. Analysis power is real (Cedar/Lean lineage) but DIY must wire schema+Analysis+enforcement themselves. Confidence high on threat model + pattern; medium on Bedrock-specific APIs as DIYable without AWS.