MusiqueCeltiqueV1, Hal, Curation, bibRecord, 000006

A Certified Compiler for Verifiable Computing

Identifieur interne : 000006 ( Hal/Curation ); précédent : 000005; suivant : 000007

A Certified Compiler for Verifiable Computing

Auteurs : Cédric Fournet [Royaume-Uni] ; Chantal Keller [France] ; Vincent Laporte [France]

Source :

RBID : Hal:hal-01397680

Abstract

In cryptology, verifiable computing aims at verifying the remote execution of a program on an untrusted machine, based on its I/O and constant-sized evidence collected during its execution. Recent cryptographic schemes and compilers enable practical verifiable computations for some programs written in C, but their soundness with regards to C semantics remains informal and poorly understood. We present the first certified, semantics-preserving compiler for verifiable computing. Based on CompCert and developed in Coq, our compiler targets an architecture whose instructions consist solely of quadratic equations over a large finite field, amenable to succinct verification using the Pinocchio cryptographic scheme. We explain how to encode the integer operations of a C program first to quadratic equations, then to a single cryptographically-checkable polynomial test. We formally prove that, when compilation succeeds, there is a correct execution of the source program for any I/O that pass this test. We link our compiler to the Pinocchio cryptographic runtime, and report experimental results as we compile, run, and verify the execution of sample C programs.

Url:

https://hal.inria.fr/hal-01397680

Links toward previous steps (curation, corpus...)

to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000006

Links to Exploration step

Hal:hal-01397680

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Certified Compiler for Verifiable Computing</title>
<author><name sortKey="Fournet, Cedric" sort="Fournet, Cedric" uniqKey="Fournet C" first="Cédric" last="Fournet">Cédric Fournet</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-15503" status="VALID">          <orgName>Microsoft Research [Cambridge]</orgName>
          <orgName type="acronym">Microsoft</orgName>
          <desc>            <address>              <addrLine>Roger Needham Building 7 J J Thomson Ave Cambridge CB3 0FB, UK</addrLine>
              <country key="GB"></country>
            </address>
            <ref type="url">http://research.microsoft.com/aboutmsr/labs/cambridge/default.aspx</ref>
          </desc>
          <listRelation>            <relation active="#struct-365620" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-365620" type="direct"><org type="institution" xml:id="struct-365620" status="VALID">          <orgName>Microsoft Research</orgName>
          <desc>            <address>              <country key="US"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Royaume-Uni</country>
</affiliation>
</author>
<author><name sortKey="Keller, Chantal" sort="Keller, Chantal" uniqKey="Keller C" first="Chantal" last="Keller">Chantal Keller</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-212219" status="VALID">          <idno type="RNSR">201221053L</idno>
          <orgName>Certified Programs, Certified Tools, Certified Floating-Point Computations</orgName>
          <orgName type="acronym">TOCCATA</orgName>
          <desc>            <address>              <addrLine>Université Paris-Sud ; LRI - bâtiment 650 ; 91405 ORSAY CEDEX</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/equipes/toccata</ref>
          </desc>
          <listRelation>            <relation active="#struct-2544" type="direct"></relation>
            <relation active="#struct-92966" type="direct"></relation>
            <relation active="#struct-300009" type="indirect"></relation>
            <relation active="#struct-411575" type="indirect"></relation>
            <relation name="UMR8623" active="#struct-441569" type="direct"></relation>
            <relation active="#struct-118511" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-2544" type="direct"><org type="laboratory" xml:id="struct-2544" status="VALID">          <idno type="RNSR">199812948M</idno>
          <orgName>Laboratoire de Recherche en Informatique</orgName>
          <orgName type="acronym">LRI</orgName>
          <desc>            <address>              <addrLine>LRI - Bâtiments 650-660 Université Paris-Sud 91405 Orsay Cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.lri.fr/</ref>
          </desc>
          <listRelation>            <relation active="#struct-92966" type="direct"></relation>
            <relation active="#struct-300009" type="direct"></relation>
            <relation active="#struct-411575" type="direct"></relation>
            <relation name="UMR8623" active="#struct-441569" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-92966" type="direct"><org type="institution" xml:id="struct-92966" status="VALID">          <orgName>Université Paris-Sud - Paris 11</orgName>
          <orgName type="acronym">UP11</orgName>
          <desc>            <address>              <addrLine>Bâtiment 300 - 91405 Orsay cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.u-psud.fr/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID">          <orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
          <orgName type="acronym">Inria</orgName>
          <desc>            <address>              <addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/en/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-411575" type="indirect"><org type="institution" xml:id="struct-411575" status="VALID">          <idno type="IdRef">184443237</idno>
          <orgName>CentraleSupélec</orgName>
          <desc>            <address>              <addrLine>3, rue Joliot Curie,Plateau de Moulon,91192 GIF-SUR-YVETTE Cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.centralesupelec.fr</ref>
          </desc>
        </org>
</tutelle>
<tutelle name="UMR8623" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID">          <idno type="IdRef">02636817X</idno>
          <idno type="ISNI">0000000122597504</idno>
          <orgName>Centre National de la Recherche Scientifique</orgName>
          <orgName type="acronym">CNRS</orgName>
          <date type="start">1939-10-19</date>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">http://www.cnrs.fr/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-118511" type="direct"><org type="laboratory" xml:id="struct-118511" status="VALID">          <idno type="RNSR">200818248E</idno>
          <orgName>Inria Saclay - Ile de France</orgName>
          <desc>            <address>              <addrLine>1 rue Honoré d'Estienne d'OrvesBâtiment Alan TuringCampus de l'École Polytechnique91120 Palaiseau</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/centre/saclay</ref>
          </desc>
          <listRelation>            <relation active="#struct-300009" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Laporte, Vincent" sort="Laporte, Vincent" uniqKey="Laporte V" first="Vincent" last="Laporte">Vincent Laporte</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-88187" status="OLD">          <idno type="RNSR">200918993K</idno>
          <orgName>Software certification with semantic analysis</orgName>
          <orgName type="acronym">CELTIQUE</orgName>
          <desc>            <address>              <addrLine>Campus de Beaulieu 35042 Rennes cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/equipes/celtique</ref>
          </desc>
          <listRelation>            <relation active="#struct-419153" type="direct"></relation>
            <relation active="#struct-300009" type="indirect"></relation>
            <relation active="#struct-419365" type="direct"></relation>
            <relation active="#struct-105128" type="indirect"></relation>
            <relation active="#struct-105160" type="indirect"></relation>
            <relation active="#struct-528860" type="indirect"></relation>
            <relation active="#struct-172265" type="indirect"></relation>
            <relation active="#struct-247362" type="indirect"></relation>
            <relation name="- RENNES" active="#struct-301232" type="indirect"></relation>
            <relation active="#struct-301262" type="indirect"></relation>
            <relation active="#struct-411575" type="indirect"></relation>
            <relation name="UMR6074" active="#struct-441569" type="indirect"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-419153" type="direct"><org type="laboratory" xml:id="struct-419153" status="VALID">          <idno type="RNSR">198018249C</idno>
          <orgName>Inria Rennes – Bretagne Atlantique </orgName>
          <desc>            <address>              <addrLine>Campus de beaulieu35042 Rennes cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/centre/rennes</ref>
          </desc>
          <listRelation>            <relation active="#struct-300009" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID">          <orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
          <orgName type="acronym">Inria</orgName>
          <desc>            <address>              <addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/en/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-419365" type="direct"><org type="department" xml:id="struct-419365" status="OLD">          <orgName>LANGAGE ET GÉNIE LOGICIEL</orgName>
          <orgName type="acronym">IRISA-D4</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">https://www.irisa.fr/fr/departements/d4-langage-genie-logiciel</ref>
          </desc>
          <listRelation>            <relation active="#struct-105128" type="direct"></relation>
            <relation active="#struct-105160" type="indirect"></relation>
            <relation active="#struct-528860" type="indirect"></relation>
            <relation active="#struct-172265" type="indirect"></relation>
            <relation active="#struct-247362" type="indirect"></relation>
            <relation active="#struct-300009" type="indirect"></relation>
            <relation name="- RENNES" active="#struct-301232" type="indirect"></relation>
            <relation active="#struct-301262" type="indirect"></relation>
            <relation active="#struct-411575" type="indirect"></relation>
            <relation name="UMR6074" active="#struct-441569" type="indirect"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-105128" type="indirect"><org type="laboratory" xml:id="struct-105128" status="OLD">          <idno type="IdRef">026386909</idno>
          <idno type="ISNI">0000 0001 2298 7270</idno>
          <idno type="RNSR">200012163A</idno>
          <orgName>Institut de Recherche en Informatique et Systèmes Aléatoires</orgName>
          <orgName type="acronym">IRISA</orgName>
          <date type="start">2000</date>
          <date type="end">2016-12-31</date>
          <desc>            <address>              <addrLine>Avenue du général LeclercCampus de Beaulieu 35042 RENNES CEDEX</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.irisa.fr</ref>
          </desc>
          <listRelation>            <relation active="#struct-105160" type="direct"></relation>
            <relation active="#struct-528860" type="indirect"></relation>
            <relation active="#struct-172265" type="direct"></relation>
            <relation active="#struct-247362" type="direct"></relation>
            <relation active="#struct-300009" type="direct"></relation>
            <relation name="- RENNES" active="#struct-301232" type="direct"></relation>
            <relation active="#struct-301262" type="direct"></relation>
            <relation active="#struct-411575" type="direct"></relation>
            <relation name="UMR6074" active="#struct-441569" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-105160" type="indirect"><org type="institution" xml:id="struct-105160" status="VALID">          <orgName>Université de Rennes 1</orgName>
          <orgName type="acronym">UR1</orgName>
          <desc>            <address>              <addrLine>2 rue du Thabor - CS 46510 - 35065 Rennes cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.univ-rennes1.fr/</ref>
          </desc>
          <listRelation>            <relation active="#struct-528860" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-528860" type="indirect"><org type="regroupinstitution" xml:id="struct-528860" status="VALID">          <orgName>Université de Rennes</orgName>
          <orgName type="acronym">UNIV-RENNES</orgName>
          <date type="start">2018-01-01</date>
          <desc>            <address>              <country key="FR"></country>
            </address>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-172265" type="indirect"><org type="institution" xml:id="struct-172265" status="VALID"><orgName>Université de Bretagne Sud</orgName>
<orgName type="acronym">UBS</orgName>
<desc><address><addrLine>BP 92116 - 56321 Lorient cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univ-ubs.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-247362" type="indirect"><org type="institution" xml:id="struct-247362" status="VALID">          <orgName>École normale supérieure - Rennes</orgName>
          <orgName type="acronym">ENS Rennes</orgName>
          <desc>            <address>              <addrLine>Campus de Ker Lann - avenue Robert Schuman - 35170 Bruz</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.ens-rennes.fr</ref>
          </desc>
        </org>
</tutelle>
<tutelle name="- RENNES" active="#struct-301232" type="indirect"><org type="regroupinstitution" xml:id="struct-301232" status="VALID">          <idno type="IdRef">162105150</idno>
          <orgName>Institut National des Sciences Appliquées</orgName>
          <orgName type="acronym">INSA</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-301262" type="indirect"><org type="institution" xml:id="struct-301262" status="OLD">          <orgName>Télécom Bretagne</orgName>
          <date type="start">1977</date>
          <desc>            <address>              <addrLine>Technopôle Brest-IroiseCS 8381829238 BREST Cedex 3</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.telecom-bretagne.eu/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-411575" type="indirect"><org type="institution" xml:id="struct-411575" status="VALID">          <idno type="IdRef">184443237</idno>
          <orgName>CentraleSupélec</orgName>
          <desc>            <address>              <addrLine>3, rue Joliot Curie,Plateau de Moulon,91192 GIF-SUR-YVETTE Cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.centralesupelec.fr</ref>
          </desc>
        </org>
</tutelle>
<tutelle name="UMR6074" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID">          <idno type="IdRef">02636817X</idno>
          <idno type="ISNI">0000000122597504</idno>
          <orgName>Centre National de la Recherche Scientifique</orgName>
          <orgName type="acronym">CNRS</orgName>
          <date type="start">1939-10-19</date>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">http://www.cnrs.fr/</ref>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Rennes</settlement>
<region type="region" nuts="2">Région Bretagne</region>
</placeName>
<orgName type="university">Université de Rennes 1</orgName>
<orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName>
<placeName><settlement type="city">Lorient</settlement>
<region type="region" nuts="2">Région Bretagne</region>
</placeName>
<orgName type="university">Université de Bretagne-Sud</orgName>
<orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01397680</idno>
<idno type="halId">hal-01397680</idno>
<idno type="halUri">https://hal.inria.fr/hal-01397680</idno>
<idno type="url">https://hal.inria.fr/hal-01397680</idno>
<date when="2016-06-27">2016-06-27</date>
<idno type="wicri:Area/Hal/Corpus">000006</idno>
<idno type="wicri:Area/Hal/Curation">000006</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">A Certified Compiler for Verifiable Computing</title>
<author><name sortKey="Fournet, Cedric" sort="Fournet, Cedric" uniqKey="Fournet C" first="Cédric" last="Fournet">Cédric Fournet</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-15503" status="VALID">          <orgName>Microsoft Research [Cambridge]</orgName>
          <orgName type="acronym">Microsoft</orgName>
          <desc>            <address>              <addrLine>Roger Needham Building 7 J J Thomson Ave Cambridge CB3 0FB, UK</addrLine>
              <country key="GB"></country>
            </address>
            <ref type="url">http://research.microsoft.com/aboutmsr/labs/cambridge/default.aspx</ref>
          </desc>
          <listRelation>            <relation active="#struct-365620" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-365620" type="direct"><org type="institution" xml:id="struct-365620" status="VALID">          <orgName>Microsoft Research</orgName>
          <desc>            <address>              <country key="US"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Royaume-Uni</country>
</affiliation>
</author>
<author><name sortKey="Keller, Chantal" sort="Keller, Chantal" uniqKey="Keller C" first="Chantal" last="Keller">Chantal Keller</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-212219" status="VALID">          <idno type="RNSR">201221053L</idno>
          <orgName>Certified Programs, Certified Tools, Certified Floating-Point Computations</orgName>
          <orgName type="acronym">TOCCATA</orgName>
          <desc>            <address>              <addrLine>Université Paris-Sud ; LRI - bâtiment 650 ; 91405 ORSAY CEDEX</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/equipes/toccata</ref>
          </desc>
          <listRelation>            <relation active="#struct-2544" type="direct"></relation>
            <relation active="#struct-92966" type="direct"></relation>
            <relation active="#struct-300009" type="indirect"></relation>
            <relation active="#struct-411575" type="indirect"></relation>
            <relation name="UMR8623" active="#struct-441569" type="direct"></relation>
            <relation active="#struct-118511" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-2544" type="direct"><org type="laboratory" xml:id="struct-2544" status="VALID">          <idno type="RNSR">199812948M</idno>
          <orgName>Laboratoire de Recherche en Informatique</orgName>
          <orgName type="acronym">LRI</orgName>
          <desc>            <address>              <addrLine>LRI - Bâtiments 650-660 Université Paris-Sud 91405 Orsay Cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.lri.fr/</ref>
          </desc>
          <listRelation>            <relation active="#struct-92966" type="direct"></relation>
            <relation active="#struct-300009" type="direct"></relation>
            <relation active="#struct-411575" type="direct"></relation>
            <relation name="UMR8623" active="#struct-441569" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-92966" type="direct"><org type="institution" xml:id="struct-92966" status="VALID">          <orgName>Université Paris-Sud - Paris 11</orgName>
          <orgName type="acronym">UP11</orgName>
          <desc>            <address>              <addrLine>Bâtiment 300 - 91405 Orsay cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.u-psud.fr/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID">          <orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
          <orgName type="acronym">Inria</orgName>
          <desc>            <address>              <addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/en/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-411575" type="indirect"><org type="institution" xml:id="struct-411575" status="VALID">          <idno type="IdRef">184443237</idno>
          <orgName>CentraleSupélec</orgName>
          <desc>            <address>              <addrLine>3, rue Joliot Curie,Plateau de Moulon,91192 GIF-SUR-YVETTE Cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.centralesupelec.fr</ref>
          </desc>
        </org>
</tutelle>
<tutelle name="UMR8623" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID">          <idno type="IdRef">02636817X</idno>
          <idno type="ISNI">0000000122597504</idno>
          <orgName>Centre National de la Recherche Scientifique</orgName>
          <orgName type="acronym">CNRS</orgName>
          <date type="start">1939-10-19</date>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">http://www.cnrs.fr/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-118511" type="direct"><org type="laboratory" xml:id="struct-118511" status="VALID">          <idno type="RNSR">200818248E</idno>
          <orgName>Inria Saclay - Ile de France</orgName>
          <desc>            <address>              <addrLine>1 rue Honoré d'Estienne d'OrvesBâtiment Alan TuringCampus de l'École Polytechnique91120 Palaiseau</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/centre/saclay</ref>
          </desc>
          <listRelation>            <relation active="#struct-300009" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Laporte, Vincent" sort="Laporte, Vincent" uniqKey="Laporte V" first="Vincent" last="Laporte">Vincent Laporte</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-88187" status="OLD">          <idno type="RNSR">200918993K</idno>
          <orgName>Software certification with semantic analysis</orgName>
          <orgName type="acronym">CELTIQUE</orgName>
          <desc>            <address>              <addrLine>Campus de Beaulieu 35042 Rennes cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/equipes/celtique</ref>
          </desc>
          <listRelation>            <relation active="#struct-419153" type="direct"></relation>
            <relation active="#struct-300009" type="indirect"></relation>
            <relation active="#struct-419365" type="direct"></relation>
            <relation active="#struct-105128" type="indirect"></relation>
            <relation active="#struct-105160" type="indirect"></relation>
            <relation active="#struct-528860" type="indirect"></relation>
            <relation active="#struct-172265" type="indirect"></relation>
            <relation active="#struct-247362" type="indirect"></relation>
            <relation name="- RENNES" active="#struct-301232" type="indirect"></relation>
            <relation active="#struct-301262" type="indirect"></relation>
            <relation active="#struct-411575" type="indirect"></relation>
            <relation name="UMR6074" active="#struct-441569" type="indirect"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-419153" type="direct"><org type="laboratory" xml:id="struct-419153" status="VALID">          <idno type="RNSR">198018249C</idno>
          <orgName>Inria Rennes – Bretagne Atlantique </orgName>
          <desc>            <address>              <addrLine>Campus de beaulieu35042 Rennes cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/centre/rennes</ref>
          </desc>
          <listRelation>            <relation active="#struct-300009" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID">          <orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
          <orgName type="acronym">Inria</orgName>
          <desc>            <address>              <addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/en/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-419365" type="direct"><org type="department" xml:id="struct-419365" status="OLD">          <orgName>LANGAGE ET GÉNIE LOGICIEL</orgName>
          <orgName type="acronym">IRISA-D4</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">https://www.irisa.fr/fr/departements/d4-langage-genie-logiciel</ref>
          </desc>
          <listRelation>            <relation active="#struct-105128" type="direct"></relation>
            <relation active="#struct-105160" type="indirect"></relation>
            <relation active="#struct-528860" type="indirect"></relation>
            <relation active="#struct-172265" type="indirect"></relation>
            <relation active="#struct-247362" type="indirect"></relation>
            <relation active="#struct-300009" type="indirect"></relation>
            <relation name="- RENNES" active="#struct-301232" type="indirect"></relation>
            <relation active="#struct-301262" type="indirect"></relation>
            <relation active="#struct-411575" type="indirect"></relation>
            <relation name="UMR6074" active="#struct-441569" type="indirect"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-105128" type="indirect"><org type="laboratory" xml:id="struct-105128" status="OLD">          <idno type="IdRef">026386909</idno>
          <idno type="ISNI">0000 0001 2298 7270</idno>
          <idno type="RNSR">200012163A</idno>
          <orgName>Institut de Recherche en Informatique et Systèmes Aléatoires</orgName>
          <orgName type="acronym">IRISA</orgName>
          <date type="start">2000</date>
          <date type="end">2016-12-31</date>
          <desc>            <address>              <addrLine>Avenue du général LeclercCampus de Beaulieu 35042 RENNES CEDEX</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.irisa.fr</ref>
          </desc>
          <listRelation>            <relation active="#struct-105160" type="direct"></relation>
            <relation active="#struct-528860" type="indirect"></relation>
            <relation active="#struct-172265" type="direct"></relation>
            <relation active="#struct-247362" type="direct"></relation>
            <relation active="#struct-300009" type="direct"></relation>
            <relation name="- RENNES" active="#struct-301232" type="direct"></relation>
            <relation active="#struct-301262" type="direct"></relation>
            <relation active="#struct-411575" type="direct"></relation>
            <relation name="UMR6074" active="#struct-441569" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-105160" type="indirect"><org type="institution" xml:id="struct-105160" status="VALID">          <orgName>Université de Rennes 1</orgName>
          <orgName type="acronym">UR1</orgName>
          <desc>            <address>              <addrLine>2 rue du Thabor - CS 46510 - 35065 Rennes cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.univ-rennes1.fr/</ref>
          </desc>
          <listRelation>            <relation active="#struct-528860" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-528860" type="indirect"><org type="regroupinstitution" xml:id="struct-528860" status="VALID">          <orgName>Université de Rennes</orgName>
          <orgName type="acronym">UNIV-RENNES</orgName>
          <date type="start">2018-01-01</date>
          <desc>            <address>              <country key="FR"></country>
            </address>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-172265" type="indirect"><org type="institution" xml:id="struct-172265" status="VALID"><orgName>Université de Bretagne Sud</orgName>
<orgName type="acronym">UBS</orgName>
<desc><address><addrLine>BP 92116 - 56321 Lorient cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univ-ubs.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-247362" type="indirect"><org type="institution" xml:id="struct-247362" status="VALID">          <orgName>École normale supérieure - Rennes</orgName>
          <orgName type="acronym">ENS Rennes</orgName>
          <desc>            <address>              <addrLine>Campus de Ker Lann - avenue Robert Schuman - 35170 Bruz</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.ens-rennes.fr</ref>
          </desc>
        </org>
</tutelle>
<tutelle name="- RENNES" active="#struct-301232" type="indirect"><org type="regroupinstitution" xml:id="struct-301232" status="VALID">          <idno type="IdRef">162105150</idno>
          <orgName>Institut National des Sciences Appliquées</orgName>
          <orgName type="acronym">INSA</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-301262" type="indirect"><org type="institution" xml:id="struct-301262" status="OLD">          <orgName>Télécom Bretagne</orgName>
          <date type="start">1977</date>
          <desc>            <address>              <addrLine>Technopôle Brest-IroiseCS 8381829238 BREST Cedex 3</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.telecom-bretagne.eu/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-411575" type="indirect"><org type="institution" xml:id="struct-411575" status="VALID">          <idno type="IdRef">184443237</idno>
          <orgName>CentraleSupélec</orgName>
          <desc>            <address>              <addrLine>3, rue Joliot Curie,Plateau de Moulon,91192 GIF-SUR-YVETTE Cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.centralesupelec.fr</ref>
          </desc>
        </org>
</tutelle>
<tutelle name="UMR6074" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID">          <idno type="IdRef">02636817X</idno>
          <idno type="ISNI">0000000122597504</idno>
          <orgName>Centre National de la Recherche Scientifique</orgName>
          <orgName type="acronym">CNRS</orgName>
          <date type="start">1939-10-19</date>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">http://www.cnrs.fr/</ref>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Rennes</settlement>
<region type="region" nuts="2">Région Bretagne</region>
</placeName>
<orgName type="university">Université de Rennes 1</orgName>
<orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName>
<placeName><settlement type="city">Lorient</settlement>
<region type="region" nuts="2">Région Bretagne</region>
</placeName>
<orgName type="university">Université de Bretagne-Sud</orgName>
<orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName>
</affiliation>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">In cryptology, verifiable computing aims at verifying the remote execution of a program on an untrusted machine, based on its I/O and constant-sized evidence collected during its execution. Recent cryptographic schemes and compilers enable practical verifiable computations for some programs written in C, but their soundness with regards to C semantics remains informal and poorly understood. We present the first certified, semantics-preserving compiler for verifiable computing. Based on CompCert and developed in Coq, our compiler targets an architecture whose instructions consist solely of quadratic equations over a large finite field, amenable to succinct verification using the Pinocchio cryptographic scheme. We explain how to encode the integer operations of a C program first to quadratic equations, then to a single cryptographically-checkable polynomial test. We formally prove that, when compilation succeeds, there is a correct execution of the source program for any I/O that pass this test. We link our compiler to the Pinocchio cryptographic runtime, and report experimental results as we compile, run, and verify the execution of sample C programs.</div>
</front>
</TEI>
<hal api="V3">          <titleStmt>            <title xml:lang="en">A Certified Compiler for Verifiable Computing</title>
            <author role="aut">              <persName>                <forename type="first">Cédric</forename>
                <surname>Fournet</surname>
              </persName>
              <idno type="halauthorid">107802</idno>
              <affiliation ref="#struct-15503"></affiliation>
            </author>
            <author role="aut">              <persName>                <forename type="first">Chantal</forename>
                <surname>Keller</surname>
              </persName>
              <email type="md5">2c7a919ba5344845cfd949172f25eb6b</email>
              <email type="domain">lri.fr</email>
              <idno type="idhal" notation="string">chantal-keller</idno>
              <idno type="idhal" notation="numeric">15985</idno>
              <idno type="halauthorid">1406364</idno>
              <idno type="ORCID">https://orcid.org/0000-0002-1282-0677</idno>
              <affiliation ref="#struct-212219"></affiliation>
            </author>
            <author role="aut">              <persName>                <forename type="first">Vincent</forename>
                <surname>Laporte</surname>
              </persName>
              <email type="md5">ba807766975d57bf99f7a1866f638f15</email>
              <email type="domain">imdea.org</email>
              <idno type="halauthorid">1357994</idno>
              <affiliation ref="#struct-88187"></affiliation>
              <affiliation ref="#struct-81272"></affiliation>
            </author>
            <editor role="depositor">              <persName>                <forename>Chantal</forename>
                <surname>Keller</surname>
              </persName>
              <email type="md5">2c7a919ba5344845cfd949172f25eb6b</email>
              <email type="domain">lri.fr</email>
            </editor>
          </titleStmt>
          <editionStmt>            <edition n="v1" type="current">              <date type="whenSubmitted">2016-11-23 10:55:10</date>
              <date type="whenModified">2018-05-16 11:23:28</date>
              <date type="whenReleased">2016-11-23 11:32:53</date>
              <date type="whenProduced">2016-06-27</date>
              <date type="whenEndEmbargoed">2016-11-16</date>
              <ref type="file" target="https://hal.inria.fr/hal-01397680/document">                <date notBefore="2016-11-16"></date>
              </ref>
              <ref type="file" subtype="author" n="1" target="https://hal.inria.fr/hal-01397680/file/csf16.pdf">                <date notBefore="2016-11-16"></date>
              </ref>
            </edition>
            <respStmt>              <resp>contributor</resp>
              <name key="108005">                <persName>                  <forename>Chantal</forename>
                  <surname>Keller</surname>
                </persName>
                <email type="md5">2c7a919ba5344845cfd949172f25eb6b</email>
                <email type="domain">lri.fr</email>
              </name>
            </respStmt>
          </editionStmt>
          <publicationStmt>            <distributor>CCSD</distributor>
            <idno type="halId">hal-01397680</idno>
            <idno type="halUri">https://hal.inria.fr/hal-01397680</idno>
            <idno type="halBibtex">fournet:hal-01397680</idno>
            <idno type="halRefHtml">IEEE 29th Computer Security Foundations Symposium, CSF 2016, Jun 2016, Lisbonne, Portugal. 2016</idno>
            <idno type="halRef">IEEE 29th Computer Security Foundations Symposium, CSF 2016, Jun 2016, Lisbonne, Portugal. 2016</idno>
          </publicationStmt>
          <seriesStmt>            <idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno>
            <idno type="stamp" n="INRIA-SACLAY">INRIA Saclay - Ile de France</idno>
            <idno type="stamp" n="UMR8623">Laboratoire de Recherche en Informatique</idno>
            <idno type="stamp" n="UNIV-RENNES1">Université de Rennes 1</idno>
            <idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno>
            <idno type="stamp" n="INRIA_TEST">INRIA - Institut National de Recherche en Informatique et en Automatique</idno>
            <idno type="stamp" n="INRIA2">INRIA 2</idno>
            <idno type="stamp" n="LRI-VALS" p="UMR8623">Laboratoire de Recherche en Informatique. Équipe: Vérification d'Algorithmes, Langages et Systèmes</idno>
            <idno type="stamp" n="UNIV-UBS">Université de Bretagne Sud</idno>
            <idno type="stamp" n="INSTITUT-TELECOM">Institut Télécom</idno>
            <idno type="stamp" n="IRISA_SET">IRISA_SET</idno>
            <idno type="stamp" n="IRISA">Irisa</idno>
            <idno type="stamp" n="UR1-HAL">Publications labos UR1 dans HAL-Rennes 1</idno>
            <idno type="stamp" n="UR1-MATH-STIC">UR1 - publications Maths-STIC</idno>
            <idno type="stamp" n="UNIV-PSUD">Université Paris Sud - Paris XI</idno>
            <idno type="stamp" n="CENTRALESUPELEC">Ecole CentraleSupélec</idno>
            <idno type="stamp" n="UR1-UFR-ISTIC">UFR ISTIC Informatique et électronique</idno>
            <idno type="stamp" n="UNIV-PSUD-SACLAY" p="UNIV-PARIS-SACLAY">Université Paris Sud pour Paris Saclay</idno>
            <idno type="stamp" n="INRIA-SACLAY-2015" p="UNIV-PARIS-SACLAY">INRIA-SACLAY-2015</idno>
            <idno type="stamp" n="UNIV-PARIS-SACLAY">Université Paris-Saclay</idno>
            <idno type="stamp" n="TEST-UNIV-RENNES">TEST Université de Rennes</idno>
            <idno type="stamp" n="TEST-UR-CSS">TEST Université de Rennes CSS</idno>
            <idno type="stamp" n="UNIV-RENNES">Université de Rennes</idno>
            <idno type="stamp" n="INRIA-RENNES">INRIA Rennes - Bretagne Atlantique</idno>
            <idno type="stamp" n="INRIA-RENGRE">INRIA-RENGRE</idno>
          </seriesStmt>
          <notesStmt>            <note type="audience" n="2">International</note>
            <note type="invited" n="0">No</note>
            <note type="popular" n="0">No</note>
            <note type="peer" n="1">Yes</note>
            <note type="proceedings" n="1">Yes</note>
          </notesStmt>
          <sourceDesc>            <biblStruct>              <analytic>                <title xml:lang="en">A Certified Compiler for Verifiable Computing</title>
                <author role="aut">                  <persName>                    <forename type="first">Cédric</forename>
                    <surname>Fournet</surname>
                  </persName>
                  <idno type="halauthorid">107802</idno>
                  <affiliation ref="#struct-15503"></affiliation>
                </author>
                <author role="aut">                  <persName>                    <forename type="first">Chantal</forename>
                    <surname>Keller</surname>
                  </persName>
                  <email type="md5">2c7a919ba5344845cfd949172f25eb6b</email>
                  <email type="domain">lri.fr</email>
                  <idno type="idhal" notation="string">chantal-keller</idno>
                  <idno type="idhal" notation="numeric">15985</idno>
                  <idno type="halauthorid">1406364</idno>
                  <idno type="ORCID">https://orcid.org/0000-0002-1282-0677</idno>
                  <affiliation ref="#struct-212219"></affiliation>
                </author>
                <author role="aut">                  <persName>                    <forename type="first">Vincent</forename>
                    <surname>Laporte</surname>
                  </persName>
                  <email type="md5">ba807766975d57bf99f7a1866f638f15</email>
                  <email type="domain">imdea.org</email>
                  <idno type="halauthorid">1357994</idno>
                  <affiliation ref="#struct-88187"></affiliation>
                  <affiliation ref="#struct-81272"></affiliation>
                </author>
              </analytic>
              <monogr>                <meeting>                  <title>IEEE 29th Computer Security Foundations Symposium, CSF 2016</title>
                  <date type="start">2016-06-27</date>
                  <date type="end">2016-07-01</date>
                  <settlement>Lisbonne</settlement>
                  <country key="PT">Portugal</country>
                </meeting>
                <imprint>                  <date type="datePub">2016-07-01</date>
                </imprint>
              </monogr>
            </biblStruct>
          </sourceDesc>
          <profileDesc>            <langUsage>              <language ident="en">English</language>
            </langUsage>
            <textClass>              <classCode scheme="halDomain" n="info.info-lo">Computer Science [cs]/Logic in Computer Science [cs.LO]</classCode>
              <classCode scheme="halDomain" n="info.info-cr">Computer Science [cs]/Cryptography and Security [cs.CR]</classCode>
              <classCode scheme="halDomain" n="info.info-cl">Computer Science [cs]/Computation and Language [cs.CL]</classCode>
              <classCode scheme="halTypology" n="COMM">Conference papers</classCode>
            </textClass>
            <abstract xml:lang="en">In cryptology, verifiable computing aims at verifying the remote execution of a program on an untrusted machine, based on its I/O and constant-sized evidence collected during its execution. Recent cryptographic schemes and compilers enable practical verifiable computations for some programs written in C, but their soundness with regards to C semantics remains informal and poorly understood. We present the first certified, semantics-preserving compiler for verifiable computing. Based on CompCert and developed in Coq, our compiler targets an architecture whose instructions consist solely of quadratic equations over a large finite field, amenable to succinct verification using the Pinocchio cryptographic scheme. We explain how to encode the integer operations of a C program first to quadratic equations, then to a single cryptographically-checkable polynomial test. We formally prove that, when compilation succeeds, there is a correct execution of the source program for any I/O that pass this test. We link our compiler to the Pinocchio cryptographic runtime, and report experimental results as we compile, run, and verify the execution of sample C programs.</abstract>
          </profileDesc>
        </hal>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Musique/explor/MusiqueCeltiqueV1/Data/Hal/Curation

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000006 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Hal/Curation/biblio.hfd -nk 000006 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Musique
   |area=    MusiqueCeltiqueV1
   |flux=    Hal
   |étape=   Curation
   |type=    RBID
   |clé=     Hal:hal-01397680
   |texte=   A Certified Compiler for Verifiable Computing
}}

This area was generated with Dilib version V0.6.38.
Data generation: Sat May 29 22:04:25 2021. Site generation: Sat May 29 22:08:31 2021

	Serveur d'exploration sur la musique celtique
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la musique celtique

A Certified Compiler for Verifiable Computing

A Certified Compiler for Verifiable Computing

Source :

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri