biblio.bib


@inproceedings{albert06:_towar_verif_java_bytec_logic_progr_tools,

  author = {Elvira Albert and Miguel G{\'o}mez-Zamalloa and Laurent Hubert

                  and Germ{\'a}n Puebla},

  title = {Towards Verification of {J}ava Bytecode using {L}ogic

                  {P}rogramming Tools},

  booktitle = {Proceedings of the International Workshop on Software

                  Verification and Validation},

  publisher = {Computing Research Repository (CoRR)},

  note = {Co-located with FLoC'06},

  year = 2006,

  address = {Seattle},

  month = {August},

  pdf = {http://www.trebuh.net/publi/2006svv.pdf}

}


@inproceedings{albert07:_verif_java_bytec_trans_analy,

  author = {Elvira Albert and Miguel G{\'o}mez-Zamalloa and Laurent Hubert

                  and Germ{\'a}n Puebla},

  title = {Verification of {J}ava Bytecode Using Analysis and

                  Transformation of Logic Programs},

  booktitle = {Practical Aspects of Declarative Languages},

  series = {LNCS},

  year = 2007,

  pages = {124-139},

  publisher = {Springer},

  url = {http://dx.doi.org/10.1007/978-3-540-69611-7_8},

  pdf = {http://www.trebuh.net/publi/2007padl.pdf},

  acceptance = {Acceptance rate : 19/58=32.8\%}

}


@mastersthesis{hubert06:_java_verif_analy_trans_logic_progr,

  author = {Laurent Hubert},

  title = {{J}ava bytecode Verification using Analysis and Transformation

                  of Logic Programs},

  school = {INSA de Rennes},

  year = 2006,

  month = {June},

  pdf = {http://www.trebuh.net/publi/MasterThesis.pdf}

}


@techreport{hubert06:_memory_and_time_consumption,

  author = {Laurent Hubert},

  title = {Memory and Time Consumption of {J}ava Bytecode Programs},

  institution = {INSA de Rennes},

  year = 2006,

  month = {February},

  pdf = {http://www.trebuh.net/publi/BibReport.pdf}

}


@techreport{hubert08:nonnull_annotations_inference,

  author = {Laurent Hubert and Thomas Jensen and David Pichardie},

  title = {Semantic foundations and inference of non-null annotations},

  year = 2008,

  month = {March},

  institution = {INRIA},

  number = 6482,

  type = {Research Report},

  url = {http://hal.inria.fr/inria-00266171/en/}

}


@inproceedings{hubert08-1:nonnull_annotations_inference,

  author = {Laurent Hubert and Thomas Jensen and David Pichardie},

  title = {Semantic foundations and inference of non-null annotations},

  booktitle = {Proceedings of the international conference on Formal Methods

                  for Open Object-Based Distributed Systems (FMOODS '08)},

  isbn = {978-3-540-68862-4},

  pages = {132-149},

  year = 2008,

  series = {LNCS},

  volume = 5051,

  month = {June},

  publisher = {Springer Berlin},

  keywords = {Java, NonNull, annotation, inference, static analysis},

  abstract = {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.},

  url = {http://dx.doi.org/10.1007/978-3-540-68863-1_9},

  pdf = {http://www.trebuh.net/publi/2008fmoods.pdf},

  slides = {http://www.trebuh.net/publi/2008fmoods_slides.pdf},

  acceptance = {acceptance rate : 14/36 = 38.9\%}

}


@inproceedings{hubert08-2:nonnull_annotation_inferencer,

  author = {Laurent Hubert},

  title = {A {Non-Null} Annotation Inferencer for {J}ava bytecode},

  booktitle = {Proceedings of the Workshop on Program Analysis for Software

                  Tools and Engineering (PASTE'08)},

  year = 2008,

  month = {November},

  publisher = {ACM},

  isbn = {978-1-60558-382-2},

  pages = {36--42},

  url = {http://doi.acm.org/10.1145/1512475.1512484},

  pdf = {http://www.trebuh.net/publi/2008paste.pdf},

  slides = {http://www.trebuh.net/publi/2008paste_slides.pdf},

  abstract = {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},

  acceptance = {acceptance rate : 13/26 = 50\%}

}


@article{hubert09:soundly_handling_static_fields,

  title = {Soundly Handling Static Fields: Issues, Semantics and

                  Analysis},

  journal = {Electronic Notes in Theoretical Computer Science},

  volume = 253,

  number = 5,

  pages = {15 - 30},

  year = 2009,

  note = {Proceedings of ByteCode'09},

  issn = {1571-0661},

  url = {http://dx.doi.org/10.1016/j.entcs.2009.11.012},

  author = {Laurent Hubert and David Pichardie},

  keywords = {Java, semantics, class initialization, static analysis,

                  control flow, verification},

  pdf = {http://www.trebuh.net/publi/2009bytecode.pdf},

  slides = {http://www.trebuh.net/publi/2009bytecode_slides.pdf},

  abstract = {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.},

  acceptance = {acceptance rate : 11/16 = 68.8\%}

}


@inproceedings{hubert10:secure_initialization,

  author = {Laurent Hubert and Thomas Jensen and Vincent Monfort and David

                  Pichardie},

  title = {Enforcing Secure Object Initialization in {J}ava},

  booktitle = {Computer Security --- ESORICS 2010},

  acceptance = {acceptance rate : 42/201 = 20.9\%},

  year = 2010,

  month = {September},

  publisher = {Springer},

  series = {LNCS},

  volume = 6345,

  isbn = {978-3-642-15496-4},

  pages = {101--115},

  pdf = {http://www.trebuh.net/publi/2010esorics.pdf},

  slides = {http://www.trebuh.net/publi/2010esorics_slides.pdf},

  abstract = {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

                  \texttt{java.lang}, \texttt{java.security} and

                  \texttt{javax.security}.}

}


@inproceedings{hubert10:sawja,

  author = {Laurent Hubert and Nicolas Barré and

                  Frédéric Besson and Delphine Demange and Thomas

                  Jensen and Vincent Monfort and David Pichardie and Tiphaine

                  Turpin},

  title = {Sawja: {S}tatic {A}nalysis {W}orkshop for {J}ava},

  booktitle = {Proc. of the International Conference on Formal Verification

                  of Object-Oriented Software (FoVeOOS)},

  year = 2010,

  series = {LNCS},

  abstract = {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.},

  pdf = {http://www.trebuh.net/publi/2010foveoos.pdf},

  slides = {http://www.trebuh.net/publi/2010foveoos_slides.pdf},

  note = {To appear},

  acceptance = {acceptance rate : 11/35 = 31.4\%}

}


@phdthesis{hubert10:thesis:foundations_SA_java_bytecode,

  author = {Laurent Hubert},

  title = {Foundations and Implementation of a Tool Bench for Static

                  Analysis of Java Bytecode Programs},

  school = {Université de Rennes 1},

  year = 2010,

  abstract = {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 (\texttt{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.  },

  pdf = {http://www.trebuh.net/publi/PhDThesis.pdf},

  slides = {http://www.trebuh.net/publi/PhDThesis_slides.pdf},

  month = dec

}