機能 / 証明された判定
判定は数学であり、プログラムはその数学を実行する。
ファイルが開くか、承認が有効か、止まった PC を解除してよいか、中身がどこへ流れてよいか、台帳が無傷か、何が PC の外へ出てよいか、パスワードを渡してよいか。これらを決める規則は Lean 4 で書かれ、機械で検査された証明を持ちます。
プログラムは一つ
zenos-decide。証明の対象と同じ定義から作る
sorry なし
定理は Lean の標準の公理だけに依っている。そうでなければビルドが失敗する
毎回のビルド
で検査。証明を壊す変更は出荷されない
どう動くのか
書く、証明する、動かす
1
書く
それぞれの判定は Lean の関数です。事実を入れると答えが出ます。ZENOS のほかの部分が同じ判定を作り直すことはありません。
2
証明する
Lean のカーネルが、ビルドのたびにすべての定理を検査します。別の検査が、公理が足されていないかを確かめます。
3
動かす
すべてのサービスが、その定義から作ったプログラムを呼び、その答えに従います。答えがない、遅い、読めないときは「いいえ」です。
- ネットワークの見張りにとっては「遮断」です
証明していること
六つの分野、一つのプログラム
ファイルを開くことと、止まった PC の解除証明済み
ファイルの中身がどこへ行けるか証明済み
改ざんが分かる台帳証明済み
何が PC の外へ出てよいか証明済み
責任者の署名は使い回せない証明済み
スマートフォンでのサインイン証明済み
謝辞
これらの判定を Lean で証明するという発想は、Web バックエンドの認可を証明する Nyx Foundation の Nyxis から得ました。Nyxis は、認可器を Lean で検証した Amazon の Cedar や、検証済みカーネル seL4 などの先行研究の上に立っています。ZENOS はそれらのコードを一切使っていません。
証明していること、していないこと
証明が届く範囲
Lean 4 で証明済み
毎回のビルドで検査
- 判定そのもの。どんな入力に対しても
- 一回ごとの判定だけでなく、どんな出来事の並びに対しても成り立つ性質
- 署名の数え方（署名は偽造できないものとして扱う）
証明ではなく信頼しているもの
テストし、一覧にして公開
- 暗号（前提として扱っている。計算量の意味での証明は範囲外）
- サービスが読み取る事実（許可レベル、登録済みの責任者、停止の状態、時計）
- つなぎのコード、ネットワークの見張り、カーネル、Python、Lean のコンパイラ