Scenario of security leak using Aorai and Value

This demo shows the usage of Aoraï and Value to generate a scenario of a security leak in the driver of a serial port (Linux kernel 2.6). It stems from the Calmos project with LabSoC at TelecomParisTech/Eurecom

C source files and the Frama-C script that launches the analysis are available in this archive.

Licence

C source files (leon-no-asm.c, serial_core.c, tty_io.c, stubs.c, n_tty.c) and header files (circ_buf.h, leon.h, serial_core.h, stubs.h, termbits.h, tty_flip.h, tty.h) have been adapted from the Linux kernel distributed by Gaisler and as such are distributed under the GNU General Public License version 2. This is also the case for the main.c, test_hook.c, cute_hook.h and calmos_hook.c files, which are copyrighted by CEA LIST

Frama-C script (script.ml) and Aoraï files (scenario.ya and scenario.ltl) are released by CEA LIST under the GNU Lesser General Public License (LGPL) version 2.1

Pre-requisite

The script works with Frama-C Fluorine 20130601. Note that if you don’t have the proprietary built-ins extensions of Value Analysis, performances will be much worse. See the script for more information about the various possible options. PathCrawler is needed if you intend to use test-case generation to find a scenario. Otherwise, use -frama-c-path-finder option

Context

A sequence of hardware events on the serial port has been identified has potentially insecure. We want to see whether this sequence can be replayed through call to the API of the driver.

Aoraï

The sequence is described as an automaton in scenario.ya

Set up context

• stubs.c provides some functions that are necessary for the analysis, mostly extracted from the kernel.
• main.c provides the main entry point:
  • we initialize the most important kernel structures
  • we put the hardware in some random state
  • we initialize the driver,
  • we enter an endless loop which randomly selects an operation in the driver’s API at each step.
• script.ml is the script that drives Frama-C’s analysis

First pass

The code for the driver cannot be used by Aoraï as such, because of function pointers. A first pass of value analysis and constant folding removes them (we use only one driver). We also eliminate dead code that could confuse Aoraï

Instrumented code

We then use Aoraï to generate contracts corresponding to the automaton: if each function in the implementation respects its contract, the code is conforming to the automaton

Extraction of the scenario

Here, we want to see a specific sequence of calls leading to the alarm state. We launch value and inspect the state of the automaton after each step of the loop, recording the chain of calls to the driver that led to this state, until we reach the alarm state.