User Tools

  • Logged in as: anonymous (anonymous)
  • Logout

Site Tools



This shows you the differences between two versions of the page.

Link to this comparison view

mantis:frama-c:aorai-security [2013/09/17 16:07] (current)
virgile created
Line 1: Line 1:
 +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 [[http://​​recherche/​labsoc.en|LabSoC]] at TelecomParisTech/​Eurecom
 +C source files and the Frama-C script that launches the analysis are available in {{:​mantis:​frama-c:​articles:​aorai-security.tar.bz2|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 [[http://​|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 ( 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.
 +[[mantis:​frama-c:​publications#​PathCrawler|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.
 +  * ''​''​ 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
 +====== 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.
mantis/frama-c/aorai-security.txt · Last modified: 2013/09/17 16:07 by virgile