How to use Frama-C to proof correctness of AVR microcontroller code

What’s different than in the previous article? This blog entry is about a specific program that’s analyzed and proofed with frama-c and ACSL.

First what’s the target of using frama-c and WP in this blog post?

• First the usage of the RTE (runtime error annotation) plugin that is used to check for common runtime errors like undefined behaviour of the C language, typical overflow and signedness bugs in arithmetic, access into undefined memory, array out of bounds conditions, etc. Most of the work of the RTE plugin is done automatically.
• Verifying correctness of some properties like the ringbuffer of the specific application working correctly (always stays inside it’s bounds, only written to when not full, never read from when empty, etc.) as well as correctness of the calculations done for stepper control.

What static analysis and proof assistants cannot do for you?

One really important point from this project that could not be proofed that way was that the code honored a given timing. Since this code is about realtime stepper control (acceleration, deceleration, constant speed, etc.) timing is an important part. This cannot be proofed by frama-c on the C source level. It would be possible however to write a machine model in CoQ, add some additional annotations and proof that the generated assembly language fulfills the given constraints. This is something that would be possible with the existing models for the RISC-V architecture for example.

On the other hand the static analysis doesn’t say anything about the correctness of the used compiler. If this is a critical point one would have to write or use an compiler that’s proofed to be correct - like CompCert that is used for example by companies like Airbus France or organizations like ESA.

The last thing that this tool cannot provide is any information about the correctness of the hardware. If this is required one should use a hardware architecture that can be proofen to be correct (like RISC-V) and where proofen synthesis methods are used to create the microprocessor footprint. Even then there are some physical effects that might not be accounted to by the analysis (like latchup effects, effect of cosmic radiation, etc.) that will have to be dealt with in some other way.

Runtime error annotations (RTE) and obligations with WP

First let’s get started with the RTE plugin. Basically one can try to execute frama-c with

frama-c -wp -wp-rte

against one’s source file. When using AVR code chances are high that there is a bunch of missing includes and definitions. To solve that I’ve taken the header files from avr-gcc and modified them a little bit:

• cli and sei are no macro definitions any more but functions that have an annotation attached that tells frama-c that they are in fact side-effect free (memory wise and variable wise).

After that frama-c is invoked via

frama-c -cpp-extra-args="-I~/framaclib/ -DF_CPU=16000000L -D__AVR_ATmega328P__" avr_dualsteppers.c

or

frama-c-gui -cpp-extra-args="-I~/framaclib/ -DF_CPU=16000000L -D__AVR_ATmega328P__" avr_dualsteppers.c

As one can see I’ve added the include directory for the custom C includes from avr-libc and specified the CPU frequency as well as the hardware platform. The first is required since I’ve embedded some delay loop code into that requires F_CPU to be defined. On the other hand the target microcontroller spec is required by the avr-libc include files to load correct definitions for the given chip since they differ in registers and capabilities.

After the first run of the WP plugin using either -wp -wp-rte or using the GUI menu at Analyses / Analyses and then selecting -wp and -wp-rte from the checkboxes (tuning the number of concurrent proof assistants and selecting a given proof assistant as required) one will see that a bunch of mem_access goals fails. These are mainly accesses to hardware registers which is the main pitfall when analyzing code for a microcontroller. This is simply solved by adding an ACSL annotation that requiers validity of the registers during the function run as a precondition:

/*@
        requires \valid_read(&TWSR) && \valid_read(&TWDR) && \valid(&TWDR) && \valid(&TWCR);

        ensures TWCR == 0xC5;
*/
ISR(TWI_vect) {
	// ...
}

In this example I’ve added annotations that require valid read on the two wire status register and data register as well as a total valid pointer to the two wire data register (for valid writes). Doing this for all hardware registers solves much trouble of using WP. Note that at least on main one has to define this validity as an axiom since these registers are never allocated:

/*@
	axiomatic hardware_registers {
		axiom valid_TCCR0A: \valid(&TCCR0A);
		axiom valid_TCCR0B: \valid(&TCCR0B);
		axiom valid_TIMSK0: \valid(&TIMSK0);
		axiom valid_PORTB: \valid(&PORTB);
		axiom valid_DDRB: \valid(&DDRB);
		axiom valid_UCSR0B: \valid(&UCSR0B);
	}
*/

These axioms define that access to these registers is always valid.

Another annotation that is required are loop invariants and loop assignments. These are used to optimize the processing of loops and are necessary for some proofs. The project annotated in this blog post contains two types of loops. Annotating the infinite for(;;) loop that contains the main program loop does not provide any additional value. On the other hand frama-c complains about some other loops not being annotated and assuming they might assign everything. For example the main stepper iteration loop from handleTimer2Interrupt iterates over all stepper states and only writes into two possible output registers as well as 3 variables. This should be stated in front of the given loop:

/*@
		loop assigns PORTD, PORTC;
		loop assigns drvRealEnabled, drvEnableState;
		loop assigns state[0 .. (STEPPER_COUNT-1)];

		loop invariant 0 <= stepperIdx < STEPPER_COUNT;

*/
for(stepperIdx = 0; stepperIdx < STEPPER_COUNT; stepperIdx = stepperIdx + 1) {
	...
}

The same goes for the main state initialization loop. Since the updateConstants function also only influences the state array:

/*@
	loop assigns state[0 .. (STEPPER_COUNT-1)];

	loop invariant 0 <= i < STEPPER_COUNT;
*/
for(i = 0; i < STEPPER_COUNT; i=i+1) {
		state[i].cmdQueueHead = 0;
		state[i].cmdQueueTail = 0;
		state[i].counterCurrent = 0;
		state[i].c_i = -1; /* Will trigger initialization after planning */

		state[i].currentPosition = 0; /* Initialize always at position 0 */

		state[i].settings.acceleration = STEPPER_INITIAL_ACCELERATION;
		state[i].settings.deceleration = STEPPER_INITIAL_DECELERATION;
		state[i].settings.alpha = STEPPER_INITIAL_ALPHA;
		state[i].settings.vmax = STEPPER_INITIAL_VMAX;

		updateConstants(i);
}

Note that the functions cli() and sei() include some inline assembly and contain the memory reference in their clobber list to prevent compiler reordering of the calls (which is obviously a hack). This of course leads to frama C complaining that we don’t have any assigns clause.

Now comes the more challenging part. In case one wants to proof that the command queue ringbuffers head will stay inside the ringbuffer array during handleTimer2Interrupt() function one could add the following annotation:

/*@
	ensures
		\forall integer iStep; 0 <= iStep < STEPPER_COUNT
			==> (state[iStep].cmdQueueHead >= 0) && (state[iStep].cmdQueueHead < STEPPER_COMMANDQUEUELENGTH);

	ensures
		\forall integer iStep; 0 <= iStep < STEPPER_COUNT
			==> (state[iStep].cmdQueueTail >= 0) && (state[iStep].cmdQueueTail < STEPPER_COMMANDQUEUELENGTH);
*/

After that RTE works under most circumstances if your code has been written correctly. Some bugs that will be spot will be the well known inter over- and underflow as well as signeness bugs that are often overseen by programmers.

Some function require additional care. For example the side effects of the function updateConstants(int stepperIndex) varies depending on a valid or invalid stepperIndex. This is done by specifying behaviours. Note that in the following case behaviours will be complete (i.e. describe all ways the function may proceed) and disjoint (i.e. the behaviours may not occur at the same time or intersect). None of these two is a requirement but it makes the live of the proof writer somewhat easier. Behaviours depend on assumptions that have to be true for the behaviour to be the action taken by the function:

/*@
	behavior unknownChannel:
		assumes (stepperIndex < 0) || (stepperIndex >= STEPPER_COUNT);
		assigns \nothing;
	behavior knownChannel:
		assumes (stepperIndex >= 0) && (stepperIndex < STEPPER_COUNT);

		requires (state[stepperIndex].settings.vmax >= STEPPER_MIN_VMAX) && (state[stepperIndex].settings.vmax <= STEPPER_MAX_VMAX);
		requires (state[stepperIndex].settings.alpha >= STEPPER_MIN_ALPHA) && (state[stepperIndex].settings.alpha <= STEPPER_MAX_ALPHA);
		requires (state[stepperIndex].settings.acceleration >= STEPPER_MIN_ACCELERATION) && (state[stepperIndex].settings.acceleration <= STEPPER_MAX_ACCELERATION);
		requires (state[stepperIndex].settings.deceleration >= STEPPER_MIN_DECELERATION) && (state[stepperIndex].settings.deceleration <= STEPPER_MAX_DECELERATION);

		assigns state[stepperIndex].constants.c1,
		 	state[stepperIndex].constants.c2,
			state[stepperIndex].constants.c3,
			state[stepperIndex].constants.c4,
			state[stepperIndex].constants.c5,
			state[stepperIndex].constants.c7,
			state[stepperIndex].constants.c8,
			state[stepperIndex].constants.c9,
			state[stepperIndex].constants.c10;

		ensures state[stepperIndex].constants.c2 == (state[stepperIndex].settings.vmax * state[stepperIndex].settings.vmax) / (2 * state[stepperIndex].settings.acceleration * state[stepperIndex].settings.alpha);
		ensures state[stepperIndex].constants.c4 == -1 * (state[stepperIndex].settings.vmax * state[stepperIndex].settings.vmax) / (2 * state[stepperIndex].settings.deceleration * state[stepperIndex].settings.alpha);
		ensures state[stepperIndex].constants.c5 == state[stepperIndex].settings.deceleration / (state[stepperIndex].settings.deceleration - state[stepperIndex].settings.acceleration);
		ensures state[stepperIndex].constants.c7 == 2 * state[stepperIndex].settings.alpha / state[stepperIndex].settings.acceleration;
		ensures state[stepperIndex].constants.c8 == state[stepperIndex].settings.acceleration / (state[stepperIndex].settings.alpha * (double)STEPPER_TIMERTICK_FRQ * (double)STEPPER_TIMERTICK_FRQ);
		ensures state[stepperIndex].constants.c9 == state[stepperIndex].settings.acceleration / (state[stepperIndex].settings.alpha * (double)STEPPER_TIMERTICK_FRQ * (double)STEPPER_TIMERTICK_FRQ);
		ensures state[stepperIndex].constants.c10 == state[stepperIndex].settings.alpha * (double)STEPPER_TIMERTICK_FRQ;

	disjoint behaviors;
	complete behaviors;
*/

During the proof process it gets proofed that while one has an invalid stepper index no side effects happen (i.e. assigns \nothing) and that the specified constants are calculated (and indeed fit into the range of the data types) of the specific stepper. It also get’s verified that the calculation indeed does what the formulas specify (i.e. there is no undefined behaviour, no over or underflow, etc.)

When one wants to ensure that some values are always assigned inside given application specific limits one can add an assertion:

/*@ assert (state[stepperIndex].constants.c2 < 4294967296); */

After all annotations have been placed into the sourcefile one can run frama-c with the wp plugin and runtime error annotations (wp-rte) to detect - and hopefully fix - possible error sources or undefined behaviour.

Some of the pitfalls that might be detected (guaranteed as long as you didn’t mess up by specifying axioms) by frama-c with rte plugin:

• Array out of bounds access
• Acessing undefined memory locations
• Datatype conversions with undefined outcome.
• Errors caused by casting different datatypes
• Off-by-one signed integer errors
• Calculations that would lead to overflow or underflow with the used datatypes (this is a common error in embedded software when processing sensor data or calculating for example motion paths via traditional formulas)

The WP plugin on the other hand guarantees that you code matched the mathematical specification you’ve added to the code as annotations. The normal design flow should - of course - be to write the ACSL specification first and then write code (best case of course to let two different people write specification and code) as usual.

Many of the potential errors might not have been caught by traditional testing since the mostly affect corner cases (that one might even not think about).

Whenever a function depends on some preconditions like for example the annotation for stepperPlanMovement_ConstantSpeed

/*@
	requires \forall integer iStep; 0 <= iStep < STEPPER_COUNT
		==> (state[iStep].settings.vmax >= STEPPER_MIN_VMAX) && (state[iStep].settings.vmax <= STEPPER_MAX_VMAX);
	requires \forall integer iStep; 0 <= iStep < STEPPER_COUNT
		==> (state[iStep].cmdQueueHead >= 0) && (state[iStep].cmdQueueHead < STEPPER_COMMANDQUEUELENGTH);
	requires \forall integer iStep; 0 <= iStep < STEPPER_COUNT
		==> (state[iStep].constants.c10 == state[iStep].settings.alpha * STEPPER_TIMERTICK_FRQ);
	requires (immediate == true) || (immediate == false);

	behavior unknownStepper:
		assumes (stepperIndex < 0) || (stepperIndex >= STEPPER_COUNT);
		assigns \nothing;
	behavior knownStepperImmediate:
		assumes (stepperIndex >= 0) && (stepperIndex < STEPPER_COUNT);
		assumes immediate == true;

		requires (v >= (state[stepperIndex].settings.alpha * STEPPER_TIMERTICK_FRQ)/(4294967295)) && (v <= state[stepperIndex].settings.alpha * STEPPER_TIMERTICK_FRQ);

		assigns state[stepperIndex].cmdQueue[\old(state[stepperIndex].cmdQueueHead)].cmdType;
		assigns state[stepperIndex].cmdQueue[\old(state[stepperIndex].cmdQueueHead)].data.constantSpeed.cConst;
		assigns state[stepperIndex].cmdQueue[\old(state[stepperIndex].cmdQueueHead)].forward;
		assigns state[stepperIndex].cmdQueueHead;
		assigns state[stepperIndex].cmdQueueTail;

		ensures state[stepperIndex].cmdQueueTail == \old(state[stepperIndex].cmdQueueHead);
		ensures state[stepperIndex].cmdQueueHead == ((\old(state[stepperIndex].cmdQueueHead) + 1) % STEPPER_COMMANDQUEUELENGTH);
		ensures state[stepperIndex].c_i == -1;
	behavior knownStepperPlanned:
		assumes (stepperIndex >= 0) && (stepperIndex < STEPPER_COUNT);
		assumes immediate == false;

		requires (v >= (state[stepperIndex].settings.alpha * STEPPER_TIMERTICK_FRQ)/(4294967295)) && (v <= state[stepperIndex].settings.alpha * STEPPER_TIMERTICK_FRQ);

		assigns state[stepperIndex].cmdQueue[\old(state[stepperIndex].cmdQueueHead)].cmdType;
		assigns state[stepperIndex].cmdQueue[\old(state[stepperIndex].cmdQueueHead)].data.constantSpeed.cConst;
		assigns state[stepperIndex].cmdQueue[\old(state[stepperIndex].cmdQueueHead)].forward;
		assigns state[stepperIndex].cmdQueueHead;

		ensures state[stepperIndex].cmdQueueHead == ((\old(state[stepperIndex].cmdQueueHead) + 1) % STEPPER_COMMANDQUEUELENGTH);
	disjoint behaviors;
	complete behaviors;
*/

In this case one sees that the requirements at the top specify that all configurable settings have to be inside the allowed boundaries. During analysis of the function itself the static analyzer will assume these conditions to be true (for example to verify that calculation results are guaranteed to stay within the datatype boundaries). On the other hand it will use these requirements and check if they are fulfilled by the calling function whenever a function call is encountered. This allows the ensure that data passed from other parts of the application is valid and meets the specification - of all parts of the program that are affected by that datatype (i.e. in this case it’s guaranteed that speed settings within the allowed boundaries always lead to step counts within a 32 bit unsigned integer range and it’s guaranteed that the communication code only accepts values inside this range).

Note that one can run frama-c of course with UI or or without UI - and can of course process only a single function at a time:

• The call used to run the proof assistant from scripts with 32 parallel proof assistant instances was frama-c -wp -rte -wp-rte -wp-dynamic -wp-timeout 300 -wp-par 32 -cpp-extra-args="-I/usr/home/tsp/framaclib/ -DF_CPU=16000000L -D__AVR_ATmega328P__" avr_dualsteppers.c
• To use the UI instead of the shell one has to use frama-c-gui and leave the parameter -wp unset (because processing would start immediately otherwise)
• To process only a single function one can pass -wp-fct and specify the function name. This cuts down the time required during working on the proofs massively

This article is tagged: Programming, Math, Formal, Security, Frama C