Effective Verification of Low-Level Software with Nested Interrupts

Abstract

Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an explosion in the number of cases to be considered. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent advances in the encoding of the execution traces of interacting, concurrent threads.We assess the performance of our method on benchmarks drawn from embedded systems code and device drivers, and experimentally compare it to conventional formal approaches that use source-to-source transformations. Our experimental results show that our method significantly outperforms conventional techniques. To the best of our knowledge, our technique is the first to demonstrate effective formal verification of low-level embedded software with nested interrupts.

Papers

NEW: TECS journal paper (log, source code: i-CBMC, i-CBMC-TO)

DATE15 conference paper

Tool usage

We implement our technique in a tool called i-CBMC, based on CBMC, a bounded model checker for the C programming language. The i-CBMC binary compiled for 64bit Linux can be found here. The corresponding source code batch is also available. For questions about i-CBMC, please contact Lihao Liang (lihao.liang AT cs.ox.ac.uk).

Modelling interrupts in i-CBMC

We use function calls to model interrupt arrivals and handling. More precisely, an interrupt is specified using a label __CPROVER_ASYNC_ followed by a function call to its corresponding ISR:

__CPROVER_ASYNC_: isr();

Then you can use the option --mm irq (or --mm irq-pre for the precise encoding) in i-CBMC to verify your interrupt-driven programs:

cbmc --mm irq file.c

Experiments

We compare our tool i-CBMC with two conventional source-to-source transformations using benchmarks derived from embedded software and Linux device drivers. These translate interrupt-driven code into sequential code and into multi-threaded code. A description of the benchmarks in our experiments can be found here.

Download

Methods	Benchmarks	Experimental Results
i-CBMC with parital-order encoding	Source code	Detailed log files
i-CBMC with precise encoding	Source code	Detailed log files
Interrupt sequentialisation	Source code	Detailed log files
Instrumentation with threads	Source code	Detailed log files

Interrupt Sequentialisation

We define a scheduling function with two global variables: count is the total number of interrupt arrivals during program execution, and irq_enabled[i] indicates whether interrupt i is enabled. To enable/disable interrupts, we just need to set the corresponding bit of the irq_enabled array to one/zero.

The scheduling function is implemented as follows:

void schedule_irq(void) {
  int j = count;
  int irq;

  for (int i = 0; i < j; i++) {
    // non-deterministically generate candidate irq
    irq = nondet_int() ;
    assume(irq >= 0 && irq < num_irqs);

    // if irq is enabled, contingently generate the interrupt
    if (count != 0 && irq_enabled[irq] && nondet_bool()) {
      count--;

      // invoke the ISR, preempting the calling program
      switch (irq) {
        case 0: isr_0(); break;
        case 1: isr_1(); break;
        ...
        default: ;
      }
    }
  }
}

We use the following tools in our experiments: BLAST, CBMC, CPAChecker, SatAbs, UFO. The tools were run using the 2014 SVCOMP configuration. The benchmarks and experimental data can be found in the Download section.

Instrumentation with Threads

The invocation of the ISR is modelled by spawning a thread that executes the ISR, which is instrumented as follows:

irqreturn_t isr_i(param_list) {
   atomic { thread_running[i] = 1; }

   /* original code */
   ...

   atomic { thread_running[i] = 0; }
   return IRQ_HANDLED;
}

Function calls are inlined and an atomic statement

atomic_assume(thread_running[0]==0 && ... && thread_running[i-1]==0)

is inserted between every single statement in the inlined code of the ISRs, assuming that if i < j then ISR call i preempts ISR call j (i.e. interrupt i is enabled in ISR j or in other ISR calls that preempt j).

We set thread_running[i] = 1 if and only if the ISR call i is executing or preempted by other ISR calls. Different calls to the same ISR require separate function bodies with different instrumentations.

We use the following tools in our experiments: CBMC, ESBMC, Impara, SatAbs, Threader. The tools were run using the 2014 SVCOMP configuration. The benchmarks and experimental data can be found in the Download section.

Benchmarks

Logger is code modelled after parts of the firmware of a temperature logging device from a major industrial enterprise. It has two interrupt-triggered tasks: the measurement task should not be preempted by the communication task. Otherwise, a measurement is written to a wrong position in the log.

Blink is an example application from the TinyOS2 distribution. It displays a pattern on three LEDs with the help of timers. TinyOS provides a virtualisation API to handle several alarms with one hardware timer. There are two interrupt-triggered tasks, for firing the alarm and updating the timer when it overflows. If the alarm firing can preempt the updating of the timer, the timer keeps running even though the alarm has already fired.

Brake is code generated from the Simulink model of a brake-by-wire system provided by Volvo Technology AB. The system consists of four threads communicating with four wheel brake controllers, together with one main thread, responsible for computing the braking torque, which should not be preempted. Otherwise, the brake torque can be miscalculated. We parameterised this benchmark by the number of wheels.

RcCore is a Linux device driver for a remote control together with a model of the Linux Kernel. The original driver uses locks to enforce priorities-namely that querying the availability of transmission protocols may not be interrupted by a modification to the protocol settings. We introduced a bug such that the driver may crash due to a NULL pointer dereference if priorities are disregarded.