開発者向けプレビュー版 · 試用と評価のための版です

機能

守りを OS に組み込む。機能ごとに、その中身まで。

世界中で多くの人がコードを直して攻撃を防いでいます。その取り組みは欠かせません。ZENOS はそれと並んで、OS のレベルでも守ります。一つのプログラムの弱点が、そのまま流出につながらないようにするためです。それぞれの機能について、どう動くのか、何を証明しているのか、まだ何ができていないのかを書いています。

動作中Lean 4 で証明済み試験中次の版で
動作中

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

すべてのファイルが L1〜L5 のレベルを持ち、保存した瞬間に暗号化されます。中身が平文になるのは、開いている間のメモリ上だけです。

詳しく見る →
動作中

開くには承認

自分のレベルより上は、責任者が自分のスマートフォンで承認します。レベルが高いほど承認者が増え、自分の申請を自分で承認することはできません。

詳しく見る →
動作中

漏えいの兆候で停止

USB への持ち出し、大量のファイルの読み出し、承認のない送信。PC はミリ秒で封じ込めます。誰かが警告を読むより前に。

詳しく見る →
動作中

外からのアクセスを見張る

外から来る新しい接続は、最初からすべて拒否します。拒否した数とサインインの失敗を数えて表示し、外されたファイアウォールは張り直します。

詳しく見る →
Lean 4 で証明済み

中身がどこへ行けるか

フォルダ、クリップボード、プリンター、AI の種類ごとに、一つの規則がすべての複製を判定します。中身が下のレベルへ移ることはなく、L5 は印刷されません。

詳しく見る →
動作中

改ざんが分かる台帳

すべての操作はハッシュの鎖につながり、別々の組織が運用する監査ノードに写されます。書き換えられた過去は見つかります。

詳しく見る →
Lean 4 で証明済み

証明された判定

ファイルを開く、鍵を渡す、止まった PC を解除する。その規則は Lean 4 で証明しており、動いているのは同じ定義から作ったプログラムです。

詳しく見る →
動作中

メッセージとビデオ通話

メッセージは Signal のプロトコルで暗号化します。ビデオ通話は自分たちで運用するサーバーで動き、エンドツーエンドで暗号化します。誰かが参加したり抜けたりするたびに鍵が変わります。

詳しく見る →
試験中

スマートフォンでサインイン

保存したパスワードは、あなたのスマートフォンが作る鍵でしか開きません。PC を盗まれても、ディスクを複製されても、パスワードは出てきません。

詳しく見る →
動作中

情報を外に出さずに AI を使う

組織の AI をつなげば、文書、表計算、プレゼンが、どの PC からでもその AI を使えます。レベルの高いファイルはその AI にしか行かず、外には出ません。特定の AI に縛られません。

詳しく見る →
試験中

分散保管

封印されたファイルは暗号化された断片に分けられ、認証されたノードに散らばります。一台のマシンがファイル全体を持つことはありません。

詳しく見る →
次の版で

Studio

音楽と写真のライブラリ、音のトリミング、音に写真をのせた動画づくり。Personal と Family の版のための機能です。

詳しく見る →