7 Counterexample-guided abstraction refinement(CEGAR). CEGAR-based SMT solver (Презентации лекций), страница 2

/ Trento / 2005 - presentGanesh / Stanford & MIT / 2005 - presentSeshia / CMU & Berkeley / 2004 - presentCombinationsVijay GaneshWednesday, 16 January, 1318Talk OutlineTopics covered in Lecture 1Motivation for SAT/SMT solvers in software engineering• Software engineering (SE) problems reduced to logic problems• Automation, engineering, usability of SE tools through solversHigh-level description of the SAT/SMT problem & logics• Rich logics close to program semantics• Demonstrably easy to solve in many practical casesModern SAT solver architecture & techniques• DPLL search, shortcomings• Modern CDCL SAT solver: propagate (BCP), decide (VSIDS), conflict analysis, clause learn, backJump,• Termination, correctness• Big lesson: learning from mistakesTopics covered in Lecture 2Modern SMT solver architecture & techniques• Rich logics closer to program semantics• DPLL(T), Combinations of solvers, Over/under approximations• My own contributions: STP & HAMPI• STP: Abstraction-refinement for solving• Applications to dynamic symbolic testing (aka concolic testing)• HAMPI: Bounded logics• SAT/SMT-based applications• Future of SAT/SMT solversVijay GaneshWednesday, 16 January, 1319STP Bit-vector & Array SolverProgramExpressionsSATSTP Solver(x = z+2 ORmem[i] + y <= 01)UNSAT• Bit-vector or machine arithmetic• Arrays for memory• C/C++/Java expressions• NP-completeVijay GaneshWednesday, 16 January, 1320The History of STP• Solver-based languages (Alloy team)1,000,000 Constraints• Solver-based debuggers• Solver-based type systems• Solver-based concurrency bugfinding• HAMPI: String Solvers• Ardilla by Ernst et al.• Kudzu & Kaluza by Song et al.• Klee by Engler et al.• George Candea’s Cloud 9 tester• STP + HAMPI exceed 100+ projects• STP• Enabled Concolic Testing• EXE by Engler et al• BAP/BitBlaze by Song et al.• Model checking by Dill et al.100,000 Constraints2005Vijay GaneshWednesday, 16 January, 132009Today21Programs Reasoning & STPWhy Bit-vectors and Arrays• STP logic tailored for software reliability applications• Support symbolic execution/program analysisC/C++/Java/...Bit-vectors and ArraysInt VarChar Var32 bit variable8 bit variableArithmetic operation(x+y, x-y, x*y, x/y,...)Arithmetic function(x+y,x-y,x*y,x/y,...)assignmentsx = expr;equalityx = expr;if conditionalif(cond) x = expr1 else x = expr2if-then-else constructx = if(cond) expr1 else expr2inequalityinequality predicateMemory read/writex = *ptr + i;Array read/writeptr[]; x = Read(ptr,i);Structure/ClassSerialized bit-vector expressionsFunctionSymbolic executionLoopsBoundingVijay GaneshWednesday, 16 January, 1322How to Automatically Crash Programs?Concolic Execution & STPProblem: Automatically generate crashing tests given only the codeProgramSymbolic ExecutionEnginewithImplicit SpecAutomatic TesterFormulasSTPSAT/UNSATCrashing TestsVijay GaneshWednesday, 16 January, 1323How to Automate Testing?Concolic Execution & STPStructured 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 GaneshWednesday, 16 January, 1324How to Automate Testing?Concolic Execution & STPStructured 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 GaneshWednesday, 16 January, 1324How to Automate Testing?Concolic Execution & STPStructured 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 GaneshWednesday, 16 January, 1324How to Automate Testing?Concolic Execution & STPStructured 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 GaneshWednesday, 16 January, 1324How STP WorksBird’s Eye View: Translate to SATSTPBit-vector&Array Formula(x = z+2 ORmem[i] + y <= 01)...TranslateToSATBooleanSAT SolverSATUNSATWhy Translate to SAT?• Both theories NP-complete• Non SAT approaches didn’t work• Translation to SAT leverages solid engineeringVijay GaneshWednesday, 16 January, 1325How STP WorksRich Theories cause MEM Blow-upSTPBit-vector&Array Formula(x = z+2 ORmem[i] + y <= 01)...TranslateFormulaToGrowthSATBooleanSAT SolverSATUNSAT• Making information explicit• Space cost• Time costVijay GaneshWednesday, 16 January, 1326Explicit Information causes Blow-upArray Memory Read ProblemLogic 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]);..if(ptr+i = ptr+j) then mem_ptr[ptr+i] = mem_ptr[ptr+j);//INTEGER OVERFLOW QUERY0 <= j <= process(len_field);ptr + i + j < ptr?• Array Aliasing is implicit• Need to make information explicit during solving• Cannot be avoidedVijay GaneshWednesday, 16 January, 1327How STP WorksArray-read MEM Blow-up Problem• Problem: O(n2) axioms added, n is number of read indices• Lethal, if n is large, say, n = 100,000; # of axioms is 10 BillionFormula Growthv0 = expr0v1 = expr1Read(Mem,i0) = expr0Read(Mem,i1) = expr1Read(Mem,i2) = expr2...Read(Mem,in) = exprn...vn = exprn(i0 = i1) => (v0 = v1)(i0 = i2) => (v0 = v2)...(i1 = i2) => (v1 = v2)...Vijay GaneshWednesday, 16 January, 1328How STP WorksThe Array-read Solution• Key Observation• Most indices don’t alias in practice• Exploit locality of memory access in typical programs• Need only a fraction of array axioms for equivalenceRead(Mem,i0) = expr0Read(Mem,i1) = expr1Read(Mem,i2) = expr2...Read(Mem,in) = exprnVijay GaneshWednesday, 16 January, 13v0 = expr0v1 = expr1...vn = exprn(i0 = i1) => (v0 = v1)29STP Key Conceptual ContributionAbstraction-refinement PrincipleInput FormulaAbstraction StepAbstractedFormulaRefinementBoolean SAT SolverCheck AnswerVijay GaneshWednesday, 16 January, 13CorrectAnswer30How STP WorksWhat to Abstract & How to Refine?AbstractionRefinement1.

Less essential parts2. Causes MEM blow-up1. Guided2. Must rememberAbstraction managesformula growth hardnessRefinement managessearch-space hardnessVijay GaneshWednesday, 16 January, 1331How STP WorksAbstraction-refinement for Array-readsInputRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000(i0,i1)SubstitutionsSimplificationsLinear SolvingArray AbstractionRefinement LoopConversion to SATBoolean SAT SolverResultVijay GaneshWednesday, 16 January, 1332How STP WorksAbstraction-refinement for Array-readsSubstitutionsRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000’(i0,i1)SimplificationsLinear SolvingArray Abstractioni0 = i1Refinement LoopConversion to SATBoolean SAT SolverResultVijay GaneshWednesday, 16 January, 1333How STP WorksAbstraction-refinement for Array-readsAbstracted InputArray Axioms DroppedInputRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000(i0,i1)v0=0v1=1…vn=10,000’ (i0,i1)Refinement LoopSubstitutionsSimplificationsLinear SolvingArray AbstractionConversion to SATBoolean SAT SolverResultVijay GaneshWednesday, 16 January, 1334How STP WorksAbstraction-refinement for Array-readsAbstracted InputArray Axioms DroppedInputRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000(i0,i1)v0=0v1=1…vn=10,000’ (i0,i1)Vijay GaneshWednesday, 16 January, 13SimplificationsLinear SolvingArray AbstractionRefinement LoopInputFormula falseinAssignmentSubstitutionsi0=0,i1=0v0=0, v1=1…Conversion to SATBoolean SAT SolverResult35How STP WorksAbstraction-refinement for Array-readsAbstracted InputArray Axioms DroppedInputRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000(i0,i1)v0=0v1=1…vn=10,000’ (i0,i1)Refinement LoopVijay GaneshWednesday, 16 January, 13SimplificationsLinear SolvingArray Abstraction(i0=i1)!v0=v1Add Axiom thatis FalsifiedSubstitutionsi0=0,i1=0v0=0, v1=1…Conversion to SATBoolean SAT SolverResult36How STP WorksAbstraction-refinement for Array-readsInputRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000(i0,i1)SubstitutionsSimplificationsLinear SolvingArray AbstractionRefinement LoopConversion to SATBoolean SAT SolverUNSATVijay GaneshWednesday, 16 January, 1337STP vs.

Other SolversTestcase (Formula Size)Result610dd9c(~15K)SATGrep65(~60K)Grep84Z3(sec)Yices(sec)STP(sec)TimeOut MemOut37UNSAT0.3 TimeOut4(~69K)SAT176 TimeOut18Grep106(~69K)SAT130 TimeOut227Blaster4(~262K)UNSATMemOut MemOut10Testcase20 (~1.2M)SATMemOut MemOut56Testcase21 (~1.2M)SATMemOut MemOut43* All experiments on 3.2 GHz, 512 Kb cache* MemOut: 3.2 GB (Memory used by STP much smaller), TimeOut: 1800 seconds* Examples obtained from Dawn Song at Berkeley, David Molnar at Berkeley and Dawson Engler at Stanford* Experiments conducted in 2007Vijay GaneshWednesday, 16 January, 1338STP vs.

Other Leading SolversSTP vs. Boolector & MathSAT on 615 SMTCOMP 2007 - 2010 examplesTime in Seconds40003000200010000BoolectorMSATSTP* All experiments on 2.4 GHz, 1 GB RAM* Timeout: 500 seconds/exampleVijay GaneshWednesday, 16 January, 1339Impact of STP• Enabled existing SE technologies to scale• Bounded model checkers, e.g., Chang and Dill• Easier to engineer SE technologies• Formal tools (ACL2+STP) for verifying Crypto, Smith & Dill• Enabled new SE technologies• Concolic testing (EXE,Klee,...) by Engler et al., Binary Analysis by Song et al.Vijay GaneshWednesday, 16 January, 1340Impact of STP: Notable Projects• Enabled Concolic Testing• 100+ reliability and security projectsCategoryResearch ProjectProject Leader/InstitutionFormal MethodsACL2 Theorem Prover + STPVerification-aware Design CheckerJava PathFinder Model CheckerEric Smith & David Dill/StanfordJacob Chang & David Dill/StanfordMehlitz & Pasareanu/NASAProgram AnalysisBitBlaze & WebBlazeBAPDawn Song et al./BerkeleyDavid Brumley/CMUAutomatic TestingSecurityKlee, EXESmartFuzzKudzuEngler & Cadar/StanfordMolnar & Wagner/BerkeleySaxena & Song/BerkeleyHardware BoundedBlue-spec BMCModel-cheking (BMC) BMCVijay GaneshWednesday, 16 January, 13Katelman & Dave/MITHaimed/NVIDIA41Impact of STPhttp://www.metafuzz.comProgram NameLines of Number ofTeamCodeBugs FoundMplayer~900,000 HundredsDavid Molnar/Berkeley & MicrosoftResearchEvince~90,000HundredsDavid Molnar/Berkeley & MicrosoftResearchUnix Utilities1000sDozensDawson Engler et al./StanfordCrypto HashImplementations1000sVerifiedEric Smith & David Dill/StanfordVijay GaneshWednesday, 16 January, 1342Rest of the Talk• STP Bit-vector and Array Solver• Why Bit-vectors and Arrays?• How does STP scale: Abstraction-refinement• Impact: Concolic testing• Experimental Results• HAMPI String Solver• Why Strings?• How does HAMPI scale: Bounding• Impact: String-based program analysis• Experimental Results• Future Work• Multicore SAT• SAT-based LanguagesVijay GaneshWednesday, 16 January, 1343HAMPI String SolverStringExpressionsSATHAMPI Solver• X = concat(“SELECT...”,v) AND (X• JavaScript and PHP Expressions• Web applications, SQL queries• NP-completeVijay GaneshWednesday, 16 January, 13UNSAT∈ SQL_grammar)44Theory of StringsThe Hampi LanguagePHP/JavaScript/C++...HAMPI: Theory of StringsNotesVar a;$a = ‘name’Var a : 1...20;a = ‘name’Bounded String VariablesString Constantsstring_expr.” is ”concat(string_expr, “ is “);Concat Functionsubstr(string_expr,1,3)string_expr[1:3]Extract Functionassignments/strcmpa = string_expr;a /= string_expr;equalitya = string_expr;a /= string_expr;Equality PredicateSanity check in regular expression RESanity check in context-free grammar CFGstring_expr in REstring_expr in SQLstring_expr NOT in SQLMembership Predicatestring_expr contains a sub_strstring_expr does not contain a sub_strstring_expr contains sub_strstring_expr NOT?contains sub_strContains Predicate(Substring Predicate)Vijay GaneshWednesday, 16 January, 1345Theory of StringsThe Hampi Language•X = concat(“SELECT msg FROM msgs WHERE topicid = ”,v)AND(X ∈ SQL_Grammar)•input ∈ RegExp([0-9]+)•X = concat (str_term1, str_term2, “c”)[1:42]ANDX contains “abc”Vijay GaneshWednesday, 16 January, 1346HAMPI Solver Motivating ExampleSQL Injection VulnerabilitiesBuggyScriptMalicious SQL QueryUnauthorizedDatabase ResultsBackendDataBaseSELECT m FROM messages WHERE id=’1’ OR 1 = 1Vijay GaneshWednesday, 16 January, 1347HAMPI Solver Motivating ExampleSQL Injection VulnerabilitiesSource: IBM Internet Security Systems, 2009Source: Fatbardh Veseli, Gjovik University College, NorwayVijay GaneshWednesday, 16 January, 1348HAMPI Solver Motivating ExampleSQL Injection VulnerabilitiesBuggy Scriptif (input in regexp(“[0-9]+”))query := “SELECT m FROM messages WHERE id=‘ ” + input + “ ’ “)• input passes validation (regular expression check)• query is syntactically-valid SQL• query can potentially contain an attack substring(e.g., 1’ OR ‘1’ = ‘1)Vijay GaneshWednesday, 16 January, 1349HAMPI Solver Motivating ExampleSQL Injection VulnerabilitiesShould be: “^[0-9]+$”Buggy Scriptif (input in regexp(“[0-9]+”))query := “SELECT m FROM messages WHERE id=‘ ” + input + “ ’ “)• input passes validation (regular expression check)• query is syntactically-valid SQL• query can potentially contain an attack substring(e.g., 1’ OR ‘1’ = ‘1)Vijay GaneshWednesday, 16 January, 1349HAMPI Solver Motivating ExampleSQL Injection Vulnerabilitiesif (input in regexp(“[0-9]+”))query := “SELECT m FROM messages WHERE id=‘ ” + input + “ ’ “)SpecificationString FormulasProgram Reasoning ToolHAMPISAT/UNSATGenerate Tests/Report VulnerabilityVijay GaneshWednesday, 16 January, 1350Rest 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, 1351Expressing the Problem in HAMPISQL 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”52Hampi Key Conceptual IdeaBounding, expressiveness and efficiencyLiComplexity of∅ = L1 ∩ ...