The MALPAS toolset consists of a number of analysers which focus on different aspects of software correctness and integrity. These analysers work with a MALPAS Intermediate Language (IL) representation of the software program which is being analysed.
IL is a universal sequential programming language into which programs written in C, Ada, etc. are translated (via automatic or manual means). The benefit of this process is that the MALPAS analysers need only know about IL, but the analysis results are relevant to the original C (or Ada, etc.) program. Therefore, the MALPAS analysers are essentially universal.
The MALPAS analysis process
Each program is translated into Intermediate Language (IL). The MALPAS analysers process the IL representation and produce reports on the integrity and correctness of the original program.
The MALPAS analysers
Control flow analysis – identifies unstructured control flow in a program. These can include multiple entry and exit points, unreachable code and infinitely looping dynamic halts. It gives an initial feel for the structure of the program and is particularly useful for assessing assembly code that lacks high level language control structures.
Data use analysis – identifies all the inputs and outputs of each procedure, whether documented or not, including any surreptitious use of global data. Data handling errors are also revealed; for example, there are checks that each variable is initialised before being read.
Information flow analysis – each procedure is analysed to deduce the information on which its outputs depend. The analysis of these dependencies is the first step towards identifying serious errors in the dynamic behaviour of the program, such as unwanted side-effects.
Semantic analysis – this analysis re-expresses the complete semantics of the procedure in a formal mathematical notation that is more explicit than the code. The analyst can use this algebraic representation to check for discrepancies between the program’s behaviour and its specification.
Compliance analysis – supports a formal proof that a procedure behaves in accordance with its specification. In other words, if the required precondition holds when the procedure is called then the required post-condition must hold when it terminates. Where this is not the case, compliance analysis will identify the input values for which the procedure will fail.