Formal verification of the Paparazzi autopilot

This project is a fork of Paparazzi UAV autopilot repository (https://github.com/paparazzi/paparazzi). The aim of this project is to verify the pprz_algebra library using Frama-C.

The GitLab project adds ACSL annotations and provides a script to automatically launch Frama-C. Frama-C analyses the code, checks for the absence of RTE (RunTime Errors) and verify some functional properties.

Required software

To run the verification, the following software are required:

• Frama-C 23.0 (Vanadium)
• Alt-Ergo 2.4.0
• CVC4 1.9-prerelease
• Z3 4.8.6
• Coq 8.12.2
• Why3 1.4.0
• ctags

How to launch the verification process

First, go to the sw/airborne directory:

cd sw/airborne

Update the variable FRAMAC_PREFIX in frama-c-analysis.sh with the path of the directory containing Frama-C binary. Then, launch the script that starts the analysis:

./frama-c-analysis.sh

The WP smoke tests can be enabled with the environment variable SMOKE as follows:

SMOKE=1 ./frama-c-analysis.sh

Quick description of modified files

• sw/airborne/frama-c-analysis.sh: a shell script that automatically launches the verification using Frama-C.
• sw/airborne/output-frama-c-analysis.sh: a Python script used by frama-c-analysis.sh to read and analyse the results from Frama-C.
• sw/airborne/math/pprz_algebra_(int|float|double).(h|c): the mathematical library of Paparazzi that has been verified. These files have been annotated with ACSL.
• sw/airborne/math/pprz_algebra_(int|float|double)_frama_c.h: files containing definition of predicates, lemmas and logical functions used to verify the absence of RTE in the library.
• sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h: definition of predicates, lemmas and logical functions for the verification of functional properties.
• sw/airborne/.frama-c/wp/interactive: Coq scripts containing the proof lemmas.
• sw/airborne/.frama-c/wp/script: WP scripts containing the tactics used to prove some goals.

Verification process

The verification process combines the analysis of the EVA and WP plugins of Frama-C. The EVA plugin requires a program entry point (a main or a function) to start its analysis. The script frama-c-analysis.sh finds automatically all the names of the functions in the library using ctags. Then, verification is launched for every function FUNCTION with the following parameters:

• -rte: adds RTE annotations in the code.
• -no-warn-left-shift-negative: allows left shift for negative values.
• -eva -lib-entry -main $FUNCTION: launches EVA analysis with $FUNCTION as the entry point. The initial state is determined by the preconditions specified in the contract of the function.
• -wp-fct $FUNCTION: launches the WP verification with the following options:
  • -wp-cache update: enables and uses cache.
  • -wp-model real+Cast+ref: enables the real model to represent the arithmetic on floating-point numbers. The Cast option enables the usage of cast in the code. Finally, the ref option is used to enable optimization for reference parameters.
  • -wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,coq,tip: adds the different provers needed to verify the goals.
  • -wp-check-memory-model: Insert memory model hypotheses in the function contracts. Necessary as we use the ref memory model.
• -cpp-extra-args=-I../include: adds the include directory of Paparazzi.
• -cpp-extra-args=-DFRAMA_C_ANALYSIS: defines a C constant in order to remove certain portions of code that are not supported by Frama-C.

More information about Paparazzi

To have information about Paparazzi, go directly on the website or on the GitLab project.