- Editors' Top :
- 協創の現場から／日立製作所
- 研究をつなぐ（KDDI総合研究所）
- シュレディンガーの水曜日
October 23, 2026
清水 亮 ryo_shimizu
新潟県長岡市生まれ。1990年代よりプログラマーとしてゲーム業界、モバイル業界などで数社の立ち上げに関わる。現在も現役のプログラマーとして日夜AI開発に情熱を捧げている。
いきなり身内に喧嘩を売るようで恐縮だが、このWirelessWire NewsはWordPressで動いている。
WordPressといえばPHPである。
筆者はもう10年以上前からPHPを使うのをやめている。別にPHPで作られたWebサイトが即座に危険というわけではないし、適切に管理すれば安全に運用できる。しかし、筆者はどうしてもPHPというものの基本的な設計思想が好きになれない。
Webサーバーで動くスクリプトが、ファイルシステムにアクセスできたり、OSのコマンドを実行できたり、外部のネットワークにアクセスできたりする。
もちろん、権限を制限することもできる。しかし、そもそもそんな権限を与えなければよいではないか。
Webサーバーの仕事は、HTTPリクエストを受け取り、必要な処理をして、HTTPレスポンスを返すことである。
それなのになぜ、UNIXのシェルを呼び出せる必要があるのか。
「呼び出せたら便利だから」
おそらく理由はそれだけである。
便利なのは結構だ。しかし、その便利さを攻撃者も利用できるようになったとき、何が起きるか。
実際、WordPressのプラグインやテーマに脆弱性が見つかることは珍しくない。もちろん、だからといってWirelessWireが現在危険だと言っているわけではない。しかし、我々は長い間、ソフトウェアに脆弱性が見つかるたびに、パッチを当てることを繰り返してきた。
それはまるで、穴の開くことが前提の船に乗っているようなものだ。
そろそろ、発想そのものを変えてもいいのではないか。
先日、筆者は10年ほど前に開発を断念したソフトウェアのデモ動画とKeynoteの資料をClaude Codeに見せた。
当時、優秀なエンジニアを何人も集めて、何億円もの予算を投入し、二年がかりで試作したようなものが、一時間もしないうちに実装されてしまった。
恐ろしい時代になったものである。
しかし、AIが何でも作れるようになったということは、AIが何でも壊せるようになったということでもある。
AIは、ユーザーから言われたことを実現しようとする。
「このサーバーからあちらのサーバーにアクセスできるようにして」
と言えば、親切にもファイアウォールの設定を変更してくれるだろう。
しかし、その変更によって想定外のポートまで開いてしまったらどうなるか。
人間ならば慎重に確認するところでも、AIは悪気なく危険な設定をしてしまう可能性がある。
ましてや、人工超知能（ASI）が登場したらどうなるのだろう。もうとっくに「登場している」と言ってもいいと思う。
人間が見つけられなかった脆弱性を一瞬で発見し、あらゆるシステムに侵入するような存在が現れたとしたら、人類はどうやって対抗すればよいのだろうか。
そこ筆者が思い出したのが、数学的証明である。
筆者は数学が苦手である。学生時代から数学はあまり好きではなかったし、今でも高度な数学の論文など全く理解できない。
しかし、数学的証明というものの強力さだけは知っている。
たとえば、無理数は有理数よりもはるかにたくさん存在する。
どちらも無限にあるのだから、直感的には同じくらいあるように感じられるかもしれない。しかし、数学的には無限の大きさにも違いがあり、有理数は可算無限、無理数は非可算無限である。
これはカントール以来の数学によって厳密に示されている。
世界中のコンピュータを使って一兆個の数を調べたところで、この事実を実験的に確かめることはできない。
しかし、数学的証明によって我々はその正しさを知ることができる。
しかも、この証明は百年後も千年後も、正しい公理と推論規則のもとでは変わらない。
宇宙人が現れても、異次元人が現れても、どれほど知能の高いASIが現れても、数学的に正しく証明された命題を覆すことはできない。
もちろん、証明の前提が成立しなければ結論も保証されない。だが、そこを明確にしたうえで成立する数学的証明は、相手の知能とは無関係な強さを持っている。
これは考えてみると、実に痛快な話だ。
人間より一億倍賢い存在に対しても、人間が検査できる数学的証明によって、ある操作が不可能だと示せるのである。
数学的証明を用いたプログラミングは、決して新しいアイデアではない。
Coq、Lean、Agda、Idrisなど、形式的証明や依存型を利用する言語や証明支援系は既に存在する。
また、seL4というマイクロカーネルでは、実装が仕様に従うことを数学的に検証する研究成果がある。
しかし、なぜこうした技術は一般的なWeb開発の中心になってこなかったのだろうか。
理由の一つは、難しすぎるからである。
プログラマーにプログラムを書かせるだけでも大変なのに、そのプログラムについて数学的証明まで書かせようとしたら、開発コストはいったいいくらになるのか。
ところがAIの登場によって、事情は一変する。
AIにプログラムを書かせればいい。
そして、AIにそのプログラムが満たすべき性質についての証明も作らせればいい。
重要なのは、証明を作ることは非常に難しくても、完成した証明が正しいかどうかを検査することは、ずっと単純な仕組みで実現できる場合があることだ。
つまり、AIを信頼する必要はない。
AIが書いたプログラムも信用しない。
AIが作った証明も無条件には信用しない。
独立した検証器が、その証明を機械的に確認する。
人類は、ASIより賢くなることなく、ASIが作ったプログラムの特定の性質を検査できるかもしれないのである。
そこで吾輩は、QEDOSという実験的なOSに、QED Scriptという新しいサーバーサイドスクリプト実行環境を作ってみた。
QEDOSは、seL4というマイクロカーネルとMicrokitを利用したHTTPSサーバー用のOSである。
基本的な考え方は極めて単純だ。
できないことは、最初からできないようにする。
QED Scriptも、この考え方を引き継いでいる。
QED Scriptは、制限されたWebAssembly（Wasm）を実行するための環境だ。
一般的なWebAssemblyのあらゆる機能をサポートするのではなく、必要な命令と機能だけを実装した小さなインタープリターを使用する。
通常のUNIXプロセスのように、好きなファイルを開いたり、シェルを呼び出したり、勝手にネットワーク接続を確立したりすることはできない。
スクリプトが利用できる機能は、限定されたAPIと署名済みのポリシーによって決められる。
メモリの使用量、実行できる命令数、関数呼び出しの深さ、レスポンスの大きさなどにも制限がある。
そして重要なのが、スクリプトを実行する領域そのものが、TLSの秘密鍵を管理する領域やネットワークを制御する領域から隔離されているという点だ。
仮にスクリプト実行環境に欠陥があったとしても、そこで動くコードに最初からTLSの秘密鍵やネットワーク操作の権限を与えていなければ、それらへの攻撃経路を大きく制限できる。
少なくとも、これがQED Scriptの目指す防御構造である。
ここは誤解のないように書いておきたい。
現時点のQED Scriptは、まだ完成した形式検証済みのプログラミング言語ではない。
2026年10月22日時点の開発版では、seL4上でQED Scriptを起動し、実際にHTTPSリクエストを処理するところまで実装できた。
メモリ境界の確認、アクセス権限の制御など、一部の性質についてはKaniやZ3を使った限定的な形式検証を行っている。また、不正なWebAssemblyや無限ループなどを想定したテストも実施した。
しかし、まだ残っている問題もある。
特に重要なのは、スクリプトに付随する数学的証明を独立に検査し、その結果に基づいて実行を許可する機構が、まだ完成していないことだ。
現在は、署名と制限付きのサンドボックスによってスクリプトを受け入れている。
数学的証明を検査してから実行する仕組みは、これから実装しなければならない。
また、独自のWasmインタープリターの仕様適合性や、実機上での安全性、タイミングなどを利用するサイドチャネル攻撃への耐性も、完全には証明されていない。
つまり、現時点で「QED Scriptは絶対に破られない」と宣言することはできない。
むしろ、それを宣言できるようになるために、何を証明すればよいのかを考えることが、このプロジェクトの目的なのである。
考えてみれば、これまでのプログラミング言語は、人間が読むことを前提に設計されてきた。
読みやすく、書きやすく、修正しやすいことが重視されてきた。
しかし、AIがプログラムを作る時代には、必ずしも同じ前提が成立するとは限らない。
人間が直接読むには難解なプログラムであっても、その重要な性質が厳密に証明され、独立した検証器によって確認できるならば、そちらのほうが信頼できる場面があるかもしれない。
人間が読むべきなのは、何万行ものプログラムではなく、そのプログラムが満たすべき仕様になる。
「このスクリプトは許可されていないメモリを読み書きしない」
「このスクリプトは指定された回数以上の外部API呼び出しを行わない」
「このスクリプトは秘密情報を外部に送信できない」
こうした命題を定義し、それを満たす実装と証明をAIに作らせる。
ただし、最後の命題のような情報の流出に関する性質は非常に難しく、単なるメモリ安全性の証明では足りない。時間や処理量の違いから情報が漏れる可能性まで考えれば、問題はさらに複雑になる。
それでも、何を保証し、何を保証していないのかを明確にできること自体が、従来の開発方法に対する大きな進歩になる。
人工超知能が人類を超えるという議論では、いつも人間の知能がAIに追い抜かれるということばかりが問題にされる。
しかし、我々は必ずしもASIより賢くなる必要はない。
正しく証明された数学的命題は、ASIがどれほど賢くなっても覆せないからだ。
もちろん、数学的証明だけでASIのあらゆる危険に対抗できるわけではない。
現実のシステムには、証明の前提となるハードウェアや実装があり、形式化されていない仕様もある。
しかし、少なくともソフトウェアの世界において、攻撃者の知能に依存しない防御を構築できる可能性があるというのは、非常に重要なことである。
そして皮肉なことに、人類がこれまで難しすぎて使いこなせなかった数学的証明は、AI自身の力によって、ようやく実用的な道具になるかもしれない。
AIが人類を脅かすほど賢くなるからこそ、AIに数学的証明を作らせ、その証明を単純な機械に検査させる。
なかなか愉快な逆転ではないか。
筆者は数学が嫌いだし、今でも自分で高度な数学的証明を書くなどというのは、考えただけで頭が痛くなる。
しかし、数学が苦手な人間でも、AIの助けを借りて数学的証明を利用したシステムを作れるようになった。
QED Scriptは、まだ発展途上の実験である。
それでも、この実験が示そうとしている方向には、一つの価値があると思っている。
AIが書いたコードを信用するのではない。AIが書いたコードを、信用する必要がないようにするのだ。
QEDOS / QED ScriptはGitHubで公開している。
https://github.com/shi3z/qedos
さて、こんなことを書いているWirelessWire自身も、依然としてWordPressで動いている。
この原稿を掲載するためにも、吾輩はPHPの動いているサーバーに原稿を送ることになる。いつセキュリティホールが突かれるかわからない。
実に皮肉な話である。
願わくば、この原稿が公開されたあとも、WirelessWireが無事に動き続けていてほしいものだ。
