9月3日、The Stackが「Cedar: the access control building block that's perfectly timed for AI agents」と題した記事を公開した。AIエージェントが自律的にAPIを呼び出し、データにアクセスし、外部サービスを操作するようになった今、「エージェントに何をさせてよいか」を数学的に保証できる認可基盤への関心が高まっている。AWSが開発したオープンソースの認可ポリシー言語「Cedar」は、形式検証によってポリシーロジックの範囲で権限の抜け穴が存在しないことを証明できる設計を持ち、まさにそのニーズに応える存在として注目されている。

アプリケーションロジックから認可を切り離す

オンラインバンキングでどの口座にアクセスできるか、写真共有サービスでどのアルバムを閲覧できるか、HRシステムで誰が給与情報を見られるか。これらは形こそ違えど、本質的に同じ問題だ。そして多くの場合、認可ロジックはアプリケーションのコードに深く絡み合っており、ポリシーをコードとして管理するアプローチ（Policy as Code）の導入を難しくしている。

Cedarは、この問題を解決するためにAWSが開発したオープンソースの認可ポリシー言語およびエンジンだ。Rustで実装された小型・高性能なエンジンを任意のアプリケーションに組み込めるよう設計されており、形式検証（Formal Verification）によって数学的にポリシーの正しさを証明できる点が特徴である。

形式検証とは、プログラムの振る舞いを数学的な手法で厳密に検証する技術だ。セキュリティ上の抜け穴をテストで発見するのではなく、論理的に「存在しない」ことを証明できる。Cedarの場合、この検証はポリシーロジック自体の正しさを対象としており、インフラ設定やアプリケーション実装側の脆弱性を網羅するものではない点には注意が必要だ。元記事によれば、CedarエンジンのコアロジックにはDafnyという形式検証言語が用いられており、数学的な証明をコード自体に組み込む形で実装されているという。

AWSの研究プロジェクトから生まれた背景

CedarはもともとAWSの研究プロジェクトとして始まった。AWSがIDおよびアクセス管理（IAM）で培ってきた知見と、RBAC（ロールベースアクセス制御）・ABAC（属性ベースアクセス制御）のアプローチを統合し、Amazon Verified Permissions（AWSが提供するマネージド認可サービス。Cedarをポリシーエンジンとして採用しており、アプリケーションの認可ロジックをAWSに委譲できる）のポリシー言語として設計されたものだ。

AWSプリンシパルエンジニアのPhil EstesはThe Stackのインタビューでこう語っている。

「研究者たちは、数学的に証明可能なポリシーシステムをどう構築するかを研究していた。形式手法をソフトウェアに適用するアプローチだ。」

その上でEstesは、エンジン自体を独立した再利用可能なコンポーネントとして分離する方針についても言及している。

「形式的に証明可能なエンジンと検査機能を独立して作り、アプリケーションにプラグインできるようにしたらどうか。Rustで書けば、パフォーマンス保証と形式手法による保証の両方が得られる。」

Amazon Verified Permissionsはすでに本番利用が可能なサービスとして提供されており、Cedarをマネージドな形で活用したい場合の実装経路となっている。スタンドアロンのライブラリとして自前のアプリケーションに直接組み込む使い方も想定されており、AWSサービスへの依存なしに導入できる点も特徴のひとつだ。

Cedarが解くのは「誰が・何に・何をできるか」

元記事によれば、Cedarの適用範囲はAWSサービスに限らない。Estesは「アクター・アクション・リソース」の3要素で認可を表現する必要があるあらゆる場面、つまりRBACやABACを使うどんなシステムにもCedarはフィットすると述べている。

Cedarのポリシーは次のような形式で記述する（公式ドキュメントより）：

permit(
  principal == User::"alice",
  action == Action::"view",
  resource == Photo::"vacation.jpg"
);

シンプルな構文で「誰が・何を・どのリソースに対して」許可するかを宣言的に記述できる。ポリシーはアプリケーションコードから分離して管理でき、エンジンが高速に評価する。また、Cedarにはスキーマ検証の仕組みも備わっており、ポリシーが定義済みのエンティティ型・アクション・属性と整合しているかを事前に検査できる。これにより、ポリシー記述のミスを実行前に発見しやすくなっている。

AIエージェント時代との親和性

AIエージェントが自律的にAPIを呼び出し、データにアクセスし、外部サービスを操作するようになった今、「エージェントが何をしてよいか」を明示的に制御する仕組みの重要性は急速に高まっている。LLMベースのエージェントは指示の解釈が曖昧になりやすく、過剰な権限を与えると意図しないデータアクセスやアクション実行が起きうる。

元記事においてもEstesはこの点に言及しており、AIエージェントが増殖する中でCedarのようなポリシーエンジンの役割が重要になると述べている。アクター・アクション・リソースという明確な3要素でポリシーを記述できるCedarは、こうしたエージェントの権限スコープを宣言的・検証可能な形で定義するための基盤として機能しうる構造を持つ。形式検証によって「このエージェントはこの条件下ではこのリソースにアクセスできない」という保証をポリシーロジックのレベルで得られる点は、セキュリティ設計において実践的な意味を持つ。

CedarのGitHubリポジトリはすでに公開されており、仕様や実装を確認できる。AWSサービスとしての利用だけでなく、スタンドアロンのライブラリとして任意のアプリケーションに組み込む使い方も想定されている。

詳細はCedar: the access control building block that's perfectly timed for AI agentsを参照していただきたい。