What you’ll learn:
- A look at the TrustInSoft Analyzer and how it functions.
- How the platform detects potential problems within a coding environment.
The TrustInSoft Analyzer is a specialized software analysis tool designed to verify and ensure the security and reliability of C and C++ source code. According to the company, the analyzer doesn’t have false negatives and has zero-to-few false positives, meaning that every bug in the code is found.
The platform functions by implementing a set of various formal methods that create mathematical proofs of the absence of undefined behavior in the analyzed code. Undefined behaviors are recognized as a significant source of software vulnerabilities. They include memory-management issues (e.g., buffer overflow and uninitialized variables), arithmetic operations (e.g., division by zero and integer overflow), and race conditions.
TrustInSoft built a full suite of C & C++ software analysis tools and services based on the Frama-C source-code analyzer developed by CEA and Inria. It’s been used in many industries to root out bugs in embedded systems, video games, telecoms, automobiles, and consumer electronics. The analyzer applies various formal methods, including abstract interpretation and deductive verification via the computation of weakest preconditions.
Its use of multiple formal methods results in an exhaustive analysis of the source code for undefined behavior. The analyzer follows a multi-step analysis, first using existing test suites, then an extensive analysis of the source code for all inputs, and finally, a complete mathematical guarantee of the software’s compliance with a formal specification written in ACSL.
The abstract interpretation technique employed by the TrustInSoft Analyzer calculates a broader set of potential values for each program variable at every juncture, considering the range of possible inputs. This method triggers an alert whenever there’s a possibility of undefined behavior, leading to a comprehensive identification of such issues in the program being analyzed. These alerts manifest as formulas expressed in ASCL format.
The abstract interpretation incorporates unique approaches, including a dedicated analysis for pinpointing strict-aliasing violations. To maintain precision code analysis with conditional branches, the platform introduces an innovative path-sensitive overview. However, users have options for guiding that analysis when the precision outcome isn’t available.
The TruthInSoft Analyzer can be integrated into the software development process, enabling developers to perform continuous analysis and verification as they write code. The tool also generates detailed reports highlighting identified vulnerabilities and explaining why they’re problematic. The reports help developers understand those issues and provide guidance on how to fix them.
Moreover, the platform continually updates and improves its analytical capability to keep pace with evolving software development practices and emerging security threats.