The new Dataflow analysis module contains an advanced industry-proven Satisfiability Modulo Theories solver engine, a technology first for deep-flow static analysis products. A combination of SMT solver technology and in-house language and parsing expertise in function control flow and detailed semantics has created a set of unique analysis checks for C and C++ code.
“The embedded software industry is dominated by use of C and C++ languages,” said Fergus Bolger, Chief Technical Officer at PRQA. “A limitation of many current static analysis tools, particularly for embedded industries, is a focus on software interface layers rather than detailed code semantics. Just as important to embedded developers is the challenge of dataflow analysis focused on a precise and detailed function level, literally on the bits and bytes of many industries’ critical software-based systems.”
Utilizing the strength of a commercially-hardened SMT solver, the Dataflow module delivers a number of sophisticated code-modelling capabilities:
• Inter-dependency between variables are included in the code modelling, both for assignments and in determination of conditional expressions (control flow).
• Modelling includes a bi-directional approach, where for example later conditional tests can identify earlier suspicious variable usage.
• Loop iterations are modelled accurately, including increments by other than ‘1’, multiple loop control variables, and nested loops.
• Bit-fields are modelled exactly as the compiler will handle them, matching the true size of all types, and yielding intelligence on unions and bit-field operations.
The real strength of the PRQA solution is the set of analysis checks available. These cover all the well known language vulnerabilities of C/C++, as well as additional value-sensitive operations that are particularly relevant to embedded applications:
• Invalid Pointer Operations: dereference and arithmetic operations on a null pointer, computing or dereferencing an invalid pointer value, e.g. buffer under- and overrun, pointer operations on unrelated pointers.
• Dangerous Arithmetic Operations: division by zero, arithmetic operations resulting in overflow or wraparound, converting a negative value to unsigned and other representation issues in conversions, bit-shifting operations that result in truncation or invalid values.
• Flow control anomalies: redundant initialisations or assignments, invariant logical operations and flow-control expressions, unreachable code, infinite loops, unset variables, return value mismatches.
The PRQA Dataflow solution includes analysis of standard library API calls, which coupled with pointer checking, delivers a comprehensive language-based detection of security vulnerabilities. Upon detecting a coding defect, path and value trace is provided by means of sub-messages.
Software engineers and their organisations need to address quality of code, in terms of prevention-oriented coding standards compliance as well as accurate and precise bug-detection. PRQA’s new Dataflow module, addresses this important need.