.Curriculum.Vitae

Here is an online version of my curriculum vitae. I will try to keep it updated.

If you print this version, it should output a nice paper version (although not as pretty as a word-processed curriculum vitae).

.Address

Laurent HUBERT
30 A, rue de Alain Gerbault
35 000 Rennes
FRANCE

laurentanti-spam@trebuh.net

.Personal.Details

Date of birth: 8^th August, 1983.
French nationality
Driving license

.Languages

French: Native

English: Fluent

Spanish: Working

.Work.Experiences

Research & development engineer

Since January 2011 - Prove & Run - Paris (France)

PhD student

October 2010 - December 2010 - 3 months - INRIA Rennes / IRISA - Rennes (France)

October 2007 - September 2010 - 3 years - CNRS/IRISA lab - Rennes (France)

Development of a framework for the conception of security analyses for embedded Java programs. (With Thomas Jensen and David Pichardie.)
During my PhD, I have contributed to several publications and tools. I have reviewed papers for international conferences and attended to different workshops and conferences, either as speaker or auditor. I also participated to several courses, either a few hours long or several days long. While I learned some management techniques in some of these courses, I also had the chance to put them into practice during several occasions:

• the organization of weekly meetings about the development of our libraries Javalib and Sawja;
• with an intern on a project of a web application to demonstrate static analyzers;
• with another intern on a the study of some optimization for the HotSpot JVM;
• with engineers on software development projects.

Teaching

In 2008 & 2009 - 120 hours - INSA - Rennes (France)

Professor assistant - coursework for under-graduate and post-graduate students on the Java Programming Language, the Scheme Programming Language, the Emacs Text Editor and Compilation Techniques

In 2007 - 50 hours - University of Leeds (United Kingdom)

Marker - assessment of under-graduate students in computing and computer science in Databases, Formal Methods (Z), program semantics, Python and Java

In 2005 - 25 hours - University of Rennes 2 - Rennes (France) - Office Automation Instructor

In 2005 - 41 hours - Domicours - Rennes (France) - Private Mathematics Teacher

Software engineer

March - June 2007 - 4 months - IRISA (INRIA) - Rennes (France)

Maintenance of a tool which transforms Java bytecode programs into rewriting systems encoding their semantics

September 2006 - February 2007 - 6 months - IRISA (CNRS) - Rennes (France)

Design and development of a null pointer analysis for Java bytecode that could be certified

Intern

February - June 2006 - 5 months - Technical University of Madrid (Spain)

Java bytecode verification via transformation and analysis of logic programs (cf. Master's Thesis)

July - August 2005 - 2 months - IRISA (INRIA) - Rennes (France)

Over-approximation of the number of iterations of intra-procedural loops

June - July 2003 - 10 weeks - La Poste - Nantes (France)

Development of a tool to extract data from HTML files and transfert them in a database

.Education

PhD in computer science - December, 2010
(Doctorat de l'Universitée de Rennes 1 en informatique)

Master of Science in computer science - 3 years - 2006
(Master de recherche et Diplôme d'ingénieur INSA)

INSA (National Institute of Applied Science) of Rennes / University of Rennes 1 - France

Subjects: proof assistants (PVS), test, semantics and abstract interpretation, the B method, compilation, computability and complexity, information system security, ray tracing, object oriented design (UML), object oriented programming (C++ and Java), functional programming (Caml), logic programming (Prolog), constraint programming, operating systems, network protocols, databases.

Bachelor of Science - 2 years - 2003
(Diplôme Universitaire de Technologie)

University of Nantes - France

Subjects: data structures, computer and system architecture, parallel programming, databases, networks, software engineering, web technologies.

.Publications

[1]	Laurent Hubert. Foundations and Implementation of a Tool Bench for Static Analysis of Java Bytecode Programs. PhD thesis, Université de Rennes 1, December 2010. [ bib | slides | .pdf ] 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.
[2]	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 | slides | .pdf ] 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.
[3]	Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie, and Tiphaine Turpin. Sawja: Static Analysis Workshop for Java. In Proc. of the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), LNCS, 2010. To appear. [ bib | slides | .pdf ] 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.
[4]	Laurent Hubert and David Pichardie. Soundly handling static fields: Issues, semantics and analysis. Electronic Notes in Theoretical Computer Science, 253(5):15 - 30, 2009. Proceedings of ByteCode'09. [ bib | slides | http | .pdf ] 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
[5]	Laurent Hubert. 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 | slides | http | .pdf ] 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
[6]	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 | slides | http | .pdf ] 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
[7]	Laurent Hubert, Thomas Jensen, and David Pichardie. Semantic foundations and inference of non-null annotations. Research Report 6482, INRIA, March 2008. [ bib | http ]
[8]	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 ]
[9]	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 ]
[10]	Laurent Hubert. Java bytecode verification using analysis and transformation of logic programs. Master's thesis, INSA de Rennes, June 2006. [ bib | .pdf ]
[11]	Laurent Hubert. Memory and time consumption of Java bytecode programs. Technical report, INSA de Rennes, February 2006. [ bib | .pdf ]

.Long.Life.Learning

National Innovation Systems in Europe, College of Doctoral Schools of Rennes (CED)

November 2010 - 4 hours

Key factors in the success of innovations, College of Doctoral Schools of Rennes (CED)

4 hours - November 2010

Code Obfuscation, by D. Pichardie and O. Heen

2 hours - November 2009

Maven, Ifsic

2 hours - November 2009

English, Matisse Doctoral School

20 hours - from March to Mai 2009

Challenge of entrepreneurs (Challenge des Entrepreneuriales), KIOSE

60 hours - from November 2008 to March 2009

Communication and management of teams and projects, College of Doctoral Schools of Rennes (CED)

3 days - December 2008

Summer School on Programming Languages (EJCP), Inria

3.5 days - June 2008

School on Security of Software and Contents, Irisa

2.5 days - January 2008

Introduction to entrepreneurism, Inria Transfer

3 days - January 2008

.Reviews.for.Colloquiums

International Conference on Software Testing, Verification and Validation (ICST), 2010

International Symposium on Applied Computing (SAC), track Software Verification, 2008

International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (ByteCode), 2009

.Attended.Colloquiums

• FMCO, Graz (Austria), December 2010, orator.
• ESORICS, Athene (Greece), September 2010, orator.
• FoVeOOS, Paris (France), June 2010, orator.
• COST Action IC0701, Lisbon (Portugal), June 2009, auditor.
• JavaOne, San Fransisco (USA), June 2009, demonstrator.
• ETAPS, York (UK), Mars 2009, auditor.
• ByteCode, York (UK), Mars 2009, orator.
• COST Action IC0701, Madrid (Spain), December 2008, orator.
• FSE, Atlanta (USA), November 2008, auditor.
• PASTE, Atlanta (USA), November 2008, orator.
• FMOODS, Oslo (Norway), June 2008, orator.
• ETAPS, Budapest (Hungary), Mars 2008, auditor.

.Associative.Experiences

2009 - 1 year

Treasurer of Nicomaque (Federation of the associations of PhD candidates and young researchers of Rennes) - Rennes (France)

2008 - 1 year

Treasurer of ADOC (association of PhD candidates and young researchers of the IRISA lab) - Rennes (France)

2005 - 5 months

President of Ouest Insa Junior Entreprise (information on the concept on www.jadenet.org) - Rennes (France)

2004 - 1 year

Member of Ouest Insa Junior Entreprise - Rennes (France)