5 Motivation for SMT solvers, and combination of decision procedures (1185841), страница 3
Текст из файла (страница 3)
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 ∩ ...
∩ 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.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
