On Friday 12/12/2008, at 10h30, in room Fermat Jaune.
PhD Thesis of Dorina Ghindici (LIFL Lille), talk given by Yves Bertot.
Title: Validation of Security Mechanisms for Embedded Systems.
Abstract:
This thesis addresses the problem of information flow security in the context of mobile code. Our work aims at providing a solution to confidentiality issues in multiapplicative systems: ensuring security for an applications running on small and autonomous systems by verifying information flow properties at deployment time. Existing work on information flow does not scale to small open systems due to resources limitations and due to lack of modularity, which is essential in a dynamically evolving environment. In order to provide a complete solution, we address both practical and theoretical aspects. We first propose a model and a tool dedicated to small open systems running Java bytecode, with support for inheritance and override. Our approach is modular, hence the verification is incremental and is performed on the target device, the only place where the security can be guaranteed. To our knowledge, it is the first information flow verifier for embedded systems. Moreover, our model improves information flow usability in such systems by limiting the overhead for adding information flow security to a Java Virtual Machine. To prove its usability, we ran different experiments and we tested the tool in several contexts: on a case study from the literature, on an application for mobile phone, and in an integrated security validation and verification framework that spans the entire software lifecycle. Secondly, we tackle the information flow issue from a theoretical point of view. We propose a formal model, based on abstract memory graphs; an abstract memory graph is a points-to graph extended with nodes abstracting input values of primitive type and flows arising from implicit flow. Again, the model is modular, which allows incremental analysis and dynamic download of new programs. Our construction is proved correct with respect to non-interference. Contrary to most type-based approached, our abstract memory graph is build independently on any security level knowledge. Information flow is checked by labeling graphs a posteriori.
