No Crash, No Exploit: Automatic Verification of Embedded Kernels

RTAS 2021 — Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival — 10.1109/rtas52030.2021.00011
PDF Technical Report Bibtex Artifact Benchmark Talk Slides
Best and Outstanding Paper Awards
Also presented at AFADL 2021
 
Topics: embedded system security; secure embedded kernels; formal methods; abstract interpretation; absence of privilege escalation.

Context

In most systems, the kernel is critical for security: it is the piece of software that ensures isolation between programs, so you don’t want it to fail in that task. You don’t want it to crash, either. We aim at verifying realistic embedded kernels (e.g. used in the Internet of Things) and for that we want to devise an almost fully automated approach that works on existing kernels.

We want to perform this verification at the executable level (“binary” code), because all kernels use low-level, architecture-specific instructions. This is a challenge due to the low-level nature of binary: no explicit control flow, no types, legitimate integer overflows, etc. Another challenge is unbounded loops. Unbounded loops are loops whose number of iterations cannot be bounded statically. A simple example of such a loop is iterating over a linked list. Analyzing unbounded loops matters, because most real-time scheduling algorithms contain such loops.

Another difficulty of analyzing embedded kernels is that they are usually parameterized: values such as task priorities, or task memory region begin and end addresses, may be constant throughout execution of the system, but are not hard-coded in the kernel; instead, they are written in a special zone of memory called the interface between kernel and tasks. The memory structure of this zone is known but the precise values and addresses are not, which forces the code analysis to step up in terms of complexity.

Contributions

  • A new method for verifying absence of privilege escalation and absence of crash in an embedded kernel, based on abstract interpretation (handles loops and verifies kernels independently of the application).
  • A new abstraction of memory based on types, handling parameterization and improving scalability precision of the analysis.
  • We applied the technique to two embedded kernels (including an industrial one), demonstrating that our method can verify kernels with less than 58 lines of manual annotations (in some cases, requiring 0 lines of annotations, i.e. the kernel is verified without human intervention).

Further information