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
}