7 Counterexample-guided abstraction refinement(CEGAR). CEGAR-based SMT solver (1185843), страница 3
Текст из файла (страница 3)
∩ LnCurrent SolversContext-freeUndecidablen/aPSPACE-completeQuantifiedBoolean LogicNP-completeSATEfficient in practiceRegularBoundedVijay GaneshWednesday, 16 January, 1353Hampi Key Idea: Bounded LogicsTesting,Vulnerability Detection,...•Finding SAT assignment is key•Bounding is sufficient•Short assignments are sufficient•Bounded logics easier to decideVijay GaneshWednesday, 16 January, 1354Hampi Key Idea: Bounded LogicsBounding vs. Completeness• Bounding leads to incompleteness• Testing (Bounded MC) vs.Verification (MC)• Bounding allows trade-off (Scalability vs. Completeness)• Completeness (also, soundness) as resourcesVijay GaneshWednesday, 16 January, 1355HAMPI Solver Motivating ExampleSQL Injection VulnerabilitiesInput StringVar v : 12;cfg SqlSmall := "SELECT ” [a-z]+ " FROM ” [a-z]+ " WHERE " Cond;SQLGrammarcfg Cond := Val "=" Val | Cond " OR " Cond;cfg Val := [a-z]+ | "'” [a-z0-9]* "'" | [0-9]+;SQL Queryval q := concat("SELECT msg FROM messages WHERE topicid='", v, "'");assert v in [0-9]+;SQLI attackconditionsVijay GaneshWednesday, 16 January, 13“q is a valid SQL query”assert q in SqlSmall;assert q contains "OR ‘1'=‘1'";“q contains an attack vector”56How Hampi WorksBird’s Eye View: Strings into Bit-vectorsvar v : 4;Hampicfg E := “()” | E E | “(“ E “)”;val q := concat( “(“, v, ”)”);assert q in E;assert q contains “()()”;NormalizerSTP EncoderBit-vectorConstraintsSTPSTP DecoderFind a 4-char string v:• (v) is in E• (v) contains ()()Vijay GaneshWednesday, 16 January, 13Bit-vectorSolutionString Solutionv = )()(57How Hampi WorksUnroll Bounded CFGs into Regular Exp.var v : 4;Hampicfg E := “()” | E E | “(“ E “)”;val q := concat( “(“, v, ”)”);assert q in E;assert q contains “()()”;NormalizerSTP EncoderBound(E,6)([()() + (())]) +()[()() + (())] +[()() + (())]()Bit-vectorConstraintsSTPSTP DecoderBit-vectorSolutionString Solutionv = )()(Vijay GaneshWednesday, 16 January, 1358How Hampi WorksUnroll Bounded CFGs into Regular Exp.var v : 4;HampiBound Auto-derivedcfg E := “()” | E E | “(“ E “)”;val q := concat( “(“, v, ”)”);assert q in E;assert q contains “()()”;NormalizerSTP EncoderBound(E,6)([()() + (())]) +()[()() + (())] +[()() + (())]()Bit-vectorConstraintsSTPSTP DecoderBit-vectorSolutionString Solutionv = )()(Vijay GaneshWednesday, 16 January, 1358How Hampi WorksBird’s Eye View: Strings into Bit-vectorsvar v : 4;Hampicfg E := “()” | E E | “(“ E “)”;val q := concat( “(“, v, ”)”);assert q in E;assert q contains “()()”;NormalizerSTP EncoderBit-vectorConstraintsSTPSTP DecoderFind a 4-char string v:• (v) is in E• (v) contains ()()Vijay GaneshWednesday, 16 January, 13Bit-vectorSolutionString Solutionv = )()(59How Hampi WorksUnroll Bounded CFGs into Regular Exp.var v : 4;Step 1:cfg E := “()” | E E | “(“ E “)”;val q := concat( “(“, v, ”)”);Auto-derivelower/upper bounds[L,B]on CFG[6,6]assert q in E;assert q contains “()()”;Step 2:cfg E := “()” | E E | “(“ E “)”Vijay GaneshWednesday, 16 January, 13Look forminimal lengthstring“()”60How Hampi WorksUnroll Bounded CFGs into Regular Exp.Length: 6Step 3:cfg E := “()” | E E | “(“ E “)”Min.
length constant: ”()”Length: 6Step 4:cfg E := “()” | E E | “(“ E “)”Min. length constant: ”()”Vijay GaneshWednesday, 16 January, 13Recursivelyexpandnon-terminals:Construct PartitionsRecursivelyexpandnon-terminals:Construct RE[4,2][2,4][3,3][5,1][1,5][1,4,1](())()()(())((()))61Unroll Bounded CFGs into Regular Exp.Managing Exponential Blow-upLength: 6cfg E := “()” | E E | “(“ E “)”Min. length constant: ”()”Recursivelyexpandnon-terminals:Construct RE(())()()(())((()))...•Dynamic programming style• Works well in practiceVijay GaneshWednesday, 16 January, 1362Unroll Bounded CFGs into Regular Exp.Managing Exponential Blow-upLength: 6cfg E := “()” | E E | “(“ E “)”Min. length constant: ”()”Bound(E,6)Vijay GaneshWednesday, 16 January, 13Recursivelyexpandnon-terminals:Construct RE(())()()(())((()))...([()() + (())]) +()[()() + (())] +[()() + (())]()63How Hampi WorksConverting Regular Exp.
into Bit-vectorsEncode regular expressions recursively• Alphabet { (, ) }0, 1• constantbit-vector constant• union +disjunction• concatenationconjunction • Kleene star *conjunction• Membership, equalityequality( v )()[()() + (())] +FormulaB[0]=0Vijay GaneshWednesday, 16 January, 131[()()+ (())]() + ([()() + (())])Formula2Formula3…64How Hampi WorksConverting Regular Exp. into Bit-vectors( v )()[()() + (())] +Formula1[()()+ (())]() + ([()() + (())])Formula2Formula3B[0]=0 ∧ B[1]=1 ∧ {B[2]=0∧B[3]=1∧B[4]=0∧B[5]=1 ∨…• Constraint Templates• Encode once, and reuse• On-demand formula generationVijay GaneshWednesday, 16 January, 1365How Hampi WorksDecoder converts Bit-vectors to Stringsvar v : 4;Hampicfg E := “()” | E E | “(“ E “)”;val q := concat( “(“, v, ”)”);assert q in E;assert q contains “()()”;NormalizerSTP EncoderBit-vectorConstraintsSTPSTP DecoderFind a 4-char string v:• (v) is in E• (v) contains ()()Vijay GaneshWednesday, 16 January, 13Bit-vectorSolutionString Solutionv = )()(66Rest of the Talk• HAMPI Logic: A Theory of Strings• Motivating Example: HAMPI-based Vulnerability Detection App• How HAMPI works• Experimental Results• Related Work: Theory and Practice• HAMPI 2.0• SMTization: Future of StringsVijay GaneshWednesday, 16 January, 1367HAMPI: Result 1Static SQL Injection Analysis10001010.11101001000100000.01100000Time To Solve (sec)100Grammar Size (# of productions)• 1367 string constraints from Wasserman & Su [PLDI’07]• Hampi scales to large grammars• Hampi solved 99.7% of constraints in < 1sec• All solvable constraints had short solutionsVijay GaneshWednesday, 16 January, 1368HAMPI: Result 2Security Testing and XSS• Attackers inject client-side script into web pages• Somehow circumvent same-origin policy in websites• echo “Thank you $my_poster for using the message board”;• Unsanitized $my_poster• Can be JavaScript• Execution can be badVijay GaneshWednesday, 16 January, 1369HAMPI: Result 2Security Testing• Hampi used to build Ardilla security tester [Kiezun et al., ICSE’09]• 60 new vulnerabilities on 5 PHP applications (300+ kLOC)• 23 SQL injection• 37 cross-site scripting (XSS)5 added toUS National Vulnerability DB• 46% of constraints solved in < 1 second per constraint• 100% of constraints solved in <10 seconds per constraintVijay GaneshWednesday, 16 January, 1370HAMPI: Result 3Comparison with Competing Tools2515CFGAnalyzer105average time (sec.)20Hampi010203040500string size (characters)• HAMPI vs.
CFGAnalyzer (U. Munich): HAMPI ~7x faster for strings of size 50+Vijay GaneshWednesday, 16 January, 1371HAMPI: Result 3Comparison with Competing ToolsRE intersection problems• HAMPI 100x faster than Rex (MSR)• HAMPI 1000x faster than DPRLE (U.Virginia)• Pieter Hooimeijer 2010 paper titled ‘Solving String Constraints Lazily’Vijay GaneshWednesday, 16 January, 1372How to Automatically Crash Programs?KLEE: Concolic Execution-based TesterProblem: Automatically generate crashing tests given only the codeProgramSymbolic ExecutionEnginewithImplicit SpecAutomatic TesterFormulasSTPSAT/UNSATCrashing TestsVijay Ganesh, Dagstuhl, Aug 8-12, 2011Wednesday, 16 January, 1373How to Automatically Crash Programs?KLEE: Concolic Execution-based TesterStructured input processing code:PDF Reader, Movie Player,...Buggy_C_Program(int* data_field, int len_field) {int * ptr = malloc(len_field*sizeof(int));int i; //uninitialized}while (i++ < process(len_field)) {//1.
Integer overflow causing NULL deref//2. Buffer overflow*(ptr+i) = process_data(*(data_field+i));}• Formula captures computation• Tester attaches formula to capture specVijay Ganesh, Dagstuhl, Aug 8-12, 2011Wednesday, 16 January, 1374How to Automatically Crash Programs?KLEE: Concolic Execution-based TesterStructured input processing code:PDF Reader, Movie Player,...Buggy_C_Program(int* data_field, int len_field) {int * ptr = malloc(len_field*sizeof(int));int i; //uninitialized}while (i++ < process(len_field)) {//1. Integer overflow causing NULL deref//2. Buffer overflow*(ptr+i) = process_data(*(data_field+i));}Equivalent Logic Formula derived usingsymbolic executiondata_field, mem_ptr : ARRAY;len_field : BITVECTOR(32); //symbolici, j, ptr : BITVECTOR(32);//symbolic..mem_ptr[ptr+i] = process_data(data_field[i]);mem_ptr[ptr+i+1] = process_data(data_field[i+1]);..• Formula captures computation• Tester attaches formula to capture specVijay Ganesh, Dagstuhl, Aug 8-12, 2011Wednesday, 16 January, 1374How to Automatically Crash Programs?KLEE: Concolic Execution-based TesterStructured input processing code:PDF Reader, Movie Player,...Buggy_C_Program(int* data_field, int len_field) {int * ptr = malloc(len_field*sizeof(int));int i; //uninitialized}while (i++ < process(len_field)) {//1.
Integer overflow causing NULL deref//2. Buffer overflow*(ptr+i) = process_data(*(data_field+i));}Equivalent Logic Formula derived usingsymbolic executiondata_field, mem_ptr : ARRAY;len_field : BITVECTOR(32); //symbolici, j, ptr : BITVECTOR(32);//symbolic..mem_ptr[ptr+i] = process_data(data_field[i]);mem_ptr[ptr+i+1] = process_data(data_field[i+1]);..• Formula captures computation• Tester attaches formula to capture specVijay Ganesh, Dagstuhl, Aug 8-12, 2011Wednesday, 16 January, 1374How to Automatically Crash Programs?KLEE: Concolic Execution-based TesterStructured input processing code:PDF Reader, Movie Player,...Buggy_C_Program(int* data_field, int len_field) {int * ptr = malloc(len_field*sizeof(int));int i; //uninitialized}while (i++ < process(len_field)) {//1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
