Arita Tomoki

情報漏洩が起きないことを数学的に保証するバックエンドフレームワーク「Nyxis」を公開しました！ たぶん世界初です。 Nyxisで書かれたバックエンドは、企業の持つ機密情報をより安全に守ることができます。 昨今急増しているサイバー攻撃を防ぐ手段として、このような方法があることをお伝えしたいと思い、今回の発表に至りました。 開発者は「どの権限を持つユーザーが何を実行可能であるか」のルールを管理するだけで、残りのコードをAIエージェントに任せても認可の安全性が担保されます。 Nyxisは大部分がLean言語で記述されており、形式検証によって 「任意のHTTPリクエスト列に対し、認証された主体の正当な権限を逸脱するデータの読取・変更・削除・権限付与は発生しない」 という認可安全性定理を機械的に証明しています。 認可の不備は、OWASP脆弱性ランキングにおいて2019年版から連続1位であり、最優先で対策すべきリスクの一つです。 形式検証を活用したこのフレームワークは、テストに頼る従来の開発に比べて、格段にセキュアなソフトウェアを実現します。 先日MicrosoftとGitHubが、形式検証を用いた開発キット「PDD Kit」を発表しました。 こちらはより幅広い性質を扱える一方、プログラムごとに仕様を作り、それが意図に合っているかを開発者が確認する必要があります。 Nyxisは証明する定理を認可安全性に絞ってあらかじめ定めているため、開発者はポリシーを管理するだけで済みます。 もちろん、一定の仮定は存在しています。証明外コードと実行環境は信頼する前提であり、開発者がポリシーを誤って書けば、意図した保護は得られません。 この定理の範囲内において、数学的保証は非常に強力です。実システムに組み込める技術としてここまでの保証を与えたものは、私の知る限りまだ存在しません。 一方で、表現力の乏しさやLeanのライブラリ不足など、改善すべき点はまだ山積みです。 本当はもっと完成度が高まった時点で公開しようと考えていましたが、昨今のセキュリティインシデントの状況を鑑みて、このタイミングで発表することにしました。 世界をセキュアにする一助になれば嬉しいです。 github.com/NyxFoundation/nyx…