- Editors' Top :
- 協創の現場から／日立製作所
- 研究をつなぐ（KDDI総合研究所）
- シュレディンガーの水曜日
Image by Unsplash
October 18, 2026
清水 亮 ryo_shimizu
新潟県長岡市生まれ。1990年代よりプログラマーとしてゲーム業界、モバイル業界などで数社の立ち上げに関わる。現在も現役のプログラマーとして日夜AI開発に情熱を捧げている。
最近、日本の企業がサイバー攻撃によって大変なことになっている。
2025年9月にはアサヒグループホールディングスがランサムウェア攻撃を受け、受注・出荷業務が停止した。翌10月にはアスクルが同様の攻撃を受け、通販サービスの受注・出荷が停止。サプライチェーン全体に影響が波及する事態となった。挙句、本来、インターネットが本業のはずのさくらインターネットまでもが個人情報流出という状況になっている。これは国家的危機だ。
いずれも我々の日常生活に深く関わる企業である。コンピュータシステムが止まるということは、単にWebサイトが見られなくなるという話ではなく、ビールが届かなくなり、文房具が買えなくなり、物流が止まるということである。
一方、AIの能力は恐ろしい速度で進歩している。
以前、セキュリティホールを発見するには、コンピュータの内部構造を熟知した高度な専門家が必要だった。脆弱性を発見し、悪用できるかどうか調査し、攻撃コードを作成するには相応の技術と時間が必要だった。
ところが最近は、AIがプログラムを読み、問題点を指摘し、場合によっては攻撃コードの作成まで支援してしまう。
もちろん、アサヒやアスクルに対する攻撃がAIによって行われたという証拠があるわけではない。しかし、AIの登場によってサイバー攻撃を行うために必要な技術的ハードルが下がりつつあるのは確かだ。
そこで、筆者はふと思った。
「AIがセキュリティホールを見つけるのが得意になったのなら、逆にAIを使ってセキュリティホールのないOSを作ればいいのではないか？」
そんなわけで、実際に作ってみた。
名前は「QEDOS（クエドス）」。
https://github.com/shi3z/qedos
数学の証明の最後に書かれる「Q.E.D.（クォド・エラト・デモンストランダム/証明終わり）」から取った名前である。厨二病みたいな名前だが、考えたのはChatGPTだから僕のせいではない。
目指したのは、いわば「絶対無敵のOS」だ。
もちろん、世の中に絶対安全なソフトウェアなど存在しない。しかし、絶対安全を目指して設計することと、最初から絶対安全を諦めることには大きな違いがある。
今回はその顛末について書いてみたい。
WindowsやLinuxは非常によくできたOSだ。
何十年もの開発の歴史があり、世界中のプログラマーが改良を重ねている。セキュリティ対策も日々行われている。
しかし、WindowsやLinuxには根本的な問題がある。
できることが多すぎるのだ。
例えばLinuxには、ファイルを読み書きする機能があり、プログラムを起動する機能があり、ユーザーを管理する機能があり、外部からSSHでログインする機能があり、ネットワークを制御する機能がある。
もちろん、これらの機能は必要だから存在している。
ただし、機能が増えれば増えるほど、攻撃できる場所も増える。
Webサーバーに脆弱性が見つかる。そこから攻撃者が侵入する。侵入した攻撃者が別のプログラムの脆弱性を利用して管理者権限を取得する。そして、システム全体を乗っ取ってしまう。
こうした攻撃の連鎖が成立するのは、そもそもOSが膨大な機能を持っているからでもある。
そもそも、Webサーバーにとって、SSHできることはメンテナンス上の都合であって必須機能ではない。
だったら、最初から余計な機能を全部なくしてしまえばいい。
メンテナンスも専用クライアントで専用に暗号化すれば、まず破ることができないようになる。
ここで重要なのは、筆者が作りたかったのは、普通のパソコンで使うためのOSではないということだ。
必要なのは、インターネットからHTTPSによるアクセスを受け付け、それを安全に内部のサーバーへ転送することだけである。
考えてみれば、そんな単純な仕事をするために、巨大なLinuxを丸ごと動かす必要があるのだろうか。
QEDOSは、LinuxでもWindowsでもFreeBSDでもない。
ベースになっているのは、seL4というマイクロカーネルである。
普通のOSは、カーネルと呼ばれる中心部分がさまざまな仕事を担当する。一方、マイクロカーネルは、OSの中心部分が担当する仕事を極端に少なくし、その他の機能を独立したプログラムとして動かすという思想で作られている。
seL4は、その中でも特に形式検証、つまり数学的な手法を使ってプログラムの正しさを検証する研究で知られている。
QEDOSは、このseL4とMicrokitという仕組みを利用し、HTTPSの受け付けに必要な機能だけを組み合わせて作られている。何しろシェルがない。
/bin/shもなければ、SSHサーバーもない。
普通のLinuxサーバーなら、SSHでログインして、コマンドを実行したり、プログラムをインストールしたりできる。
QEDOSにはそういう操作をするための仕組み自体がない。
攻撃者が何らかの方法で侵入したとしても、一般的なサーバーのようにシェルを起動して好き勝手に操作することはできない。
もちろん、シェルがないだけで攻撃が不可能になるわけではない。メモリ破壊や権限設定の欠陥があれば、別の方法で攻撃される可能性はある。
しかし、そもそも攻撃者に利用される可能性のある機能を最初から作らなければ、その機能に由来する脆弱性も存在しなくなる。
これは、セキュリティの世界で「攻撃対象領域（Attack Surface）を減らす」と呼ばれる考え方である。
QEDOSでは、この考え方を極端なところまで突き詰めた。
とはいえ、機能を減らすだけでは不十分だ。
どれほど慎重に作ったプログラムでも、バグがないとは限らない。
そこでQEDOSでは、システムの機能を5つの独立した領域に分離している。
最初の領域はTCP通信を受け付ける。次の領域はTLSによる暗号化通信を処理する。3番目の領域がHTTPを解析し、4番目がアクセスの許可を判定し、最後の領域が内部のバックエンドサーバーに接続する。
重要なのは、これらの領域が互いに独立しており、必要最小限の権限しか持たないことである。
例えば、TLSを処理する領域には、通信に必要な秘密鍵が存在する。
しかし、この領域には内部サーバーへ自由に接続する権限が与えられていない。
一方、内部サーバーへの接続を担当する領域には、TLSの秘密鍵を読み取る権限がない。
つまり、仮にHTTPを解析するプログラムにセキュリティホールが発見されたとしても、そのプログラムを乗っ取るだけでは、暗号鍵を盗んだり、任意の内部サーバーに接続したりできないように設計されている。
これは「Capability-Based Security」と呼ばれる考え方に基づいている。
普通のOSでは、プログラムが管理者権限を獲得すると、システム全体に対して非常に強い権限を行使できる場合がある。
Capability-Based Securityでは、それぞれのプログラムに対して、何をしてよいかを明示的に与える。
権限を持っていない操作は、そもそも実行できない。
この仕組みによって、攻撃者が一つのプログラムを乗っ取ったとしても、その被害を限定された範囲に閉じ込められる可能性が高まる。
QEDOSでは、暗号鍵を保持する領域とバックエンドへ接続する領域が直接通信できないことなどを、権限構成のモデルに対して検証している。
この「侵入されること」と「システム全体を乗っ取られること」を切り離す発想が重要なのである。
ここからが今回の本題である。
普通のソフトウェア開発では、プログラムを書いた後にテストをする。
いろいろな入力を与えてみて、期待通りに動くかどうかを確認する。
しかし、テストには根本的な限界がある。
例えば、あるプログラムに100万通りの入力を与え、全部正常に動いたとしても、100万1通り目にバグが存在しないとは言い切れない。
どれほどテストを増やしても、すべての入力を試すことは現実的ではない。
そこで登場するのが「形式検証」である。
形式検証とは、プログラムが満たすべき条件を数学的に定義し、その条件を破る状態が存在するかどうかを論理的に調べる技術だ。
例えば、HTTPリクエストを解析するプログラムなら、「入力データの範囲を超えてメモリにアクセスしない」という条件を設定する。
あるいは、アクセス先を決定するプログラムなら、「あらかじめ許可されたバックエンド以外には接続しない」という条件を設定する。そして、それらが常に成立するかどうかを検証するのだ。
QEDOSでは、HTTPの解析、アクセス制御、設定ファイルの処理といった重要な部分をRustで記述している。
Rustは、メモリの不正な取り扱いによるバグを防ぐ仕組みを言語そのものに組み込んでいる。
さらに、重要な部分にはunsafeなコードを禁止した。
そのうえで、Kaniという検証ツールを使い、13件の検証項目について有界モデル検査を行った。
例えば、HTTPの解析中に配列の境界を超えてしまわないか。数字の変換でオーバーフローが起きないか。許可されていないバックエンドが選択される可能性はないか。電子署名が検証されていない設定が有効化されないか。
公開した検証結果では、13件すべての検査を通過した。
もちろん、これはOS全体にあらゆるバグが存在しないと証明したことを意味するわけではない。検証は対象のプログラム、入力範囲、前提条件に限定される。
しかし、ただ何となく「安全そうだ」と言っているのと、重要な安全条件を数学的に記述し、それを機械的に検証しているのとでは、意味がまるで違う。
筆者が面白いと思ったのは、こうした検証作業そのものをAIに手伝わせられるということだ。
AIにプログラムを書かせるだけなら、今では珍しくない。
だが、AIにプログラムの安全条件を考えさせ、その条件を検証するコードまで作らせ、検証が失敗したら修正させる。これは、単なるバイブコーディングとは少し違う。
AIが書いたプログラムを、AIが支援する形式検証によって確かめるのである。
AIがプログラムを書く時代から、AIがプログラムの正しさを検証する時代へ移行するのだ。
筆者は、ここに今後のソフトウェア開発の重要な方向性があると考えている。
QEDOSにはもう一つ、重要な特徴がある。
耐量子暗号(PQC;Post Quantum Cryptography)への対応だ。
現在のインターネットで使われている暗号技術の一部は、将来、十分に強力な量子コンピュータが実現した場合、破られる可能性がある。
特に問題なのは、通信を今のうちに記録しておき、将来の量子コンピュータで復号するという攻撃である。
これは「Harvest Now, Decrypt Later」と呼ばれている。
筆者は以前、この問題についても本欄で取り上げた。量子コンピュータが登場するのは将来の話だとしても、今の通信が将来解読される可能性は、現在の問題なのである。つまり、今普通に使っている暗号通信は、来るべき時がきたら全て解読されていると思って良い。つまり人にバレてはいけない情報は、決して、インターネットに載せてはいけないのだ。
今我々が当たり前のように使っている暗号通信も、従来型の公開鍵暗号による鍵交換に依存している限り、将来、十分に強力な量子コンピュータが実現したときには、過去にさかのぼって解読される可能性があるのだ。
通信した瞬間には世界最高水準の暗号で守られていたとしても、10年後、20年後には、その内容がすべて筒抜けになっているかもしれない。
これは恐ろしい話である。なぜなら、一度インターネットに流れてしまった情報を、後から取り戻すことはできないからだ。
SSHだろうがHTTPSだろうが、従来型の鍵交換を使っている限り、この問題から逃れることはできない。通信経路が暗号化されているから安全、という常識そのものが崩れようとしているのである。
つまり、長期にわたって絶対に人に知られてはならない情報は、耐量子暗号などによる十分な対策が確認できない限り、安易にインターネットに載せてはいけないのだ。
もっとも、すでに耐量子暗号を使うSSHやHTTPSも登場している。しかし、対応していることと、実際の通信でその方式が選択されていることは別の話だ。
だから筆者は、QEDOSでは耐量子暗号を「使えるようにする」のではなく、「使わなければ接続できない」という設計にした。
古い暗号方式への後方互換性よりも、将来にわたる通信の秘密を優先したのである。
そこでQEDOSでは、TLS 1.3による暗号化通信に加え、「X25519MLKEM768」というハイブリッド鍵交換方式を必須とした。
これは、従来の楕円曲線暗号を利用するX25519と、耐量子暗号アルゴリズムであるML-KEM-768を組み合わせた方式である。
面白いのは、単に耐量子暗号に対応しているだけではないところだ。
耐量子暗号を使わない通信は、最初から拒否する。TLS 1.2も使えない。従来型の鍵交換だけを要求するクライアントも接続できない。
普通のサーバーでは、古いクライアントとの互換性を維持するために、複数の暗号方式を許可することが多い。しかし、互換性のために古い方式を残すと、それが攻撃の足がかりになる可能性がある。だったら、古い方式を最初からサポートしなければいい。
QEDOSではそう考えた。ちなみに、このハイブリッド鍵交換はChromeでも利用できる。実際にChromeからHTTPSで接続できることも確認している。
ただし、現時点ではサーバー証明書の認証には従来型のECDSAを使用しているため、認証まで含めて完全に耐量子暗号化されているわけではない。
このあたりは、ブラウザ側の対応状況も関係する。いずれ専用ブラウザか、Chrome用の専用プラグインのようなものを作るかもしれない。
こうした話をすると、「理屈はわかったけど、本当に動くの？」と言われそうである。
筆者もそう思う。
数学的に安全だと主張するだけで、まともに通信できなければ意味がない。
そこで、QEDOSは実際に動作するところまで作った。
現在、x86-64向けのseL4とMicrokitを利用したQEDOSは、QEMUというバーチャルマシン上で起動する。
実際にHTTPSでアクセスし、TLSの暗号化通信を行い、HTTPリクエストを解析し、許可されたバックエンドサーバーへ転送できる。
5つの独立した領域が連携して動作し、暗号化通信からバックエンドへの転送まで一通り処理できることを確認した。
さらに、怪しいHTTPリクエストを与えても、許可されていないバックエンドへ転送しないことを検証している。
例えば、../を使って本来アクセスできないディレクトリを指定しようとする攻撃や、不正なHTTPヘッダーを使う攻撃などである。
こうした入力を拒否できることは、通常のテストとバックエンド側の通信記録によって確認した。
また、性能についても実験した。
HTTPSサーバーとして重要なのは、大量の同時接続を処理できるかどうかである。
これは古くから「C10K問題」と呼ばれてきた。1万本の同時接続をどう処理するか、という問題だ。
QEDOSには、同じHTTP解析・アクセス制御コードを共有するLinux上の参照実装もある。
この参照実装を用いて1万本の同時TLS接続を試験したところ、すべての接続を維持することができた。
1万本のTLS接続を維持した状態でのメモリ使用量は、ピークで約285MBだった。
さらに、一定の負荷条件では毎秒約1万3400リクエストを処理することができた。
もちろん、これはLinux上の参照実装を同一マシン内で試験した結果であり、seL4上のQEDOS本体で同じ性能が出ると確認されたわけではない。
今後は実際のx86-64マシンで起動し、物理ネットワークインターフェースを使い、実機でも1万接続を処理できるか検証する必要がある。
つまり、まだ完成品ではない。
しかし、単なる机上の空論でもなくなった。
ここまで読んで、「そこまでしなくても、Linuxをきちんと設定すればいいのではないか」と思う人もいるだろう。
実際、それはその通りである。
Linuxにも強力なセキュリティ機能がある。不要なサービスを止め、権限を制限し、コンテナを使い、適切な設定を行えば、非常に堅牢なシステムを作ることができる。
QEDOSがLinuxより安全だと、現時点で一般的に証明されたわけでもない。
しかし、筆者が今回試してみたかったのは、もう少し根本的なことだった。
「これからのコンピュータシステムは、最初から安全性を数学的に検証できるように作るべきではないか？」
という問いである。
従来のコンピュータシステムは、まず機能を実現するために作られ、その後からセキュリティ対策が追加されることが多かった。
その結果、巨大なOSの上に巨大なミドルウェアが載り、その上にさらに複雑なアプリケーションが載るという構造になった。それぞれの層にセキュリティホールが存在する可能性があり、どこか一つが破られると被害が広がる。
AIが普及し、攻撃者もAIを使うようになれば、この問題はさらに深刻になるかもしれない。
これまでは、人間の専門家が苦労して探していたセキュリティホールを、AIが大量に探索できるようになる。
一方、防御する側は、発見されるたびにパッチを当て続けなければならない。
それでは、いつか人間の対応速度が追いつかなくなるのではないか。だからこそ、発想を変える必要がある。プログラムを書いてから脆弱性を探すのではなく、最初から満たすべき安全条件を定義する。それを満たすプログラムをAIに作らせ、形式検証によって事前に確認する。
システムを複数の独立した領域に分離し、仮に一つの領域が破られても、他の領域には侵入できないようにする。そして、そもそも必要のない機能は実装しない。
QEDOSは、こうした考え方を実際のOSとして形にした実験なのである。
もう一つ、今回の開発で感じたことがある。
それは、AIの登場によって、個人が挑戦できるソフトウェア開発の規模が根本的に変わりつつあるということだ。
昔、OSを作るというのは大変な仕事だった。
ハードウェアを制御し、ネットワークを実装し、暗号を扱い、メモリを管理し、プログラム間の通信を設計しなければならない。
しかも、それぞれの分野に深い専門知識が必要になる。
一人のプログラマーがすべてを理解して実装するのは、かなり骨の折れる作業だ。作業を分担すれば、効率は上がるが隙はできる。セキュリティホールというのは「その隙」のことだ。
ところが今は違う。AIに既存の技術を調べさせ、設計を検討させ、コードを書かせ、テストを作らせ、失敗した原因を分析させることができる。
もちろん、AIは平気で間違える。存在しないAPIを使おうとしたり、動くはずのないコードを書いたり、検証が終わっていないのに成功したと主張したりもする。だから、AIを盲信してはいけない。
むしろ、AIが書いたコードだからこそ、客観的に検証できる仕組みが重要になる。今回のQEDOSでは、そこで形式検証が重要な役割を果たした。
AIの説明が正しいかどうかではなく、検証ツールが実際に条件を満たすと判定するかどうかを事前に確認する。人間の理性が生み出した最強の武器である数学的証明によって。
AIが「大丈夫です」と言ったから大丈夫と考えるのではなく、数学的に検証できる条件を作り、それを満たしたことを確認して、初めて次の段階へ進む。
これはAI時代のソフトウェア開発における、一つの重要な方法論になるのではないか。
最後に、最初の問いに戻ろう。
絶対に破られないOSは作れるのだろうか。
残念ながら、現時点でQEDOSが絶対に破られないと証明できたわけではない。
形式検証にも適用範囲があり、暗号ライブラリにもバグはあり得るし、ハードウェアの脆弱性も存在する。そもそも、今回利用したseL4の形式検証実績が、そのままQEDOSのx86-64構成全体に適用されるわけでもない。
セキュリティの世界で「絶対」という言葉を使うのは、非常に危険なことである。
しかし、だからといって「絶対安全など不可能だから仕方がない」と諦めるのも、少し違う気がする。
空を飛ぶことが不可能だと言われていた時代に、人類は飛行機を作り、月へ行くことが不可能だと言われていた時代に、人類は月面に到達した。絶対に安全なOSが存在しないからといって、それを目指してはいけない理由にはならない。
QEDOSは、まだ一日だけ行ったささやかな実験に過ぎないが、筆者はこの実験を通じて、AI時代のセキュリティには別の可能性があるのではないかと感じた。
AIがセキュリティホールを発見する速度に、人間がパッチを当てる速度で対抗するのではなく、そもそもセキュリティホールが生まれにくく、万一存在しても被害が広がらず、安全条件を数学的に検証できるシステムを作る。
AIによって攻撃が高度化するなら、AIによって防御の設計思想そのものを進化させればいい。
絶対無敵のOSが本当に実現するかどうかは、まだわからない。
しかし、少なくともそれを目指すための道具は、すでに我々の手の中にある。
