Precision Even path sensitive analysis approximates behavior due to: ·loops/recursion ·unrealizable paths 1.if(an+bn=cn&&n>2&&a>0&&b>0&&c>0) 2. X=7; 3.else Unrealizable path. 4. X=8; x will always be 8 16
Precision Even path sensitive analysis approximates behavior due to: • loops/recursion • unrealizable paths 1. if(an + b n = c n && n>2 && a>0 && b>0 && c>0) 2. x = 7; 3. else 4. x = 8; Unrealizable path. x will always be 8 16
最 20 Control Flow Integrity implementation 17
Control Flow Integrity implementation [1] 17
CFl Overview Invariant:Execution must follow a path in a control flow graph (CFG)created ahead of run time. Method: build CFG statically,e.g.,at compile time instrument (rewrite)binary,e.g.,at install time add IDs and ID checks;maintain ID uniqueness verify CFI instrumentation atload time directjump targets,presence of IDs and ID checks,ID uniqueness .perform ID checks at run time indirectjumps have matchingIDs 18
CFI Overview Invariant: Execution must follow a path in a control flow graph (CFG) created ahead of run time. Method: • build CFG statically, e.g., at compile time • instrument (rewrite) binary, e.g., at install time – add IDs and ID checks; maintain ID uniqueness • verify CFI instrumentation at load time – direct jump targets, presence of IDs and ID checks, ID uniqueness • perform ID checks at run time – indirect jumps have matching IDs 18
最 Build CFG ······>direct calls →indirect calls bool lt(int x,int y){ sort2(): sort(): 1t(): return x y; label 17 3 call sort ca1117,R F bool gt(int x,int y){ -ret 23 return x y; label 55 label 23 3 3 gt(): call sort ret 55 Mlabel 17 sort2(int a[],int b[],int len) label 55 3 ret 23 sort(a,len,lt ) sort(b,len,gt ) ret .. Two possible return sites due to contextinsensitivity 19
Build CFG 19 Two possible return sites due to context insensitivity direct calls indirect calls
Instrument Binary bool lt(int x,int y){ sort2(): sort () 1t(): return x y; label 17 } call sort' ca1117,R 3 bool gt(int x,int y){ ---ret23 return x y; label 55 label 23 gt(): call sort ret 55 Mlabel 17 sort2(int a[],int b[],int len) 3 label 55 sort(a,len,lt ) ret 23 sort(b,len,gt ) ret .. Insert a unique number at each destination Two destinations are equivalent if CFG contains edges to each from the same source 20
Instrument Binary • Insert a unique number at each destination • Two destinations are equivalent if CFG contains edges to each from the same source 20