5 Motivation for SMT solvers, and combination of decision procedures (1185841), страница 4
Текст из файла (страница 4)
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.
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]);..//INTEGER OVERFLOW QUERY0 <= j <= process(len_field);ptr + i + j = 0?• Formula captures computation• Tester attaches formula to capture specVijay Ganesh, Dagstuhl, Aug 8-12, 2011Wednesday, 16 January, 1374HAMPI: Result 4Helping KLEE Pierce ParsersMark InputSymbolicParserSemantic CoreKLEESymbolic ExecutionEnginewithImplicit SpecFormulasSTPSAT/UNSATCrashing TestsVijay GaneshWednesday, 16 January, 1375HAMPI: Result 4Helping KLEE Pierce ParsersGenerate InputUsing HAMPI;Mark Partially SymbolicParserSemantic CoreKLEESymbolic ExecutionEnginewithImplicit SpecFormulasSTPSAT/UNSATCrashing TestsVijay GaneshWednesday, 16 January, 1376HAMPI: Result 4Helping KLEE Pierce Parsers• Klee provides API to place constraints on symbolic inputs• Manually writing constraints is hard• Specify grammar using HAMPI, compile to C code• Particularly useful for programs with highly-structured inputs• 2-5X improvement in line coverageVijay GaneshWednesday, 16 January, 1377Impact of Hampi: Notable ProjectsCategoryResearch ProjectProject Leader/InstitutionStatic AnalysisSQL-injection vulnerabilitiesWasserman & Su/UC, DavisSecurity TestingArdilla for PHP (SQL injections,cross-site scripting)Kiezun & Ernst/MITKleeKudzuNoTamperEngler & Cadar/StanfordSaxena & Song/BerkeleyBisht & Venkatakrishnan/U ChicagoKaluzaSaxena & Song/BerkeleyConcolic TestingNew SolversVijay GaneshWednesday, 16 January, 1378Impact of Hampi: Notable ProjectsTool NameKudzuNoTamperVijay GaneshWednesday, 16 January, 13DescriptionProject Leader/InstitutionJavaScript Bug Finder & Vulnerability DetectorSaxenaAkhaweHannaMaoMcCamantSong/BerkeleyParameter Tamper DetectionBishtHinrichs/U of ChicagoSkrupskyBobrowiczVekatakrishnan/ U.
of Illinois,Chicago79Impact of Hampi: Notable ProjectsNoTamperServer• Client-side checks (C), no server checks• Find solutions S1,S2,... to C, and solutions E1,E2,... to ~C by calling HAMPI• E1,E2,... are candidate exploits• Submit (S1, E1),... to server• If server response same, ignore• If server response differ, report errorVijay GaneshWednesday, 16 January, 1380Related Work (Practice)Tool NameRexProject Leader/InstitutionBjorner, Tillman,Vornkov et al.(Microsoft Research, Redmond)MonaKarlund et al. (U. of Aarhus)DPRLEHooimeijer (U.
of Virginia)Vijay GaneshWednesday, 16 January, 13Comparison with HAMPI• HAMPI+ Length+Replace(s1,s2,s3)- CFG• Translation to int. linear arith. (Z3)• Can encode HAMPI & Rex• User work• Automata-based• Non-elementary• Regular expression constraints81Related Work (Theory)ResultPerson (Year)NotesUndecidability of QuantifiedWord EquationsQuine (1946)Multiplication reduced to concatUndecidability of QuantifiedWord Equations with singlealternationDurnev (1996), G.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
