機能 / 中身がどこへ行けるか

Lean 4 で証明済み動作中

すべての複製の行き先を、一つの規則で決める。

フォルダ、ウィンドウ、クリップボード、プリンター、そして AI の種類ごとに、すべてが同じ証明済みの判定に問い合わせます。ファイルの中身は上のレベルへは移れても下へは移れず、どの場所にも超えられない上限があります。

規則は一つ

ファイルの中身の複製が届きうる、すべての場所に

上へは行けても下へは行けない

あるレベルの中身は、同じかそれより上にだけ届く

L5

は印刷されず、L5 の場所にとどまる

どう動くのか

問い合わせる、判定する、記録する

1

問い合わせる

名前を付けて保存、貼り付け、クリップボード、印刷、AI への送信は、どれも動く前に問い合わせます。アプリ、ブラウザ、鍵管理サービスのクリップボードが、同じ問いを使います。

2

判定する

答えは、Lean の証明から作った一つのプログラムが出します。答えが出せないときの答えは「いいえ」です。

  • どこでも同じ規則です
  • アプリごとの例外はありません
3

記録する

複製も拒否も、レベルと一緒に台帳に残ります。漏れたとき、誰の複製だったかが分かります。

  • 印刷したページには、レベル、ファイル名、人、時刻が入ります

上限

それぞれの場所が持てる最も高いレベル

システムのクリップボードL2
政府の外の AIL2
政府の AIL3
プリンター(方針の初期値は L3)L4
省庁自身の AIL5
フォルダとウィンドウそれぞれのレベル

L3 以上がシステムのクリップボードや政府の外の AI に届くことはありません。L4 以上は、省庁自身の AI にしか届きません。

証明していること、していないこと

中身の行き先についての六つの定理

Lean 4 で証明済み

毎回のビルドで検査

  • あるレベルの中身は、同じかそれより上のレベルのフォルダとウィンドウにしか届かない
  • 設定がどうであれ、どの場所も上限を超えるものは持たない
  • L3 以上はシステムのクリップボードにも、政府の外の AI にも届かない
  • L5 は印刷されない
  • 複製を何度渡しても、レベルが下がることはない
証明ではなく信頼しているもの

テストし、一覧にして公開

  • AI については、パケットフィルタは PC で開いた最も高いレベルで判断し、ZENOS に知らされた AI のサービスだけが対象
  • ZENOS のアプリ以外のプログラム
  • 画面に向けたカメラ

プレビュー版で試す

自分で試す

1

L4 の表を開く

Red フォルダから、許可か承認があれば開けます。

2

外にコピーしてみる

Ctrl+C を押してもクリップボードは変わりません。別の L4 のウィンドウへの貼り付けはできます。

3

印刷してみる

方針で決めたレベルより上は、印刷が拒否され、記録されます。