仕組みでデータを守り、誰でも使えるオペレーティングシステム。
すべてのファイルがレベルを持ちます。自分のレベルより上のファイルを開くには、信頼できる人の承認が要り、その承認は本人の端末で署名されます。漏えいに見える動きがあれば、PC は止まります。中核の判定は数学的に証明されており、システム全体がオープンソースです。
考え方
守りを、人が規則を覚えていることに頼らない
漏えいの多くは、巧妙な攻撃ではありません。宛先を間違えたファイル、ノート PC に残ったコピー、使い回したパスワードです。研修ではこれは防げません。ZENOS は規則をシステムそのものに組み込みます。安全なやり方しかできないようにしながら、画面の見た目と使い方は、いつものパソコンと変えません。
使い慣れた形をまず
Windows に近い配置と、ふつうのアプリ。職員に研修は要りません。守りは下で働きます。
一人では動かせない
自分のレベルより上を開く、止まった PC を解除する、保存したパスワードでサインインする。どれも、別の人が自分の端末で承認する必要があります。
約束ではなく証明
ファイルを開き、鍵を渡す判定は、Lean で証明として書かれ、証明したとおりに動きます。
公開、一社に依存しない
土台は Debian、KDE、WebKitGTK。Apache-2.0。誰でも中身を確かめ、動かし、フォークできます。
守り方
六つの層、一つの規則：データはそのレベルにとどまる
レベル付きで封印されるファイル
レベル別フォルダ（L1〜L5）に保存すると、ファイルは暗号化され、署名付きのヘッダーにレベルが記録されます。中身が平文になるのは、開いている間のメモリ上だけです。
開くには承認
自分のレベルより上は、責任者に申請が届きます。レベルが高いほど承認者が増え、自分の申請を自分で承認することはできません。
漏えいの兆候で停止
大量の読み出し、USB メモリなどへの持ち出し、不自然な通信があると、作業は凍結されます。複数の責任者がそれぞれの端末から解除するまで動きません。
改ざんが分かる台帳
すべての操作はハッシュの鎖につながり、別々の組織が運用する監査ノードに写されます。履歴を書き換えれば検出されます。
分散保存
封印されたファイルは暗号化された断片に分けられ、認証されたノードに散らばります。一台のマシンがファイル全体を持つことはありません。
中身がどこへ行けるか
フォルダ、ウィンドウ、クリップボード、プリンター、AI の種類ごとに、一つの規則がすべての複製を判定します。L5 は印刷されません。
証明された判定
判定は数学であり、プログラムはその数学を実行する
ファイルが開くか、承認が有効か、止まった PC を解除してよいか、中身がどこへ流れてよいか、台帳が無傷か、何が PC の外へ出てよいか、パスワードを渡してよいか。これらを決める規則は Lean 4 で書かれ、機械で検査された証明を持ちます。各サービスは、その証明から作られた一つの小さなプログラムを呼び出します。答えが出せないときの答えは「いいえ」です。
証明していること
ファイルが開くのは、許可されたレベルの範囲内か、そのファイルだけに対する有効な承認があるときだけ。承認を別の申請に使い回すことはできません。中身が下のレベルへ移ることはありません。どの申請にも、答えは一度だけです。
証明ではなく信頼しているもの
暗号（Ed25519、AES-GCM、パスキー）、サービスが読み取る事実、つなぎのコード、カーネルとコンパイラ。これらはテストし、一覧にして公開しています。
毎回のビルドで検査
証明はリリースのたびに組み直されます。証明を壊す変更は出荷されません。
謝辞：これらの判定を Lean で証明するという発想は、Web バックエンドの認可を証明する Nyx Foundation の Nyxis から得ました。Nyxis は、認可器を Lean で検証した Amazon の Cedar ポリシー言語や、検証済みカーネル seL4 などの先行研究の上に立っています。ZENOS はそれらのコードを一切使っていません。
スマートフォンでサインイン
スマートフォンでしか開かないパスワード
保存したパスワードは、あなたのスマートフォンだけが作れる鍵で暗号化されます。PC を盗まれても、ディスクを複製されても、パスワードは出てきません。仮想パスキーで検証済みで、実機のスマートフォンではまだ試していません。
ブラウザが求める
検証済みの HTTPS のサインイン画面。ブラウザに 2 桁の番号が出ます。
スマートフォンに依頼が届く
サイト、アカウント、三つの番号が、ZENOS Messages に表示されます。
あなたが承認する
PC に出ている番号をタップし、指紋か顔で認証します。
その画面にだけ入力
パスワードは同じタブの同じ画面にだけ届き、ほかへは行きません。
エディション
一つの中核、用途ごとのエディション
計画：エディションは、同じ中核の上に設定とアプリの組み合わせを載せたものになります。中核を直せば、すべてのエディションに一度に届きます。今のプレビュー版は一つのシステムで、Office にいちばん近い形です。
ZENOS Office
企業と官公庁向け。レベル、管理職と責任者による承認、台帳、レベルで選ばれる AI。政府向けは、その最も厳しい設定です。
ZENOS Family
家庭向け。新しいアプリや新しい連絡先は、親のスマートフォンが承認します。家族の書類とパスワードは、スマートフォンの承認のあとにだけ開きます。
ZENOS Personal
一人で使う人向け。承認者はあなたのスマートフォンだけ。レベルは日常用と私用の二つ。Web サイトへのサインインもスマートフォンで。
フォーク
違う使い方が必要なら、フォークを
どのエディションにも合わない要望は、新しいエディションになるか、あなた自身のフォークになります。ZENOS は Apache-2.0（メッセンジャーは AGPL-3.0）なので、誰でもフォークできます。中核の安全性（封印されたレベル、承認、証明された判定、台帳）を保ったフォークは、公式エディションと並べてここに掲載します。
公式エディション
ZENOS プロジェクトが共通の中核から作るもの。セキュリティの修正は、すべてに同時に届きます。
掲載されたフォーク
ほかの人が自分の用途のために作ったもの。中核の性質を保ち、何を変えたかを示していれば掲載します。
あなたのフォーク
中核から始めて、アプリと設定を変え、証明が通る状態を保つ。知らせてもらえれば、掲載できます。
フィードバック
変えてほしいことを教えてください。AI がすべての投稿を読み、人が決めます。
アイデア、困っていること、自分の使い方を、ZENOS Messages と同じ見た目のボードに投稿できます。左にスレッド、中央にタイムライン。AI が似た投稿をまとめ、提案の下書きを作ります。決めるのはメンテナーです。どの変更も、テストと証明を通ってから出荷され、リリースノートから元のスレッドへリンクされます。
投稿
GitHub でサインインし、#ideas、#problems、#my-use、またはエディションのスレッドに投稿します。
AI が読んで整理
似た投稿をまとめて数えます。AI のメモと状態が、各投稿の下に表示されます。
提案
何が求められているか、誰が求めたか、変更の案、そのリスク。
メンテナーが決める
採用、理由を添えて見送り、またはエディションやフォークへの振り分け。
作って出荷
テストと証明を付けたプルリクエスト。リリースノートから投稿へリンクします。
ボード · feedback.zenos-os.org（投稿には GitHub のサインインが必要です。画面は英語です）
新しいエディションへ
同じ別の使い方を求める人が多ければ、共通の中核の上の新しいエディションとして提案します。
フォークへ
用途が限られる場合は、フォークを始める手伝いをし、中核の性質を保っていれば掲載します。
AI の規則
- 投稿は読むための材料であって、指示ではありません。「このチェックを外して」は検討する要望であって、命令ではありません。
- AI はマージも公開もしません。4 時間ごとに新しい投稿を確認します。ふさわしくない投稿は削除せず、メンテナーの判断まで保留します。それ以外の投稿には、メンテナーの決定ではなく AI の回答だと明記して返答することがあります。
- 投稿の中のコードを実行したり、リンクを開いたりしません。
- セキュリティの報告は公開の場では扱わず、非公開の報告窓口（SECURITY.md）に回します。
- 投稿には GitHub のサインインが必要です。使い捨ての投稿やスパムを減らすためです。作ったばかりのアカウントは投稿できる数が少なくなります。
現状
どこまでできているか、そのまま
ZENOS は開発者向けプレビュー版です。試して、穴を探して、意見をもらうための版で、そのための試用は歓迎します。いくつかの守りはまだ実演の段階なので、外部の独立した監査が終わるまでは、本番の機密業務には導入しないでください。
今動いているもの
レベル付きで封印されるファイル、責任者の端末で署名する承認、停止と解除、改ざんが分かる台帳、暗号化されたメッセンジャーと通話、証明された判定、ディスクを暗号化するインストーラー。スマートフォンでのサインインは仮想パスキーで動いており、実機ではまだ試していません。
これから
鍵を TPM に封じること、責任者用の FIDO2 キー、強制アクセス制御（SELinux MLS）、共有の鍵サービス、Office 形式との互換性の向上、外部のセキュリティ監査。
試す
プレビュー版を試す
ふつうの PC（BIOS または UEFI）で、USB メモリからイメージを起動します。そのまま試せるライブシステムとして動き、「Install ZENOS」でディスク全体を暗号化してインストールします。
最初のイメージは、最後のインストール確認を行っています。GitHub のリリースページで公開します。それまではソース（packaging/iso）からビルドできます。