Conference: Oakland 2010 Link: https://users.ece.cmu.edu/~aavgerin/papers/Oakland10.pdf

1 Introduction

Dynamic:

• reason about actual executions
• based upon run-time information
• two common security techniques:
  • Dynamic taint analysis runs a program and observes which computations are affected by predefined taint sources.
  • Dynamic forward symbolic execution automatically builds a logical formula describing a program execution path, which reduces the problem to the domain of logic (instead of concrete values).

Paper contributions:

• formalize dynamic taint analysis and forward symbolic execution
• show how this formalization can be used to tease out and describe common implementation details

2 SIL (Simple Intermediate Language)

Overview

• a program consists of a sequence of statements, including assignments, assertions, jumps and conditional jumps

• get_input(src) returns input from source

  • get_input(.) : the exact input source is not relevant

• operational semantics:

  • statement rule