機能 / レベル付きで封印されるファイル

動作中Lean 4 で証明済み

すべてのファイルがレベルを持ち、保存した瞬間に封印される。

レベル別フォルダに保存すると、ZENOS はファイルを暗号化し、署名付きのヘッダーにレベルを書き込みます。鍵は利用者ではなくシステムが持つので、コピーしたファイルは他の場所では開けず、許可されたレベルより上の人にも開けません。

AES-256-GCM

で暗号化。レベルは署名付きのヘッダーに記録

メモリ上だけ

中身が平文になるのは、開いている間のメモリ上だけ

L1〜L5

Basic から特定秘密まで、五つのレベル

どう動くのか

封印する、開く、守る

1

封印する

レベル別フォルダ(Basic、Green、Red、Black)に保存すると、root で動く鍵管理サービスを通してファイルが暗号化されます。

  • 利用者がレベルの鍵を持つことはありません
  • 封印と開封はすべて台帳に記録されます
2

開く

鍵管理サービスが平文を渡すのは、利用者に許可されたレベルまでか、責任者が署名した承認がある一つのファイルだけです。

  • Office 形式のファイルはメモリ上の写しで編集します
  • 保存すると再び封印されます
3

守る

L3 以上は、画面に出ている間、アプリからのコピーと画面の取り込みを拒否します。

  • レベル付きのクリップボードは、L4 の内容を L4 以上にだけ貼り付けます
  • 方針で決めたレベルより上は印刷できません

レベル

レベルごとに求めるもの

L1 Basic:日常のファイル承認は不要
L2・L3 Green:L3 からはコピーと画面の取り込みを拒否許可レベルより上は責任者 1 人
L4 Red:開いている間は新しい外向きの通信を遮断許可レベルより上は責任者 2 人
L5 Black:特定秘密。印刷されない許可レベルより上は責任者 3 人

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

開けるかどうかの判断は、数学で決まる

Lean 4 で証明済み

毎回のビルドで検査

  • ファイルの平文が渡されるのは、許可されたレベルの範囲内か、そのファイルだけに対する有効な承認があるときだけ
  • どんな出来事の並びでも、PC が止まっている間にファイルが開かれることはない
  • あるレベルの中身は、同じかそれより上のレベルの場所にしか届かない
  • 複製を何度渡しても、レベルが下がることはない
証明ではなく信頼しているもの

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

  • 暗号(AES-GCM と Ed25519)
  • 鍵は root が持つファイルで、まだ TPM には封じていない
  • 強制アクセス制御(SELinux)を入れるまでは、他のプログラムが複製を書き出せる
  • 画面に向けたカメラ

プレビュー版で試す

自分で試す

1

Red · L4 に保存する

デスクトップの Red フォルダにファイルをドラッグします。封印された .zen ファイルになります。

2

許可レベルより下から開く

L2 までの許可しかないアカウントで開くと、責任者に申請が届きます。

3

二人のスマートフォンで承認する

責任者がそれぞれ ZENOS Messages で承認すると、そのファイルだけが開きます。