7 Counterexample-guided abstraction refinement(CEGAR). CEGAR-based SMT solver (Презентации лекций), страница 4
Описание файла
Файл "7 Counterexample-guided abstraction refinement(CEGAR). CEGAR-based SMT solver" внутри архива находится в папке "Презентации лекций". PDF-файл из архива "Презентации лекций", который расположен в категории "". Всё это находится в предмете "boolean sat-smt solvers for software engineering" из 11 семестр (3 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 4 страницы из PDF
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. (2011)2-counter machines reduced towords with single quantifier alter.Decidability (PSPACE) of QFTheory of Word EquationsMakanin (1977)Makanin result very difficultPlandowski (1996, 2002/06) Simplified by PlandowskiDecidability (PSPACEcomplete) of QF Theory ofWord Equations + RESchultz (1992)RE membership predicateQF word equations + Length()Matiyasevich (1971)(?)UnsolvedReduction to DiophantineQF word equations in solvedform + Length() + REPracticalVijay GaneshWednesday, 16 January, 13G.
(2011)82Future of HAMPI & STP• HAMPI will be combined with STP• Bit-vectors and Arrays• Integer/Real Linear Arithmetic• Uninterpreted Functions• Strings• Floating Point• Non-linear• Additional features planned in STP• UNSAT Core• Quantifiers• Incremental• DPLL(T)• Parallel STP• MAXSMT?• Extensibility and hackability by non-expertVijay GaneshWednesday, 16 January, 1383Future of Strings• Strings SMTization effort started• Nikolaj Bjorner, G.• Andrei Voronkov, Ruzica Piskac, Ting Zhang• Cesare Tinelli, Clark Barrett, Dawn Song, Prateek Saxena, Pieter Hooimeijer, Tim Hinrichs• SMT Theory of Strings• Alphabet (UTF, Unicode,...)• String Constants and String Vars (parameterized by length)• Concat, Extract, Replace, Length Functions• Regular Expressions, CFGs (Extended BNF)• Equality, Membership Predicate, Contains Predicate• Applications• Static/Dynamic Analysis for Vulnerability Detection• Security Testing using Concolic Idea• Formal Methods• SynthesisVijay GaneshWednesday, 16 January, 1384Conclusions & Take Away• SMT solvers essential for testing, analysis, verification,...• Core SMT ideas• Combinations• DPLL(T)• Over/Under approximations (CEGAR,...)• SAT solvers• Future of SMT solvers• SMT + Languages• SMT + Synthesis• Parallel SAT/SMT• Demand for even richer theories• Attribute grammars• String theories with lengthVijay GaneshWednesday, 16 January, 1385Modern SMT Solver ReferencesThese websites and handbook have all the references you will need1.
Armin Bierre, Marijn Heule, Hans van Maaren, and Toby Walsh (Editors). Handbook of Satisfiability. 2009. IOS Press. http://www.st.ewi.tudelft.nl/sat/handbook/2. SAT Live: http://www.satlive.org/3. SMT LIB: http://www.smtlib.org/4. SAT/SMT summer school: http://people.csail.mit.edu/vganesh/summerschool/Vijay GaneshWednesday, 16 January, 1386Topics CoveredTopics 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 approximationsMy own contributions: STP & HAMPI• Abstraction-refinement for solving• Bounded logicsSAT/SMT-based applications• Dynamic systematic testing• Static, dynamic analysis for vulnerability detectionFuture of SAT/SMT solversVijay GaneshWednesday, 16 January, 1387Key Contributionshttp://people.csail.mit.edu/vganeshNameKey ConceptImpactPubsSTPBit-vector & Array Solver1,2Abstraction-refinementfor SolvingConcolicTestingCAV 2007CCS 2006TISSEC 2008HAMPIString Solver1App-driven Bounding for Analysis ofSolvingWeb AppsISSTA 20093TOSEM 2011(CAV 2011)Taint-based FuzzingInformation flow ischeaper than concolicScales betterthan concolicICSE 2009Acceptability Envelope:Fix the input, not theprogramNew way ofUnderapproaching SE SubmissionAutomatic InputRectification1.
100+ research projects use STP and HAMPI2. STP won the SMTCOMP 2006 and 2010 competitions for bit-vector solvers3. HAMPI: ACM Best Paper Award 20094. Retargetable Compiler (DATE 1999)5. Proof-producing decision procedures (TACAS 2003)6. Error-finding in ARBAC policies (CCS 2011)Vijay Ganesh, Dagstuhl, Aug 8-12, 2011Wednesday, 16 January, 1388.
