Introduction

The aim of this document is to help the user to study a C or C++ application with TrustInSoft Analyzer.

The main goal of this kind of study is to verify that none of the detected software weaknesses listed in the CWE-subset are present in the application. This document explains step by step how to achieve that goal.

The definitions of some of the words and expressions used in this document are given in the Glossary.

Analysis Overview

The main steps of an analysis are:

  • First, to prepare the source code in order to make it understandable by the tool. This mainly consists of finding out which options are used to compile it (see Prepare the Sources). At the end of this step, the tool should be able to run the analysis without errors (see Check Preparation).
  • Then, to define the perimeter to study (see Prepare the Analysis). This is a user choice depending on the part of the application that has to be verified. The goal of this step is to build the context in which the application will be analyzed.
  • To run value analysis in order to detect alarms related to the software weaknesses listed in the CWE-subset. Value analysis can be tuned to increase the precision, either globally or locally, which helps in reducing the number of alarms (see Study the Alarms).
  • Each remaining alarm must be examined to find out whether it is relevant or not (i.e. if it can actually happen or not). Some annotations can be added to help the analyzer in removing it if it appears to be a false alarm (see ACSL Properties).
  • Finally, it is important to check all the annotations as they are used as hypotheses at the previous step. Some of them can be formally proven using the WP tool that involves theorem prover techniques (see Prove Annotations with WP). The others have to be carefully reviewed since all the results of the analysis rely on these hypotheses.

Here and there, extracting information, either to understand the results or to produce a report, is also useful. This can be done by combining options and scripts. How to do it is also explained in Get the Information.

Although the tool can be used purely from the command line interface, it also provides a GUI (see the TIS GUI Manual) that is very convenient for exploring the computed results.