Thomas Jensen

Thomas Jensen 

INRIA 
Campus de Beaulieu, 35042 Rennes, France

Tel: (+33 / 0) 2 99 84 74 78 
Fax: (+33 / 0) 2 99 84 71 71 


SHORT CV

Directeur de recherche INRIA.

Cand. scient. in Computing and Mathematics, University of Copenhagen,1990. PhD Imperial College, Univ. of London,1992. Habilitation à diriger des recherches, Université Rennes 1, 1999.
In 1993 I joined the CNRS as Chargé de recherche at the Computing Laboratory at Ecole Polytechnique. From 1997, I have been affiliated with IRISA, Rennes where I became directeur de recherche CNRS in 2003. Since 2010 I am at INRIA where I have been leader of the Lande research team (1999-2009) and the Celtique team (2009-2022). Since 2022, I am in charge of the Epicure project-team on semantic analysis and compilation for secure execution platforms. 

SOME RECENT PUBLICATIONS

List of publications (2022)


RESEARCH AREAS

Program analysis

Static program analysis aims at determining properties of the behaviour of a program without actually executing it. Static analysis is founded on the theory of abstract interpretation for proving the correctness of analyses with respect to the semantics of a programming language.  My work has among other things been concerned with
  • type-based static analysis
  • analyses for the particular language paradigms (in particular functional and object-oriented) 
  • control-flow analysis of programs, used e.g. in the activity on software security
  • certification of static analysis
Some recent publications:
  • Analysis of model transformation languages: A. Salim Al-Sibahi, A. S. Dimovski, T. Jensen, A. Wasowski, Verification of High-Level Transformations with Inductive Refinement Types, 17th ACM Int. Conference on Generative Programming: Concepts & Experience GPCE 2018, p. 1–14, November 2018. Best paper award.
  • Abstract interpretation from big-step operational semantics: M. Bodin, Ph. Gardner, T. Jensen, A. Schmitt. Skeletal semantics and their interpretations. Proc. of 46th ACM Symp. on Principles of Programming Languages (POPL 2019). 2019.
  • Inter-procedural relational I/O analysis: O. Andreescu, T. Jensen, S. Lescuyer, B. Montagu. Inferring frame conditions with static correlation analysis. Proc. of 46th ACM Symp. on Principles of Programming Languages (POPL 2019). 2019.

I have been working on security of various versions of embedded Java, including Java Card and Java for mobile telephones. Java security can be further enhanced by extending the static byte code verification to other properties. The  SAWJACard project developed a tool for certifying Java Card applications according to NFC industry norms.
  • F. Besson, T. Jensen, P. Vittet. SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. Proc. of 21st Static Analysis Symposium (SAS 2014). Springer LNCS vol. 8858, pp. 51 – 67, 2014.

Software security

The particular branch of information security called "language-based security"  is concerned with the study of programming language features for ensuring the security  of software. Programming languages such as Java offer a variety of language constructs for securing an application. Verifying that these constructs have been used properly to ensure a given security property is a challenge for program analysis,

I am interested in mixing static and dynamic program analysis for precise information flow control. Such hybrid analysis aims at computing a precise estimation of attacker knowledge, with application eg. to identification of web tracking scripts.
  •  N . Bielova, F. Besson, T. Jensen. Hybrid information flow analysis against web tracking. Proc. of Symp. on Computer Security Foundations (CSF’13), pp. 240–254, IEEE, 2013
  • N. Bielova, F. Besson, T. Jensen. Hybrid monitoring of attacker knowledge. Proc. of Symp. on Computer Security Foundations (CSF’16), pp. 225—238, IEEE, 2016.

Software Fault Isolation is a technique for executing untrusted code without jeopardizing the host system's integrity, by placing the code in a sandbox that limits its actions. Classical SFI relies on a code verifier that checks that the sandboxing is done correctly. This verifiercan be formalized as an abstract interpretation:

  • F. Besson, T. Jensen, J. Lepiller. Modular Software Fault Isolation as Abstract Interpretation. Proc. of 25th International Static Analysis Symposium (SAS 2018). Springer LNCS vol. 11002, pp. 166-186, 2018.

It is also possible to do away with the a posteriori verifier by integrating SFI in to a verified compiler such as CompCert:

  • Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas Jensen, Pierre Wilke. Compiling Sandboxes: Formally Verified Software Fault Isolation. 19th European Symposium On Programming (ESOP 2019). Springer LNCS vol. 11423, pp. 499-524, 2019.

SELECTED RESEARCH PROJECTS (past and present)