AWSが公開したオープンソースのポリシー記述言語Cedarを紹介

Amazon Web Servicesが公開したオープンソースのポリシー記述言語CedarをThe New Stackの動画から解説する。The New Stackはオープンソースに限らず最新のソフトウェアを紹介するメディアとして、KubeCon＋CloudNativeCon、OpenSourceSummitのイベントにおいて現地でインタビューを行っている。今回の動画はOpenSourceSummit North America 2023で収録されたインタビューだ。

●動画：Demo of the Cedar Programming Language - The Open Source Language from AWS

The New Stackは最新の注目すべきソフトウェアや企業、エンジニアにフォーカスしてインタビュー動画を多数公開している。他にも多くの動画が公開されているので以下の公式チャネルから参照して欲しい。

●The New StackのYouTubeチャネル：The New Stack

今回はAWSのSenior Principal Applied Scientistという肩書を持つMike Hicks氏による15分弱のインタビューとデモを収めた動画でCedarを解説している。

Cedarを紹介するHicks氏は「サイエンティスト」というタイトルを持つ

Cedarそのものは2023年5月にAWSの公式日本語サイトでも紹介されている。

●AWSの公式アナウンス：アクセス制御用のオープンソース言語 Cedar の紹介

この解説文は英語からの翻訳であるためか非常に堅苦しい文章となっているが、ポイントは以下の文章だろう。「Cedarの正確性とセキュリティについて高い保証を提供する新しい検証ガイド付き開発プロセスを採用しています。これによりAWSはCedarの認証エンジンやその他のツールを正式にモデル化し、自動推論を使用するそれらの安全性と正確性を証明し、モデルがRustの実装と一致することを厳密にテストします。」

すでにAWSのサービスの中で実装されているとしてAmazon Verified Permissionsが実装例として紹介されており、実装にCedarが使われていることがこのプレビュー版のサービス告知のページにも記載されている。

●参考：Amazon Verified Permissions

アナウンスに書かれている参照元としての英文によるCedarのブログ記事は、より詳細にAutomated Reasoning（自動で実行される推論機能）が主な訴求ポイントとなっている。

●参考：Cedarの自動推論の解説：How we built Cedar with automated reasoning and differential testing

このブログを書いたのがMike Hicks氏であり、Cedarのコンセプトを語るには最適な人材ということになるのだろう。このブログ記事ではCedarのポイントとして2点を挙げており、それがAutomated ReasoningとDifferential random testingであるという。単にポリシーをRegoやYAMLで記述するのであれば先行するOPA（Open Policy Agent、ポリシー記述はRego）やKyverno（ポリシールールはYAMLで記述）などが存在する。

●参考：
OPAのポリシー言語解説
Kyvernoのポリシールール

ポリシーの書き方はそれぞれであるが、AWSが特に強調したいのがAutomated Reasoningである点に注目したい。Hicks氏はポリシーを書く場合に、最初はシンプルだったポリシーのルールが徐々に複雑化して、更新や追加を行う際、以前に記述されたポリシールールと新たに追加されたルールの間で齟齬が生じることを問題点とみなしている。それを解消するのがAutomated Reasoningであるというのが、The New Stackの動画の最後の部分で簡単に説明されている。Automated Reasoningは、書かれたポリシールールが既存のルールと矛盾しないかをチェックする機能だ。

この動画ではTinyTodoというToDoリストを管理するシンプルなアプリを例に挙げてToDoの作成、更新、参照などを複数のユーザーを切り替えて実行し、ToDoアイテムへのアクセス権の可否を見せることでポリシーが有効化されていることを示している。

PythonのクライアントからRustで書かれたサーバーにアクセスする際にCedarがアクセス可否を判定

このサンプルアプリケーションもGitHubで公開されているので、より詳細に中身を確認する場合は以下のリンクから行って欲しい。ポリシーの記述内容はpolicies.cedarというファイルにある。

●参考：https://github.com/cedar-policy/cedar-examples/tree/main/tinytodo

●ポリシーの記述：https://github.com/cedar-policy/cedar-examples/blob/main/tinytodo/policies.cedar

デモとしてVisual Studio Codeで実際の記述内容を見せながら、誰に何が許可されるのかを解説している。

エディターでポリシーの記述を見せながら解説

Pythonで書かれたクライアントからRustで書かれたサーバーにコマンドを送り、ユーザーを切り替えてポリシーが適用される部分を見せている。

コマンドをクライアントからサーバーに送ることでアクセスの可否を見せる

Cedarのポリシーは非常にわかりやすい英文に似た構文で構成されており、「誰が何に対して何をどのような条件であれば実行可能なのか？」を記述する構造になっている。

Cedarの言語の基本構造

この他にもCedarにはチュートリアル、Playgroundが用意されており、先行するOPAやKyvernoとは異なり、後発ならではの豊富な機能が用意されている。

●Cedarのチュートリアル：https://www.cedarpolicy.com/en/tutorial
●CedarのPlayground：https://www.cedarpolicy.com/en/playground

Cedarの基本的な機能であるAutomated ReasoningとDifferential random testingについては、以下の記述が参考になるだろう。

Automated ReasoningとDifferential random testingを解説

CedarのAutomated Reasoningは、Dafnyというプログラミング言語がベースになっているという。またDifferential random testingについてはRustで書かれたテストモジュールがランダムにテストを実行してルールに矛盾がないかをチェックするという構造だ。

●参考：Dafnyの公式サイト：https://dafny.org/

Dafnyは7人というコントリビューターで構成されている小さなオープンソースプロジェクトだが、MIT Pressから2023年に書籍も発表されている。著者はK. Rustan M. Leino氏、Hicks氏と同じAWSのSenior Principal Applied Scientistだ。

●参考：https://mitpress.mit.edu/9780262546232/program-proofs/

Automated ReasoningとDifferential random testingを図式化

Differential random testingについても解説が行われており、RustのビルドツールであるCargoのファジングテストフレームワークが使われていると説明されている。同じテストをDafnyのモデルエンジンとRustで書かれたプロダクションエンジンに与えて同じ結果が出ればOK、そうでなければどこかにバグが存在しているというのがこのDifferential random testingの概要だ。

Rustのファジングテストフレームワークを使ってファズテストを実行

単にルールを書き、それを実装するだけではなく、ルールが増加した場合に既存のルールと齟齬がないかどうかをチェックする仕組みが予め組み込まれているというのが、OPAやKyvernoとの差別化だろう。またAWSが自身のサービスで利用していることも大きなポイントと言える。アプリケーション内部でアクセス制御を実装するのではなく、ルールの記述とチェックを切り出せるのはアプリケーションデベロッパーにとっては大きな利点だし、運用担当者にとってもポリシールールの齟齬をあらかじめ発見できるのはプラスになるだろう。今後、AWS以外での実装がどれだけ増えていくのか、注目したい。

●Cedar公式サイト：https://www.cedarpolicy.com/en

Cedar公式サイトに書かれている3つのポイント

Cedarの公式ページにも、以下に示した3つのポイントが挙げられている。

• シンプルでわかりやすい記法
• 高速であること
• Automated Reasoningによる分析機能

ちなみに先行するOPAにはエンタープライス版が存在し、OPAの開発を行っているStyraが公開しているドキュメントによればEnterprise OPAのLive Impact Analysis（LIA）がこのAutomated Reasoningと同じ機能を果たすようだ。この辺りも先行する同じ領域のソフトウェアから学んでいるということだろうか。

●参考：Enterprise OPAのLive Impact Analysis