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 Java Bytecode using Logic Programming
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 = {Java 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 Java 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}
}
@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 = 69\%}
}
@INPROCEEDINGS{hubert10:secure_initialization,
AUTHOR = {Laurent Hubert and Thomas Jensen and Vincent},
TITLE = {Enforcing Secure Object Initialization in Java},
BOOKTITLE = {Proceeding of ESORICS 2010},
YEAR = 2010,
MONTH = {September},
PUBLISHER = {Springer},
SERIES = {LNCS},
PDF = {http://www.trebuh.net/publi/2010esorics.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 to prove the absence of bugs
which 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 our of
\texttt{java.lang}, \texttt{java.security} and
\texttt{javax.security}.}
}
@TECHREPORT{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: Static Analysis Workshop for Java},
INSTITUTION = {CNRS, INRIA, ENS Cachan},
YEAR = 2010,
TYPE = {Technical Report},
MONTH = {June},
NOTE = {Presented at the International Conference on Formal
Verification of Object-Oriented Software (FoVeOOS)},
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}
}