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 |
---|
7 | gsave |
---|
8 | newpath |
---|
9 | 20 20 moveto |
---|
10 | 20 220 lineto |
---|
11 | 220 220 lineto |
---|
12 | 220 20 lineto |
---|
13 | closepath |
---|
14 | 2 setlinewidth |
---|
15 | gsave |
---|
16 | .4 setgray fill |
---|
17 | grestore |
---|
18 | stroke |
---|
19 | grestore |
---|
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 | \title{CerCo: Certified Complexity\thanks{The project CerCo acknowledges the |
---|
74 | financial support of the Future and Emerging Technologies (FET) programme within |
---|
75 | the Seventh Framework Programme for Research of the European Commission, under |
---|
76 | FET-Open grant number: 243881}} |
---|
77 | \subtitle{Source-level complexity analysis for a large fragment of C} |
---|
78 | \journalname{Journal of Automated Reasoning} |
---|
79 | \titlerunning{Certified Complexity} |
---|
80 | \date{Received: date / Accepted: date} |
---|
81 | \author{Jaap Boender \and Brian Campbell \and Dominic P. Mulligan \and Claudio Sacerdoti~Coen |
---|
82 | \and %Roberto |
---|
83 | Roberto~M. Amadio \and |
---|
84 | Nicolas Ayache \and |
---|
85 | Fran\c{c}ois Bobot \and |
---|
86 | Ilias Garnier \and |
---|
87 | Antoine Madet \and |
---|
88 | James McKinna \and |
---|
89 | Mauro Piccolo \and |
---|
90 | Randy Pollack \and |
---|
91 | Yann R\'{e}gis-Gianas \and |
---|
92 | Ian Stark \and |
---|
93 | Paolo Tranquilli} % who else? |
---|
94 | \authorrunning{Boender, Campbell, Mulligan, and Sacerdoti~Coen} |
---|
95 | \institute{Roberto M. Amadio, Antoine Madet, and Yann R\'{e}gis-Gianas \at |
---|
96 | Universit\'e Paris Diderot (Paris 7), Paris, France. |
---|
97 | \and |
---|
98 | Nicolas Ayache \at |
---|
99 | IKOS Consulting, France. |
---|
100 | \and |
---|
101 | Fran\c{c}ois Bobot \at |
---|
102 | Software Reliability Laboratory, CEA, France. |
---|
103 | \and |
---|
104 | Jaap Boender \at |
---|
105 | Middlesex University London, United Kingdom. |
---|
106 | \and |
---|
107 | Brian Campbell, James McKinna, Randy Pollack, and Ian Stark \at |
---|
108 | University of Edinburgh, United Kingdom. |
---|
109 | \and |
---|
110 | Ilias Garnier, \at |
---|
111 | \'Ecole Normale Sup\'erieure, Paris, France. |
---|
112 | \and |
---|
113 | Dominic P. Mulligan \at |
---|
114 | University of Cambridge, United Kingdom. |
---|
115 | \and |
---|
116 | Claudio Sacerdoti~Coen \at |
---|
117 | University of Bologna, Italy.} |
---|
118 | |
---|
119 | \begin{document} |
---|
120 | |
---|
121 | \maketitle |
---|
122 | |
---|
123 | \begin{abstract} |
---|
124 | Concrete 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. |
---|
125 | Indeed, for many application domains, concrete complexity analysis is arguably more important than any asymptotic complexity analysis. |
---|
126 | Libraries exporting cryptographic primitives that must be impervious to timing side-channel attacks, or real-time applications with hard timing limits on responsiveness, are examples. |
---|
127 | |
---|
128 | Worst Case Execution Time tools, based on abstract interpretation, currently represent the state-of-the-art in determining concrete time bounds for a program execution. |
---|
129 | These 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. |
---|
130 | Further, these tools are often complex pieces of software, whose analysis is hard to trust. |
---|
131 | More 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. |
---|
132 | How 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. |
---|
133 | |
---|
134 | In this paper, we describe the scientific contributions of the European Union's FET-Open Project CerCo (`Certified Complexity'). |
---|
135 | CerCo'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. |
---|
136 | The 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. |
---|
137 | This instrumentation exposes, and tracks precisely, the concrete (non-asymptotic) computational cost of the input program at the source level. |
---|
138 | Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code. |
---|
139 | |
---|
140 | We describe the architecture of our C compiler, its proof of correctness, and the associated toolchain developed around the compiler. |
---|
141 | Using our toolchain, we describe a case study in applying our technique to the verification of concrete timing bounds for cryptographic code. |
---|
142 | |
---|
143 | \keywords{Verified compilation \and Complexity analysis \and Worst Case Execution Time analysis \and CerCo (`Certified Complexity') \and Matita} |
---|
144 | \end{abstract} |
---|
145 | |
---|
146 | \include{introduction} |
---|
147 | \include{architecture} |
---|
148 | \include{proof} |
---|
149 | \include{development} |
---|
150 | \include{framac} |
---|
151 | \include{conclusions} |
---|
152 | |
---|
153 | \begin{acknowledgements} |
---|
154 | \end{acknowledgements} |
---|
155 | |
---|
156 | \bibliographystyle{spmpsci} |
---|
157 | \bibliography{cerco} |
---|
158 | |
---|
159 | \end{document} |
---|