Slide 1Bug Catching with SAT-SolversPrograms and ClaimsWhy use a SAT Solver?A (very) simple example (1)A (very) simple example (2)What about loops?!CBMC: C Bounded Model CheckerCBMC: Supported Language FeaturesSlide 10Using CBMC from Command LineHow does it workCBMC: Bounded Model Checker for C A tool by D. Kroening/OxfordControl Flow SimplificationsLoop UnwindingLoop UnwindingLoop UnwindingLoop UnwindingUnwinding assertionUnwinding assertionExample: Sufficient Loop UnwindingExample: Insufficient Loop UnwindingTransforming Loop-Free Programs Into Equations (1)Transforming Loop-Free Programs Into Equations (2)What about conditionals?What about conditionals?Adding Unbounded ArraysExamplePointersPointer Typecast ExampleDynamic ObjectsSlide 32From Programming to ModelingExampleUsing nondet for modelingAssume-Guarantee Reasoning (1)Assume-Guarantee Reasoning (2)Dangers of unrestricted assumptionsExample: Prophecy variablesSlide 40Context-Bounded Analysis (CBA)CBA via SequentializationKey IdeaSequentialization in PicturesCBA Sequentialization in a NutshelCBA Sequentialization 1/2CBA Sequentialization: Task Body 2/2Slide 48© 2011 Carnegie Mellon UniversityIntroduction to CBMCSoftware Engineering InstituteCarnegie Mellon UniversityPittsburgh, PA 15213Arie GurfinkelDecember 5, 2011based on slides byDaniel Kroening2Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityBug Catching with SAT-SolversMain Idea: Given a program and a claim use a SAT-solver to find whether there exists an execution that violates the claim. ProgramClaimAnalysisEngineSATSolverUNSAT(no counterexample found)SAT(counterexample exists)CNF3Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityPrograms and Claims•Arbitrary ANSI-C programs•With bitvector arithmetic, dynamic memory, pointers, …•Simple Safety Claims •Array bound checks (i.e., buffer overflow)•Division by zero•Pointer checks (i.e., NULL pointer dereference)•Arithmetic overflow•User supplied assertions (i.e., assert (i > j) )•etc4Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityWhy use a SAT Solver?•SAT Solvers are very efficient•Analysis is completely automated•Analysis as good as the underlying SAT solver•Allows support for many features of a programming language•bitwise operations, pointer arithmetic, dynamic memory, type casts5Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityA (very) simple example (1)int x;int y=8,z=0,w=0;if (x) z = y – 1;else w = y + 1;assert (z == 7 || w == 9)int x;int y=8,z=0,w=0;if (x) z = y – 1;else w = y + 1;assert (z == 7 || w == 9)y = 8,z = x ? y – 1 : 0,w = x ? 0 :y + 1,z != 7,w != 9y = 8,z = x ? y – 1 : 0,w = x ? 0 :y + 1,z != 7,w != 9Program ConstraintsUNSATno counterexampleassertion always holds!6Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityA (very) simple example (2)int x;int y=8,z=0,w=0;if (x) z = y – 1;else w = y + 1;assert (z == 5 || w == 9)int x;int y=8,z=0,w=0;if (x) z = y – 1;else w = y + 1;assert (z == 5 || w == 9)y = 8,z = x ? y – 1 : 0,w = x ? 0 :y + 1,z != 5,w != 9y = 8,z = x ? y – 1 : 0,w = x ? 0 :y + 1,z != 5,w != 9Program ConstraintsSATcounterexample found!y = 8, x = 1, w = 0, z = 77Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityWhat about loops?!•SAT Solver can only explore finite length executions!•Loops must be bounded (i.e., the analysis is incomplete)ProgramClaimAnalysisEngineSATSolverUNSAT(no counterexample ofbound n is found)SAT(counterexample exists)CNFBound (n)8Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityCBMC: C Bounded Model Checker•Developed at CMU by Daniel Kroening et al.•Available at: http://www.cprover.org/cbmc•On Ubuntu: apt-get install cbmc •Supported platafoms: Windows (requires VisualStudio’s CL), Linux•Provides a command line (and Eclipse-based) interfaces•Known to scale to programs with over 30K LOC•Was used to find previously unknown bugs in MS Windows device drivers9Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityCBMC: Supported Language FeaturesANSI-C is a low level language, not meant for verification but for efficiencyComplex language features, such as•Bit vector operators (shifting, and, or,…)•Pointers, pointer arithmetic•Dynamic memory allocation: malloc/free•Dynamic data types: char s[n]•Side effects•float / double•Non-determinism© 2011 Carnegie Mellon UniversityDEMO11Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityUsing CBMC from Command Line•To see the list of claimscbmc --show-claims -I include file.c•To check a single claimcbmc --unwind n --claim x –I include file.c•For help•cbmc --help12Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityHow does it workTransform a programs into a set of equations1. Simplify control flow 2. Unwind all of the loops3. Convert into Single Static Assignment (SSA)4. Convert into equations5. Bit-blast6. Solve with a SAT Solver7. Convert SAT assignment into a counterexample13Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityCBMC: Bounded Model Checker for CA tool by D. Kroening/OxfordParserParserStatic AnalysisStatic AnalysisCNF-genCNF-genSAT solverSAT solverCEX-genCEX-genCBMCC ProgramSAFEUNSAFE + CEXSATUNSAT CNFgoto-programequations14Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityControl Flow SimplificationsAll side effect are removed•e.g., j=i++ becomes j=i;i=i+1•Control Flow is made explicit•continue, break replaced by goto•All loops are simplified into one form•for, do while replaced by while15Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityLoop Unwinding•All loops are unwound•can use different unwinding bounds for different loops•to check whether unwinding is sufficient special “unwinding assertion” claims are added•If a program satisfies all of its claims and all unwinding assertions then it is correct!•Same for backward goto jumps and recursive functions16Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityLoop Unwinding while() loops are unwound iterativelyBreak / continue replaced by gotovoid f(...) { ... while(cond) { Body; } Remainder;}void f(...) { ... while(cond) { Body; } Remainder;}17Introduction to CBMCArie Gurfinkel© 2011 Carnegie Mellon UniversityLoop Unwindingwhile() loops are unwound iterativelyBreak / continue