💻 computer science

SEAL: Symbolic Execution with Separation Logic (Competition Contribution)

SEALは、分離論理とSMTベースのAstralソルバを活用することで、LinkedListsカテゴリにおいて競争力のある結果を実現しつつ、将来の開発に向けた大幅な拡張性を提供する、非限定的な連結データ構造を持つプログラムを検証するためのモジュール式プロトタイプ静的解析器である。

原著者： Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

公開日 2026-02-09

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

あなたは、複雑で絶えず変化する道路や建物が並ぶ街が、安全にナビゲート可能かどうかを確認しようとしていると想像してください。あなたは、誰も橋から落ちず（「NULLポインタ・デリファレンス」）、誰もすでに存在しない建物を解体しようとせず（「use-after-free」エラー）、誰も誤って同じ建物を二度壊さないこと（「double-free」エラー）を確認する必要があります。

これはまさにSEALが行っていることですが、対象となるのは街ではなく、複雑で変化するデータ（連結リストのようなもの）を管理するコンピュータプログラムです。

以下は、論文がSEALをどのように説明しているかを、シンプルな概念に分解したものです。

1. コアとなるアイデア：特化した探偵

これらのプログラムをチェックするほとんどのツールは、あらゆる種類の犯罪に対して特定の固定されたルールブックを使用する探偵のようなものです。SEALは異なります。SEALは、ASTRALと呼ばれる汎用的な「ロジックエンジン」を使用しています。

ASTRALを、超スマートな翻訳者だと考えてください。SEALがメモリ内でデータがどのように接続されているかという複雑なパズルに遭遇したとき、ASTRALはそのパズルを、標準的で強力なコンピュータソルバー（SMTソルバーと呼ばれます）が完璧に理解できる言語へと翻訳します。これにより、SEALは非常に柔軟になります。それは、一つの方言に縛られるのではなく、あらゆる専門家と話すために言語を切り替えることができる探偵を持っているようなものです。

2. 課題：無限 vs 有限

SEALがチェックするプログラムには、多くの場合、連結リスト（一つのアイテムが次のアイテムを指し示すデータの鎖）が含まれています。

問題点: リストの中には、短くて固定されたもの（3つのリンクを持つ鎖のようなもの）もあれば、**無制限（unbounded）**なものもあります。つまり、10個のリンクかもしれないし、10,000個、あるいは無限かもしれません。
困難な点: 無限の鎖のあらゆる可能な長さをチェックしようとすることは、コンピュータにとって不可能です。永遠に時間がかかってしまいます。
SEALのトリック: SEALは**抽象化（abstraction）**という手法を使用します。非常に長い列車を見ているところを想像してください。すべての車両を数える代わりに、SEALは「これは『長い列車』である」と言います。鎖の中間にある煩雑な詳細は、一つの整ったラベル（「述語（predicate）」）に置き換えます。これにより、詳細に迷い込むことなく、鎖全体について推論することが可能になります。

3. 仕組み：「シェイプ（形状）」アナライザー

SEALは「シェイプ・アナライザー」です。単に数字を見るのではなく、メモリの**形状（シェイプ）**を見ます。

シンボリック・ヒープ: SEALは「シンボリック・ヒープ」を用いてメモリのマップを作成します。これは、「ここにメモリブロックがあり、それがこの他のブロックに接続している」という設計図のようなものです。
ループ・フィックスポイント: プログラムがループ（同じ動作を繰り返すこと）を実行するとき、SEALはメモリの「形状」が安定したかどうかをチェックします。現在のラウンドの形状が前のラウンドと比較して「十分に安全」に見える場合、チェックを停止し、そのループが安全であると宣言します。

4. 現在の強みと弱点

論文は、SEALがまだプロトタイプ（初期バージョン）であることを認めていますが、驚くべき統計も示しています。

良いニュース（強み）:

「無制限（Unbounded）」クラブ: 最近のコンペティションでは、無限のリストを持つプログラムを検証する20のツールがありました。そのうち、成功したのはわずか4つのツールだけでした。SEALはそのうちの一つでした。
将来の可能性: SEALは、その柔軟な「翻訳者（ASTRAL）」を使用しているため、新しい形状を教え込むことが容易です。著者らは、他のツールが苦戦するツリー構造やスキップリスト（データのマルチレベル・ハイウェイのようなもの）といった複雑な構造も、最終的には扱えるようになると信じています。

悪いニュース（弱点）:

限定的な語彙: SEALは現在、C言語の限られたサブセットしか理解できません。複雑な数値計算や、多くの種類のポインタを扱うことはまだできません。
推測ゲーム: 時として、SEALはコードがどのようなデータ構造を構築しているのかを推測しなければなりません。もし推測を誤ると（例：複雑な構造を単純なリストだと勘違いした場合）、バグを見逃したり、「わからない」という回答を出したりすることがあります。
偽陽性（False Positives）: 抽象化（詳細の簡略化）を使用しているため、実際には問題がないのに、プログラムが安全ではないと判断してしまうことがあります。論文では、簡略化せずにチェックを再実行することでこれを修正できる可能性があると述べています。ただし、それにはより多くの時間がかかります。

5. まとめ

SEALは、複雑で無限のデータ鎖を管理するプログラムが安全であることを証明するために設計された、新しいモジュール型のツールです。まだ完璧ではなく、C言語のすべての機能を理解しているわけではありませんが、そのユニークな設計（ロジックパズルを解くための汎用的な翻訳者を使用すること）により、最も困難なメモリ安全性問題に対処できる数少ないツールの一つとなっています。著者らは、システムを柔軟に保つことで、将来のコンペティションにおいてさらに優れたものにできると考えています。

技術要約：SEAL – 分離論理を用いた記号実行

問題提起

非限定的な連結データ構造を操作するプログラムの検証は、静的解析における重要な課題であり続けている。多くのツールは有界モデル検査や特殊なヒューリスティックに依存しているが、これらのアプローチは、任意のリスト長や複雑なメモリ形状に関する推論の複雑さに苦慮することが多い。さらに、既存の分離論理（Separation Logic: SL）ベースの解析器は、多くの場合、解析を専用の非モジュール型ソルバーと結合させており、拡張性や他の論理理論との統合能力を制限している。

手法

SEALは、非限定的な連結データ構造を操作するプログラムの検証のために設計された静的解析器である。SEALは、分離論理（SL）の論理式に対する**前方抽象解釈（forward abstract interpretation）**を採用している。その中核となる手法は、解析エンジンと論理推論エンジンを明確に分離したモジュール型アーキテクチャによって特徴付けられる。

コアコンポーネント

抽象領域（記号的ヒープ / Symbolic Heaps）:
- SEALは、抽象的なメモリ状態を $\exists x_1, \dots, x_m. \phi_1 * \dots * \phi_n$ の形式を持つSL論理式である記能的ヒープとして表現する。
- 原子論理式（ $\phi_i$ $ϕ_{i}$ ）には以下が含まれる：
  - 純粋論理式（Pure formulae）: ポインタの（不等）価や非ポインタ値の制約を記述する。
  - ポインツ・トゥ原子（Points-to atoms）: 単一のヒープセルを記述する。
  - 帰納的述語（Inductive predicates）: 非限定的なポインタのシーケンス（例：リスト）を記述する。
  - 解放済みメモリ（Free memory）: 到達可能なまま残っている解放されたメモリを明示的に表す特別な述語。
- このドメインは、設定可能な範囲（デフォルトは $[-5, 5]$ ）内の正確な整数値を追跡する。プログラム位置における状態は、記号的ヒープの選言（集合）として表現される。
抽象化と拡大（Abstraction and Widening）:
- ループと無限の状態空間を扱うために、SEALはメモリ形状を一般化することで拡大を行う。これには、適合する空間的述語（ポインツ・トゥまたはリスト述語）を見つけ出し、それらを単一のリスト述語へと結合するプロセスが含まれる。ただし、これは結合する場所が外部のポインタやプログラム変数によってターゲットにされていない場合に限られる。
- システムは、抽象化時の循環性を保証するために、固定の制限値までの最小リスト長を追跡する。
- 述語の推測（Predicate Guessing）: 現在、SEALは解析前にフィールド数に基づいてC構造体の期待される帰納的述敵を推測する（例：自己参照フィールドが1つ $\to$ SLL、2つ $\to$ DLL）。このヒューリスティックは、誤分類（例：入れ子になったリストとして意図されている構造が、二重連結リストとして分類される）を招く可能性がある。
ASTRAL ソルバー:
- ほとんどのSLベースのツールが充足可能性や含意のために専用のヒューリスティックを使用するのに対し、SEALは汎用的な分離論理ソルバーであるASTRALに依存している。
- ASTRALは、述敵の展開（unfolding）に境界を設けることで、SL論理式をSMT理論（具体的にはビットベクトルと配列）へと翻訳する。
- 翻訳された論理式は、BITWUZLA SMTソルバーへと渡される。
- ASTRALはユーザー定義の帰納的述語をサポートしており、これによりSEALは、組み込みのソルバーサポートを持たない独自の述敵を定義できる。
解析メカニズム:
- ループ不動点（Loop Fixpoints）: 現在のループ反復状態（ $S$ ）と前の反復状態（ $T$ ）の間の含意が妥当であるときに、不動点に到達する。これは、すべてのヒープについて、 $T$ がそれを包含するヒープが存在するかどうかを確認することによって近似される。
- 関数間解析（Interprocedural Analysis）: 関数呼び出しはサマリー（前置条件／後置条件のペア）を用いて最適化される。
- 簡略化（Simplification）: システムは、等価クラスの削減やスコープ外の変数の除去といった構文的な簡略化を適用する。

主な貢献

モジュール型アーキテクチャ: 解析エンジンをASTRALを介して論理推論エンジンから分離することで、SEALは、他の理論における推論と組み合わせやすく、拡張しやすい設計を実現している。
汎用的な解決策: ASTRALの統合により、SEALはSLの含意および充足可能性のために、カスタムの専用ソルバーを必要とせず、SMTソルバーを活用できる。
非限定リストの検証: 本ツールは、非限定的な連結リストを扱うプログラムを検証することが可能であり、これは競合する多くのツールが失敗するカテゴリである。

実験結果

SEALは、SV-COMPコンペティションの MemSafety-LinkedLists カテゴリに参加した。

全体的なパフォーマンス: 全134プログラムのうち、SEALは55件を「True」（正解）として検証し、4件の「False」（バグ）を発見し、75件は結果なしとなった。
非限定リストのサブセット: 非限定的なデータ構造の推論を必要とする69プログラムのサブセットにおいて、SEALは14プログラムを正解として検証し、2つのバグを発見した。
比較:
- SEALは、2LS（3つの非限定プログラムのみを検証）を上回った。
- SEALは、PREDATORHP（46件を検証）およびCPACHECKER（40件を検証）よりも検証件数が少なかった。これら両者は記号的メモリグラフ（SMG）を使用している。
- SEALは、このカテゴリにおいて非限定リストを含むプログラムを検証できたわずか4つの解析器のうちの一つであった。

意義と主張

本論文は、SEALを、即時的な生のパフォーマンスの優位性よりも、特定の拡張性に焦点を当てた有望なプロトタイプとして位置づけている。

将来の可能性: 著者らは、SEALのモジュール型設計とASTRALへの依存が、SMGでは容易に表現できない複雑なデータ構造（スキップリストや木構造など）をサポートするための強力な基盤を提供すると主張している。
限界: 初期のプロトタイプであるため、SEALは現在限定的なC（限定的なポインタ演算、特定の整数追跡）のみをサポートしており、ヒューリスティックな述敵推測に依存している。そのため、整数情報が欠落している場合に誤検知（false positive）が発生したり、違反を報告できなかったりすることがある。
ロードマップ: 著者らは、解析中の述敵選択の改善、例からの帰納的述敵の合成、および、より複雑な非ポインタ値を扱うためにSEALをFrama-C EVAフレームワーク内の抽象領域として組み込む可能性を検討している。

要約すると、SEALは、汎用的なSMTベースの分離論理ソルビングのアプローチが、専門化されたヒューリスティックに代わる実行可能かつ拡張可能な選択肢であることを示しており、将来のコンペティションにおける複雑な非限定連結データ構造の検証への道筋を示している。