| Home | Phone: +33 1 39 63 52 64 | Last modified: November 14, 2007 |
(This summary dates back to 2004.)
Most of my research interests lie in the area of static typing. More precisely, I am interested in various flavors and applications of a technique known as type inference.
Type inference is a way of analyzing a program's behavior. It is static, that is, it does not require running the program at hand. It consists in associating with each program component a specification called a type. Furthermore, the type of every component can be deduced from the types of its sub-components according to predetermined rules. If this process succeeds, then the type associated with the whole program can be considered a description of its behavior. Thus, it provides certain guarantees about its execution. The most basic, and most common, guarantee is the absence of runtime errors; however, it is possible to imagine more ambitious type systems, capable of also providing security guarantees, such as the protection of certain sensitive resources or pieces of information against illegitimate use. If the type inference process fails, then no guarantee can be obtained, which often means that the program is faulted.
For several years, I have been interested in a technique called constraint-based type inference, which consists in refining the analysis by incorporating logic assertions of limited power, called constraints, within types. My Ph.D. thesis studies the case where these constraints are subtyping assertions, and is applied to a language of the ML family, that is, a lambda-calculus-based programming language. Since joining INRIA, I have pursued these investigations in several directions. First, I have studied an extension of the constraint language with so-called conditioal constraints, and showed that the system thus obtained is expressive enough to describe certain advanced features of modern programming languages, such as record concatenation, or the use of messages as first-class values in an object-oriented language. I have written a library for constraint resolution and simplification, called Wallace. Besides, I have studied constraint-based type inference in general, given a simplified soundness proof for the type system HM(X) -- a constraint-based type inference system for the lambda-calculus -- and adapted this system, together with Sylvain Conchon, to the join-calculus, a kernel language for concurrent and distributed programming.
Executing any program involves a risk, because the program may, purposely or not, damage or divulge sensitive information. Thus, it is desirable, before running the program, to be given some kind of guarantee about its behavior. I have taken interest in applications of type inference to this problem.
Two recent programming languages, Java and C, propose a dynamic access control mechanism. It consists in associating with each code fragment a set of access rights -- the more trusted that code fragment, the larger -- and in checking, during execution, that every resource access request is backed up by the corresponding rights. Furthermore, a costly stack inspection mechanism attempts to ensure that no attacker may indirectly cause a legitimate code fragment to wrongly make use of its rights. In joint work with Scott Smith and Christian Skalka, I have suggested that these checks may, to a certain extent, be performed statically, using a type inference system. This lessens their cost, and allows certain security violations to be detected prior to execution.
Every access control mechanism rests on the notion of trust, which is always subject to abuse. To eliminate this defect, researchers have imagined resorting to a program analysis, called information flow analysis. Such an analysis determines how the program manipulates the data which it is given, and is able, in principle, to guarantee that no confidential data can be divulged, and that no important data can be damaged. This analysis can be formulated as a type inference problem. I have showed, together with Sylvain Conchon, how to construct such an analysis in a systematic way for a purely functional language, and how to establish its correctness in a simple manner. Vincent Simonet and I have subsequently generalized these results to a language equipped with imperative features and with exceptions. Thus, we have established the correctness of an information flow analysis that is able to deal with the kernel of the ML language. This analysis has been implemented by Vincent Simonet in the Flow Caml system.