フナイログ

「情報漏洩が起きないことを数学的に保証」を手元で確かめた ―― Lean 製バックエンド Nyxis の敵対的レビュー

Lean で認可の安全性を形式証明したバックエンドフレームワーク Nyxis を手元でビルドし、公開時のポストの主張を一つずつ確かめました。定理は検査を通る一方、POST リクエストの 403/201 の差から他人の下書きの有無が分かる経路を再現しています。