Symbolic Execution Note

  • finding bugs, symbolic execution, EXE

Bugs

  • Major source of security exploits.

  • Bugs ~ Exploit

    • maybe hard, but should assume it is possible

    • e.g., not buffer overrun is an exploit, but it maybe possible to exploit

Approaches To Finding Bugs

  • Verification : eliminate classes of bugs

  • Testing : known bugs

  • Fuzzing : unknown bugs

  • Symbolic Execution

可能的情境

  • Bugs 可能的類型：

    • Crash

      • Divide By Zero

      • Null Pointer Reference

    • Array Out-Of-Bound

    • App Specific

Goal : Find Deep Bugs

Ideas :

  • compute on symbolic values

  • create path conditions

  • Use solver to see if a branch is possible.

EXE Overview

這邊 EXE 可能是指 EXE: Automatically Generating Inputs of Death 這篇論文。

  • Compile Time

  • Runtime : explore paths

Runtime Components

Example

1
2
3
4
5
6
7
8
example:
1. read x, y
2. if x > y:
3.   x = y
4. if x < y:
5.   x = x + 1
6. if x + y == 7
7.   error()

  • Line 6 可以想成 assert(x + y != 7) 。

  • 目標是找到什麼樣的 x, y 會讓 Line 7 error() 被觸發。

  • EX: one path

    Line x (a) y (b) Path Condition {}
    1. a b {}
    2t. a b {a > b}
    3. b b {a > b}
    4. No Fork No Fork No Fork
    6. No Fork No Fork No Fork

    • 這次我們在 line 2 選擇探索 true case 。

    • Falls Though at line 4.

    • Line 6 處我們不需要再更進一步去下探 (因為 7 是奇數) ，故 No Fork 。

  • EX: Another Path

    Line x (a) y (b) Path Condition {}
    1. a b {}
    2f. a b {a <= b}
    4t. a b {a < b}
    5. a + 1 b {a < b}
    6. a + 1 b {a + 1 + b == 7}

    • 這次我們在 line 2 選擇探索 false case 、在 line 4 選擇 true case 。

    • 到 line 6 我們可以知道此範例會不會有解，這題解可以是 a=2, b=4 。

更真實的例子： BPF (Berkeley Packet Filter)

Variables Are Bit Arrays