「動的バイナリ解析の基礎 with Intel Pin」の付録

技術書典６ え１１ バイナリイーターによる
「動的バイナリ解析の基礎 with Intel Pin」の付録として
「動的バイナリ計装に基づく動的記号実行」を随時掲載予定

付録目次
A1. 動的バイナリ計装に基づく動的記号実行
A1.1. 記号実行
    A2.1.1. パス制約
    A2.1.2. 記号状態
    A2.1.3. 制約解消
    A2.1.4. 静的記号実行の課題
        A2.1.4.1. 制約解消系の限界
        A2.1.4.2. パス選択の現実化
A2.2. 動的記号実行
    A2.2.1. 動的記号実行の動機
    A2.2.2. パス制約と記号状態の部分的具体化
    A2.2.3. パス選択の具体化
A2.3. 動的バイナリ計装に基づく動的記号実行の実装
    A2.3.1. パス制約の動的収集の実装
    A2.3.2. 記号状態の動的管理の実装
    A2.3.3. 制約解消の動的実行の実装
    A2.3.4. PinとZ3を用いた網羅的バッファオーバフロー検出の実装