Home PLDI 2024論文解説: Cedar — 表現力・高速・安全・解析可能を両立した認可言語の設計と実装
投稿
キャンセル

📄 PLDI 2024論文解説: Cedar — 表現力・高速・安全・解析可能を両立した認可言語の設計と実装

投稿日 11/03/2026
投稿者 0h-n0
24 分読了時間

本記事は arXiv:2403.04651 “Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization”（PLDI 2024採択）の解説記事です。

論文概要（Abstract）

Cedarは、認可ポリシーを記述するためのオープンソースプログラミング言語である。principal（主体）がresource（資源）に対してaction（操作）を実行する条件をpermit/forbidで宣言的に記述する。Lean 4によるリファレンス意味論、Rust本番実装との差分テスト、SMTベースの自動推論を備えた言語理論的アプローチで設計されている。Amazon Verified PermissionsとAWS IAM Identity Centerに採用され、2022年11月から本番運用されている。

この記事は Zenn記事: Bedrock AgentCoreのエピソード記憶×Policy制御でマルチターンエージェントの応答精度を高める の深掘りです。Zenn記事ではCedarポリシーによるエージェントのツール呼び出し制御を解説しているが、本記事ではCedar言語そのものの設計原則と形式的基盤を深掘りする。

情報源

カンファレンス情報

PLDIはプログラミング言語の設計と実装に関するトップカンファレンスの1つである。ACM SIGPLANが主催し、言語設計、型システム、コンパイラ、形式検証の分野で高い評価を受けている。Cedarの採択は、認可言語を言語理論の観点から厳密に設計した成果が認められたものである。

技術的詳細（Technical Details）

Cedarの4つの設計目標

著者らは、既存の認可言語（OPA/Rego、AWS IAM JSON、XACML、Casbin）が表現力・速度・安全性・解析可能性のトレードオフに直面していると指摘し、Cedarでこれら4つを同時に達成することを目指している。

設計目標意味既存手法の課題
Expressive実際のビジネス要件を自然に記述IAM JSONは属性ベース制御が限定的
Fast認可チェックをp99 < 1msで実行XACMLはXML解析のオーバーヘッドが大きい
Safeポリシーの終了性保証、型安全OPA/RegoはTuring完全に近く停止性を保証しない
AnalyzableSMTで等価性・充足可能性を自動判定Casbin、IAM JSONには自動推論機能がない

言語構文とPARC モデル

Cedarは PARC（Principal, Action, Resource, Context）モデルを採用している。ポリシーは permit または forbid キーワードで始まる。

// パターン1: ロールベースアクセス制御
permit (
  principal in Group::"admins",
  action in [Action::"read", Action::"write"],
  resource in Folder::"shared"
);

// パターン2: 属性ベースの条件付き許可
permit (
  principal,
  action == Action::"viewDocument",
  resource
)
when {
  resource.classification == "public" ||
  (resource.classification == "confidential" &&
   principal.department == resource.department)
};

// パターン3: コンテキスト条件（MFA + IP制限）
permit (
  principal,
  action == Action::"sensitiveOp",
  resource
)
when {
  context.mfa_authenticated &&
  context.ip.isInRange(ip("192.168.1.0/24"))
};

エンティティ階層: エンティティはグループ/親子関係を持ち、in 演算子で推移的に評価される。User::"alice" in Group::"admins" は、aliceがadminsの直接メンバーか、その祖先グループのメンバーかをチェックする。

評価モデル: Default-Deny と Forbid-Wins

Cedarの認可決定は以下のルールで行われる。

\[\text{isAuthorized}(\Pi, r, E) = \begin{cases} \text{Deny} & \text{if } \exists p \in \Pi : p.\text{effect} = \texttt{forbid} \land \text{matches}(p, r, E) \\ \text{Permit} & \text{if } \exists p \in \Pi : p.\text{effect} = \texttt{permit} \land \text{matches}(p, r, E) \\ \text{Deny} & \text{otherwise (default-deny)} \end{cases}\]

ここで $\Pi$ はポリシーセット、$r$ はリクエスト、$E$ はエンティティストアである。

  1. いずれかの forbid ポリシーが適用されれば → 拒否（forbid-wins）
  2. 少なくとも1つの permit が適用され、かつ forbid なし → 許可
  3. 該当する permit なし → 拒否（default-deny）

この「forbidがpermitに常に優先する」設計は、セキュリティ上の安全策として意図的に採用されている。Zenn記事で紹介されているAgentCore Policyも、この同一のセマンティクスでエージェントのツール呼び出しを制御している。

形式的意味論（Lean 4）

著者らはCedarのリファレンス意味論をLean 4で記述している。これにより以下が保証される。

  • 決定論性: 同一入力に対して常に同一出力
  • 全域性: すべての入力に対して定義された出力（例外なし）
  • 型安全性の機械的証明: 型システムの健全性をLeanで証明

Lean形式化の構造:

1
2
3
4
5
6
7

cedar-spec/
├── CedarSpec/
│   ├── Expr.lean          # 式の構文定義
│   ├── Eval.lean          # 評価器
│   ├── Validator.lean     # 型チェッカー
│   └── Authorization.lean # 認可判定ロジック
└── DiffTest/              # Lean-Rust差分テスト

差分テストによる正確性保証

著者らは、Lean形式化とRust本番実装の一貫性を差分ファジングで検証している。

  1. ランダムなポリシー・リクエスト・エンティティストアを自動生成
  2. Lean実装とRust実装の両方で評価
  3. 結果の一致を確認

著者らの報告では、10億回以上のテストケースで検証を実施し、発見された不一致は両実装のバグ修正に活用された。

型システム

Cedarの型:

  • プリミティブ型: Long（64bit整数）, String, Boolean, Entity
  • コレクション型: Set<T>, Record { field: T, ... }
  • 拡張型: IPアドレス、Decimal

型チェッカーはスキーマに基づき、以下を検出する。

  • 存在しない属性へのアクセス
  • 型の不一致（数値と文字列の比較など）
  • スコープで許可されていないエンティティ型の使用

健全性定理: 型チェックが通ったポリシーは、スキーマに合致するエンティティストアに対して実行時型エラーを起こさない（Leanで機械的に証明）。

SMTベース自動推論（Cedar Analyzer）

Cedar AnalyzerはZ3 SMTソルバーをバックエンドに使用し、以下のクエリをサポートする。

クエリ種別質問用途
Satisfiabilityこのポリシーがpermitを返すリクエストは存在するか？空ポリシーの検出
Equivalence2つのポリシーセットは全入力で同じ決定を返すか？リファクタリング前後の動作保証
DifferentialポリシーAでPermit、Bで Denyになるリクエストは？変更の影響範囲特定
Partial Evalprincipalを固定した場合の許可範囲は？権限の可視化

SMTエンコーディングの主要課題:

  • エンティティ階層（in演算子）: 推移的閉包を事前計算し、ビットベクタでエンコード
  • 拡張型: IPアドレスのビット演算をSMTビットベクタ演算にマッピング
  • Optional属性: 属性不存在のエラー処理をOptional型でモデル化

実装のポイント（Implementation）

Cedarを実際にプロダクションで使用する際の注意点:

  • スキーマの定義を先行: スキーマなしでも動作するが、型チェックが弱くなる。本番環境ではスキーマを強く推奨
  • forbidポリシーの慎重な設計: forbid-winsセマンティクスにより、意図しない全面拒否が発生しうる。Cedar Analyzerの「always-deny」チェックを活用
  • テンプレートリンクの活用: 大量の個別ポリシーを生成せず、テンプレートにエンティティをリンクする設計が推奨される
  • エラーはDenyとして扱われる: 属性不存在などのランタイムエラーはfail-closeで拒否される。errorsフィールドでデバッグ可能

実験結果（Results）

パフォーマンス比較

著者らの報告では、Amazon Verified Permissionsの本番トラフィックを模したワークロードで以下の結果が得られている。

指標CedarOPA (Open Policy Agent)
レイテンシ (p99)< 1ms5-50ms
スループット数百万 req/s（シングルスレッド）数万〜数十万 req/s

高速化の主要因（論文Section 6より）:

  1. Turing完全でない設計による最適化容易性
  2. スコープ条件でのポリシー事前フィルタリング（部分評価）
  3. エンティティ階層のビットセット演算への変換
  4. Rustの型システムを活用したコンパイル済み評価エンジン

既存認可言語との比較

言語表現力型安全自動推論パフォーマンス
Cedar高（ABAC+階層）あり（Lean証明）SMTベースp99 < 1ms
OPA/Rego非常に高限定的なし5-50ms
AWS IAM JSON中なしなし高速
XACML高限定的一部低速

（論文Table 1相当の比較、Section 9より）

査読者の評価（Peer Review Insights）

PLDI 2024で採択された本論文は、以下の点が評価されていると考えられる。

  • 言語理論と実用の橋渡し: 形式検証（Lean 4）と本番運用（Amazon Verified Permissions）の両方を達成
  • 差分テストの規模: 10億回以上のLean-Rust差分ファジングによる正確性保証
  • 設計上のトレードオフの明確化: Turing完全性を意図的に排除することで得られる安全性・解析可能性の議論

Production Deployment Guide

AWS実装パターン（コスト最適化重視）

Cedar認可をプロダクション環境で運用する場合、Amazon Verified Permissions（マネージドサービス）またはCedar SDK（セルフホスト）を選択できる。

規模月間リクエスト推奨構成月額コスト主要サービス
Small~3,000 (100/日)Serverless$30-100Lambda + Verified Permissions
Medium~30,000 (1,000/日)Hybrid$200-500Lambda + Verified Permissions + ElastiCache
Large300,000+ (10,000/日)Container$1,000-3,000EKS + Cedar SDK (self-hosted)

Small構成の詳細 (月額$30-100):

  • Verified Permissions: ポリシー評価 ($20/月、100万リクエストまで無料枠)
  • Lambda: API Gateway統合 ($10/月)
  • CloudWatch: 基本監視 ($5/月)

コスト試算の注意事項:

  • 上記は2026年3月時点のAWS ap-northeast-1（東京）リージョン料金に基づく概算値です
  • Verified Permissionsの料金は認可リクエスト数に依存します
  • 最新料金は AWS料金計算ツール で確認してください

Terraformインフラコード

Small構成 (Serverless): Lambda + Verified Permissions

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76

resource "aws_verifiedpermissions_policy_store" "agent_authz" {
  validation_settings {
    mode = "STRICT"
  }
}

resource "aws_verifiedpermissions_schema" "agent_schema" {
  policy_store_id = aws_verifiedpermissions_policy_store.agent_authz.id

  definition {
    value = jsonencode({
      AgentCore = {
        entityTypes = {
          User = {
            shape = {
              type = "Record"
              attributes = {
                role       = { type = "String" }
                department = { type = "String" }
              }
            }
          }
        }
        actions = {
          processRefund = {
            appliesTo = {
              principalTypes = ["User"]
              resourceTypes  = ["Gateway"]
            }
          }
        }
      }
    })
  }
}

resource "aws_iam_role" "lambda_avp" {
  name = "cedar-authz-lambda-role"

  assume_role_policy = jsonencode({
    Version = "2012-10-17"
    Statement = [{
      Action    = "sts:AssumeRole"
      Effect    = "Allow"
      Principal = { Service = "lambda.amazonaws.com" }
    }]
  })
}

resource "aws_iam_role_policy" "avp_invoke" {
  role = aws_iam_role.lambda_avp.id
  policy = jsonencode({
    Version = "2012-10-17"
    Statement = [{
      Effect   = "Allow"
      Action   = ["verifiedpermissions:IsAuthorized", "verifiedpermissions:IsAuthorizedWithToken"]
      Resource = aws_verifiedpermissions_policy_store.agent_authz.arn
    }]
  })
}

resource "aws_lambda_function" "authz_handler" {
  filename      = "lambda.zip"
  function_name = "cedar-authz-handler"
  role          = aws_iam_role.lambda_avp.arn
  handler       = "index.handler"
  runtime       = "python3.12"
  timeout       = 10
  memory_size   = 256

  environment {
    variables = {
      POLICY_STORE_ID = aws_verifiedpermissions_policy_store.agent_authz.id
    }
  }
}

セキュリティベストプラクティス

  • IAMロール: Verified PermissionsのIsAuthorizedのみ許可
  • ポリシー管理: Cedar Analyzerで変更前にalways-deny/always-allowチェック
  • 暗号化: ポリシーストアはAWS管理キーで暗号化
  • 監査: CloudTrailで全認可リクエストを記録

運用・監視設定

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

import boto3

cloudwatch = boto3.client('cloudwatch')

# Cedar認可レイテンシ監視
cloudwatch.put_metric_alarm(
    AlarmName='cedar-authz-latency',
    ComparisonOperator='GreaterThanThreshold',
    EvaluationPeriods=2,
    MetricName='Duration',
    Namespace='AWS/Lambda',
    Period=300,
    Statistic='p99',
    Threshold=100,
    AlarmDescription='Cedar認可レイテンシ異常（p99 > 100ms）'
)

コスト最適化チェックリスト

  • ~100 req/日 → Verified Permissions (マネージド) - $30-100/月
  • ~1000 req/日 → Verified Permissions + ElastiCache - $200-500/月
  • 10000+ req/日 → Cedar SDK (self-hosted on EKS) - $1,000-3,000/月
  • ポリシー評価結果のキャッシュ（同一リクエストの再評価防止）
  • Verified Permissions無料枠の活用（月100万リクエスト）
  • Cedar Analyzerによるポリシー最適化（未使用ポリシー削除）
  • AWS Budgets: 月額予算設定
  • CloudTrail: 認可ログの長期保存（S3 + Glacier）
  • ポリシーバージョニング: 変更履歴の管理
  • テンプレートリンク: 個別ポリシー数の削減

実運用への応用（Practical Applications）

Zenn記事で紹介されているBedrock AgentCore Policyは、まさにCedar言語をエージェントのツール呼び出し制御に適用したものである。本論文の知見は以下の形でAgentCoreの設計に反映されている。

  • Default-deny + Forbid-wins: エージェントのツール呼び出しは明示的にpermitされない限り拒否。forbidポリシーでの制限はpermitより常に優先
  • 自動スキーマ生成: AgentCore GatewayのMCPツール定義からCedarスキーマを自動生成し、ポリシーバリデーションに使用
  • 自然言語→Cedar変換: コンプライアンスチームがCedar構文を学ばずにポリシーを定義可能。自動推論によるバリデーションで意図しない許可・拒否を検出

Cedar言語のTuring完全でない設計は、エージェントのポリシー評価がAPI呼び出しのクリティカルパスに入る場合に特に重要である。p99 < 1msの評価速度により、エージェントの応答レイテンシへの影響を最小化できる。

関連研究（Related Work）

  • OPA/Rego: Turing完全に近い汎用ポリシー言語。表現力は高いが、自動推論とパフォーマンスでCedarに劣る
  • XACML: XML ベースの認可標準。表現力は高いがXML解析のオーバーヘッドが大きい
  • Margrave: ファイアウォールポリシーのSMTベース解析ツール。Cedar Analyzerの先行研究
  • SEAL: AWS IAMポリシーの自動推論ツール。Cedarと同じAWSエコシステムで並存

まとめと今後の展望

Cedarは、表現力・高速・安全・解析可能の4目標を同時に達成した認可言語として設計され、PLDI 2024に採択された。著者らの報告では、Lean 4による形式的意味論、10億回以上の差分テスト、SMTベース自動推論により、高い正確性と実用性を実現している。

Bedrock AgentCore Policyの基盤技術として、Cedarの設計原則（default-deny、forbid-wins、p99 < 1ms）は、LLMエージェントのガバナンスにおいて不可欠な役割を果たしている。今後は、エージェントの動的なポリシー更新（Reflection結果に基づく権限調整）やマルチテナント環境での大規模ポリシー管理が課題となる。

参考文献

:::message この記事はAI（Claude Code）により自動生成されました。論文の主張や数値は原著論文に基づいていますが、実際の利用時は原論文もご確認ください。 :::

blog paper conference
cedar authorization policy formal-verification AWS
この投稿は CC BY 4.0 でライセンスされています。
最近の更新
目次