CWE-compatible static analysis tool detects buffer overflow

Article By : AdaCore

CodePeer is an Ada source code analyser that detects run-time and logic errors.

AdaCore has announced that its CodePeer advanced static analysis tool for Ada has been formally designated as “CWE-Compatible” by the MITRE Corporation’s Common Weakness Enumeration (CWE) Compatibility and Effectiveness Program, a web-based initiative that consolidates and organises information about cyber-security products and services.

CodePeer is an Ada source code analyser that detects run-time and logic errors. It assesses potential bugs before program execution, serving as an automated peer reviewer, helping to find errors efficiently and early in the development life-cycle. It can also be used to perform impact analysis when introducing changes to the existing code, as well as helping vulnerability analysis for legacy systems. Using control-flow, data-flow and other advanced static analysis techniques, CodePeer detects errors that would otherwise only be found through labour-intensive debugging.

The tool’s deep analysis can directly support formal certification against industry-specific safety standards. For avionics applications CodePeer has been qualified as a Software Verification Tool under DO-178B, automating a number of verification activities defined in paragraph 6.3.4f. These activities include detecting errors such as values outside the bounds of an Ada type or subtype, buffer overflows, integer overflow or wraparound, division by zero, use of uninitialised variables and floating point underflow.

CodePeer has also been qualified for EN 50128, the highest international standard for safety integrity concerning software for railway control and protection, including communications, signalling and processing systems, according to AdaCore.

The EN 50128 qualification material addresses the following:

• Boundary value analysis to detect attempts to dereference a pointer that could be null, values outside the bounds of an Ada type or subtype, buffer overflows, integer overflow or wraparound, and division by zero.
• Control flow analysis to detect suspicious and potentially incorrect control flows, such as unreachable code, redundant conditionals, loops that either run forever or fail to terminate normally, and subprograms that never return.
• Data flow analysis to detect suspicious and potentially incorrect data flows, such as variables that are read before they are written (uninitialised variables), variables written more than once without being read (redundant assignments), variables that are written but never read, and parameters with an incorrect mode (unread “in” parameter, unassigned “out” parameter).

Qualification materials for DO-178B and EN 50128 are available as an option with CodePeer.

CodePeer is fully integrated into Adacore’s GNAT Pro development environment and comes with a number of complementary static analysis tools common to the technology—a coding standard verification tool (GNATcheck), a source code metric generator (GNATmetric) and a document generator.