シーダー：認可ポリシーへの新しいアプローチ

シーダーは、認可ポリシーを書くために設計された新しいオープンソースの言語だよ。このポリシーは、アプリケーション内のリソースへのアクセスを制御するんだ。この記事では、シーダーが検証ガイド開発（VGD）という方法を使って開発された経緯について説明するよ。このアプローチは、ソフトウェアが正しい、セキュア、メンテナンスしやすいことを確保するのに役立つんだ。

#シーダーって何？

シーダーは、開発者がアプリケーションのための権限を分かりやすく表現できるようにするんだ。アプリケーションが敏感な操作を実行する必要があるとき、シーダーの認可エンジンにリクエストを送って、関連するポリシーを評価してリクエストを許可するか拒否するかを決めるんだ。ポリシーはアプリケーションコードとは別に書かれているから、更新や監査が簡単なんだ。

シーダーはいろんなアクセス制御スタイル、例えば役割ベースのアクセス制御（RBAC）や属性ベースのアクセス制御（ABAC）をサポートしてる。この柔軟性によって、開発者はアプリ内で誰が何をできるかを具体的に指定できるんだ。

#検証ガイド開発（VGD）

VGDはシーダーを開発するための二部構成のプロセスだよ。最初の部分は、シーダーのコンポーネントのシンプルで理解しやすい形式モデルを作成すること。これらのモデルはLeanというプログラミング言語で書かれてる。目的は、モデルが重要な正確性の特性を満たしていることを証明することなんだ。つまり、モデルがシーダーの期待される動作を正確に表していることを確認するんだ。

VGDの第二部は、差分ランダムテスト（DRT）。この技術はシーダーのプロダクションコードが形式モデルに合致しているかをチェックするんだ。DRTは何百万ものランダムな入力（ポリシー、データ、リクエスト）を生成して、LeanのモデルとRustで書かれたプロダクションコードの両方をテストするの。出力を比較することで、開発者は不一致を特定して、コードのバグを見つけられるんだ。

#VGDの利点

VGDを使うことで、シーダーの開発にはいくつかの利点があるよ。開発プロセスの初期でバグを見つけて修正することでデザインの改善が得られるんだ。形式モデルの作業中に、開発者たちはコードがリリースされる前にいくつかのバグを見つけて修正できたんだ。さらに、DRTや別の手法であるプロパティベースのテスト（PBT）を使って、シーダーのさまざまな部分でもっとバグが見つかったよ。

VGDは高い正確性の保証と開発のしやすさのバランスを取ってる。他の方法が複雑な形式検証に依存しすぎたり、テストだけに頼りすぎるのとは違って、VGDは両方のアプローチをうまく組み合わせているんだ。

#シーダーの認可エンジン

シーダーの認可エンジンは、そのセキュリティの重要な要素だよ。これは、アプリケーションのセキュリティに不可欠なすべてのコンポーネントを含む、いわゆる信頼できるコンピューティングベース（TCB）の一部なんだ。エンジンは、受け取ったポリシーと入力に基づいて決定を下すよ。

これらの決定が正しいことを保証するために、シーダーはVGDを使って開発されたんだ。最初のステップは、エンジンのコンポーネントの分かりやすい形式モデルを作成して、重要な正確性の特性を満たしていることを確認すること。次のステップは、DRTを使ってモデルとプロダクションコードが同じ結果を出力することをテストすることだよ。

#ポリシー構造

シーダーポリシーは、効果、範囲、条件の3つの部分から成り立ってる。

• 効果: ポリシーがアクセスを許可するか禁止するかを示す。
• 範囲: 誰（プリンシパル）、どのアクションが取れるか、どのリソースにアクセスするかを制約する。
• 条件: これらはオプションで、リクエストコンポーネントの属性に基づいたさらなる制約を追加する。

この構造により、開発者はアプリ内のリソースへのアクセスを規定する非常に具体的なポリシーを作成できるんだ。

#差分ランダムテスト（DRT）によるテスト

DRTは、プロダクションコードが形式モデルに合致しているかを確認するのに重要だよ。コードの動作を徹底的にチェックするために、多種多様なテスト入力を生成するんだ。入力生成にスマートなアプローチが必要で、エラーハンドリングコードを過剰にテストしてコアロジックのテストが不足しないようにすることが大事なんだ。

開発者たちはタイプ指向の入力生成器を作ったんだ。まずスキーマを確立して、その後対応するエンティティストアを作り、最後にこのスキーマに従ったポリシーやリクエストを生成するんだ。これにより、テストがコアロジックを効果的に行使できるようになるよ。

#プロパティベースのテスト（PBT）

DRTがモデルとプロダクションコードの出力の一致に焦点を当てているのに対して、PBTはプロダクションコンポーネントの特定のプロパティを直接チェックするために使われるんだ。PBTは、モデルでまだ正式に証明されていない領域を探求できるから、テストの幅が広がるんだ。

DRTとPBTの両方が、シーダーのバグを見つけたり修正するのに効果的だったよ。チームはテストのための入力を生成するさまざまな戦略を使って、異なるシナリオをカバーするために十分な包括性を持たせるようにしてたんだ。

#課題と解決策

シーダーの開発中、開発者たちはソフトウェアエンジニアリングで典型的な課題に直面したよ、とりわけコードの正確性を確保することについてね。特定のバグは広範なテストを通じてのみ特定されたんだ。例えば、一部のバグはモデルとプロダクションコードでのポリシーの実装の違いに関するものだったよ。

これらの課題に対処するために、開発者たちは厳格なテストプロセスを確立し、DRTとPBTの両方を使用したんだ。また、コードの包括的なカバレッジを確保するために、入力生成戦略を洗練させることにも時間を投資したんだ。

#結論

シーダーはアプリケーション内の認可ポリシーを定義するための強力なツールだよ。検証ガイド開発を採用することで、シーダーチームは形式モデルと厳密なテストを効果的に組み合わせて、セキュアで開発しやすくメンテナンスしやすい言語を生み出したんだ。

このアプローチは、高い保証が求められるソフトウェアを作成するための実用的なフレームワークを提供して、セキュリティ上重要なコンポーネントの正確性を保証しつつ、開発者にとって使いやすいものにしているよ。シーダーはオープンソースだから、他の開発者も使ったり、継続的な改善に貢献できるんだ。