Source-linked AI summary
SMT-Based Bounded Model Checking for Embedded ANSI-C Software
Lucas Cordeiro, Bernd Fischer, Joao Marques-Silva
TL;DR
The paper addresses limitations of propositional bounded model checking for embedded ANSI-C, including growing formula size and lost high-level structure. It develops richer SMT encodings and integrates multiple solvers with CBMC, finding improved scalability and verification performance across embedded software applications.
Problem
Propositional bounded model checking can produce large formulae, lose high-level information, and inadequately represent important ANSI-C constructs and arithmetic overflow.
Method
The authors develop accurate quantifier-free SMT encodings for ANSI-C constructs and integrate CVC3, Boolector, and Z3 with CBMC, using high-level code optimizations.
Results
Experiments show that the approach analyzes larger embedded-software problems and substantially improves verification performance, including consistent 20-40-factor gains over SMT-CBMC with Z3.
Takeaways & Limitations
SMT-based BMC can accurately verify embedded ANSI-C programs involving bit operations, unions, floating-point arithmetic, pointers, and overflow while scaling better on demanding problems.
Takeaways & Limitations
CBMC remains limited by large propositional encodings, lost high-level information, and encoding growth with array size.
Abstract
from arXiv · showhide
Propositional bounded model checking has been applied successfully to verify embedded software but is limited by the increasing propositional formula size and the loss of structure during the translation. These limitations can be reduced by encoding word-level information in theories richer than propositional logic and using SMT solvers for the generated verification conditions. Here, we investigate the application of different SMT solvers to the verification of embedded software written in ANSI-C. We have extended the encodings from previous SMT-based bounded model checkers to provide more accurate support for finite variables, bit-vector operations, arrays, structures, unions and pointers. We have integrated the CVC3, Boolector, and Z3 solvers with the CBMC front-end and evaluated them using both standard software model checking benchmarks and typical embedded applications from telecommunications, control systems and medical devices. The experiments show that our approach can analyze larger problems and substantially reduce the verification time.
1. Introduction
The paper addresses limitations of propositional BMC for embedded ANSI-C by preserving richer word-level structure through SMT encodings. It extends ANSI-C support and evaluates multiple SMT solvers, reporting improved scalability and verification time.
- Motivation and approach: SMT-based BMC keeps predicates in decidable background theories instead of encoding them as propositional variables.The resulting quantifier-free verification condition is checked directly by an SMT solver.
- Motivation and approach: Previous SMT-based software BMC lacked encodings for several ANSI-C constructs, including bit operations, floating-point arithmetic, pointers, and unions.It also lacked arithmetic-overflow checking and high-level simplification of the unrolled formula.
- Contributions: The work provides an accurate ANSI-C translation into quantifier-free formulae and demonstrates improved software-model-checking performance across embedded systems.The contributions also cover arithmetic overflow and programs using bit-level operations, pointers, unions, and floating-point arithmetic.
- Contributions: ESW-CBMC integrates CVC3, Boolector, and Z3 with CBMC and uses high-level information to simplify and reduce unrolled formula size.The evaluation includes standard benchmarks and embedded applications.
2. Background
The background introduces BMC and SMT foundations, CBMC’s propositional workflow and limitations, and the theory constructs used to represent ANSI-C programs.
- CBMC: CBMC parses ANSI-C/C++, builds typed internal representations, and generates constraints and safety properties guarded by control-flow predicates.Its generated checks include arithmetic overflow and underflow, array bounds, null-pointer dereferences, and assertions.
- CBMC: CBMC’s propositional encoding grows with complex data paths and arrays while losing high-level information during conversion to propositional logic.These limitations motivate retaining richer theories in SMT-based analysis.
- BMC and SMT foundations: SMT generalizes propositional satisfiability by combining decidable theories such as arithmetic, bit-vectors, tuples, arrays, and uninterpreted functions.Quantifier-free formulae are checked for satisfiability in the selected theory combination.
- BMC and SMT foundations: BMC unrolls a transition system to bound k and checks whether the resulting verification condition has a counterexample within that bound.Satisfiability indicates a counterexample; unsatisfiability establishes the property up to k.
- SMT theories: The theory syntax represents Boolean formulae, numerical and bit-vector terms, extraction, extensions, conditional expressions, and overflow-aware arithmetic operators.Signedness and variable domains determine the semantics of relational, arithmetic, and shift operations.
- SMT theories: Arrays use select and store operations governed by axioms stating when a store changes or preserves a selected value.Tuples provide analogous operations for modeling ANSI-C structures and unions.
3. ESW-CBMC
This section presents the software components and encoding techniques forming the SMT-based CBMC back-end for translating embedded ANSI-C verification conditions.
- Back-end architecture: The SMT-based back-end converts constraints and properties from embedded ANSI-C into the background theories supported by SMT solvers.It constitutes the implementation basis for the subsequent ESW-CBMC analysis.
3.1. SMT-based CBMC Back-End
The back-end reuses CBMC’s SSA-producing front-end, selects solver-specific encoders, simplifies constraints and properties, and checks the resulting formula with SMT.
- Back-end architecture: CBMC’s unchanged front-end generates constraints and properties for the unrolled C program in single static assignment form.The back-end adds solver-specific encoding functions selected by the user.
- SSA transformation: The running example converts a valid C program with an out-of-bounds write into SSA containing conditionals, assignments, and assertions.Seven verification conditions check array bounds and the user assertion.
- Formula generation: Definition literals encode the truth of individual clauses, after which the constraints and properties are rewritten into a solver-checkable form.These literals connect clause-level structure to the generated formula.
- Formula simplification: Local and recursive transformations remove functionally redundant expressions and literals before the resulting C∧¬P formula is passed to an SMT solver.This differs from Armando et al.’s implication check and conditional-normal-form transformation.
- Modeling choices: Modeling variables as fixed-width bit-vectors can preserve ANSI-C precision, whereas integer or real models may solve faster but abstract overflow behavior.The choice therefore trades speed against accuracy in formal verification.
3.2. Code Optimizations
ESW-CBMC uses constant folding and forward substitution to optimize embedded ANSI-C verification conditions. The examples apply these techniques to cyclic redundancy check and fast Fourier transform code.
- Constant folding: Constant folding replaces arithmetic operations involving known constants with result constants during verification.For the cyclic redundancy check example, known values of j and the constant array it allow expressions to use only SMT solver store functions.
- Forward substitution: Forward substitution reuses repeated expressions when their operands remain unchanged between evaluations.The fast Fourier transform example applies this optimization to repeated expressions inside nested loops.
- Forward substitution: With an unwinding bound of 1024, the expression x + i is repeated 1024 times in the modeled program.The repetition occurs because nested loops invoke the inner loop n times while the address of array x remains unchanged.
3.3. Encodings
The encodings represent ANSI-C scalar types, arithmetic behavior, arrays, structures, unions, and pointers using SMT theories and tuple operations. They also model overflow and pointer-safety properties needed for embedded-software verification.
- Scalar Data Types: Scalar types can be encoded as SMT integers, reals, or fixed-width bit-vectors, with operators and casts adapted to operand types.Conversions use extraction, sign extension, zero extension, and conditional expressions; floating-point types use fixed-point arithmetic.
- Arithmetic Overflow and Underflow: Unsigned arithmetic overflow is encoded modulo 2^w, while signed overflow and underflow are checked for addition, subtraction, multiplication, division, and negation.Signed overflow behavior is not defined by ANSI-C, so the encoding explicitly adds constraints for these operations.
- Arrays: Arrays use SMT store and select operations, with out-of-bounds index results treated as nondeterministically chosen free variables.The WITH operator maps to store, and indexing maps to select.
- Structures and Unions: Structures and unions are encoded as SMT tuples whose fields are updated and accessed through store and select operations.Structures containing arrays, pointers, and scalar data are manipulated through the same update and access operations.
- Pointers: Pointers are tuples containing an object field and an index field, enabling checks for same-object access, NULL pointers, and invalid objects.CBMC generates pointer-safety properties for object validity and non-NULL, non-invalid dereferencing; pointer indices represent array positions.
4. Experimental Evaluation
The evaluation compares SMT solvers on ANSI-C benchmarks, then compares ESW-CBMC with SMT-CBMC and CBMC on embedded software. Results identify Z3 for continued development and show ESW-CBMC advantages on several benchmark classes.
- 4.1. Comparison of SMT solvers: The evaluation used fifteen ANSI-C programs and three SMT solvers to identify the most promising solver for further development.The solvers were CVC3, Boolector, and Z3.
- 4.1. Comparison of SMT solvers: Z3 ran slightly faster than Boolector and CVC3 except on StrCmp and SumArray, and was selected because it supported most occurring operations.The stated purpose was to prioritize solver integration rather than define the best SMT solver.
- 4.2. Comparison to SMT-CBMC: ESW-CBMC with Z3 consistently outperformed SMT-CBMC by a factor of 20-40.With CVC3, both tools encountered memory failures or analysis failures on several larger programs.
- 4.3. Comparison to CBMC: CBMC could not check fft1k and lms because of memory limitations, while ESW-CBMC was considerably faster on ludcmp, qurt, and laplace.ESW-CBMC was also faster on adpcm, exStbHDMI, and exStbLED; CBMC was faster only on exStbResolution.
- 4.3. Comparison to CBMC: For the remaining benchmarks, ESW-CBMC and CBMC had very close verification times.ESW-CBMC’s encoding time was slightly faster for all analyzed programs.
- 4.3. Comparison to CBMC: ESW-CBMC scaled significantly better than CBMC for problems combining non-linear arithmetic, bit operations, pointers, and array manipulations.Both tools found previously undiscovered bugs involving arithmetic overflow, invalid pointers, and pointer arithmetic.
5. Related Work
Related work applies SMT-based verification and static checking to software and systems, but often restricts supported ANSI-C constructs or trades precision for scalability. The paper distinguishes its broader encoding scope from these approaches.
- SMT-based BMC: Earlier SMT-based BMC work combined theories such as uninterpreted functions, arrays, and linear arithmetic but omitted key ANSI-C constructs.The omitted constructs included bit operations, floating-point arithmetic, and pointers.
- SMT-CBMC: SMT-CBMC supported linear arithmetic, arrays, records, and bit-vectors but did not address non-linear arithmetic or bit-shift operations.These omissions limited its treatment of important ANSI-C programming-language constructs.
- Other SMT-based approaches: Other work used SMT solvers for timed automata, RTL descriptions, and Spark verification conditions.These approaches targeted different verification settings or replaced an existing prover with SMT solvers and a theorem prover.
- Static checkers: Calysto supports arithmetic overflow, null-pointer dereferences, and assertions but does not support floating-point operations and unsoundly unrolls loops once.Its verification conditions are passed to the customized SMT solver SPEAR.
- Static checkers: Saturn scales to larger systems but loses precision by supporting only common integer operators and performing at most two loop unwindings.The related static checkers explicitly trade off scalability and precision.
6. Conclusions
The paper presents accurate ANSI-C encodings and high-level simplification for SMT-based BMC of embedded software. Experiments report better performance than CBMC and SMT-CBMC, while CBMC remains limited by propositional encoding growth and lost high-level information.
- Conclusions: The encodings accurately represent bit operations, unions, floating-point arithmetic, pointers, and pointer arithmetic.The work also improves SMT-based BMC performance using high-level information to simplify the unrolled formula.
- Conclusions: The experiments provide a substantial evaluation over industrial applications and report that the approach outperforms CBMC and SMT-CBMC for embedded-software verification.The conclusion attributes SMT-CBMC’s limitations to verification time and incomplete encodings of important ANSI-C constructs.
- Conclusions: CBMC’s propositional formula size increases with large data-paths, while conversion to propositional logic loses high-level information that could reduce the explored state space.The paper identifies these as limitations of CBMC’s approach.
- Conclusions: Future work includes termination analysis and reduction methods to simplify the kmodel.These directions are stated as planned extensions.