publi.bib
@inproceedings{ESOP12:Barthe:demange:Pichardie,
author = {Gilles Barthe and Delphine Demange and David Pichardie},
title = {A formally verified SSA-based middle-end - Static Single Assignment meets CompCert},
booktitle = {Proc. of 21th European Symposium on Programming (ESOP 2012)},
year = {2012},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
pdf = {papers/esop12.pdf},
note = {To appear},
abstract = {CompCert is a formally verified compiler that generates compact and
efficient PowerPC, ARM and x86 code for a large and realistic subset
of the C language. However, CompCert foregoes using Static Single
Assignment (SSA), an intermediate representation that allows for
writing simpler and faster optimizers, and is used by many
compilers. In fact, it has remained an open problem to verify
formally a SSA-based compiler middle-end.
We report on a formally verified, SSA-based, middle-end for
CompCert. Our middle-end performs conversion from CompCert
intermediate form to SSA form, optimization of SSA programs,
including Global Value Numbering, and transforming out of SSA to
intermediate form. In addition to provide the first formally
verified SSA-based middle-end, we address two problems
raised by Leroy: giving a simple and intuitive formal
semantics to SSA, and leveraging the global properties
of SSA to reason locally about program optimizations.}
}
@inproceedings{CPP11:Besson:Cornilleau:Pichardie,
author = {Frédéric Besson and Pierre-Emmanuel Cornilleau and David Pichardie},
title = {Modular SMT Proofs for Fast Reflexive Checking inside Coq},
booktitle = {Proc. of the 1st International Conference on Certified Programs and Proofs (CPP 2011)},
year = {2011},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
pdf = {papers/cpp11.pdf},
pages = {151-166},
volume = {7086},
abstract = { We present a new methodology for exchanging unsatisfiability
proofs between an untrusted SMT solver and a sceptical proof
assistant with computation capabilities like Coq. We advocate
modular SMT proofs that separate boolean reasoning and theory
reasoning; and structure the communication between theories
using Nelson-Oppen combination scheme. We present the design
and implementation of a Coq reflexive verifier that is modular
and allows for fine-tuned theory-specific verifiers. The
current verifier is able to verify proofs for quantifier-free
formulae mixing linear arithmetic and uninterpreted functions.
Our proof generation scheme benefits from the efficiency of
state-of-the-art SMT solvers while being independent from a
specific SMT solver proof format. Our only requirement for the
SMT solver is the ability to extract unsat cores and generate
boolean models. In practice, unsat cores are relatively small
and their proof is obtained with a modest overhead by our
proof-producing prover. We present experiments assessing the
feasibility of the approach for benchmarks obtained from the
SMT competition.}
}
@inproceedings{ESOP11:Jensen:Kirchner:Pichardie,
author = {Thomas Jensen and Florent Kirchner and David Pichardie},
title = {Secure the Clones: Static Enforcement of Policies for Secure Object Copying},
booktitle = {Proc. of 20th European Symposium on Programming (ESOP 2011)},
year = {2011},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
pdf = {papers/esop11.pdf},
pages = {317-337},
volume = {6602},
abstract = { Exchanging mutable data objects with untrusted code is a delicate
matter because of the risk of creating a data space that is
accessible by an attacker. Consequently, secure programming guidelines for
Java stress the importance of using defensive copying before accepting or
handing out references to an internal mutable object.
However, implementation of a copy method (like clone()) is entirely
left to the programmer. It may not provide a sufficiently deep copy of
an object and is subject to overriding by a malicious sub-class. Currently
no language-based mechanism supports secure object cloning.
This paper proposes a type-based annotation system for defining modular
copy policies for class-based object-oriented programs.
A copy policy specifies the maximally allowed sharing between an
object and its clone. We present a static
enforcement mechanism that will guarantee that all classes fulfill their
copy policy, even in the presence of overriding of copy methods, and
establish the semantic correctness of the overall approach in Coq.
The mechanism has been implemented and experimentally evaluated on
clone methods from several Java libraries.}
}
@article{TSI11:Cachera:Pichardie,
author = {David Cachera and David Pichardie},
title = {Programmation d'un interpr\'eteur abstrait certifi\'e en logique constructive},
journal = {Technique et Science Informatiques (TSI)},
year = 2011,
volume = {30},
number = {4},
year = {2011},
pages = {381-408}
}
@proceedings{BYTECODE10:Pichardie,
editor = {David Pichardie},
title = {Fifth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2010). Proceedings},
booktitle = {BYTECODE 2010},
series = {Electronic Notes in Theoretical Computer Science},
year = {2010}
}
@inproceedings{FOVEOOS10: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},
year = 2010,
booktitle = {Proc. of the 1st International Conference on Formal
Verification of Object-Oriented Software (FoVeOOS 2010)},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
pdf = {papers/foveoos10.pdf},
pages = {92-106},
volume = {6461},
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.
Efficiency and precision of such a tool rely partly on low level
components which only depend on the syntactic structure of the
language and therefore should not be redesigned for each
implementation of a new static analysis. This paper describes the
Sawja library: a static analysis workshop 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 a program with implicit sharing and lazy parsing,
ii) an intermediate stack-less representation, and iii) fast
computation and manipulation of complete programs. We provide
experimental evaluations of the different features with respect to
time, memory and precision.}
}
@inproceedings{APLAS10:Demange:Jensen:Pichardie,
author = {Delphine Demange and Thomas Jensen and David Pichardie},
title = {A Provably Correct Stackless Intermediate Representation for {J}ava Bytecode},
booktitle = {Proc. of the 8th Asian Symposium on Programming Languages and Systems (APLAS 2010)},
year = {2010},
pages = {97-113},
volume = {6461},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
pdf = {papers/aplas10.pdf},
abstract = {The Java virtual machine executes stack-based bytecode. The
intensive use of an operand stack has been identified as a
major obstacle for static analysis and it is now common for
static analysis tools to manipulate a stackless
intermediate representation (IR) of bytecode programs.
This paper provides such a bytecode
transformation, describes its semantic
correctness and evaluates its performance.
We provide the semantic foundations for proving that an initial
program and its IR behave similarly, in particular with respect
to object creation and throwing of exceptions. The correctness
of this transformation is proved with respect to a relation on
execution traces taking into account that the object allocation
order is not preserved by the transformation.}
}
@inproceedings{ESORICS10:Hubert:Pichardie,
author = {Laurent Hubert and Thomas Jensen and Vincent Monfort and David Pichardie},
title = {Enforcing Secure Object Initialization in {J}ava},
booktitle = {Proc. of the 15th European Symposium on Research in Computer Security (ESORICS 2010)},
year = {2010},
pages = {101-115},
volume = {6345},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
pdf = {papers/esorics10.pdf},
abstract = { Sun and the CERT recommend for secure Java development to not allow
partially initialized objects to be accessed. The CERT considers the
severity of the risks taken by not following this recommendation as
high. The solution currently used to enforce object initialization is
to implement a coding pattern proposed by Sun, which is not formally checked.
We propose a modular type system to formally specify the initialization policy
of libraries or programs and a type checker to statically check at load time
that all loaded classes respect the policy. This allows to prove the absence
of bugs which have allowed some famous privilege escalations in Java. Our
experimental results show that our safe default policy allows to prove 91\% of
classes of java.lang, java.security and
javax.security safe without any annotation and by adding 57 simple
annotations we proved all classes but four safe. The type system and its
soundness theorem have been formalized and machine checked using Coq.}
}
@inproceedings{ITP10:Cachera:Pichardie,
author = {David Cachera and David Pichardie},
title = {A Certified Denotational Abstract Interpreter},
booktitle = {Proc. of International Conference on Interactive Theorem Proving (ITP-10)},
year = {2010},
pages = {9-24},
volume = {6172},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
pdf = {papers/itp10.pdf},
abstract = {Abstract Interpretation proposes advanced techniques for static
analysis of programs that raise specific challenges for
machine-checked soundness proofs. Most classical dataflow analysis
techniques iterate operators on lattices without infinite ascending
chains. In contrast, abstract interpreters are looking for fixpoints
in infinite lattices where widening and narrowing are used for
accelerating the convergence. Smart iteration strategies are crucial
when using such accelerating operators because they directly impact
the precision of the analysis diagnostic. In this paper, we show
how we manage to program and prove correct in Coq an abstract
interpreter that uses iteration strategies based on program syntax.
A key component of the formalization is the introduction of an
intermediate semantics based on a generic least-fixpoint operator
on complete lattices and allows us to decompose the soundness proof in an
elegant manner.}
}
@inproceedings{TGC10:Besson:Jensen:Pichardie:Turpin,
author = {Fr\'ed\'eric Besson and Thomas Jensen and David Pichardie and Tiphaine Turpin},
title = {Certified Result Checking for Polyhedral Analysis of Bytecode Programs},
booktitle = {Proc. of the 5th International Symposium on Trustworthy Global Computing (TGC 2010)},
year = {2010},
pages = {253-267},
volume = {6084},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
pdf = {papers/tgc10.pdf}
}
@inproceedings{SSTIC10:JAVASEC,
author = {Guillaume Hiet and Frédéric Guihéry and Goulven Guiheux and David Pichardie and Christian Brunette},
title = {S\'ecurit\'e de la plate-forme d'ex\'ecution {J}ava : limites et propositions d'am\'eliorations},
booktitle = {Proc. of Symposium sur la s\'ecurit\'e des technologies de l'information et des communications (SSTIC 2010)},
year = {2010},
pdf = {papers/sstic10.pdf}
}
@article{JCS10:Besson:Jensen:Dufay:Pichardie,
author = {Fr\'ed\'eric Besson and Thomas Jensen and Guillaume Dufay and David Pichardie},
title = {Verifying Resource Access Control on Mobile Interactive Devices},
journal = {Journal of Computer Security},
volume = {18},
number = {6},
pages = {971-998},
year = 2010,
pdf = {papers/jcs10.pdf}
}
@inproceedings{FOSAD09:BessonCacheraJensenPichardie,
author = {Fr{\'e}d{\'e}ric Besson and
David Cachera and
Thomas P. Jensen and
David Pichardie},
title = {Certified Static Analysis by Abstract Interpretation},
booktitle = {Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009
Tutorial Lectures},
year = {2009},
pages = {223-257},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {5705},
pdf = {papers/fosad09.pdf}
}
@inproceedings{TPHOLs09:Dabrowski:Pichardie,
author = {Fr\'ed\'eric Dabrowski and David Pichardie},
title = {A Certified Data Race Analysis for a {J}ava-like Language},
booktitle = {Proc. of 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09)},
year = {2009},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {5674},
pages = {212-227},
pdf = {papers/tphols09.pdf}
}
@article{NFM09:Cachera:Pichardie,
author = {David Cachera and David Pichardie},
title = {Comparing Techniques for Certified Static Analysis},
journal = {Proc. of the 1st NASA Formal Methods Symposium (NFM'09)},
year = {2009},
pages = {111-115},
publisher = {NASA Ames Research Center },
pdf = {papers/nfm09.pdf}
}
@article{BYTECODE09:Hubert:Pichardie,
author = {Laurent Hubert and David Pichardie},
title = {Soundly Handling Static Fields: Issues, Semantics and Analysis},
journal = {Proc. of the 4th International Workshop on
Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09)},
series = {Electronic Notes in Theoretical Computer Science},
year = {2009},
volume = {253},
number = {5},
pages = {15-30},
pdf = {papers/bytecode09.pdf}
}
@inproceedings{SEFM08:Barthe:Kunz:Pichardie:Forlese,
author = {Gilles Barthe and C\'esar Kunz and David Pichardie and Juli\'an Samborski Forlese},
title = {Preservation of Proof Obligations for Hybrid Certificates},
booktitle = {Proc. of the 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08)},
year = {2008},
publisher = {IEEE Computer Society},
pages = {127-136},
pdf = {papers/sefm08.pdf}
}
@inproceedings{FMOODS08:HubertJensenPichardie,
author = {Laurent Hubert and Thomas Jensen and David Pichardie},
title = {{Semantic foundations and inference of non-null annotations}},
booktitle = {Proc. of the 10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08)},
year = {2008},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {5051},
pages = {132-149},
pdf = {papers/fmoods08.pdf}
}
@inproceedings{FICS08:Pichardie,
author = {David Pichardie},
title = {{Building certified static analysers by modular construction of well-founded lattices}},
year = 2008,
series = {Electronic Notes in Theoretical Computer Science},
booktitle = {Proc. of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS'08)},
pdf = {papers/fics08.pdf},
volume = {212},
pages = {225-239}
}
@inproceedings{FMCO7:BCGJP,
author = {Gilles Barthe and Pierre Cr\'egut and Benjamin Gr\'egoire and Thomas Jensen and David Pichardie},
title = {{The MOBIUS Proof Carrying Code infrastructure}},
booktitle = {Proc. of the 6th International Symposium on Formal Methods for Components and Objects (FMCO'07)},
year = {2007},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {5382},
pages = {1-24}
}
@inproceedings{BPR07,
author = {Gilles Barthe and David Pichardie and Tamara Rezk},
title = {{A Certified Lightweight Non-Interference {J}ava Bytecode Verifier}},
booktitle = {Proc. of 16th European Symposium on Programming (ESOP'07)},
year = {2007},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {4421},
pages = {125-140},
pdf = {papers/esop07.pdf}
}
@article{TCSAppSem:BessonJensenPichardie,
author = {Fr\'ed\'eric Besson and Thomas Jensen and David Pichardie},
title = {Proof-Carrying Code from Certified Abstract Interpretation to Fixpoint Compression},
journal = {Theoretical Computer Science},
year = 2006,
volume = 364,
number = 3,
pages = {273--291},
pdf = {papers/tcs06.pdf}
}
@inproceedings{EAAI:BessonJensenPichardie,
author = {Fr\'ed\'eric Besson and Thomas Jensen and David Pichardie},
title = {{A PCC Architecture based on Certified Abstract Interpretation}},
publisher = {Springer-Verlag},
year = 2006,
series = {ENTCS},
booktitle = {Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06)},
pdf = {papers/eaai06.pdf}
}
@inproceedings{BartheFPR06,
author = {Gilles Barthe and
Julien Forest and
David Pichardie and
Vlad Rusu},
title = {Defining and Reasoning About Recursive Functions: A Practical
Tool for the Coq Proof Assistant.},
pages = {114-129},
booktitle = {Proc. of 8th International Symposium on Functional and Logic Programming (FLOPS'06)},
series = {Lecture Notes in Computer Science},
publisher = {{Springer-Verlag}},
volume = {3945},
year = {2006},
pdf = {papers/flops06.pdf}
}
@phdthesis{Pich:these,
author = {Pichardie David},
title = {Interprétation abstraite en logique intuitionniste~: extraction d'analyseurs {J}ava certifiés},
school = {Université Rennes~1},
year = {2005},
pdf = {papers/these-pichardie.pdf},
note = {In french}
}
@inproceedings{Pich05ParamConcr,
author = {David Pichardie},
title = {Modular proof principles for parameterized concretizations},
booktitle = {Proc. of 2nd International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2005)},
year = {2005},
number = {3956},
pages = {138--154},
series = {Lecture Notes in Computer Science},
publisher = {{Springer-Verlag}},
pdf = {papers/param.pdf}
}
@inproceedings{CaJePiSc05MemoryUsage,
author = {David Cachera and Thomas Jensen and David Pichardie and Gerardo Schneider},
title = {{Certified Memory Usage Analysis}},
booktitle = {Proc. of 13th International Symposium on Formal Methods (FM'05)},
year = {2005},
pages = {91--106},
number = {3582},
series = {Lecture Notes in Computer Science},
publisher = {{Springer-Verlag}},
pdf = {papers/memoryusage.pdf}
}
@article{CaJePiRu05TCSExtractAnalyser,
author = {David Cachera and Thomas Jensen and David Pichardie and Vlad Rusu},
title = {{Extracting a Data Flow Analyser in Constructive Logic}},
journal = {Theoretical Computer Science},
year = {2005},
volume = {342},
number = {1},
pages = {56-78},
month = {September},
pdf = {papers/extract_TCS.pdf},
note = {Extended version of \cite{CaJePiRu04ExtractAnalyser}}
}
@inproceedings{CaJePiRu04ExtractAnalyser,
author = {David Cachera and Thomas Jensen and David Pichardie and Vlad Rusu},
title = {{Extracting a Data Flow Analyser in Constructive Logic}},
booktitle = {Proc. of 13th European Symposium on Programming (ESOP'04)},
year = {2004},
pages = {385--400},
number = {2986},
series = {Lecture Notes in Computer Science},
publisher = {{Springer-Verlag}},
pdf = {papers/extractDataFlow.pdf}
}
@inproceedings{GeJeKoPi04Converter,
author = {Thomas Genet and Thomas Jensen and Vikash Kodati and David Pichardie},
title = {{A {J}ava Card CAP converter in PVS}},
booktitle = {Proc. of 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003), Electronic Notes in Theoretical Computer Science},
volume = {82},
issue = {2},
publisher = {{Elsevier}},
editor = {Jens Knoop and Wolf Zimmermann},
year = {2004},
pdf = {papers/capConverter.pdf}
}
@inproceedings{CaPi03AffineRec,
author = {David Cachera and David Pichardie},
title = {{Embedding of Systems of Affine Recurrence Equations in Coq}},
booktitle = {Proc. of 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03)},
year = {2003},
pages = {155--170},
number = {2758},
series = {Lecture Notes in Computer Science},
publisher = {{Springer-Verlag}},
pdf = {papers/embedSARE.pdf}
}
@inproceedings{BePi01Convexhull,
author = {David Pichardie and Yves Bertot},
title = {{Formalizing Convex Hulls Algorithms}},
booktitle = {Proc. of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01)},
year = {2001},
pages = {346--361},
number = {2152},
series = {Lecture Notes in Computer Science},
publisher = {{Springer-Verlag}},
pdf = {papers/hulls.pdf}
}
This file was generated by bibtex2html 1.95.