技術的概要：発散型マルチバージョン実行（DME）

問題定義

従来の冗長化メカニズム、すなわちロックステップ実行やトリプルモジュラ冗長（TMR）は、同一のバイナリを同一のメモリレイアウトで実行することに依存している。独立した故障に対しては効果的であるが、これらのシステムは相関故障に対して脆弱である。実験的研究（Dutertre らなど）は、電磁気的故障注入のような物理的擾乱が、すべてのレプリカ間で同一の摂動（例えば、特定の $\Delta PC$）を同時に引き起こし得ることを実証している。従来のシステムにおいて、このような相関した摂動は、すべてのレプリカを同じ誤った実行経路へ誘導し、すべてのレプリカが同一の誤った状態を生成するため検出されないサイレントデータ破損をもたらす。さらに、従来の冗長化は、初期化されていないポインタや戻りアドレスの書き換えなど、レプリカ間で同一に現れる特定のクラスのソフトウェアバグ、またはコンパイラ/リンカの欠陥を検出できないことが多い。

手法

本論文は、同一の数値的摂動が意味的に発散する実行経路をもたらすことを保証することで、相関故障を検出するように設計されたランタイム意味的整合性検証器である**発散型マルチバージョン実行（DME）**を提案する。

基本原理

DME は、コンパイル時に強制される 4 つの基本原理に基づいて動作する。

1. 独立コンパイル: $N$ 個のレプリカは、同一のソースコードから独立してコンパイルされる。これにより、オプコードレベルの意味と同型な制御フローグラフを維持しつつ、物理的なコードとデータのメモリレイアウトがそれぞれ異なるものとなる。
2. 粗粒度の非相関化: 関数や基本ブロックは、補完的な分岐変位パターン（例えば、あるレプリカでは前方分岐が別のレプリカでは後方分岐となる）を用いて、レプリカ間で異なるアドレスに配置される。これにより、同一の制御フロー摂動が意味的に異なる経路にマッピングされることを保証する。
3. 細粒度の非相関化: レプリカ固有のオフセット（$offset_r = \frac{l}{N} \cdot r$）に周期的な NOP 命令が挿入される。これにより、対応する論理命令間の最小空間的分離が生まれ、小規模なプログラムカウンタ（PC）摂動の検出を可能にする。
4. データアドレス非相関化: グローバル変数、スタックフレーム、ヒープ割り当てには、各レプリカに対して一意の絶対ベースアドレスが割り当てられる。

故障検出メカニズム

DME は、二重層の検出戦略を採用する。

1. 意味層（標準化命令トレース）:

   • システムは、レプリカ間で「標準化トレース」を比較する。標準化トレースには、オプコード、レジスタ識別子、即値オペランド、読み書きされた値、および計算結果が含まれる。
   • 重要なのは、絶対アドレスがトレースから除外されることである。
   • 故障のない実行下では、すべてのレプリカが同一の標準化トレースを生成する。実行の意味を変更する任意の故障（異なる命令の実行や異なる結果の計算など）は、トレースの発散を引き起こす。

2. 構造的層（アドレス空間非相関化と非エイリアシング）:

   • DME は、レプリカ間での物理アドレスの等しさ（例：$PC_1 = PC_2 = \dots = PC_N$）を、許容可能な状態ではなく、構造的独立性の違反として扱う。
   • アドレス非エイリアシング不変条件: システムは、意味的に対応するメモリアクセス（データまたは命令）が、レプリカ間で異なる実効アドレスをターゲットにしなければならないことを強制する。
   • 故障（バッファオーバーフローや null ポインタの参照外しなど）がすべてのレプリカに同じ誤ったアドレスを計算させる場合、システムは直ちにエラーをトリガーする。これにより、意味的発散が発生する前にポインタ破損や戻りアドレスの書き換えを検出できる。

故障モデルと検出領域

本論文は、摂動の性質に基づいて検出保証を分類する。

• 決定論的検出:

  • 全レプリカで $\Delta PC$ が同一である完全相関故障に適用される。
  • $|\Delta PC| \geq l/N$（ここで $l$ は NOP 挿入ストライド）の場合、その摂動は少なくとも 1 つのレプリカが異なる論理命令を実行することを保証し、即座にトレースの発散をもたらす。
  • アドレス空間の崩壊（同一の PC またはポインタ）は、構造的違反として即座に検出される。

• 確率的検出:

  • 部分的に相関した故障（$\Delta PC$ がレプリカ間で異なる場合）または $|\Delta PC| < l/N$ の故障に適用される。
  • 検出は、レプリカが偶然に同一の論理命令に整列し、同一の結果を生成する可能性が低いことに依存する。
  • $k$ ステップにわたって検出されない確率は、$(\frac{C}{|S|} \cdot \epsilon)^k$ によって制限される。ここで、$C$ は標準的に等価な命令の数、$|S|$ は命令空間の総数、$\epsilon$ は同一の結果となる確率である。典型的な 32 ビット ISA の場合、この確率は指数関数的に減少する（例：$\epsilon \leq 2^{-52}$）。

主要な貢献

1. 構造的アドレス空間非相関化: 本論文は、コンパイル中にメモリレイアウトと分岐変位を積極的に多様化させることで、相関する低レベルの摂動を可観測な意味的発散に変換する方法を導入する。
2. 標準化トレース監視: アドレス依存情報を破棄しつつ、意味的実行（オプコード、レジスタ、結果）を捉えるレイアウトに依存しないトレース表現を定義し、多様なバイナリ間での堅牢な比較を可能にする。
3. 二重層検出: DME は、意味的トレース比較と構造的アドレス監視を組み合わせる。これにより、従来の冗長化が結果として生じる実行経路が偶然同一である場合に検出を見逃す可能性のある「アドレス崩壊」イベント（例：同一の戻りアドレス）を即座に検出できる。
4. 形式的正しさとモデル: 本論文は、ランタイム意味的正しさ（トレースの等しさ）とシステムレベルの正しさ（意味的等しさ＋構造的独立性）を区別する。構造的独立性が、相関故障の可観測性を保証するための十分条件であることを形式的に証明する。

結果と主張

本論文は、DME が以下のことを提供すると主張している。

• 摂動の大きさが非相関化ストライドを超える（$|\Delta PC| \geq l/N$）相関 PC 故障に対する決定論的検出。
• 命令セットアーキテクチャの状態空間によって制限され、他の故障タイプに対する指数関数的減衰を伴う確率的検出。
• アドレス非エイリアシング不変条件を介したポインタ意味違反（null ポインタ、値をポインタとして扱うエラーなど）の即時検出。これは、多くの場合、意味的発散よりも早期に検出される。
• 実用的実現可能性: 著者は、Altera Cyclone IV FPGA 上で動作する 32 ビットソフトプロセッサ（3o|||sheet）上のプロトタイプ実装と、Cortex-M コア上の仮想マシン実装を引用しており、オーバーヘッドは管理可能であることを示している（例：レプリカあたり 3000 LUT と 16 KB BRAM）。

重要性

本論文は、DME を安全クリティカルな組み込みシステムにおける冗長化の再定義として位置づけている。主にエクスプロイトの移植性を阻害するために多様化を使用するマルチバリアント実行環境（MVEE）とは異なり、DME は物理的擾乱によって引き起こされるビットレベルの破損を検出するための形式的ランタイム正しさ不変条件として構造的非相関化を使用する。

著者は、DME が既存のフォールトトレランスにおける特定のギャップ、すなわち状態の等しさを維持しつつプログラム意味を侵害する相関命令レベルの摂動を検出できないという従来の冗長化の限界に対処していると強調している。構造的独立性を強制することで、DME は同一の数値的故障が同一の論理的動作をもたらすことを防ぎ、サイレントデータ破損のリスクを検出可能な事象に変換する。この研究は、電磁気的または環境的な故障注入が現実的な脅威となる環境に適した、ハードウェアに依存せず形式的に解析可能なメカニズムとして提示されている。