システムの「正しさ」は記述できるか？ Cedar に学ぶ検証可能な仕様の作り方

この 1 年、生成 AI によりコードの実装コストは劇的に下がりました。一方、生成されたコードの正しさをレビューする人間の側がボトルネックになりつつあります。逆に考えれば、「正しさ」を機械的に検証可能な形で与えることの重要性がより増したとも言えるでしょう。

本講演では、AWS が分析可能性（Analyzability）を出発点に設計した認可エンジン Cedar を取り上げます。しかし真のテーマは認可やセキュリティではなく、「検証可能な仕様とは何か」という切り口から設計・検証のプロセスを解説します。

Cedar では、最適化や設定変更における意味論的な同値性を仕様として保証し、さらに CI により仕様と実装の一致も検証しています。これらはいずれも、包括的に満たされるべき性質（Property）として仕様を記述し、最適化前後・変更前後・仕様と実装の「比較」により正しさを保証する考え方に基づきます。

本講演の対象はセキュリティ担当だけでなく、複雑な仕様と戦う全てのエンジニアです。テストしづらい仕様に出会ったとき、「比較」の思考で検証可能な性質を切り出す技法を持ち帰って頂ければ幸いです。