Séminaire des équipes de recherche
Hybrid Information Flow Analysis for Real-World C Code
Information flow analysis models the propagation of data through a software system and can identify unintended information leaks. There is a wide range of such analyses, tracking flows statically, dynamically at run time, or in a hybrid way combining both static and dynamic approaches.
- Date : 14/11/2016
- Lieu : Inria Paris - 2 rue Simone Iff - Salle Lions 1, bâtiment C
- Intervenant(s) : Gergö Barany (CEA)
We present a hybrid information flow analysis for a large subset of the C programming language. Extending previous work that handled a few difficult features of C, our analysis can deal with pointers, arrays, pointer arithmetic, structures, dynamic memory allocation, complex control flow, and statically resolvable indirect function calls. The analysis is implemented as a plugin to the Frama-C framework.
We demonstrate the applicability and precision of our analyzer by applying it to an open-source cryptographic library. We verify an information flow policy that proves the absence of control-flow based timing attacks against the implementations of many common cryptographic algorithms. Conversely, we demonstrate that our analysis is able to detect a known instance of this kind of vulnerability in another cryptographic primitive.