Dynamic Symbolic Execution

Dynamic Symbolic Execution

Dynamic Symbolic Execution Mayur Naik CIS 700 Fall 2018 Motivation Writing and maintaining tests is tedious and error-prone Idea: Automated Test Generation Generate regression test suite Execute all reachable statements Catch any assertion violations Approach Dynamic Symbolic Execution Stores program state concretely and symbolically Solves constraints to guide execution at branch points Explores all execution paths of the unit tested Example of Hybrid Analysis Collaboratively combines dynamic and static analysis Execution Paths of a Program Program can be seen as binary tree with possibly infinite depth Called Computation Tree Each node represents the execution of a conditional statement F 1 T 7

F T 8 Each edge represents the execution of a sequence of nonconditional statements Each path in the tree represents an equivalence class of inputs 2 F 10 T 3 F 9 T 12 11 T 4 T 5

F 6 T 13 Example of Computation Tree void test_me(int x, int y) { if (2*y == x) { if (x <= y+10) F 2*y== x T print(OK); else { print(something bad); ERROR; F x <= y+10 ERROR } } else print(OK); } assert(b)

if (!b) ERROR; T Existing Approach I Random Testing Generate random inputs Execute the program on those (concrete) inputs Problem: Probability of reaching error could be astronomically small void test_me(int x) { if (x == 94389) { ERROR; } } Probability of ERROR: 1/232 0.000000023% Existing Approach II Symbolic Execution Use symbolic values for inputs Execute program symbolically on symbolic input values Collect symbolic path constraints Use theorem prover to check if a branch can be taken void test_me(int x) { if (x*3 == 15) {

if (x % 5 == 0) print(OK); else { print(something bad); ERROR; } } else print(OK); } Problem: Does not scale for large programs Existing Approach II Symbolic Execution Use symbolic values for inputs Execute program symbolically on symbolic input values Collect symbolic path constraints Use theorem prover to check if a branch can be taken Problem: void test_me(int x) { // c = product of two // large primes if (pow(2,x) % c == 17) { print(something bad); ERROR; } else print(OK); }

Symbolic execution will say both branches are reachable: False Positive Does not scale for large programs Combined Approach Dynamic Symbolic Execution (DSE) Start with random input values Keep track of both concrete values and symbolic constraints Use concrete values to simplify symbolic constraints Incomplete theorem-prover int foo(int v) { return 2*v; } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } An Illustrative Example int foo(int v) { return 2*v; } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR;

} Concrete Execution concrete state Symbolic Execution symbolic state x = 22 x = x0 y = 7 y = y0 path condition An Illustrative Example int foo(int v) { return 2*v; } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete

Execution concrete state symbolic state x = 22 x = x0 y = 7 y = y0 z = 14 Symbolic Execution z = 2*y0 path condition An Illustrative Example int foo(int v) { return 2*v; } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; }

Concrete Execution concrete state symbolic state x = 22 x = x0 y = 7 y = y0 z = 14 Symbolic Execution z = 2*y0 path condition 2*y0 != x0 An Illustrative Example int foo(int v) { return 2*v; } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10)

ERROR; } Concrete Execution concrete state symbolic state x = 22 x = x0 y = 7 y = y0 z = 14 Symbolic Execution path condition 2*y0 != x0 z = 2*y0 Solve: 2*y0 == x0 Solution: x0 = 2, y0 = 1 An Illustrative Example int foo(int v) { return 2*v; }

void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 2 x = x0 y = 1 y = y0 path condition An Illustrative Example int foo(int v) { return 2*v; } void test_me(int x, int y) { int z = foo(y);

if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 2 x = x0 y = 1 y = y0 z = 2 z = 2*y0 path condition An Illustrative Example int foo(int v) { return 2*v; } void test_me(int x, int y) {

int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 2 x = x0 y = 1 y = y0 z = 2 z = 2*y0 path condition 2*y0 == x0 An Illustrative Example int foo(int v) { return 2*v;

} void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 2 x = x0 y = 1 y = y0 z = 2 z = 2*y0 path condition 2*y0 == x0 x0 <= y0+10

An Illustrative Example int foo(int v) { return 2*v; } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 2 x = x0 y = 1 y = y0 z = 2 z = 2*y0 path

condition 2*y0 == x0 x0 <= y0+10 Solve: (2*y0 == x0) and (x0 > y0+10) Solution: x0 = 30, y0 = 15 An Illustrative Example int foo(int v) { return 2*v; } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 30 x = x0 y = 15

y = y0 path condition An Illustrative Example int foo(int v) { return 2*v; } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 30 x = x0 y = 15 y = y0

z = 30 z = 2*y0 path condition An Illustrative Example int foo(int v) { return 2*v; } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 30 x = x0 y = 15 y = y0

z = 30 z = 2*y0 path condition 2*y0 == x0 An Illustrative Example Concrete Execution int foo(int v) { return 2*v; concrete state } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Program Error Symbolic Execution symbolic state

x = 30 x = x0 y = 15 y = y0 z = 30 z = 2*y0 path condition 2*y0 == x0 x0 > y0+10 QUIZ: Computation Tree Check all constraints that DSE might possibly solve in exploring the computation tree shown below: C1 C2 C1 C2 C1 C2 C1 C2 C1 C2 C1 C2 F C 1

F T C 2 T QUIZ: Computation Tree Check all constraints that DSE might possibly solve in exploring the computation tree shown below: C1 C2 C1 C2 C1 C2 C1 C2 C1 C2 C1 C2 F C 1 F T C 2

T A More Complex Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 22 x = x0 y = 7 y = y0 path condition A More Complex Example

int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state symbolic state x = 22 x = x0 y = 7 y = y0 z = z = 601...129 Symbolic Execution secure_hash(y0) path

condition A More Complex Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state path condition x = 22 x = x0 secure_hash(y0) y = 7 y = y0

z = != x0 z = 601...129 Solve: secure_hash(y0) secure_hash(y0) == x0 Dont know how to solve! Stuck? A More Complex Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) } NotERROR; stuck! Use concrete state: replace y0 by 7 Concrete Execution concrete state

Symbolic Execution symbolic state path condition x = 22 x = x0 secure_hash(y0) y = 7 y = y0 z = != x0 z = 601...129 Solve: secure_hash(y0) secure_hash(y0) == x0 Dont know how to solve! Stuck? A More Complex Example int foo(int v) {

return secure_hash(v); } void test_me(int x, int y) { int z = foo(y); if (z == x) } Concrete Execution concrete state Symbolic Execution symbolic state path condition x = 22 x = x0 secure_hash(y0) y = 7 y = y0 z = != x0 z =

601...129 secure_hash(y0) if (x > y+10) Solve: 601...129 == x0 ERROR; Solution: x0 = 601...129, y0 = 7 A More Complex Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state x = 601...129 y = 7 Symbolic Execution symbolic

state x = x0 y = y0 path condition A More Complex Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state x = 601...129 z = y = 7 601...129 Symbolic Execution symbolic state x = x0 y = y0 z = secure_hash(y0)

path condition A More Complex Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { int z = foo(y); if (z == x) if (x > y+10) ERROR; } Concrete Execution concrete state x = 601...129 z = y = 7 601...129 Symbolic Execution symbolic state path condition x = x0 secure_hash(y0)

y = y0 z = == x0 secure_hash(y0) A More Complex Example Concrete Execution int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { int z = foo(y); if (z == x) concrete state x = 601...129 z = y = 7 601...129 if (x > y+10) ERROR; } Program Error Symbolic Execution

symbolic state path condition x = x0 secure_hash(y0) y = y0 z = == x0 secure_hash(y0) x0 > y0+10 QUIZ: Example Application DSE tests the below program starting with input x = 1. What is the input and constraint (C1 C2 C3) solved in each run of DSE? Use depth-first search and leave trailing constraints blank if unused. Ru n x C1 C2 C3 1

1 5 != x0 7 != x0 9 == x0 2 3 4 int test_me(int x) { int[] A = { 5, 7, 9 }; int i = 0; while (i < 3) { if (A[i] == x) break; i++; } return i; } QUIZ: Example Application DSE tests the below program starting with input x = 1. What is the input and constraint (C1 C2 C3) solved in each run of DSE? Use depth-first search and leave trailing constraints blank if unused. Ru n x C1

C2 C3 1 1 5 != x0 7 != x0 9 == x0 2 9 5 != x0 7 == x0 3 7 5 == x0 4 5

int test_me(int x) { int[] A = { 5, 7, 9 }; int i = 0; while (i < 3) { if (A[i] == x) break; i++; } return i; } A Third Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { if (x != y) if (foo(x) == foo(y)) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 22

x = x0 y = 7 y = y0 path condition A Third Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { if (x != y) if (foo(x) == foo(y)) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 22 x = x0 y = 7

y = y0 path condition x0 != y0 A Third Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { if (x != y) if (foo(x) == foo(y)) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state x = 22 x = x0 y = 7 y = y0

path condition x0 != y0 secure_hash(x0) != secure_hash(y0) Solve: x0 != y0 and secure_hash(x0) == secure_hash(y0) Use concrete state: replace y0 by 7. A Third Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { if (x != y) if (foo(x) == foo(y)) ERROR; } Concrete Execution concrete state Symbolic Execution symbolic state

x = 22 x = x0 y = 7 y = y0 path condition x0 != y0 secure_hash(x0) != secure_hash(y0) Solve: x0 != 7 and secure_hash(x0) == 601...129 Use concrete state: replace x0 by 22. A Third Example int foo(int v) { return secure_hash(v); } void test_me(int x, int y) { if (x != y) Concrete Execution concrete state Symbolic Execution

symbolic state x = 22 x = x0 y = 7 y = y0 } False negative! x0 != y0 secure_hash(x0) != if (foo(x) == foo(y)) ERROR; path condition secure_hash(y0) Solve: 22 != 7 and 438...861 == 601...129 Unsatisfiable! QUIZ: Properties of DSE Assume that programs can have infinite computation trees. Which statements are true of DSE applied to such programs?

DSE is guaranteed to terminate. DSE is complete: if it ever reaches an error, the program can reach that error in some execution. DSE is sound: if it terminates and did not reach an error, the program cannot reach an error in any execution. QUIZ: Properties of DSE Assume that programs can have infinite computation trees. Which statements are true of DSE applied to such programs? DSE is guaranteed to terminate. DSE is complete: if it ever reaches an error, the program can reach that error in some execution. DSE is sound: if it terminates and did not reach an error, the program cannot reach an error in any execution. Another Example: Testing Data Structures Random Test Driver: random value for x random memory graph reachable from p typedef struct cell { int data; struct cell *next; } cell; int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) Probability of reaching ERROR is extremely low if (p != NULL) if (foo(x) == p->data) if (p->next == p)

ERROR; return 0; } Data-Structure Example typedef struct cell { int data; struct cell *next; } cell; int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } Concrete Execution concrete state x = 236 p = NULL Symbolic Execution symbolic state x = x0 p = p0

path condition Data-Structure Example typedef struct cell { int data; struct cell *next; } cell; int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } Concrete Execution concrete state x = 236 p = NULL Symbolic Execution symbolic state path condition

x = x0 p = p0 x0 > 0 Data-Structure Example typedef struct cell { int data; struct cell *next; } cell; int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } Concrete Execution concrete state x = 236 p = NULL Symbolic Execution symbolic state path

condition x = x0 p = p0 x0 > 0 p0 == NULL Data-Structure Example typedef struct cell { int data; struct cell *next; } cell; int foo(int v) { return 2*v + 1; } Concrete Execution concrete state x = 236 p = NULL Symbolic Execution symbolic state path condition x = x0 p = p0

x0 > 0 p0 == NULL int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } Solve: x0 > 0 and p0 != NULL Solution: x0 = 236, p0 634 NULL Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell; int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0;

} p Symbolic Execution concrete state symbolic xstate = x0 x = 236 p = p0 p->data = v0 p->next = n0 634 NULL path condition Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell;

int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } p Symbolic Execution concrete state symbolic xstate = x0 path condition x = 236 p = p0 p->data = v0 p->next = n0 x0 > 0

634 NULL Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell; int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } p Symbolic Execution concrete state symbolic xstate = x0 path condition

x = 236 p = p0 p->data = v0 p->next = n0 x0 > 0 p0 != NULL 634 NULL Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell; int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } p

Symbolic Execution concrete state symbolic xstate = x0 path condition x = 236 p = p0 p->data = v0 p->next = n0 x0 > 0 p0 != NULL 2*x0+1 != v0 634 NULL Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next;

} cell; int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) p Symbolic Execution concrete state symbolic xstate = x0 path condition x = 236 p = p0 p->data = v0 p->next = n0 x0 > 0 p0 != NULL 2*x0+1 != v0

634 NULL Solve: x0 > 0 and p0 != NULL and 2*x0+1==v0 ERROR; return 0; } Solution: x0 = 1, p0 3 NULL Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell; concrete state int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data)

if (p->next == p) ERROR; return 0; } x = 1 p 3 NULL Symbolic Execution symbolic xstate = x0 p = p0 p->data = v0 p->next = n0 path condition Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell;

concrete state int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } x = 1 p 3 NULL Symbolic Execution symbolic xstate = x0 path condition p = p0 p->data = v0 p->next = n0

x0 > 0 Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell; concrete state int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } x = 1 p 3 NULL Symbolic Execution symbolic

xstate = x0 path condition p = p0 p->data = v0 p->next = n0 x0 > 0 p0 != NULL Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell; concrete state int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR;

return 0; } x = 1 p 3 NULL Symbolic Execution symbolic xstate = x0 path condition p = p0 p->data = v0 p->next = n0 x0 > 0 p0 != NULL 2*x0+1 == v0 Data-Structure Example typedef struct cell { Concrete Execution

int data; struct cell *next; } cell; concrete state int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } x = 1 p 3 NULL Symbolic Execution symbolic xstate = x0 path condition p = p0 p->data =

v0 p->next = n0 x0 > 0 p0 != NULL 2*x0+1 == v0 n0 != p0 Solve: x0 > 0 and p0 != NULL and 2*x0+1==v0 and n0 == p0 Solution: x0 = 1, p0 3 Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell; concrete state int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data)

if (p->next == p) ERROR; return 0; } x = 1 p 3 Symbolic Execution symbolic xstate = x0 p = p0 p->data = v0 p->next = n0 path condition Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell; concrete state

int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } x = 1 p 3 Symbolic Execution symbolic xstate = x0 path condition p = p0 p->data = v0 p->next = n0 x0 > 0 Data-Structure Example typedef struct cell {

Concrete Execution int data; struct cell *next; } cell; concrete state int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } x = 1 p 3 Symbolic Execution symbolic xstate = x0 path condition

p = p0 p->data = v0 p->next = n0 x0 > 0 p0 != NULL Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell; concrete state int foo(int v) { return 2*v + 1; } int test_me(int x, cell *p) { if (x > 0) if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } x = 1 p

3 Symbolic Execution symbolic xstate = x0 path condition p = p0 p->data = v0 p->next = n0 x0 > 0 p0 != NULL 2*x0+1 == v0 Data-Structure Example typedef struct cell { Concrete Execution int data; struct cell *next; } cell; concrete state int foo(int v) { return 2*v +

1; } int test_me(int x, cell *p) { if (x > 0) x = 1 p if (p != NULL) if (foo(x) == p->data) if (p->next == p) ERROR; return 0; } Program Error 3 Symbolic Execution symbolic xstate = x0 path condition p = p0 p->data = v0 p->next = n0 x0 > 0 p0 !=

NULL 2*x0+1 == v0 n0 != p0 Approach in a Nutshell Generate concrete inputs, each taking different program path On each input, execute program both concretely and symbolically Both cooperate with each other: Concrete execution guides symbolic execution Enables it to overcome incompleteness of theorem prover Symbolic execution guides generation of concrete inputs Increases program code coverage QUIZ: Characteristics of DSE The testing approach of DSE is: Automated, black-box Automated, white-box Manual, black-box Manual, white-box The input search of DSE is: Randomized Systematic The static analysis of DSE is: Flow-insensitive Flow-sensitive The instrumentation in DSE is: Sampled Non-sampled Path-sensitive QUIZ: Characteristics of DSE The testing approach of DSE is:

Automated, black-box Automated, white-box Manual, black-box Manual, white-box The input search of DSE is: Systematic Randomized The static analysis of DSE is: Flow-insensitive Flow-sensitive The instrumentation in DSE is: Non-sampled Sampled Path-sensitive Case Study: SGLIB C Library Found two bugs in sglib 1.0.1 reported to authors, fixed in sglib 1.0.2 Bug 1: doubly-linked list segmentation fault occurs when a non-zero length list is concatenated with zero-length list discovered in 140 iterations (< 1 second) Bug 2: hash-table an infinite loop in hash-table is_member function 193 iterations (1 second) Case Study: SGLIB C Library Name Run

# % # # time # branches branch functions bugs (sec.) iterations explored coverage tested found Array Quick Sort 2 732 43 97.73 2 0 Array Heap Sort 4 1764 36 100.00 2 0

Linked List 2 570 100 96.15 12 0 Sorted List 2 1020 110 96.49 11 0 Doubly Linked List 3 1317 224 99.12 17

1 Hash Table 1 193 46 85.19 8 1 Red Black Tree 2629 1,000,000 242 71.18 17 0 Case Study: Needham-Schroeder Protocol Tested a C implementation of a security protocol (Needham-Schroeder) with a known (man-in-themiddle) attack 600 lines of code Took fewer than 13 seconds on a machine with 1.8 GHz processor and 2 GB RAM to discover the attack In contrast, a software model-checker (VeriSoft) took

8 hours Realistic Implementations KLEE: LLVM (C family of languages) PEX: .NET Framework jCUTE: Java Jalangi: Javascript SAGE and S2E: binaries (x86, ARM, ...) Case Study: SAGE Tool at Microsoft SAGE = Scalable Automated Guided Execution Found many expensive security bugs in many Microsoft applications (Windows, Office, etc.) Used daily in various Microsoft groups, runs 24/7 on 100s of machines What makes it so useful? Works on large applications => finds bugs across components Focus on input file fuzzing => fully automated Works on x86 binaries => easy to deploy (not dependent on language or build process) Example: SAGE Crashing a Media Parser after a few more iterations: What Have We Learned? What is (dynamic) symbolic execution? Systematically generate (numeric and pointer) inputs Computation tree and error reachability Tracking concrete state, symbolic state, path condition Combined dynamic and static analysis => Hybrid analysis Complete, but no soundness or termination guarantees

Recently Viewed Presentations

  • Module 5 Chemical Properties

    Module 5 Chemical Properties

    In a compound made up of two elements, the name of the first element stays the same. The ending of the second element changes to -ide. 18-3 - Chemical Formulas. Some of the compounds above contain parentheses in their chemical...
  • Chapter 1

    Chapter 1

    CHAPTER OBJECTIVES CHAPTER OUTLINE Plane-Stress Transformation General Equations of Plane Stress Transformation Principal Stresses and Maximum In-Plane Shear Stress Mohr's Circle - Plane Stress Stress in Shafts Due to Axial Load and Torsion Stress Variations Throughout a Prismatic Beam Absolute...
  • The Elements of Poetry

    The Elements of Poetry

    Monday, April 16th Hello, class. Today you will have time to edit your assignment from Friday, but first we will take notes to remind ourselves of the elements of poetry. Your warm-up is to be ready to start your notes...
  • Course: Public Relations: The Profession and Practice

    Course: Public Relations: The Profession and Practice

    Public relations became a respected, sophisticated and expanded profession during the post-WWII era, largely through governmental and public influence. Currently public relations is evolving as a force for adaptation to public concerns on vital issues. In Summary… Since its inception,...
  • Chapter 3: Probability

    Chapter 3: Probability

    Chapter 3 Probability § 3.2 Conditional Probability and the Multiplication Rule Conditional Probability Conditional Probability Independent Events Probability § 3.2 Conditional Probability and the Multiplication Rule Conditional Probability Conditional Probability Independent Events A conditional probability is the probability of an...
  • From Classical to Contemporary

    From Classical to Contemporary

    Defining the Renaissance HUM 2052: Civilization II Summer 2010 Dr. Perdigao May 20, 2010 Diego Velazquez's Las Meninas (The Maids in Waiting) (1656) Those in the court of Philip IV: Margarita, the daughter of Philip IV, her maids in waiting,...
  • ` For Thursday, Dec. 2, read (and write

    ` For Thursday, Dec. 2, read (and write

    Agent Causation and Mental Causation Nida-Rumelin claims that the self is motivated by mental states, including perceptions and consciously held propositional attitudes, but the self is not caused to do anything by these states. Subject Causation Once a body has...
  • CIS 570 Advanced Computer Systems

    CIS 570 Advanced Computer Systems

    Alpha 21164, 0.6 GHz. Alpha 21264, 0.6 GHz ... CIS 570 Advanced Computer Systems Author: Michael J. Geiger Last modified by ... Multiprocessing Flynn's Taxonomy Back to Basics Centralized Shared Memory Multiprocessors Distributed Memory Multiprocessors Centralized-Memory Machines Shared Memory ...