source: Papers/jar-cerco-2017/cerco.tex @ 3657

Last change on this file since 3657 was 3657, checked in by mulligan, 3 years ago

more cannibalisation

File size: 6.6 KB
Line 
1\begin{filecontents*}{example.eps}
2%!PS-Adobe-3.0 EPSF-3.0
3%%BoundingBox: 19 19 221 221
4%%CreationDate: Mon Sep 29 1997
5%%Creator: programmed by hand (JK)
6%%EndComments
7gsave
8newpath
9  20 20 moveto
10  20 220 lineto
11  220 220 lineto
12  220 20 lineto
13closepath
142 setlinewidth
15gsave
16  .4 setgray fill
17grestore
18stroke
19grestore
20\end{filecontents*}
21
22\RequirePackage{fix-cm}
23
24\documentclass[smallextended]{svjour3}
25
26\usepackage{amsfonts}
27\usepackage{amsmath}
28\usepackage{amssymb} 
29\usepackage[british]{babel}
30\usepackage{color}
31\usepackage{fancybox}
32\usepackage{fancyvrb}
33\usepackage{graphicx}
34\usepackage[colorlinks,
35            bookmarks,bookmarksopen,bookmarksdepth=2]{hyperref}
36\usepackage{hyphenat}
37\usepackage[utf8x]{inputenc}
38\usepackage{listings}
39\usepackage{mdwlist}
40\usepackage{microtype}
41\usepackage{stmaryrd}
42\usepackage{url}
43
44\usepackage{tikz}
45\usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes}
46
47\lstset{language=C,basicstyle=\tt,basewidth=.5em,lineskip=-1.5pt}
48\def\lstlanguagefiles{lst-grafite.tex}
49
50\newlength{\mylength}
51\newenvironment{frametxt}%
52        {\setlength{\fboxsep}{5pt}
53                \setlength{\mylength}{\linewidth}%
54                \addtolength{\mylength}{-2\fboxsep}%
55                \addtolength{\mylength}{-2\fboxrule}%
56                \Sbox
57                \minipage{\mylength}%
58                        \setlength{\abovedisplayskip}{0pt}%
59                        \setlength{\belowdisplayskip}{0pt}%
60                }%
61                {\endminipage\endSbox
62                        \[\fbox{\TheSbox}\]}
63
64\smartqed
65
66\lstset{extendedchars=false}
67\lstset{inputencoding=utf8x}
68\DeclareUnicodeCharacter{8797}{:=}
69\DeclareUnicodeCharacter{10746}{++}
70\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
71\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
72
73\newcommand{\cerco}{CerCo}
74\newcommand{\ocaml}{OCaml}
75\newcommand{\clight}{Clight}
76\newcommand{\matita}{Matita}
77\newcommand{\sdcc}{\texttt{sdcc}}
78
79\title{CerCo: Certified Complexity\thanks{The project CerCo acknowledges the
80financial support of the Future and Emerging Technologies (FET) programme within
81the Seventh Framework Programme for Research of the European Commission, under
82FET-Open grant number: 243881}}
83\subtitle{Source-level complexity analysis for a large fragment of C}
84\journalname{Journal of Automated Reasoning}
85\titlerunning{Certified Complexity}
86\date{Received: date / Accepted: date}
87\author{Jaap Boender \and Brian Campbell \and Dominic P. Mulligan \and Claudio Sacerdoti~Coen
88        \and %Roberto
89Roberto~M. Amadio \and
90Nicolas Ayache \and
91Fran\c{c}ois Bobot \and
92Ilias Garnier \and
93Antoine Madet \and
94James McKinna \and
95Mauro Piccolo \and
96Randy Pollack \and
97Yann R\'{e}gis-Gianas \and
98Ian Stark \and
99Paolo Tranquilli} % who else?
100\authorrunning{Boender, Campbell, Mulligan, and Sacerdoti~Coen}
101\institute{Roberto M. Amadio, Antoine Madet, and Yann R\'{e}gis-Gianas \at
102            Universit\'e Paris Diderot (Paris 7), Paris, France.
103           \and
104           Nicolas Ayache \at
105            IKOS Consulting, France.
106           \and
107           Fran\c{c}ois Bobot \at
108           Software Reliability Laboratory, CEA, France.
109           \and
110           Jaap Boender \at
111              Middlesex University London, United Kingdom.
112           \and
113           Brian Campbell, James McKinna, Randy Pollack, and Ian Stark \at
114              University of Edinburgh, United Kingdom.
115           \and
116           Ilias Garnier, \at
117             \'Ecole Normale Sup\'erieure, Paris, France.
118           \and
119           Dominic P. Mulligan \at
120             University of Cambridge, United Kingdom.
121           \and
122           Claudio Sacerdoti~Coen \at
123              University of Bologna, Italy.}
124
125\begin{document}
126
127\maketitle
128
129\begin{abstract}
130Concrete non-functional properties of programs---for example, time and space usage as measured in basal units of measure such as milliseconds and bytes allocated---are important components of the specification of a program, and therefore overall program correctness.
131Indeed, for many application domains, concrete complexity analysis is arguably more important than any asymptotic complexity analysis.
132Libraries exporting cryptographic primitives that must be impervious to timing side-channel attacks, or real-time applications with hard timing limits on responsiveness, are examples.
133
134Worst Case Execution Time tools, based on abstract interpretation, currently represent the state-of-the-art in determining concrete time bounds for a program execution.
135These tools suffer from a number of disadvantages, not least the fact that all analysis is performed on machine code, rather than high-level source code, making results hard to interpret by programmers.
136Further, these tools are often complex pieces of software, whose analysis is hard to trust.
137More 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 understood by the programmer.
138How one could incorporate the precision of traditional static analyses into such a high-level approach---and how this could be done reliably---is not \emph{a priori} clear.
139
140In this paper, we describe the scientific contributions of the European Union's FET-Open Project CerCo (`Certified Complexity').
141CerCo's main achievement is the development of a technique for analysing non-functional properties of programs at the source level, with little or no loss of accuracy, and a small trusted code base.
142The core component of the project is a compiler for a large fragment of the C programming language, verified in the Matita theorem prover, that produces an instrumented copy of the source code in addition to generating object code.
143This instrumentation exposes, and tracks precisely, the concrete (non-asymptotic) computational cost of the input program at the source level.
144Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code.
145
146We describe the architecture of our C compiler, its proof of correctness, and the associated toolchain developed around the compiler.
147Using our toolchain, we describe a case study in applying our technique to the verification of concrete timing bounds for cryptographic code.
148
149\keywords{Verified compilation \and Complexity analysis \and Worst Case Execution Time analysis \and CerCo (`Certified Complexity') \and Matita}
150\end{abstract}
151
152\include{introduction}
153\include{architecture}
154\include{proof}
155\include{development}
156\include{framac}
157\include{conclusions}
158
159\begin{acknowledgements}
160\end{acknowledgements}
161
162\bibliographystyle{spmpsci}
163\bibliography{cerco}
164
165\end{document}
Note: See TracBrowser for help on using the repository browser.