[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 rely-guarantee methodology. In Proc. of the 8th International Conference on Interactive Theorem Proving (ITP 2017), volume 10499 of Lecture Notes in Computer Science. Springer-Verlag, 2017. [ bib ]
[3] Sandrine Blazy, David Pichardie, and Alix Trieu. Verifying constant-time 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. Springer-Verlag, 2017. [ bib ]
[4] Sandrine Blazy, Vincent Laporte, and David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying 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 information-flow architecture. Journal of Computer Security, 24(6):689--734, 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 Lengauer-Tarjan 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 depth-first search numbers in the dominator tree.

In this work, we aim at integrating such techniques in verified compilers. We present a formally verified validator of untrusted dominator trees, on top of which we implement and prove correct a fast dominance test following these principles. We conduct our formal development in the Coq proof assistant, and integrate it in the middle-end of the CompCertSSA verified compiler. We also provide experimental results showing performance improvement over previous formalizations.

[8] Delphine Demange David Pichardie and Léo Stefanesco. Verifying fast and sparse ssa-based 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 dominance-based reasoning steps required in proofs of SSA-based optimizations. Our experimental evaluations indicate both a better precision, and a significant compilation time speedup.

[9] Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In 42nd symposium Principles of Programming Languages, pages 247--259. 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 run-time errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. Verasco integrates with the CompCert formally-verified 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 well-known 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 semantics-preserving 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. System-level non-interference for constant-time cryptography. In ACM SIGSAC Conference on Computer and Communications Security, CCS'14. ACM, 2014. [ bib | .pdf ]
Cache-based attacks are a class of side-channel attacks that are particularly effective in virtualized or cloud-based environments, where they have been used to recover secret keys from cryptographic implementations. One common approach to thwart cache-based attacks is to use constant-time 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 constant-time implementations are protected against concurrent cache-attacks in virtualization platforms with shared cache; moreover, many prominent implementations are not constant-time. An alternative approach is to rely on system-level 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 constant-time, called S-constant-time, which encompasses some widely used cryptographic implementations. However, there is no rigorous analysis of stealth memory and S-constant-time, and no tool support for checking if applications are S-constant-time. We propose a new information-flow analysis that checks if an x86 application executes in constant-time, or in S-constant-time. Moreover, we prove that constant-time (resp. S-constant-time) 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 constant-time implementations (resp. S-constant-time implementations) are non-interfering 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 high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory 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 high-level actions are translated into sequences of non-atomic actions with compiler-injected snippets of racy code; the behavior of this code depends not only on the actions of other threads, but also on out-of-order 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 refinement-based 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 low-level 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 high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory 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 high-level actions are translated into sequences of non-atomic actions with compiler-injected snippets of racy code; the behavior of this code depends not only on the actions of other threads, but also on out-of-order 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 refinement-based 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 low-level 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 ssa-based middle-end 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 SSA-based compiler. We report on a formally verified, SSA-based, middle-end for CompCert. In addition to providing a formally verified SSA-based middle-end, 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 low-level self-modifying code. In Proc. of the 5th International Conference on Interactive Theorem Proving (ITP 2014), volume 8558 of Lecture Notes in Computer Science, pages 128--143. 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 self-modifying 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 self-modifying 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 Worst-Case Execution Time Analysis, WCET 2014, July 8, 2014, Ulm, Germany, volume 39, pages 11--20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. [ bib | .pdf ]
The application of formal methods in the development of safety-critical 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 machine-checked 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 state-of-the-art 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 information-flow architecture. In Proc. of the 41th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pages 165--178. ACM, 2014. [ bib | .pdf ]
SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained 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 information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to control information flow in SAFE and an end- to-end 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 281--303. Springer-Verlag, 2013. [ bib | .pdf ]
Worst-case 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 non-structured 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 324--344. Springer-Verlag, 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 error-prone. 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 C-compiler. 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 Frama-C 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 SIGPLAN-SIGACT 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 real-world languages. Java with its type-safety 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 well-suited for integration within a verifying compiler infrastructure. Moreover, the specification is given in an axiomatic style that is distant from the intuitive reordering-based 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 non-interference Java bytecode verifier. Mathematical Structures in Computer Science (MSCS), 23(5):1032--1081, 2013. [ bib | .pdf ]
Non-interference 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 non-interference has focused on calculi or high-level programming languages, and existing type systems for low-level languages typically omit objects, exceptions, and method calls. We define an information flow type system for a sequential JVM-like language that includes all these programming features, and we prove, in the Coq proof assistant, that it guarantees non-interference. 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 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 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 SSA-based middle-end - Static Single Assignment meets CompCert. In Proc. of 21th European Symposium on Programming (ESOP 2012), volume 7211 of Lecture Notes in Computer Science, pages 47--66. Springer-Verlag, 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 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.

[24] Frédéric Besson, Pierre-Emmanuel 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 151--166. Springer-Verlag, 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 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.

[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 317--337. Springer-Verlag, 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.

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.

[26] David Cachera and David Pichardie. Programmation d'un interpréteur abstrait certifié en logique constructive. Technique et Science Informatiques (TSI), 30(4):381--408, 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 Object-Oriented Software (FoVeOOS 2010), volume 6461 of Lecture Notes in Computer Science, pages 92--106. Springer-Verlag, 2010. [ bib | .pdf ]
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.

[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 97--113. Springer-Verlag, 2010. [ bib | .pdf ]
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.

[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 101--115. Springer-Verlag, 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 (ITP-10), volume 6172 of Lecture Notes in Computer Science, pages 9--24. Springer-Verlag, 2010. [ bib | .pdf ]
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.

[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 253--267. Springer-Verlag, 2010. [ bib | .pdf ]
[33] Guillaume Hiet, Frédéric Guihéry, Goulven Guiheux, David Pichardie, and Christian Brunette. Sécurité de la plate-forme 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):971--998, 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 223--257. Springer-Verlag, 2009. [ bib | .pdf ]
[36] Frédéric Dabrowski and David Pichardie. A certified data race analysis for a Java-like 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 212--227. Springer-Verlag, 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 111--115, 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):15--30, 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 127--136. IEEE Computer Society, 2008. [ bib | .pdf ]
[40] Laurent Hubert, Thomas Jensen, and David Pichardie. Semantic foundations and inference of non-null annotations. In Proc. of the 10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), volume 5051 of Lecture Notes in Computer Science, pages 132--149. Springer-Verlag, 2008. [ bib | .pdf ]
[41] David Pichardie. Building certified static analysers by modular construction of well-founded 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 225--239, 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 1--24. Springer-Verlag, 2007. [ bib ]
[43] Gilles Barthe, David Pichardie, and Tamara Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier. In Proc. of 16th European Symposium on Programming (ESOP'07), volume 4421 of Lecture Notes in Computer Science, pages 125--140. Springer-Verlag, 2007. [ bib | .pdf ]
[44] Frédéric Besson, Thomas Jensen, and David Pichardie. Proof-carrying code from certified abstract interpretation to fixpoint compression. Theoretical Computer Science, 364(3):273--291, 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. Springer-Verlag, 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 114--129. Springer-Verlag, 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 138--154. Springer-Verlag, 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 91--106. Springer-Verlag, 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):56--78, 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 385--400. Springer-Verlag, 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 155--170. Springer-Verlag, 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 346--361. Springer-Verlag, 2001. [ bib | .pdf ]

This file was generated by bibtex2html 1.98.