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

27 Nov 2019 - tsp

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?

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:

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:

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:

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


Dipl.-Ing. Thomas Spielauer, Wien (webcomplains389t48957@tspi.at)

This webpage is also available via TOR at http://jugujbrirx3irwyx.onion/

Valid HTML 4.01 Strict Powered by FreeBSD IPv6 support