Research overview

PostDoc: The goal of the project I'm involved in is to cryptographically secure information flows of distributed programs. We build and prove the correctness of a translation mechanism from sequential source programs to distributed target programs. The source program is a sequential program with annotations regarding the distribution of the target program. The source program uses a shared memory whose protection mechanism relies on security labels associated to variables. The translation mechanism returns a distributed program whose threads use local memory for their execution. Communication of values between threads of the target language is achieved through a shared memory of encrypted and signed values.

Thesis: My thesis concerned the development of dynamic information flow analyses for confidentiality monitoring. The monitors rely on both dynamic and static analyses. We followed two approaches. The first one is based on a security automaton directing a noninterference monitoring semantics. The second approach is semantics-based and uses context-sensitive static information flow analyses. Noninterference monitors have been developed for a sequential language and a concurrent language including synchronization commands. Those monitors have been proved to be sound with regard to the notion of noninterference. They also have been proved to be more precise than their equivalent type systems developed by Volpano, Smith et Irvine.

Keywords: Program analysis, Monitoring, Programming Language Semantics, Security, Confidentiality, Noninterference, Test, Cryptography

Publications

[BDLG12]
Musard Balliu, Mads Dam, and Gurvan Le Guernic. ENCOVER: Symbolic Exploration for Information Flow Security. In Proceedings of the IEEE Computer Security Foundations Symposium, June 2012. To appear.
[ bib ]

We address the problem of program verification for information flow policies by means of symbolic execution and model checking. Noninterference-like security policies are formalized using epistemic logic. We show how the policies can be accurately verified using a combination of concolic testing and SMT solving. As we demonstrate, many scenarios considered tricky in the literature can be solved precisely using the proposed approach. This is confirmed by experiments performed with ENCOVER, a tool based on Java Pathfinder which we have developed for concolic information flow testing.

[BDLG11]
Musard Balliu, Mads Dam, and Gurvan Le Guernic. Epistemic Temporal Logic for Information Flow Security. In Aslan Askarov and Joshua Guttman, editors, Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, page Article No 6, New York, NY, USA, June 2011. ACM Digital Library. Co-located with FCRC 2011.
[ bib | DOI | .pdf ]

Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing program outputs. This approach is shown to elegantly capture standard notions of noninterference and declassification in the literature as well as information flow properties where sensitive and public data intermingle in delicate ways.

[FLGR09]
Cédric Fournet, Gurvan Le Guernic, and Tamara Rezk. A Security-Preserving Compiler for Distributed Programs. In Ehab Al-Shaer, Somesh Jha, and Angelos D. Keromytis, editors, Proceedings of the ACM Conference on Computer and Communications Security, pages 432-441, New York, NY, USA, November 2009. ACM Press.
[ bib | DOI | .pdf ]

We enforce information flow policies in programs that run at multiple locations, with diverse levels of security. We build a compiler from a small imperative language with locality and security annotations down to distributed code linked to concrete cryptographic libraries. Our compiler splits source programs into local threads; inserts checks on auxiliary variables to enforce the source control flow; implements shared distributed variables using instead a series of local replicas with explicit updates; and finally selects cryptographic mechanisms for securing the communication of updates between locations. We establish computational soundness for our compiler: under standard assumptions on cryptographic primitives, all confidentiality and integrity properties of the source program also hold with its distributed code, despite the presence of active adversaries that control all communications and some of the program locations. We also present performance results for the code obtained by compiling sample programs.

[LG08a]
Gurvan Le Guernic. Precise Dynamic Verification of Confidentiality. In Bernhard Beckert and Gerwin Klein, editors, Proceedings of the International Verification Workshop, volume 372 of CEUR Workshop Proceedings, pages 82-96. CEUR-WS.org, August 10-11 2008. In connection with IJCAR 2008.
[ bib | http | .pdf ]

Confidentiality is maybe the most popular security property to be formally or informally verified. Noninterference is a baseline security policy to formalize confidentiality of secret information manipulated by a program. Many static analyses have been developed for the verification of noninterference. In contrast to those static analyses, this paper considers the run-time verification of the respect of confidentiality by a single execution of a program. It proposes a dynamic noninterference analysis for sequential programs based on a combination of dynamic and static analyses. The static analysis is used to analyze some unexecuted pieces of code in order to take into account all types of flows. The static analysis is sensitive to the current program state. This sensitivity allows the overall dynamic analysis to be more precise than previous work. The soundness of the overall dynamic noninterference analysis with regard to confidentiality breaches detection and correction is proved.

[LG08b]
Gurvan Le Guernic. Precise Dynamic Verification of Noninterference. Technical report, INRIA-MSR, July 2008.
[ bib | http | .pdf ]

Confidentiality is maybe the most popular security property to be formally or informally verified. Noninterference is a baseline security policy to formalize confidentiality of secret information manipulated by a program. Many static analyses have been developed for the verification of noninterference. In contrast to those static analyses, this paper considers the run-time verification of the respect of confidentiality by a single execution of a program. It proposes a dynamic noninterference analysis for sequential programs based on a combination of dynamic and static analyses. The static analysis is used to analyze some unexecuted pieces of code in order to take into account all types of flows. The static analysis is sensitive to the current program state. This sensitivity allows the overall dynamic analysis to be more precise than previous work. The soundness of the overall dynamic noninterference analysis with regard to confidentiality breaches detection and correction is proved.

[LG07e]
Gurvan Le Guernic. Information Flow Testing. In Iliano Cervesato, editor, Proceedings of the Annual Asian Computing Science Conference, volume 4846 of Lecture Notes in Computer Science, pages 33-47. Carnegie Mellon University Qatar Campus, Springer-Verlag, December 9-11 2007.
[ bib | http | .pdf ]

Noninterference, which is an information flow property, is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. Noninterference verification mechanisms are usually based on static analyses and, to a lesser extent, on dynamic analyses. In contrast to those works, this paper proposes an information flow testing mechanism. This mechanism is sound from the point of view of noninterference. It is based on standard testing techniques and on a combination of dynamic and static analyses. Concretely, a semantics integrating a dynamic information flow analysis is proposed. This analysis makes use of static analyses results. This special semantics is built such that, once a path coverage property has been achieved on a program, a sound conclusion regarding the noninterfering behavior of the program can be established.

[LG07d]
Gurvan Le Guernic. Confidentiality Enforcement Using Dynamic Information Flow Analyses. PhD thesis, Kansas State University, 2007.
[ bib | http | .pdf ]

With the intensification of communication in information systems, interest in security has increased. The notion of noninterference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. This notion, based on ideas from classical information theory, has first been introduced by Goguen and Meseguer (1982) as the absence of strong dependency (Cohen, 1977).
“information is transmitted from a source to a destination only when variety in the source can be conveyed to the destination” Cohen (1977)
Building on the notion proposed by Goguen and Meseguer, a program is typically said to be noninterfering if the values of its public outputs do not depend on the values of its secret inputs. If that is not the case then there exist illegal information flows that allow an attacker, having knowledge about the source code of the program, to deduce information about the secret inputs from the public outputs of the execution.
In contrast to the vast majority of previous work on noninterference which are based on static analyses (especially type systems), this PhD thesis report considers dynamic monitoring of noninterference. A monitor enforcing noninterference is more complex than standard execution monitors.
“the information carried by a particular message depends on the set it comes from. The information conveyed is not an intrinsic property of the individual message.” Ashby (1956)
The work presented in this report is based on the combination of dynamic and static information flow analyses. The practicality of such an approach is demonstrated by the development of a monitor for concurrent programs including synchronization commands. This report also elaborates on the soundness with regard to noninterference and precision of such approaches.

[LG07c]
Gurvan Le Guernic. Dynamic Noninterference Analysis Using Context Sensitive Static Analyses. Technical Report 2007-5, Kansas State University, 234 Nichols Hall, Manhattan, KS 66506, USA, July 2007.
[ bib | .html | .pdf ]

This report proposes a dynamic noninterference analysis for sequential programs. This analysis is well-suited for the development of a monitor enforcing the absence of information flows between the secret inputs and the public outputs of a program. This implies a sound detection of information flows and a sound correction of forbidden flows during the execution. The monitor relies on a dynamic information flow analysis. For unexecuted pieces of code, this dynamic analysis uses any context sensitive static information flow analysis which respects a given set of three hypotheses. The soundness of the overall monitoring mechanism with regard to noninterference enforcement is proved, as well as its higher precision than the automaton-based mechanism proposed in previous work.

[LG07a]
Gurvan Le Guernic. Automaton-based Confidentiality Monitoring of Concurrent Programs. In Proceedings of the 20th IEEE Computer Security Foundations Symposium, pages 218-232. IEEE Computer Society Press, July 6-8 2007.
[ bib | .pdf ]

Noninterference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. In contrast to static checking of noninterference, this paper considers dynamic, automaton-based, monitoring of information flow for a single execution of a concurrent program. The monitoring mechanism is based on a combination of dynamic and static analyses. During program execution, abstractions of program events are sent to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. All monitored executions are proved to be noninterfering (soundness) and executions of programs that are well-typed in a security type system similar to the one of Smith and Volpano are proved to be unaltered by the monitor (partial transparency).

[LGP07]
Gurvan Le Guernic and Julien Perret. FLIC: Application to Caching of a Dynamic Dependency Analysis for a 3D Oriented CRS. In Proceedings of the International Workshop on Rule-Based Programming, volume 219 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 3-18. Elsevier, June 29 2007.
[ bib | .pdf ]

FL-systems are conditional rewriting systems. They are used for programming (describing) and evaluating (generating) huge 3D virtual environments, such as cities and forests. This paper presents a formal semantics and a dynamic dependency analysis for FL-systems. This analysis allows the characterization of a set of terms which are joinable with the currently rewritten term. Consequently, it is possible to speed up the rewriting steps of the environments generation by using a cache mechanism which is smarter than standard ones. This work can be seen as a dynamic completion of a set of rewriting rules. This completion increases the number of terms which are rewritten in normal form by the application of a single rewriting rule.

[LG07b]
Gurvan Le Guernic. Automaton-based Non-interference Monitoring of Concurrent Programs. Technical Report 2007-1, Department of Computing and Information Sciences, College of Engineering, Kansas State University, 234 Nichols Hall, Manhattan, KS 66506, USA, February 2007.
[ bib | .html | .pdf ]

Earlier work [LGBJS06] presents an automaton-based non-interference monitoring mechanism for sequential programs. This technical report extends this work to a concurrent setting. Monitored programs are constituted of a set of threads running in parallel. Those threads run programs equivalent to those of [LGBJS06] except for the inclusion of a synchronization command. The monitoring mechanism is still based on a security automaton and on a combination of dynamic and static analyses. As in [LGBJS06], the monitoring semantics sends abstractions of program events to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. All monitored executions are proved to be non-interfering (soundness).

[LGBJS06]
Gurvan Le Guernic, Anindya Banerjee, Thomas Jensen, and David Schmidt. Automata-based Confidentiality Monitoring. In Proceedings of the Annual Asian Computing Science Conference, volume 4435 of Lecture Notes in Computer Science, pages 75-89. Springer-Verlag, December 6-8 2006.
[ bib | .pdf ]

Non-interference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. In contrast to static checking of non-interference, this paper considers dynamic, automaton-based, monitoring of information flow for a single execution of a sequential program. The mechanism is based on a combination of dynamic and static analyses. During program execution, abstractions of program events are sent to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. The mechanism proposed is proved to be sound, to preserve executions of well-typed programs (in the security type system of Volpano, Smith and Irvine), and to preserve some safe executions of ill-typed programs.

[BLG06]
Nicolas Bonnel and Gurvan Le Guernic. Système de recherche de méthodes Java basé sur leur signature. In Proceedings of Majecstic 2006, November 2006.
[ bib | .pdf ]

L'objectif de cet article est de proposer une démarche permettant de mettre en place un moteur de recherche de méthodes au sein d'un langage de programmation. Un tel outil s'avère particulièrement utile aux développeurs. Des solutions ont déjà été proposées mais elles sont pour la plupart basées sur une recherche textuelle, c'est-à-dire uniquement basées sur le contenu textuel de la description des différentes méthodes. Nous proposons dans cet article une nouvelle approche basée sur la signature des méthodes. Le langage utilisé tout au long de cet article est le langage Java.

[LGBS06]
Gurvan Le Guernic, Anindya Banerjee, and David Schmidt. Automaton-based Non-interference Monitoring. Technical Report 2006-1, Department of Computing and Information Sciences, College of Engineering, Kansas State University, 234 Nichols Hall, Manhattan, KS 66506, USA, April 2006.
[ bib | .html | .pdf ]

This report presents a non-interference monitoring mechanism for sequential programs. Non-interference is a property of the information flows of a program. It implies the respect of the confidentiality of the secret information manipulated. The approach taken uses an automaton based monitor. During the execution, abstractions of the events occurring are sent to the automaton. The automaton uses those inputs to track the information flows and to control the execution by forbidding or editing dangerous actions. The mechanism proposed is proved to be sound and more efficient than a type system similar to the historical one developed by Volpano, Smith and Irvine.

[LGP05]
Gurvan Le Guernic and Julien Perret. FL-system's Intelligent Cache. In Alexandre Vautier and Sylvie Saget, editors, Proceedings of Majecstic 2005, pages 79-88, November 2005.
[ bib | .pdf ]

Cet article présente une application de techniques issues du génie logiciel à la modélisation d'environnements virtuels. Ces derniers, dès lors qu'ils sont complexes, constituent des masses de données particulièrement volumineuses et, de ce fait, difficiles à manipuler. De plus, les descriptions exhaustives de ces environnements, c'est-à-dire explicites, sont peu évolutives. Pour résoudre ces problèmes, il existe des méthodes basées sur des systèmes de réécriture permettant de décrire de fac¸on générique les objets de l'environnement. Chaque objet est ainsi décrit par un axiome qui est réécrit lors de la génération de l'environnement. Lors de cette phase, il est fréquent de retrouver deux séquences de réécriture aboutissant à un même objet. Il est alors possible d'utiliser un mécanisme tel que le cache afin d'améliorer les performances en profitant des calculs déjà effectués. Cependant, se contenter de mettre en correspondance les noms et paramètres des axiomes n'est pas suffisant pour établir l'ensemble des réécritures identiques. En effet, les réécritures d'un même axiome avec des paramètres effectifs différents peuvent aboutir au même objet. Le système proposé dans cet article effectue une analyse dynamique des réécritures afin d'améliorer les performances du cache en d´etectant de tels cas. La première partie de cet article présente le système de réécriture, la seconde l'analyse utilisée, et la dernière le mécanisme proposé.

[LGJ05]
Gurvan Le Guernic and Thomas Jensen. Monitoring Information Flow. In Andrei Sabelfeld, editor, Proceedings of the Workshop on Foundations of Computer Security, pages 19-30. DePaul University, June 2005.
[ bib | .pdf ]

We present an information flow monitoring mechanism for sequential programs. The monitor executes a program on standard data that are tagged with labels indicating their security level. We formalize the monitoring mechanism as a big-step operational semantics that integrates a static information flow analysis to gather information flow properties of non-executed branches of the program. Using the information flow monitoring mechanism, it is then possible to partition the set of all executions in two sets. The first one contains executions which are safe and the other one contains executions which may be unsafe. Based on this information, we show that, by resetting the value of some output variables, it is possible to alter the behavior of executions belonging to the second set in order to ensure the confidentiality of secret data.

[LG03]
Gurvan Le Guernic. Roles & Security, October 2003. Dagstuhl Seminar 03411: Language-Based Security.
[ bib ]

This file has been generated by bibtex2html 1.75

External links

Webpage on Academia.edu

"Gurvan LE GUERNIC" on: portal.acm.org, scholar.google.fr, dblp.uni-trier.de, ira.uka.de, link.springer.com, citeseer.ist.psu.edu, academic.research.microsoft.com

Stop the Numbers Game: Counting papers slows the rate of scientific progress.
Publish or perish

Valid XHTML 1.1

Valid CSS 2