シェルもSSHも無いOS「QEDOS」、侵入されても好き勝手できない

どんなアプリか

QEDOS は、seL4 というマイクロカーネルの上に作られた実験的な OS です。インターネットから HTTPS のアクセスを受け付け、内部のサーバーへ転送する役目に絞って作られています。

「AIがセキュリティホールを見つけるのが得意になったのなら、逆にAIを使ってセキュリティホールのないOSを作ればいいのではないか？」

shi3z さん、WirelessWire & Schrödinger’s の記事（2026-10-18）

シェル（/bin/sh）も SSH サーバーも入っていません。ログインしてコマンドを実行したり、プログラムを入れたりする仕組みそのものを持たない作りです。

機能は、TCP の受け付け、TLS の処理、HTTP の解析、アクセスの許可の判定、バックエンドへの接続という5つの独立した領域に分けられています。暗号鍵を持つ領域とバックエンドへ接続する領域が直接通信できないことなどは、権限構成のモデルに対して検証されています。

HTTP の解析、アクセス制御、設定ファイルの処理は Rust で書かれています。検証ツール Kani による有界モデル検査を13件の項目について行い、公開された結果では13件すべてを通過しています。

通信は TLS 1.3 に加えて、ハイブリッド鍵交換方式「X25519MLKEM768」が必須です。耐量子暗号を使わない通信は拒否します。Chrome から HTTPS で接続できることは作り手が確認しています。

現在は x86-64 向けの構成が QEMU という仮想マシンの上で起動し、HTTPS の受け付けから許可されたバックエンドへの転送まで動きます。リポジトリにはビルド済みのイメージが含まれていて、Mac の上でもクロスツールチェーンを作り直さずに起動して試せます。

入れる前に

作り手は、QEDOS をまだ完成品ではないとしています。1万本の同時 TLS 接続の試験（ピークのメモリ使用量は約285MB）は Linux 上の参照実装を同じマシンの中で動かした結果で、seL4 上の QEDOS 本体で同じ性能が出ることは確かめられていません。

サーバー証明書の認証には従来型の ECDSA を使っているため、認証まで含めて耐量子暗号になっているわけではありません。形式検証も、対象のプログラム・入力範囲・前提条件に限られ、OS 全体にバグが無いことを示すものではないと作り手は書いています。

TLS 1.2 では接続できず、従来型の鍵交換しか使えないクライアントもつながりません。

aarch64 向けは実験的な扱いで、Raspberry Pi 4 向けのイメージはビルドできるものの、実機ではまだ起動していません。README は、aarch64 の乱数源が開発用の仮のもので安全ではないと注意しています。

README は最初に docs/STATUS.md を読むよう求めていて、そこで検証済みの部分とハードウェアに左右される部分を分けて説明しています。GitHub のリポジトリには、ライセンスが書かれていません。