I am a research and development engineer working in a young start-up, Prove&Run. I obtained a PhD in computer science from the University of Rennes in December 2010. I previously obtained an Engineering degree and a Master degree from the National Institute of Applied Sciences (INSA) of Rennes.
For more information about my curriculum, please see the dedicated page.
- Static Analysis and Abstract Interpretation
- Java and Bytecode Verification
- Functional Programming
My work has been focused on the verification and analysis of Java bytecode programs. I have worked at the UPM with German Puebla on the decompilation from Java bytecode to PROLOG to be able to use the already developed analyses of PROLOG on those decompiled programs. In Rennes, with Thomas Genet, we have developed a software to compile Java bytecode programs to Term Rewriting Systems (TRS). With David Pichardie, we have worked on a null pointer analysis for Java bytecode, where the challenge is to deal with field initialization, on the initialization of classes, which is lazy in Java, and on a type-system to improve Java security by ensuring the correct initialization of objects.
This tool is a checker that verifies that a Java (bytecode) program respects an initialization policy. An initialization policy is a description, using Java annotations, of which variables (field, method parameter, receiver or return value) may point to an object under initialization (i.e., which has not finished its constructor). It allows to enforce the recommendation of Sun, the Cert, and Joshua Blosh in Effective Java to not allow partially initialized objects to be accessed.
- KFKC: Key-Free Key-Chain
KFKC is a kind of keychain, or password manager, which does not store any password and allows for very strong password. It uses different passwords for each website and each identity. It therefore offers a very high level of security. It works by computing a different password for each identity (login) and website from a master password using a cryptographic function (a hash function: SHA-1).
- NIT: Nullability Inference Tool
Nit infers nullness properties of variables and can in theory prove that a program is NullPointer-Exception free. In practice, it proves more than 80% of dereferences safe and allows finding suitable nullability annotations for fields, method parameters, return values and local variables.
- JavaLib & Sawja
JavaLib is a library to parse Java .class files (compiled classes) into OCaml data structures, thus enabling the OCaml programmer to extract information from class files, to manipulate and to generate valid class files. Sawja is a layer on top of JavaLib which ease the development of static analyzer by providing an implementation of some of the JVM algorithms useful for static analysis (method and field look-up and resolution, etc.). It also provides standard control flow analyses, a way to represent constraints on Java programs, a constraint solver, etc.
Foundations and Implementation of a Tool Bench for Static
Analysis of Java Bytecode Programs.
PhD thesis, Université de Rennes 1, December 2010.
[ bib |
In this thesis we study the static analysis of Java bytecode and its semantics foundations. The initialization of an information system is a delicate operation where security properties are enforced and invariants installed. Initialization of fields, objects and classes in Java are difficult operations. These difficulties may lead to security breaches and to bugs, and make the static verification of software more difficult. This thesis proposes static analyses to better master initialization in Java. Hence, we propose a null pointer analysis that finely tracks initialization of fields. It allows proving the absence of dereferencing of null pointers (NullPointerException) and refining the intra-procedural control flow graph. We present another analysis to refine the inter-procedural control flow due to class initialization. This analysis directly allows inferring more precise information about static fields. Finally, we propose a type system that allows enforcer secure object initialization, hence offering a sound and automatic solution to a known security issue. We formalize these analyses, their semantic foundations, and prove their soundness. Furthermore, we also provide implementations. We developed several tools from our analyses, with a strong focus at having sound but also efficient tools. To ease the adaptation of such analyses, which have been formalized on idealized languages, to the full-featured Java bytecode, we have developed a library that has been made available to the community and is now used in other research labs across Europe.
Laurent Hubert, Thomas Jensen, Vincent Monfort, and David Pichardie.
Enforcing secure object initialization in Java.
In Computer Security - ESORICS 2010, volume 6345 of
LNCS, pages 101-115. Springer, September 2010.
[ bib |
Sun and the CERT recommend for secure Java development to “not allow partially initialized objects to be accessed”. The solution currently used to enforce object initialization is to implement a coding pattern. We propose a modular type system to formally specify initialization policies and a type checker. The type system and its soundness theorem have been formalized and machine checked using Coq. This allows proving the absence of bugs that have allowed some famous privilege escalations in Java. Our experimental results show that by adding 57 simple annotations we proved safe all classes but 4 out of java.lang, java.security and javax.security.
Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine
Demange, Thomas Jensen, Vincent Monfort, David Pichardie, and Tiphaine
Sawja: Static Analysis Workshop for Java.
In Proc. of the International Conference on Formal Verification
of Object-Oriented Software (FoVeOOS), LNCS, 2010.
[ bib |
Static analysis is a powerful technique for automatic verification of programs but raises major engineering challenges when developing a full-fledged analyzer for a realistic language such as Java. This paper describes the Sawja library: a static analysis framework fully compliant with Java 6 which provides OCaml modules for efficiently manipulating Java bytecode programs. We present the main features of the library, including (i) efficient functional data-structures for representing program with implicit sharing and lazy parsing, (ii) an intermediate stack-less representation, and (iii) fast computation and manipulation of complete programs.
Laurent Hubert and David Pichardie.
Soundly handling static fields: Issues, semantics and analysis.
Electronic Notes in Theoretical Computer Science, 253(5):15 -
Proceedings of ByteCode'09.
[ bib |
Although in most cases class initialization works as expected, some static fields may be read before being initialized, despite being initialized in their corresponding class initializer. We propose an analysis that can be applied to identify the static fields that may be read before being initialized and show how this can improve the precision of a null-pointer analysis.
Keywords: Java, semantics, class initialization, static analysis, control flow, verification
A Non-Null annotation inferencer for Java bytecode.
In Proceedings of the Workshop on Program Analysis for Software
Tools and Engineering (PASTE'08), pages 36-42. ACM, November 2008.
[ bib |
We present a non-null annotations inferencer for the Java bytecode language. This paper proposes extensions to our former analysis in order to deal with the Java bytecode language. We have implemented both analyses and compared their behaviour on several benchmarks. The results show a substantial improvement in the precision and, despite being a whole-program analysis, production applications can be analyzed within minutes.
Keywords: Java, NonNull, annotation, inference, static analysis
Laurent Hubert, Thomas Jensen, and David Pichardie.
Semantic foundations and inference of non-null annotations.
In Proceedings of the international conference on Formal Methods
for Open Object-Based Distributed Systems (FMOODS '08), volume 5051 of
LNCS, pages 132-149. Springer Berlin, June 2008.
[ bib |
This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in object-oriented programs. We prove the analysis correct with respect to a semantics of a minimalistic OO language and complete with respect to the non-null type system proposed by Fähndrich and Leino, in the sense that for every typable program the analysis is able to prove the absence of null dereferences without any hand-written annotations. Experiments with a prototype implementation of the analysis show that the inference is feasible for large programs.
Keywords: Java, NonNull, annotation, inference, static analysis
|||Laurent Hubert, Thomas Jensen, and David Pichardie. Semantic foundations and inference of non-null annotations. Research Report 6482, INRIA, March 2008. [ bib | http ]|
|||Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert, and Germán Puebla. Verification of Java bytecode using analysis and transformation of logic programs. In Practical Aspects of Declarative Languages, LNCS, pages 124-139. Springer, 2007. [ bib | http | .pdf ]|
|||Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert, and Germán Puebla. Towards verification of Java bytecode using Logic Programming tools. In Proceedings of the International Workshop on Software Verification and Validation, Seattle, August 2006. Computing Research Repository (CoRR). Co-located with FLoC'06. [ bib | .pdf ]|
|||Laurent Hubert. Java bytecode verification using analysis and transformation of logic programs. Master's thesis, INSA de Rennes, June 2006. [ bib | .pdf ]|
|||Laurent Hubert. Memory and time consumption of Java bytecode programs. Technical report, INSA de Rennes, February 2006. [ bib | .pdf ]|