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ël Gué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 = {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.
  }
}