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.
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
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
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.
The sequence is described as an automaton in
stubs.cprovides some functions that are necessary for the analysis, mostly extracted from the kernel.
main.cprovides the main entry point:
driver's API at each step.
script.mlis the script that drives Frama-C's analysis
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ï
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
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.