Changeset 3626

Mar 6, 2017, 7:22:26 PM (3 weeks ago)

Changes to main cerco.tex file:

Changed subtitle to something a little more snappy (still not really happy with it),
Rewrote abstract to be less defensive, too.

1 edited


  • Papers/jar-cerco-2017/cerco.tex

    r3619 r3626  
    6868the Seventh Framework Programme for Research of the European Commission, under
    6969FET-Open grant number: 243881}}
    70 \subtitle{Verified lifting of concrete complexity annotations through a realistic C compiler}
    7171\journalname{Journal of Automated Reasoning}
    7272\titlerunning{Certified Complexity}
    7575\authorrunning{Boender, Campbell, Mulligan, and Sacerdoti~Coen}
    7676\institute{Jaap Boender \at
    77               Faculty of Science and Technology,\\
    78                                                         Middlesex University London,\\
    79                                                         United Kingdom.\\
     77              Faculty of Science and Technology, Middlesex University London, United Kingdom.\\
    8078              \email{}
    8179           \and
    8280           Brian Campbell \at
    83               Department of Informatics,\\
    84               University of Edinburgh,\\
    85               United Kingdom.\\
     81              Department of Informatics, University of Edinburgh, United Kingdom.\\
    8682              \email{}
    8783           \and
    8884           Dominic P. Mulligan \at
    89              Computer Laboratory,\\
    90              University of Cambridge, \\
    91              United Kingdom.\\
     85             Computer Laboratory, University of Cambridge, United Kingdom.\\
    9286             \email{}
    9387           \and
    9488           Claudio Sacerdoti~Coen \at
    95               Dipartimento di Informatica---Scienza e Ingegneria (DISI),\\
    96               University of Bologna,\\
    97               Italy.\\
     89              Dipartimento di Informatica---Scienza e Ingegneria (DISI), University of Bologna, Italy.\\
    9890              \email{}}
    105 We provide an overview of the FET-Open Project CerCo (`Certified Complexity').  Our main achievement is the development of a technique for analysing non-functional properties of programs (time, space) at the source level with little or no loss of accuracy and a small trusted code base.
     97Intensional properties of programs---time and space usage, for example---are an important component of the specification of a program, and therefore overall program correctness.
     98Here, intensional properties can be analysed \emph{asymptotically}, or \emph{concretely}, with the latter analyses computing resource bounds in terms of clock cycles, bits transmitted, bytes allocated, or other basal units of resource consumption, for a program execution.
     99For many application domains, for instance libraries exporting cryptographic primitives that must be hardened against timing side-channel attacks, concrete complexity analysis is arguably more important than asymptotic.
    107 The core component is a C compiler, verified in the Matita theorem prover, that produces an instrumented copy of the source code in addition to generating object code.
     101Traditional static analysis tools for resource analysis suffer from a number of disadvantages.
     102They are sophisticated, complex pieces of software, that must be incorporated into the trusted codebase of an application if their analysis is to be believed.
     103They also reason on the machine code produced by a compiler, rather than at the level of the source-code that the application programmer is familiar with, and understands.
     104More ideal would be a mechanism to `lift' a cost model from the machine code generated by a compiler, back to the source code level, where analyses could be performed in terms of source code, abstractions, and control-flow constructs written and understood by the programmer.
     105However: incorporating the precision of traditional static analyses into a high-level approach is a challenge, and how to do this reliably is not \emph{a priori} clear.
     107In this paper, we describe the scientific achievements of the European Union's FET-Open Project CerCo (`Certified Complexity').
     108CerCo's main achievement is the development of a technique for analysing intensional properties of programs at the source level, with little or no loss of accuracy and a small trusted code base.
     109The core component of the project a C compiler, verified in the Matita theorem prover, that produces an instrumented copy of the source code, in addition to generating object code.
    109110This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level.
    110111Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code.
     113We describe the architecture of our C compiler, its proof of correctness, the associated toolchain developed around the compiler, as well as a case study in applying this toolchain to the verification of concrete timing bounds on cryptographic code.
    111115\keywords{Verified compilation \and Complexity analysis \and CerCo (`Certified Complexity')}
Note: See TracChangeset for help on using the changeset viewer.