Notes, Articles & Publications

This section regroups my recent scientific communications, with links to bibliographic references files and electronic editions when available. An exhaustive list of papers, organized by referring type, is available here.

• Secure the Clones: Static Enforcement of Secure Object Copying. [ee] [bib] [...]
• Programming Languages and Systems, volume 6602 of Lecture Notes in Computer Science, 2011.
• with Thomas Jensen and David Pichardie.
• 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.

• Thinking Outside the (Arithmetic) Box: Certifying RAHD Computations. [ee] [bib]
• Short paper, Logics for System Analysis, 2010.
• with Grant Olney Passmore.
• RAHD is a tool that takes advantage of a heterogeneous collection of proof procedures to decide the satisfiability of formulas in the existential fragment of the theory of real closed fields. But system analysts can rarely restrict themselves only to arithmetic-based problems: they might want to use RAHD as part of a more diverse formal toolbox. In this paper, we present ongoing work on an architecture that enables the skeptical integration of RAHD into general-purpose proof assistants. We will present a system-level view of how this integration can be performed, and examine efficiency concerns for this implementation.

• The Proof Monad. [ee] [bib]
• The Journal of Logic and Algebraic Programming, Volume 79, Issues 3-5, 2010.
• with César Muñoz.
• A formalism for expressing the operational semantics of proof languages used in procedural theorem provers is proposed. It is argued that this formalism provides an elegant way to describe the computational features of proof languages, such as side effects, exception handling, and backtracking. The formalism, called proof monads, finds its roots in category theory, and in particular satisfies the monad laws. It is shown that the framework’s monadic operators are related to fundamental tactics and strategies in procedural theorem provers. Finally, the paper illustrates how proof monads can be used to implement semantically clean control structure mechanisms in actual proof languages.

More recent, yet-unpublished work include an article on quantitative program analysis and a conference note on the design of a distributed proof system.

Software + Proofs

With applications that range from quantitative program analysis to safety of ATC algorithms, decision methods for the existential theory of reals make a growingly important class of tools for interactive and automatic theorem provers. The ECDB is a centralized data store that is designed to allow the sharing and incremental certification, by external provers, of complex proofs in real algebra generated by RAHD. It is currently work in progress, and can be previewed by cloning the rahd+ecdb branch of the RAHD repository.

The Evidential Tool Bus takes a novel approach towards formal verification tools composition and interoperability, by relying on asynchronous message passing with a unified proof data structure. Prototyping work was carried out during my postdoctoral visit at SRI International, there are no immediate plans to make it public.

fsp is a proof assistant using sequent calculus logics and proof terms. It is designed to generate proof scripts for other formal tools, such as Coq and PVS. More information, and download options, are found on its website. A library of real closed fields has been developed for fsp, using results derived from von Neumann, Gödel and Bernays' theory of classes to encode second-order formulas in the prover's first-order framework. Documented specifications and proofs are also available online.

Practicals is a PVS package that aims at defining a simple strategy language for the prover. Its implementation is based on a categorical construction, encoded as a datatype and associated functions, called a proof monad.

Contact

For all intents and purposes, my GPG key is available either here, or from the MIT servers.

Colophon

The body text is set 14/21px on a 725px measure with Le Monde Sans and Journal for body text, and Tisa Pro for headers. Font delivery courtesy of Typekit. The source code of this website is available from github; feel free to fork it, submit patches, and offer suggestions.