インターネットと私たちの携帯電話を、毎秒数十億ものメッセージが建物間を駆け巡る、巨大で活気ある都市だと想像してみてください。この都市を機能させ続けるためには、ニューヨークの電話が東京の基地局と混乱することなく通信できるように、共通の言語が必要です。この言語がASN.1であり、コンピュータに対して、情報をいかに効率的に小さなデジタルボックスへと詰め込むかを正確に伝える文法や語彙のような役割を果たします。しかし、ここからが厄解なところです。スペースを節約し速度を上げるために、これらのボックスは非常に密に詰め込まれており、標準的なコンピュータの単語（バイト単位）のような整然とした行には並んでいません。代わりに、データの最小単位であるビットレベルまで極限まで詰め込まれています。この特定の、超高密度なパッキング手法がUPERと呼ばれます。

問題は、これら極小のビットレベルのボックスを解凍するための「翻訳機（パーサー）」を書くことが非常に困難であるという点です。もし翻訳機がわずかなミスを犯せば（例えば、たった1ビットを読み間違えたり、未知の新情報に対するルールを忘れたりすれば）、システム全体がクラッシュしたり、秘密が漏洩したり、ハッカーが内部に侵入したりする原因となります。長年、エンジニアたちは、何百万ものランダムなメッセージでこれらの翻訳機をテストすることで、これらのバグを見つけようと試みてきました。しかし、これは、単に干し草を揺らすことで、干し草の中から針を見つけようとするようなものです。針を見つけることはできるかもしれませんが、すべての針を見つけ出したとは言い切れませんし、見つけたものが本当に探していた「本物の針」であるとも断言できません。

そこで、ペンシルベニア州立大学の研究者たちが開発した、ゲームチェンジャーとなるツール、VUPERが登場します。VUPERは、単に干し草を揺らすのではなく、ゼロから数学的に完璧な翻訳機を構築します。これは、コンピュータによる数学的証明によって100%正しいことが保証された「ゴールドスタンダード（黄金基準）」の辞書と文法書を作成することに似ています。研究者たちは、この完璧な翻訳機を使用して、実際の5Gネットワークや車載通信（V2X）で使用されている他の11種類の一般的なパーサーをテストしました。その結果、広く使われているこれらの翻訳機の多くが、実はかなり不適合であり、20種類の異なるルールの欠落があることを発見しました。場合によっては、この不適合によって、ハッカーがスマートフォンをクラッシュさせたり、ネットワークに暗号化されていないメッセージを送らせたりすることが可能になっていました。VUPERは、私たちが現在持っている翻訳機を必ずしも信頼できない一方で、数学的に安全であることが保証された翻訳機を構築し、それを用いて壊れたものを修正できることを証明しています。

VUPERの物語：完璧な翻訳機の構築

コンピュータネットワークの世界では、データはパイプの中を流れる長い水の流れのようなものです。メッセージを送信するために、コンピュータはデータを「シリアライズ（直列化）」し、データをコンパクトなビットのストリームへと圧縮します。これを受信するために、別のコンピュータは、そのビットのストリームを「パース（解析）」し、読み取り可能なメッセージへと展開します。5Gセルラーネットワークや車載通信（V2X）という極めて重要な世界では、このプロセスにUPER（Unaligned Packed Encoding Rules：非整列パッキング符号化規則）と呼ばれる特定のルールセットが使用されます。「非整列（アンアラインド）」と呼ばれる理由は、それがバイト境界を気にせず、帯域幅を節約するためにビット単位でデータを可能な限り密にパッキングするためです。

課題は、UPERの公式ルールブックが、コードではなく、難解で記述的なテキストで書かれていることです。これにより、エンジニアはルールの実装方法を推測せざるを得なくなり、それが微妙なエラーにつながります。VUPERの開発者は、推測することをやめることにしました。彼らは、パーサーが正しいことを形式的に証明するフレームワークを構築しました。彼らは単にコードを書いて動くことを期待したのではなく、強力な数学的ツールであるRocq proverを使用して、ロジックのあらゆるステップを検証しました。

「ラウンドトリップ」テスト

VUPERの仕組みを理解するために、本を秘密のコードに変換し、また元に戻す魔法の翻訳機を想像してみてください。「ラウンドトリップ」テストとは、ある文章をコードに変換し、そのコードを再び文章に戻すことを意味します。もし全く同じ文章が得られたなら、その翻訳機は正しく機能しています。

しかし、UPERには特別な仕掛けがあります。それは拡張（エクステンション）です。テクノロジーが進化するにつれ（4Gから5Gへの移行のように）、メッセージには新しい機能が追加されます。古い翻訳機は、新しいメッセージを読み取り、自分が理解できない新しい部分を無視しつつ、古い部分を正しく理解できなければなりません。これは前方互換性と呼ばれます。VUPERは、以下の2点を証明することでこれに対処します。

1. 厳密なラウンドトリップ（Strict Round-Trip）: メッセージが同じバージョンのものである場合、翻訳機はそれを元の全く同じビットパターンに戻さなければなりません。余分なビットも、足りないビットも許されません。
2. 緩やかなラウンドトリップ（Weak Round-Trip）: メッセージに未知の拡張が含まれている場合、翻訳機はそれらをスキップできますが、既知の部分については依然として有効なメッセージとして復元できなければなりません。元のビットと完全に一致する必要はありません（未知の部分は失われているため）が、残りの部分を壊してはなりません。

バグの発見

研究者たちは、「信頼できるオラクル（真実の判定器）」、つまりVUPERによって生成された完璧なパーサーを構築し、それを使用して他の11種類のパーサーをテストしました。これには、7つのオープンソースツール（asn1cやpycrateなど）と、4つの商用パーサー（あなたの電話をネットワークに接続するハードウェアである、実際の4Gおよび5G基地局内で使用されているもの）が含まれます。

彼らは単にランダムなゴミを送りつけたのではありません。メッセージの構造を理解するスマートな「ファザー（Fuzzer）」を使用して、何百万ものトリッキーなテストケースを作成しました。結果を比較したところ、他のパーサーにおいて20種類の異なる不整合が見つかりました。

興味深い発見の例は以下の通りです：

• 「長すぎる」問題: 一部のパーサーは、割り当てられたスペースに対して大きすぎる数値や、データと一致しない長さを受け入れてしまいました。これは、郵便配達員が「5ページあります」と書かれた手紙を受け取ったのに、実際には100ページあったために、郵便受けが溢れてクラッシュしてしまうようなものです。
• 「未知の拡張」による混乱: メッセージに古いパーサーが知らない新しい機能が含まれていたとき、一部のパーサーは混乱し、メッセージの誤った部分を別のものとして読み始めてしまいました。これは、翻訳者が外国語の新しい単語に出会い、混乱した結果、文章の残りの部分を誤って翻訳してしまうようなものです。
• 「デフォルト値」のミス: ルールでは、値を節約するために、値が「デフォルト」である場合は送信しないことになっています。しかし、一部のパーサーは依然としてその値を送信していたり、それが欠落していることを認識できなかったりしました。

現実世界の危険性

この論文は、単に理論的なバグを見つけただけではありません。それらがどのように悪用されるかを明らかにしました。研究者たちは、4つの具体的な攻撃を実証しました。

1. スマートフォンのクラッシュ: ネットワークIDのリストが（制約に違反して）わずかに長すぎるメッセージを送信することで、スマートフォンのソフトウェアをクラッシュさせ、サービス拒否（DoS）を引き起こしました。
2. 基地局のクラッシュ: 乗っ取られたセルタワーが、別のタワーに対して不正なメッセージを送信し、その第2のタワーが処理中にクラッシュさせることを実証しました。
3. 情報の漏洩: パーサーが未知の拡張によってメッセージを誤認した場合、セキュリティ設定が「オン」であるべきところを「オフ」だと判断したり、その逆だったりすることがあります。これにより、スマートフォンは安全に通信していると考えているのに、実際にはネットワークがデータを平文で送信しており、盗聴者が内容を読み取れる状況が生じる可能性があります。
4. デバイス・フィンガープリント（指紋採取）: パーサーによってエラーの処理方法が異なるため、ハッカーは特定の「トリック」メッセージを送り、デバイスの反応を観察することができます。もしデバイスが奇妙なメッセージを受け入れた場合、ハッカーはそのデバイスが特定のブランドのハードウェア（Samsungのベースバンドなど）を使用していることを知り、そのデバイス特有の既知の脆弱性を狙うことができます。

パフォーマンスと未来

研究者たちは、自分たちの完璧な数学的検証済みパーサーが、現時点では最も高速なものではないことも認めています。それは、業界で使用されている高度に最適化されたCライブラリよりも約4倍遅いです。しかし、Pythonベースのパーサーよりは4倍速いです。

VUPERの目的は、すぐに高速なパーサーに取って代わることではなく、**リファレンス実装（参照実装）**として機能することです。マスターシェフが料理を味わってレシピのどこが間違っているかを正確に指摘できるのと同様に、VUPERはエンジニアに対し、パーサーのどこに失敗があるかを正確に教えることができます。研究者たちは、VUPERを使用してこれらのバグを見つけて修正することで、業界が最終的に、高速でありながら数学的に安全であることが保証されたパーサーを構築できることを期待しています。

結局のところ、VUPERは、複雑で高速な5Gとその先の領域において、「十分である」というレベルのテストではもはや通用しないことを示しています。私たちのデジタル都市を安全かつ確実に、スムーズに稼働させ続けるためには、数学的に証明された翻訳機が必要なのです。