publis.bib
@unpublished{gueneau-pottier-protzenko-13,
author = {Armaël Guéneau and François Pottier and Jonathan
Protzenko},
title = {The ins and outs of iteration in {Mezzo}},
note = {Talk proposal for HOPE 2013},
month = jul,
year = {2013},
pdf = {http://gallium.inria.fr/~fpottier/publis/gueneau-pottier-protzenko-iteration-in-mezzo.pdf},
abstract = {This is a talk proposal for HOPE 2013. Using iteration
over a collection as a case study, we wish to
illustrate the strengths and weaknesses of the
prototype programming language {Mezzo}.}
}
@inproceedings{gueneau-myreen-kumar-norrish-17,
author = {Armaël Guéneau and Magnus O. Myreen and Ramana Kumar and Michael Norrish},
title = {Verified Characteristic Formulae for {CakeML}},
booktitle = {European Symposium on Programming (ESOP)},
year = {2017},
pdf = {http://gallium.inria.fr/~agueneau/publis/gueneau-myreen-kumar-norrish-cf-cakeml.pdf},
abstract = { Characteristic Formulae (CF) offer a productive, principled
approach to generating verification conditions for
higher-order imperative programs, but so far the soundness of
CF has only been considered with respect to an informal
specification of a programming language (OCaml). This leaves a
gap between what is established by the verification framework
and the program that actually runs. We present a
fully-fledged CF framework for the formally specified CakeML
programming language. Our framework extends the existing CF
approach to support exceptions and I/O, thereby covering the
full feature set of CakeML, and comes with a formally verified
soundness theorem. Furthermore, it integrates with existing
proof techniques for verifying CakeML programs. This validates
the CF approach, and allows users to prove end-to-end theorems
for higher-order imperative programs, from specification to
language semantics, within a single theorem prover. }
}
@inproceedings{gueneau-chargueraud-pottier-coq-bigO,
author = {Armaël Guéneau and Arthur Charguéraud and François Pottier},
title = {A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification},
booktitle = {European Symposium on Programming (ESOP)},
year = {2018},
pdf = {http://gallium.inria.fr/~agueneau/publis/gueneau-chargueraud-pottier-coq-bigO.pdf},
abstract = { We present a framework for simultaneously verifying the
functional correctness and the worst-case asymptotic time
complexity of higher-order imperative programs. We build on
top of Separation Logic with Time Credits, embedded in an
interactive proof assistant. We formalize the O notation,
which is key to enabling modular specifications and proofs. We
cover the subtleties of the multivariate case, where the
complexity of a program fragment depends on multiple
parameters. We propose a way of integrating complexity bounds
into specifications, present lemmas and tactics that support a
natural reasoning style, and illustrate their use with a
collection of examples. },
soft = {https://gitlab.inria.fr/agueneau/coq-bigO/}
}
@unpublished{gueneau-procrastination-18,
author = {Arma{\"{e}}l Gu{\'{e}}neau},
title = {Procrastination, a proof engineering technique},
note = {Talk proposal for the FLoC Coq Workshop 2018},
month = apr,
year = {2018},
pdf = {http://gallium.inria.fr/~agueneau/publis/procrastination.pdf},
abstract = {We present a small Coq library for collecting side conditions and deferring their proof.},
soft = {https://github.com/Armael/coq-procrastination}
}
@inproceedings{gueneau-chargueraud-jourdan-pottier-19,
author = {Armaël Guéneau and Jacques-Henri Jourdan and
Arthur Charguéraud and François Pottier},
title = {Formal Proof and Analysis of an Incremental Cycle
Detection Algorithm},
booktitle = {Interactive Theorem Proving (ITP)},
month = sep,
year = {2019},
url = {http://gallium.inria.fr/~agueneau/publis/gueneau-jourdan-chargueraud-pottier-2019.pdf},
abstract = { We study a state-of-the-art incremental cycle detection algorithm
due to Bender, Fineman, Gilbert,and Tarjan. We propose a
simple change that allows the algorithm to be regarded as
genuinely online. Then, we exploit Separation Logic with Time
Credits to simultaneously verify the correctness and the
worst-case amortized asymptotic complexity of the modified
algorithm. },
soft = {https://gitlab.inria.fr/agueneau/incremental-cycles},
off = {http://drops.dagstuhl.de/opus/volltexte/2019/11073/}
}
@inproceedings{georges-etal-ucaps-21,
author = {Aïna Linn Georges and Armaël Guéneau and Thomas van Strydonck
and Amin Timany and Alix Trieu and Sander Huyghebaert and
Dominique Devriese and Lars Birkedal},
title = {Efficient and Provable Local Capability Revocation using Uninitialized Capabilities},
booktitle = {POPL},
year = {2021},
url = {http://gallium.inria.fr/~agueneau/publis/georges-etal-ucaps-2021.pdf},
abstract = {
Capability machines are a special form of CPUs that offer fine-grained privilege separation using a form of
authority-carrying values known as capabilities. The CHERI capability machine offers local capabilities, which
could be used as a cheap but restricted form of capability revocation. Unfortunately, local capability revocation
is unrealistic in practice because large amounts of stack memory need to be cleared as a security precaution.
In this paper, we address this shortcoming by introducing uninitialized cap abilities: a new form of capabilities
that represent read/write authority to a block of memory without exposing the memory’s initial contents. We
provide a mechanically verified program logic for reasoning about programs on a capability machine with the
new feature and we formalize and prove capability safety in the form of a universal contract for untrusted
code. We use uninitialized capabilities for making a previously-proposed secure calling convention efficient
and prove its security using the program logic. Finally, we report on a proof-of-concept implementation of
uninitialized capabilities on the CHERI capability machine.},
soft = { https://github.com/logsem/cerise-stack/releases/tag/POPL2021 }
}
@inproceedings{georges-etal-lse-fr-21,
author = {Aïna Linn Georges and Armaël Guéneau and Thomas van Strydonck
and Amin Timany and Alix Trieu and
Dominique Devriese and Lars Birkedal},
title = {Cap’ ou pas cap’ ? {Preuve} de programmes pour une machine à capacités en presence de code inconnu},
booktitle = {JFLA},
year = {2021},
url = {http://gallium.inria.fr/~agueneau/publis/georges-etal-lse-fr-2021.pdf},
abstract = {
Une machine à capacités est un type de microprocesseur permettant une
séparation des permissions précise grâce à l'utilisation de
capacités, mots machine porteurs d'une certaine autorité.
Dans cet article, nous présentons une méthode permettant de vérifier la
correction fonctionnelle de programmes exécutés par la machine alors même que
ceux-ci appellent ou sont appelés par du code inconnu (et potentiellement
malveillant).
Le bon fonctionnement de tels programmes repose sur leur utilisation
judicieuse des capacités. Du point de vue logique, notre approche permet donc
de tirer parti des garanties fournies par la machine pour raisonner
formellement sur des programmes.
Les éléments clefs de cette approche sont la définition d'une logique de
programmes puis d'une relation logique dont on démontre qu'elle fournit une
spécification pour du code inconnu, le tout étant formalisé en Coq.
La méthodologie en question sous-tend le travail précédent des auteurs lié à
la formalisation d'une convention d'appel sûre en présence d'un nouveau type
de capacités, mais n'est pas détaillée dans
l'article en question.
L'article présent se veut être une introduction pédagogique à cette
méthodologie, dans un cadre plus simple (sans nouvelles capacités exotiques),
et sur un exemple minimal.
},
soft = { https://github.com/logsem/cerise }
}
@unpublished{iris-capabilities-lse-draft,
author = {Aïna Linn Georges and Armaël Guéneau and Thomas van Strydonck
and Amin Timany and Alix Trieu and
Dominique Devriese and Lars Birkedal},
title = {Cerise: Program verification on a capability machine in presence of untrusted code},
note = {Draft},
month = oct,
year = 2020,
url = {http://gallium.inria.fr/~agueneau/publis/iris-capabilities-lse-draft.pdf},
soft = {https://github.com/logsem/cerise}
}
@inproceedings{birkedal-etal-tffsl-21,
author = {Lars Birkedal and Thomas Dinsdale-Young and Armaël Guéneau and
Guilhem Jaber and Kasper Svendsen and Nikos Tzevelekos},
title = {Theorems for Free from Separation Logic Specifications},
booktitle = {ICFP},
year = {2021},
url = {http://gallium.inria.fr/~agueneau/publis/birkedal-etal-tffsl-2021.pdf},
soft = { https://github.com/logsem/free-theorems-sl },
abstract = {
Separation logic specifications with abstract predicates intuitively enforce a discipline that constrains when
and how calls may be made between a client and a library. Thus a separation logic specification of a library
intuitively enforces a protocol on the trace of interactions between a client and the library. We show how to
formalize this intuition and demonstrate how to derive “free theorems” about such interaction traces from
abstract separation logic specifications. We present several examples of free theorems. In particular, we prove
that a so-called logically atomic concurrent separation logic specification of a concurrent module operation
implies that the operation is linearizable. All the results presented in this paper have been mechanized and
formally proved in the Coq proof assistant using the Iris higher-order concurrent separation logic framework.
}
}
@inproceedings{caps-mmio-csf22,
author = {Thomas Van Strydonck and Aïna Linn Georges and Armaël Guéneau and Alix Trieu and Amin Timany and Frank Piessens and Lars Birkedal and Dominique Devriese},
title = {Proving Full-System Security Properties under Multiple Attacker Models on Capability Machines},
booktitle = {CSF},
year = {2022},
url = {http://gallium.inria.fr/~agueneau/publis/caps-mmio-csf22.pdf},
abstract = {
Assembly-level protection mechanisms (virtual mem-
ory, trusted execution environments, virtualization) make it
possible to guarantee security properties of a full system in
the presence of arbitrary attacker provided code. However, they
typically only support a single trust boundary: code is either
trusted or untrusted, and protection cannot be nested. Capability
machines provide protection mechanisms that are more fine-
grained and that do support arbitrary nesting of protection. We
show in this paper how this enables the formal verification of full-
system security properties under multiple attacker models: differ-
ent security objectives of the full system can be verified under a
different choice of trust boundary (i.e. under a different attacker
model). The verification approach we propose is modular, and
is robust: code outside the trust boundary for a given security
objective can be arbitrary, unverified attacker-provided code. It is
based on the use of universal contracts for untrusted adversarial
code: sound, conservative contracts which can be combined with
manual verification of trusted components in a compositional
program logic. Compositionality of the program logic also allows
us to reuse common parts in the analyses for different attacker
models. We instantiate the approach concretely by extending
an existing capability machine model with support for memory-
mapped I/O and we obtain full system, machine-verified security
properties about external effect traces while limiting the manual
verification effort to a small trusted computing base relevant for
the specific property under study.
}
}
@unpublished{cerise-nwpt21,
author = {Aïna Linn Georges and Armaël Guéneau and Thomas van Strydonck
and Amin Timany and Alix Trieu and
Dominique Devriese and Lars Birkedal},
title = {Cerise: Program verification on a capability machine in presence of untrusted code},
note = {Talk proposal for NWPT'21},
pdf = {http://gallium.inria.fr/~agueneau/publis/nwpt21.pdf}
}
@unpublished{caps-prisc21,
author = {Aïna Linn Georges and Armaël Guéneau and
Alix Trieu and Lars Birkedal},
title = {Towards Complete Stack Safety for Capability Machines},
note = {Talk proposal for PriSC'21},
pdf = {http://gallium.inria.fr/~agueneau/publis/prisc21-stack-safety.pdf}
}
@inproceedings{melocoton23,
author = {Armaël Guéneau and
Johannes Hostert and
Simon Spies and
Michael Sammler and
Lars Birkedal and
Derek Dreyer},
title = {Melocoton: A Program Logic for Verified Interoperability Between OCaml and C},
booktitle = {OOPSLA},
year = {2023},
url = {http://gallium.inria.fr/~agueneau/publis/melocoton.pdf},
soft = { https://github.com/logsem/melocoton }
}
@inproceedings{thunks23,
author = {François Pottier and Armaël Guéneau and Jacques-Henri Jourdan and Glen Mével},
title = {Thunks and debits in Separation Logic with Time Credits},
booktitle = {POPL},
year = {2023},
url = {http://gallium.inria.fr/~agueneau/publis/pottier-gueneau-jourdan-mevel-thunks-debits.pdf},
soft = {https://gitlab.inria.fr/cambium/iris-time-proofs}
}