Lean言語で権限逸脱が起きないことを数学的に証明、「Nyxis」が保証する安全性とは

Nyxisは、Webアプリのサーバー側を組み立てるバックエンドフレームワークだ。仕組みの核は、モデル内のデータ操作を認可判定に通す構造と、その構造の安全性をLean言語で確かめる証明にある。

DBを直接操作できない構造にする

認証は「誰か」の確認、認可は「何をしてよいか」の判断だ。Nyxisでは、権限ルールを記述する言語Cedarで、許可条件をポリシーに、データの項目・型をスキーマに定義する。

HTTPの要求を受けて実行する処理をハンドラと呼ぶ。Nyxisのモデルでは、ハンドラは「値を返して終了する」か「アクションを呼び、その結果を受けて続ける」かの組合せで表す。DBを直接読み書きする命令は、この仕組みに含まれていない。

例えば投稿の編集なら、ハンドラは編集アクション・投稿のID・新しい値を渡す。認可層が現在の利用者と投稿を照合し、Cedarのポリシーが許可した場合だけ、宣言済みの項目を更新する操作を発行する。

編集要求は認可層を通り、許可された場合だけ更新操作が発行される。

利用者が投稿の編集を要求ハンドラが編集アクション・投稿ID・新しい値を渡す

Nyxisの認可層で判定承認済みポリシーと、現在の利用者・投稿を照合

作者または管理者許可する編集ポリシーの条件を満たす

更新操作を発行入力・整合性の検査後、タイトル・本文が対象

どちらにも該当しない拒否する編集ポリシーの条件を満たさない

更新操作を発行しないこの編集要求で投稿を変更しない

公式掲示板のモデル上の流れ。対象の存在や入力の妥当性など、認可以外の検査も必要。

判定に使う利用者は、認証結果から実行側が渡す。モデル内のハンドラは、アクションの呼び出し時に別の利用者へ差し替えられない。操作を認可層に集め、ハンドラが権限判定を飛ばす経路をモデルからなくしている。

Leanは、プログラムと数学的な証明を書き、証明の論理が正しいかを機械で検査できる言語だ。こうした数学的な方法で処理の性質を確かめることを、形式検証という。Nyxisの認可安全性の証明は、次の順に組み立てられている。

これにより、特定の利用者や入力だけを試すテストより広く、モデルが表す要求列全体について権限逸脱が起きないことを示す。証明はビルド時にLeanが検査する。

Nyxisは、AIがハンドラを書き、人がスキーマとポリシーを承認する開発を想定している。このハンドラの形式に従う限り、AIが処理の順序や分岐を変えても、データ操作には認可層を通る必要がある。

証明が扱うのは、このモデル内の処理だ。ビルドや起動時のコードまで含めてAIを隔離する仕組みではなく、検査と開発・運用の前提を保つ必要がある。

モデルの証明を実システムへ適用するには、コード・実環境・運用の前提が要る。

Nyxisの証明と、その外側の前提

モデルで証明する性質各操作が、設定した権限ルールの範囲に収まる

実運用でこの性質を成り立たせる次の3つを前提として信頼する

証明の外で動くコード処理系・ライブラリ・未証明の接続処理が想定どおり動く

認証・DB・通信の実環境本人確認とデータ操作が正しく、別経路からのアクセスを制限する

人が決める権限と運用意図に合うポリシーを承認し、検査済みコード・設定・鍵を管理する

認可された操作からSQLを生成する処理には証明済みの部分があるが、実DBへの効果やHTTP通信との対応には未証明の部分が残る。情報漏洩全般の防止は証明の対象外だ。

また、非公開文書に誤って「全員が閲覧できる」と設定すれば、文書を返してもルールには従っている。誰に何を許すかは人が判断する。Nyxisは2026年10月27日時点で開発中であり、導入時は自社の権限ルールを表せるかと、実環境で前提を維持できるかを確かめたい。

自社システムの認可設計やセキュリティ対策について、お気軽にご相談ください。