最近、日本の企業がサイバー攻撃によって大変なことになっている
今AIの能力は恐ろしい速度で進歩？している
以前、セキュリティホールを発見するには、コンピュータの内部構造を熟知した高度な専門家が必要だった
脆弱性を発見し、悪用できるかどうか調査し、攻撃コードを作成するには相応の技術と時間が必要だった
ところが最近は、AIがプログラムを読み、問題点を指摘し、場合によっては攻撃コードの作成まで支援してしまう
AIの登場によってサイバー攻撃を行うために必要な技術的ハードルが下がりつつある
そこで
「AIがセキュリティホールを見つけるのが得意になったのなら、逆にAIを使ってセキュリティホールのないOSを作ればいいのではないか？」
名前はQEDOS（クエドス）
数学の証明の最後に書かれるQ.E.D.（クォド・エラト・デモンストランダム/証明終わり)から取った名前
厨二病みたいな名前だが、考えたのはChatGPT
目指したのは絶対無敵のOS
世の中に絶対安全なソフトウェアなど存在しない
しかし、絶対安全を目指して設計することと、最初から絶対安全を諦めることには大きな違いがある
そもそも、なぜOSにはセキュリティホールがあるのか
WindowsやLinuxは非常によくできたOS
何十年もの開発の歴史があり、世界中のプログラマーが改良を重ねている
セキュリティ対策も日々行われている。
しかし、WindowsやLinuxには根本的な問題がある
できることが多すぎる
例えばLinuxには
ファイルを読み書きする
プログラムを起動する機能
ユーザーを管理する機能
外部からSSHでログインする機能
ネットワークを制御する機能がある
これらの機能は必要だから存在している
ただし機能が増えれば増えるほど、攻撃できる場所も増える
Webサーバーに脆弱性が見つかる
そこから攻撃者が侵入する
侵入した攻撃者が別のプログラムの脆弱性を利用して管理者権限を取得
そしてシステム全体を乗っ取ってしまう
こうした攻撃の連鎖が成立するのは、そもそもOSが膨大な機能を持っているからでもある
そもそもWebサーバーにとって、SSHできることはメンテナンス上の都合であって必須機能ではない
だったら最初から余計な機能を全部なくしてしまえばいい
メンテナンスも専用クライアントで専用に暗号化すれば、まず破ることができないようになる
ここで重要なのは、作りたかったのは普通のパソコンで使うためのOSではない
必要なのはインターネットからHTTPSによるアクセスを受け付け、それを安全に内部のサーバーへ転送することだけ
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では暗号鍵を保持する領域とバックエンドへ接続する領域が直接通信できないことなどを権限構成のモデルに対して検証している
この、侵入されること と システム全体を乗っ取られること を切り離す発想が重要
AIがバグを見つけるなら、AIにバグがないことも証明させる
ここからが今回の本題
普通のソフトウェア開発では、プログラムを書いた後にテストをする
いろいろな入力を与えてみて、期待通りに動くかどうかを確認する
しかし、テストには根本的な限界がある
例えば、あるプログラムに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も使えない
従来型の鍵交換だけを要求するクライアントも接続できない
普通のサーバーでは、古いクライアントとの互換性を維持するために複数の暗号方式を許可することが多い
しかし互換性のために古い方式を残すと、それが攻撃の足がかりになる可能性がある
だったら古い方式を最初からサポートしなければいい
ちなみに、このハイブリッド鍵交換は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時代には作れるもの の常識が変わる
もう一つ、今回の開発で感じたことがある。
それはAIの登場によって、個人が挑戦できるソフトウェア開発の規模が根本的に変わりつつある
昔、OSを作るというのは大変な仕事だった
ハードウェアを制御し、ネットワークを実装し、暗号を扱い、メモリを管理し、プログラム間の通信を設計しなければならない
しかも、それぞれの分野に深い専門知識が必要になる
一人のプログラマーがすべてを理解して実装するのは無理
作業を分担すれば、効率は上がるが隙はできる
セキュリティホールというのは、その隙のこと
今は違う
AIに既存の技術を調べさせ、設計を検討させ、コードを書かせ、テストを作らせ、失敗した原因を分析させることができる
もちろんAIは平気で間違える
存在しないAPIを使おうとしたり、動くはずのないコードを書いたり、検証が終わっていないのに成功したと主張したりもする
だからAIを盲信してはいけない
AIが書いたコードだからこそ、客観的に検証できる仕組みが重要になる
今回のQEDOSでは、そこで形式検証が重要な役割を果たした
AIの説明が正しいかどうかではなく、検証ツールが実際に条件を満たすと判定するかどうかを事前に確認する
人間の理性が生み出した最強の武器である数学的証明によって
AIが「大丈夫です」と言ったから大丈夫と考えるのではなく
数学的に検証できる条件を作り、それを満たしたことを確認して、初めて次の段階へ進む
絶対に破られないOSは作れるのだろうか
残念ながら、現時点でQEDOSが絶対に破られないと証明できたわけではない
形式検証にも適用範囲があり、暗号ライブラリにもバグはあり得るし、ハードウェアの脆弱性も存在する
そもそも今回利用したseL4の形式検証実績が、そのままQEDOSのx86-64構成全体に適用されるわけでもない
セキュリティの世界で絶対という言葉を使うのは、非常に危険
しかし、だからといって「絶対安全など不可能だから仕方がない」と諦めるのはNG
QEDOSは、まだ一日だけ行ったささやかな実験に過ぎないが、筆者はこの実験を通じてAI時代のセキュリティには別の可能性があるのではないかと感じた
AIがセキュリティホールを発見する速度に、人間がパッチを当てる速度で対抗するのではなく
そもそもセキュリティホールが生まれにくく、万一存在しても被害が広がらず、安全条件を数学的に検証できるシステムを作る
AIによって攻撃が高度化するなら、AIによって防御の設計思想そのものを進化させればいい
絶対無敵のOSが本当に実現するかどうかは、まだわからない
しかし少なくともそれを目指すための道具は、すでに我々の手の中にある
・・・頻発するAIによるハッキングetc
無力感にトらわれる昨今
こういうアプローチが実行されれば・・・
今日も～
ハチ の巣
去年もあった
なんせ、餌になるチョウの幼虫がウヨウヨいるんで・・・
