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{\'e} 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
}