[1]  Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, and Alix Trieu. Verified translation validation of static analyses. In IEEE 30th Computer Security Foundations Symposium, CSF 2017. IEEE Computer Society, 2017. [ bib ] 
[2]  Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, and Jan Vitek. Verifying a concurrent garbage collector using a relyguarantee methodology. In Proc. of the 8th International Conference on Interactive Theorem Proving (ITP 2017), volume 10499 of Lecture Notes in Computer Science. SpringerVerlag, 2017. [ bib ] 
[3]  Sandrine Blazy, David Pichardie, and Alix Trieu. Verifying constanttime implementations by abstract interpretation. In Proc. of the 22nd European Symposium on Research in Computer Security (ESORICS 2017), volume 10492 of Lecture Notes in Computer Science. SpringerVerlag, 2017. [ bib ] 
[4]  Sandrine Blazy, Vincent Laporte, and David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Lowlevel Selfmodifying Code. Journal of Automated Reasoning, 56(3):26, 2016. [ bib  http ] 
[5]  Sandrine Blazy, Vincent Laporte, and David Pichardie. An Abstract Memory Functor for Verified C Static Analyzers. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), page 14, Nara, Japan, September 2016. ACM. [ bib  http ] 
[6]  Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. A verified informationflow architecture. Journal of Computer Security, 24(6):689734, 2016. [ bib  http ] 
[7] 
Sandrine Blazy, Delphine Demange, and David Pichardie.
Validating dominator trees for a fast, verified dominance test.
In Proc. of the 6th International Conference on Interactive
Theorem Proving (ITP 2015), Lecture Notes in Computer Science. Springer,
2015.
[ bib 
.pdf ]
The problem of computing dominators in a control flow graph is central to numerous modern compiler optimizations. Many efficient algorithms have been proposed in the litterature, but mechanizing the correctness of the most sophisticated algorithms is still considered as too hard problems, and to this date, verified compilers use less optimized implementations. In contrast, production compilers, like GCC or LLVM, implement the classic, efficient LengauerTarjan algorithm, to compute dominator trees. And subsequent optimization phases can then determine whether a CFG node dominates another node in constant time by using their respective depthfirst search numbers in the dominator tree.

[8] 
Delphine Demange David Pichardie and Léo Stefanesco.
Verifying fast and sparse ssabased optimizations in coq.
In Proc. of the 24th International Conference on Compiler
Construction (CC 2015), Lecture Notes in Computer Science. Springer, 2015.
[ bib 
.pdf ]
Abstract The Static Single Assignment (SSA) form is a predominant technology in modern compilers, enabling powerful and fast program optimizations. Despite its great success in the implementation of pro duction compilers, it is only very recently that this technique has been introduced in verified compilers. As of today, few evidence exist on that, in this context, it also allows faster and simpler optimizations. This work builds on the CompCertSSA verified compiler (an SSA branch of the verified CompCert C compiler). We implement and verify two prevail ing SSA optimizations: Sparse Conditional Constant Propagation and Global Value Numbering. For both transformations, we mechanically prove their soundness in the Coq proof assistant. Both optimization proofs are embedded in a single sparse optimization framework, factoring out many of the dominancebased reasoning steps required in proofs of SSAbased optimizations. Our experimental evaluations indicate both a better precision, and a significant compilation time speedup.

[9] 
JacquesHenri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David
Pichardie.
A formallyverified C static analyzer.
In 42nd symposium Principles of Programming Languages, pages
247259. ACM Press, 2015.
[ bib 
.pdf ]
This paper reports on the design and soundness proof, using the Coq proof assistant, of Verasco, a static analyzer based on abstract interpretation for most of the ISO C 1999 language (excluding recursion and dynamic allocation). Verasco establishes the absence of runtime errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and nonrelational. Verasco integrates with the CompCert formallyverified C compiler so that not only the soundness of the analysis results is guaranteed with mathematical certitude, but also the fact that these guarantees carry over to the compiled code.

[10] 
Sandrine Blazy, André Maroneze, and David Pichardie.
Verified validation of program slicing.
In Proc. of the 5th Conference on Certified Programs and Proofs,
CPP 2015. ACM, 2015.
[ bib 
.pdf ]
Program slicing is a wellknown program transformation which simplifies a program with respect to a given criterion while preserving its semantics. Since the seminal paper published by Weiser in 1981, program slicing is still widely used in various application domains. State of the art program slicers operate over program de pendence graphs (PDG), a sophisticated data structure combining data and control dependences. In this paper, we follow the a posteriori validation approach to formally verify (in Coq) a general program slicer. Our validator for program slicing is efficient and validates the results of a run of an unverified program slicer. Program slicing is interesting for a posteriori validation because the correctness proof of program slicing requires to compute new supplementary information from the PDG, thus decoupling the slicing algorithm from its proof. Our semanticspreserving program slicer is integrated into the CompCert formally verified compiler. It operates over an intermediate language of the compiler having the same expressiveness as C. Our experiments show that our formally verified validator scales on large realistic programs.

[11] 
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, and David
Pichardie.
Systemlevel noninterference for constanttime cryptography.
In ACM SIGSAC Conference on Computer and Communications
Security, CCS'14. ACM, 2014.
[ bib 
.pdf ]
Cachebased attacks are a class of sidechannel attacks that are particularly effective in virtualized or cloudbased environments, where they have been used to recover secret keys from cryptographic implementations. One common approach to thwart cachebased attacks is to use constanttime implementations, i.e., which do not branch on secrets and do not perform memory accesses that depend on secrets. However, there is no rigorous proof that constanttime implementations are protected against concurrent cacheattacks in virtualization platforms with shared cache; moreover, many prominent implementations are not constanttime. An alternative approach is to rely on systemlevel mechanisms. One recent such mechanism is stealth memory, which provisions a small amount of private cache for programs to carry potentially leaking computations securely. Stealth memory induces a weak form of constanttime, called Sconstanttime, which encompasses some widely used cryptographic implementations. However, there is no rigorous analysis of stealth memory and Sconstanttime, and no tool support for checking if applications are Sconstanttime. We propose a new informationflow analysis that checks if an x86 application executes in constanttime, or in Sconstanttime. Moreover, we prove that constanttime (resp. Sconstanttime) programs do not leak confidential information through the cache to other operating systems executing concurrently on virtualization platforms (resp. platforms supporting stealth memory). The soundness proofs are based on new theorems of independent interest, including isolation theorems for virtualization platforms (resp. platforms supporting stealth memory), and proofs that constanttime implementations (resp. Sconstanttime implementations) are noninterfering with respect to a strict information flow policy which disallows that control flow and memory accesses depend on secrets. We formalize our results using the Coq proof assistant and we demonstrate the effectiveness of our analyses on cryptographic implementations, including PolarSSL AES, DES and RC4, SHA256 and Salsa20.

[12] 
Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, and Jan
Vitek.
Atomicity refinement for verified compilation.
ACM Trans. Program. Lang. Syst. (TOPLAS), 36(2):1, 2014.
[ bib 
.pdf ]
We consider the verified compilation of highlevel managed languages like Java or C# whose intermediate representations provide support for sharedmemory synchronization and automatic memory management. Our development is framed in the context of the Total Store Order relaxed memory model. Ensuring complier correctness is challenging because highlevel actions are translated into sequences of nonatomic actions with compilerinjected snippets of racy code; the behavior of this code depends not only on the actions of other threads, but also on outoforder executions performed by the processor. A naïve proof of correctness would require reasoning over all possible thread interleavings. In this paper we propose a refinementbased proof methodology that precisely relates concurrent code expressed at different abstraction levels, cognizant throughout of the relaxed memory semantics of the underlying processor. Our technique allows the compiler writer to reason compositionally about the atomicity of lowlevel concurrent code used to implement managed services. We illustrate our approach with examples taken from the verification of a concurrent garbage collector.

[13] 
Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, and Jan
Vitek.
Atomicity refinement for verified compilation.
In ACM SIGPLAN Conference on Programming Language Design and
Implementation, PLDI'14, page 5. ACM, 2014.
Submitted and accepted to TOPLAS vol 36, presented at PLDI the same
year.
[ bib 
.pdf ]
We consider the verified compilation of highlevel managed languages like Java or C# whose intermediate representations provide support for sharedmemory synchronization and automatic memory management. Our development is framed in the context of the Total Store Order relaxed memory model. Ensuring complier correctness is challenging because highlevel actions are translated into sequences of nonatomic actions with compilerinjected snippets of racy code; the behavior of this code depends not only on the actions of other threads, but also on outoforder executions performed by the processor. A naïve proof of correctness would require reasoning over all possible thread interleavings. In this paper we propose a refinementbased proof methodology that precisely relates concurrent code expressed at different abstraction levels, cognizant throughout of the relaxed memory semantics of the underlying processor. Our technique allows the compiler writer to reason compositionally about the atomicity of lowlevel concurrent code used to implement managed services. We illustrate our approach with examples taken from the verification of a concurrent garbage collector.

[14] 
Gilles Barthe, Delphine Demange, and David Pichardie.
Formal verification of an ssabased middleend for compcert.
ACM Trans. Program. Lang. Syst. (TOPLAS), 36(1):4, 2014.
[ bib 
.pdf ]
CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler, faster optimizers. In fact, it has remained an open problem to verify formally an SSAbased compiler. We report on a formally verified, SSAbased, middleend for CompCert. In addition to providing a formally verified SSAbased middleend, we address two problems raised by Leroy in 2009: giving an intuitive formal semantics to SSA, and leveraging its global properties to reason locally about program optimizations.

[15] 
Sandrine Blazy, Vincent Laporte, and David Pichardie.
Verified abstract interpretation techniques for disassembling
lowlevel selfmodifying code.
In Proc. of the 5th International Conference on Interactive
Theorem Proving (ITP 2014), volume 8558 of Lecture Notes in Computer
Science, pages 128143. Springer, 2014.
[ bib 
.pdf ]
Static analysis of binary code is challenging for several reasons. In particular, standard static analysis techniques operate over control flow graphs, which are not available when dealing with selfmodifying programs which can modify their own code at runtime. We formalize in the Coq proof assistant some key abstract interpretation techniques that automatically extract memory safety properties from binary code. Our analyzer is formally proved correct and has been run on several selfmodifying challenges, provided by Cai et al in their PLDI 2007 paper.

[16] 
André Maroneze, Sandrine Blazy, David Pichardie, and Isabelle Puaut.
A formally verified wcet estimation tool.
In 14th International Workshop on WorstCase Execution Time
Analysis, WCET 2014, July 8, 2014, Ulm, Germany, volume 39, pages 1120.
Schloss Dagstuhl  LeibnizZentrum fuer Informatik, 2014.
[ bib 
.pdf ]
The application of formal methods in the development of safetycritical embedded software is recommended in order to provide strong guarantees about the absence of software errors. In this context, WCET estimation tools constitute an important element to be formally verified. We present a formally verified WCET estimation tool, integrated to the formally verified CompCert C compiler. Our tool comes with a machinechecked proof which ensures that its WCET estimates are safe. Our tool operates over C programs and is composed of two main parts, a loop bound estimation and an Implicit Path Enumeration Technique (IPET)based WCET calculation method. We evaluated the precision of the WCET estimates on a reference benchmark and obtained results which are competitive with stateoftheart WCET estimation techniques.

[17] 
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange,
Catalin Hritcu, David Pichardie, Benjamin Pierce, Randy Pollack, and Andrew
Tolmach.
A verified informationflow architecture.
In Proc. of the 41th ACM SIGPLANSIGACT Symposium on Principles
of Programming Languages, POPL 2014, pages 165178. ACM, 2014.
[ bib 
.pdf ]
SAFE is a cleanslate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports finegrained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an informationflow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machinechecked model of the key hardware and software mechanisms used to control information flow in SAFE and an end toend proof of noninterference for this model.

[18] 
Sandrine Blazy, André Maroneze, and David Pichardie.
Formal verification of loop bound estimation for WCET analysis.
In Proc. of the 5th Working Conference on Verified Software:
Theories, Tools, and Experiments (VSTTE 2013), volume 8164 of Lecture
Notes in Computer Science, pages 281303. SpringerVerlag, 2013.
[ bib 
.pdf ]
Worstcase execution time (WCET) estimation tools are complex pieces of software performing tasks such as computation on control flow graphs (CFGs) and bound calculation. In this paper, we present a formal verification (in Coq) of a loop bound estimation. It relies on program slicing and bound calculation. The work has been integrated into the CompCert verified C compiler. Our verified analyses directly operate on nonstructured CFGs. We extend the CompCert RTL intermediate language with a notion of loop nesting (a.k.a. weak topological ordering on CFGs) that is useful for reasoning on CFGs. The automatic extraction of our loop bound estimation into OCaml yields a program with competitive results, obtained from experiments on a reference benchmark for WCET bound estimation tools.

[19] 
Sandrine Blazy, Vincent Laporte, André Maroneze, and David Pichardie.
Formal verification of a C value analysis based on abstract
interpretation.
In Proc. of the 20th Static Analysis Symposium (SAS 2013),
volume 7935 of Lecture Notes in Computer Science, pages 324344.
SpringerVerlag, 2013.
[ bib 
.pdf ]
Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still errorprone. This paper presents a formal verification using the Coq proof assistant: a formalization of a value analysis (based on abstract interpretation), and a soundness proof of the value analysis. The formalization relies on generic interfaces. The mechanized proof is facilitated by a translation validation of a Bourdoncle fixpoint iterator. The work has been integrated into the CompCert verified Ccompiler. Our verified analysis directly operates over an intermediate language of the compiler having the same expressiveness as C. The automatic extraction of our value analysis into OCaml yields a program with competitive results, obtained from experiments on a number of benchmarks and comparisons with the FramaC tool.

[20] 
Delphine Demange, Vincent Laporte, Lei Zhao, David Pichardie, Suresh
Jagannathan, and Jan Vitek.
Plan B: A buffered memory model for Java.
In Proc. of the 40th ACM SIGPLANSIGACT Symposium on Principles
of Programming Languages, POPL 2013. ACM, 2013.
[ bib 
.pdf ]
Recent advances in verification have made it possible to envision trusted implementations of realworld languages. Java with its typesafety and fully specified semantics would appear to be an ideal candidate; yet, the complexity of the translation steps used in production virtual machines have made it a challenging target for verifying compiler technology. One of Java's key innovations, its memory model, poses significant obstacles to such an endeavor. The Java Memory Model is an ambitious attempt at specifying the behavior of multithreaded programs in a portable, hardware agnostic, way. While experts have an intuitive grasp of the properties that the model should enjoy, the specification is complex and not wellsuited for integration within a verifying compiler infrastructure. Moreover, the specification is given in an axiomatic style that is distant from the intuitive reorderingbased reasonings traditionally used to justify or rule out behaviors, and ill suited to the kind of operational reasoning one would expect to employ in a compiler. This paper takes a step back, and introduces a Buffered Memory Model (BMM) for Java. We choose a pragmatic point in the design space sacrificing generality in favor of a model that is fully characterized in terms of the reorderings it allows, amenable to formal reasoning, and which can be efficiently applied to a specific hardware family, namely x86 multiprocessors. Although the BMM restricts the reorderings compilers are allowed to perform, it serves as the key enabling device to achieving a verification pathway from bytecode to machine instructions. Despite its restrictions, we show that it is backwards compatible with the Java Memory Model and that it does not cripple performance on TSO architectures.

[21] 
Gilles Barthe, David Pichardie, and Tamara Rezk.
A certified lightweight noninterference Java bytecode verifier.
Mathematical Structures in Computer Science (MSCS),
23(5):10321081, 2013.
[ bib 
.pdf ]
Noninterference guarantees the absence of illicit information flow throughout program execution. It can be enforced by appropriate information flow type systems. Much of previous work on type systems for noninterference has focused on calculi or highlevel programming languages, and existing type systems for lowlevel languages typically omit objects, exceptions, and method calls. We define an information flow type system for a sequential JVMlike language that includes all these programming features, and we prove, in the Coq proof assistant, that it guarantees noninterference. An additional benefit of the formalization is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to our best knowledge, the first sound and certified information flow type system for such an expressive fragment of the JVM.

[22] 
Thomas Jensen, Florent Kirchner, and David Pichardie.
Secure the clones: Static enforcement of policies for secure object
copying.
Logical Methods in Computer Science (LMCS), 8(2), 2012.
[ bib 
.pdf ]
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 subclass. Currently no languagebased mechanism supports secure object cloning. This paper proposes a typebased annotation system for defining modular copy policies for classbased objectoriented 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 fulfil 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.

[23] 
Gilles Barthe, Delphine Demange, and David Pichardie.
A formally verified SSAbased middleend  Static Single
Assignment meets CompCert.
In Proc. of 21th European Symposium on Programming (ESOP 2012),
volume 7211 of Lecture Notes in Computer Science, pages 4766.
SpringerVerlag, 2012.
[ bib 
.pdf ]
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 SSAbased compiler middleend. We report on a formally verified, SSAbased, middleend for CompCert. Our middleend 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 SSAbased middleend, 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.

[24] 
Frédéric Besson, PierreEmmanuel Cornilleau, and David Pichardie.
Modular SMT proofs for fast reflexive checking inside Coq.
In Proc. of the 1st International Conference on Certified
Programs and Proofs (CPP 2011), volume 7086 of Lecture Notes in
Computer Science, pages 151166. SpringerVerlag, 2011.
[ bib 
.pdf ]
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 NelsonOppen combination scheme. We present the design and implementation of a Coq reflexive verifier that is modular and allows for finetuned theoryspecific verifiers. The current verifier is able to verify proofs for quantifierfree formulae mixing linear arithmetic and uninterpreted functions. Our proof generation scheme benefits from the efficiency of stateoftheart 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 proofproducing prover. We present experiments assessing the feasibility of the approach for benchmarks obtained from the SMT competition.

[25] 
Thomas Jensen, Florent Kirchner, and David Pichardie.
Secure the clones: Static enforcement of policies for secure object
copying.
In Proc. of 20th European Symposium on Programming (ESOP 2011),
volume 6602 of Lecture Notes in Computer Science, pages 317337.
SpringerVerlag, 2011.
[ bib 
.pdf ]
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.

[26]  David Cachera and David Pichardie. Programmation d'un interpréteur abstrait certifié en logique constructive. Technique et Science Informatiques (TSI), 30(4):381408, 2011. [ bib ] 
[27]  David Pichardie, editor. Fifth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2010). Proceedings, Electronic Notes in Theoretical Computer Science, 2010. [ bib ] 
[28] 
Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas
Jensen, Vincent Monfort, David Pichardie, and Tiphaine Turpin.
Sawja: Static Analysis Workshop for Java.
In Proc. of the 1st International Conference on Formal
Verification of ObjectOriented Software (FoVeOOS 2010), volume 6461 of
Lecture Notes in Computer Science, pages 92106. SpringerVerlag, 2010.
[ bib 
.pdf ]
Static analysis is a powerful technique for automatic verification of programs but raises major engineering challenges when developing a fullfledged 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 datastructures for representing a program with implicit sharing and lazy parsing, ii) an intermediate stackless 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.

[29] 
Delphine Demange, Thomas Jensen, and David Pichardie.
A provably correct stackless intermediate representation for Java
bytecode.
In Proc. of the 8th Asian Symposium on Programming Languages and
Systems (APLAS 2010), volume 6461 of Lecture Notes in Computer
Science, pages 97113. SpringerVerlag, 2010.
[ bib 
.pdf ]
The Java virtual machine executes stackbased 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.

[30] 
Laurent Hubert, Thomas Jensen, Vincent Monfort, and David Pichardie.
Enforcing secure object initialization in Java.
In Proc. of the 15th European Symposium on Research in Computer
Security (ESORICS 2010), volume 6345 of Lecture Notes in Computer
Science, pages 101115. SpringerVerlag, 2010.
[ bib 
.pdf ]
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.

[31] 
David Cachera and David Pichardie.
A certified denotational abstract interpreter.
In Proc. of International Conference on Interactive Theorem
Proving (ITP10), volume 6172 of Lecture Notes in Computer Science,
pages 924. SpringerVerlag, 2010.
[ bib 
.pdf ]
Abstract Interpretation proposes advanced techniques for static analysis of programs that raise specific challenges for machinechecked 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 leastfixpoint operator on complete lattices and allows us to decompose the soundness proof in an elegant manner.

[32]  Frédéric Besson, Thomas Jensen, David Pichardie, and Tiphaine Turpin. Certified result checking for polyhedral analysis of bytecode programs. In Proc. of the 5th International Symposium on Trustworthy Global Computing (TGC 2010), volume 6084 of Lecture Notes in Computer Science, pages 253267. SpringerVerlag, 2010. [ bib  .pdf ] 
[33]  Guillaume Hiet, Frédéric Guihéry, Goulven Guiheux, David Pichardie, and Christian Brunette. Sécurité de la plateforme d'exécution Java : limites et propositions d'améliorations. In Proc. of Symposium sur la sécurité des technologies de l'information et des communications (SSTIC 2010), 2010. [ bib  .pdf ] 
[34]  Frédéric Besson, Thomas Jensen, Guillaume Dufay, and David Pichardie. Verifying resource access control on mobile interactive devices. Journal of Computer Security, 18(6):971998, 2010. [ bib  .pdf ] 
[35]  Frédéric Besson, David Cachera, Thomas P. Jensen, and David Pichardie. Certified static analysis by abstract interpretation. In Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, volume 5705 of Lecture Notes in Computer Science, pages 223257. SpringerVerlag, 2009. [ bib  .pdf ] 
[36]  Frédéric Dabrowski and David Pichardie. A certified data race analysis for a Javalike language. In Proc. of 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), volume 5674 of Lecture Notes in Computer Science, pages 212227. SpringerVerlag, 2009. [ bib  .pdf ] 
[37]  David Cachera and David Pichardie. Comparing techniques for certified static analysis. Proc. of the 1st NASA Formal Methods Symposium (NFM'09), pages 111115, 2009. [ bib  .pdf ] 
[38]  Laurent Hubert and David Pichardie. Soundly handling static fields: Issues, semantics and analysis. Proc. of the 4th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09), 253(5):1530, 2009. [ bib  .pdf ] 
[39]  Gilles Barthe, César Kunz, David Pichardie, and Julián Samborski Forlese. Preservation of proof obligations for hybrid certificates. In Proc. of the 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08), pages 127136. IEEE Computer Society, 2008. [ bib  .pdf ] 
[40]  Laurent Hubert, Thomas Jensen, and David Pichardie. Semantic foundations and inference of nonnull annotations. In Proc. of the 10th International Conference on Formal Methods for Open Objectbased Distributed Systems (FMOODS'08), volume 5051 of Lecture Notes in Computer Science, pages 132149. SpringerVerlag, 2008. [ bib  .pdf ] 
[41]  David Pichardie. Building certified static analysers by modular construction of wellfounded lattices. In Proc. of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS'08), volume 212 of Electronic Notes in Theoretical Computer Science, pages 225239, 2008. [ bib  .pdf ] 
[42]  Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas Jensen, and David Pichardie. The MOBIUS Proof Carrying Code infrastructure. In Proc. of the 6th International Symposium on Formal Methods for Components and Objects (FMCO'07), volume 5382 of Lecture Notes in Computer Science, pages 124. SpringerVerlag, 2007. [ bib ] 
[43]  Gilles Barthe, David Pichardie, and Tamara Rezk. A Certified Lightweight NonInterference Java Bytecode Verifier. In Proc. of 16th European Symposium on Programming (ESOP'07), volume 4421 of Lecture Notes in Computer Science, pages 125140. SpringerVerlag, 2007. [ bib  .pdf ] 
[44]  Frédéric Besson, Thomas Jensen, and David Pichardie. Proofcarrying code from certified abstract interpretation to fixpoint compression. Theoretical Computer Science, 364(3):273291, 2006. [ bib  .pdf ] 
[45]  Frédéric Besson, Thomas Jensen, and David Pichardie. A PCC Architecture based on Certified Abstract Interpretation. In Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), ENTCS. SpringerVerlag, 2006. [ bib  .pdf ] 
[46]  Gilles Barthe, Julien Forest, David Pichardie, and Vlad Rusu. Defining and reasoning about recursive functions: A practical tool for the coq proof assistant. In Proc. of 8th International Symposium on Functional and Logic Programming (FLOPS'06), volume 3945 of Lecture Notes in Computer Science, pages 114129. SpringerVerlag, 2006. [ bib  .pdf ] 
[47]  Pichardie David. Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés. PhD thesis, Université Rennes 1, 2005. In french. [ bib  .pdf ] 
[48]  David Pichardie. Modular proof principles for parameterized concretizations. In Proc. of 2nd International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2005), number 3956 in Lecture Notes in Computer Science, pages 138154. SpringerVerlag, 2005. [ bib  .pdf ] 
[49]  David Cachera, Thomas Jensen, David Pichardie, and Gerardo Schneider. Certified Memory Usage Analysis. In Proc. of 13th International Symposium on Formal Methods (FM'05), number 3582 in Lecture Notes in Computer Science, pages 91106. SpringerVerlag, 2005. [ bib  .pdf ] 
[50]  David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science, 342(1):5678, September 2005. Extended version of [51]. [ bib  .pdf ] 
[51]  David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. In Proc. of 13th European Symposium on Programming (ESOP'04), number 2986 in Lecture Notes in Computer Science, pages 385400. SpringerVerlag, 2004. [ bib  .pdf ] 
[52]  Thomas Genet, Thomas Jensen, Vikash Kodati, and David Pichardie. A Java Card CAP converter in PVS. In Jens Knoop and Wolf Zimmermann, editors, Proc. of 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003), ENTCS, volume 82. Elsevier, 2004. [ bib  .pdf ] 
[53]  David Cachera and David Pichardie. Embedding of Systems of Affine Recurrence Equations in Coq. In Proc. of 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03), number 2758 in Lecture Notes in Computer Science, pages 155170. SpringerVerlag, 2003. [ bib  .pdf ] 
[54]  David Pichardie and Yves Bertot. Formalizing Convex Hulls Algorithms. In Proc. of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), number 2152 in Lecture Notes in Computer Science, pages 346361. SpringerVerlag, 2001. [ bib  .pdf ] 
This file was generated by bibtex2html 1.98.