1 | \documentclass{beamer} |
---|
2 | |
---|
3 | \usepackage[english]{babel} |
---|
4 | \usepackage[utf8]{inputenc} |
---|
5 | %\usepackage[utf-8]{fontenc} |
---|
6 | \usepackage{xspace} |
---|
7 | \usepackage{amsmath, amssymb, amsfonts} |
---|
8 | \usepackage{stmaryrd} |
---|
9 | \usepackage{graphics,color} |
---|
10 | \usepackage{latexsym} |
---|
11 | \usepackage{array} |
---|
12 | \usepackage[all]{xy} |
---|
13 | \usepackage{array} |
---|
14 | |
---|
15 | \input{macros} |
---|
16 | \input{mybeamer} |
---|
17 | \newcommand{\BlueLabelled}[1]{#1^{\textcolor{blockTColor}{\mathcal{L}}}} |
---|
18 | \newcommand\hili[1]{\textcolor{blue}{#1}} |
---|
19 | \newcommand{\cl}[1]{{\cal #1}} % \cl{R} to make R calligraphic |
---|
20 | \newcommand{\comp}{\circ} % functional composition |
---|
21 | \newcommand{\w}[1]{{\it #1}} %To write in math style |
---|
22 | \newcolumntype{M}[1]{>{\raggedright}m{#1}} |
---|
23 | |
---|
24 | \title{WP5: Interfaces and Interactive Components} |
---|
25 | |
---|
26 | \date{} |
---|
27 | |
---|
28 | \begin{document} |
---|
29 | |
---|
30 | \begin{frame} |
---|
31 | \titlepage |
---|
32 | \begin{columns} |
---|
33 | \hspace{1cm} |
---|
34 | \begin{column}{3cm} |
---|
35 | \includegraphics[width=2.5cm]{cerco_logo} |
---|
36 | \end{column} |
---|
37 | \begin{column}{8.5cm} |
---|
38 | \tiny |
---|
39 | This work was (partially) supported by the Information and |
---|
40 | Communication Technologies (ICT) Programme as Project |
---|
41 | FP7-ICT-2009-C-243881 CerCo. |
---|
42 | \end{column} |
---|
43 | \end{columns} |
---|
44 | \end{frame} |
---|
45 | |
---|
46 | \begin{frame} |
---|
47 | \frametitle{A tool to reason about the complexity of C programs} |
---|
48 | |
---|
49 | \begin{center} |
---|
50 | \includegraphics[width=10cm]{Pics/architecture} |
---|
51 | \end{center} |
---|
52 | |
---|
53 | \end{frame} |
---|
54 | |
---|
55 | \begin{frame} |
---|
56 | \frametitle{Frama-C} |
---|
57 | |
---|
58 | \begin{center} |
---|
59 | \includegraphics[width=12cm]{Pics/frama-c.png} |
---|
60 | \end{center} |
---|
61 | |
---|
62 | \end{frame} |
---|
63 | |
---|
64 | \begin{frame} |
---|
65 | \frametitle{Overview of the plugin} |
---|
66 | |
---|
67 | \begin{block}{} |
---|
68 | \begin{itemize} |
---|
69 | \item {\sf Cost}, a plugin for Frama-C that: |
---|
70 | \begin{itemize} |
---|
71 | \item[(i)] takes C program $P$ as input ; |
---|
72 | \item[(ii)] applies the CerCo compiler to enrich $P$ with cost annotations ; |
---|
73 | \item[(iii)] applies some heuristics to produce a tentative bound on the |
---|
74 | cost of executing the C functions of the program as a function of the value of their |
---|
75 | parameters. |
---|
76 | \end{itemize} |
---|
77 | \item The deductive tool $\textsf{Jessie}$ is used to discharge the proof obligations. |
---|
78 | \end{itemize} |
---|
79 | \end{block} |
---|
80 | \end{frame} |
---|
81 | |
---|
82 | \begin{frame} |
---|
83 | \frametitle{{\sf Cost} plugin in action (1/2)} |
---|
84 | |
---|
85 | \begin{center} |
---|
86 | \framebox{\footnotesize\begin{tabular}{l} |
---|
87 | \texttt{int is\_sorted (int *tab, int size) \{}\\ |
---|
88 | \quad \texttt{int i, res = 1;}\\ |
---|
89 | \quad \texttt{for (i = 0 ; i < size-1 ; i++)} \\ |
---|
90 | \qquad \texttt {if (tab[i] > tab[i+1]) } \\ |
---|
91 | \quad \qquad \texttt{res = 0; }\\ |
---|
92 | \quad \texttt{return res; } \\ |
---|
93 | \texttt{\} } \\ |
---|
94 | \end{tabular}} |
---|
95 | \end{center} |
---|
96 | |
---|
97 | \end{frame} |
---|
98 | |
---|
99 | \begin{frame} |
---|
100 | \frametitle{{\sf Cost} plugin in action (2/2)} |
---|
101 | |
---|
102 | \begin{center} |
---|
103 | \framebox{\footnotesize\begin{tabular}{l} |
---|
104 | \texttt{int \_cost = 0;}\\\\ |
---|
105 | {\color{red} \texttt{/*@ ensures (\_cost $\le$ |
---|
106 | $\backslash$old(\_cost)+(101+(0<size-1?(size-1)*195:0))); */} }\\ |
---|
107 | \texttt{int is\_sorted (int *tab, int size) \{}\\ |
---|
108 | \quad \texttt{int i, res = 1, \_cost\_tmp0;}\\ |
---|
109 | \quad \texttt{\_cost += 97; \_cost\_tmp0 = \_cost;}\\ |
---|
110 | {\color{red} \quad \texttt{/* @ loop invariant (0 < size-1) $\Rightarrow$ (i $\le$ |
---|
111 | size-1);}} \\ |
---|
112 | {\color{red} \quad \texttt{\ \ \ @ loop invariant (0 $\ge$ size-1) $\Rightarrow$ (i |
---|
113 | $\equiv$ 0);} }\\ |
---|
114 | {\color{red} \quad \texttt{\ \ \ @ loop invariant (\_cost $\le$ |
---|
115 | \_cost\_tmp0 + i * 195);} }\\ |
---|
116 | {\color{red} \quad \texttt{\ \ \ @ loop variant (size-1)-i; */} }\\ |
---|
117 | \quad \texttt{for (i = 0; i < size-1; i++) \{}\\ |
---|
118 | \quad \quad \texttt{\_cost += 91;}\\ |
---|
119 | \quad \quad \texttt{if (tab[i] > tab[i+1]) \{ \_cost += 104; res = |
---|
120 | 0; \}}\\ |
---|
121 | \quad \quad \texttt{else \_cost += 84; \}}\\ |
---|
122 | \quad \texttt{\_cost += 4; } ** |
---|
123 | \quad \texttt{return res; } \\ |
---|
124 | \texttt { \}}\\ |
---|
125 | \end{tabular}} |
---|
126 | \end{center} |
---|
127 | |
---|
128 | \end{frame} |
---|
129 | |
---|
130 | \begin{frame} |
---|
131 | \frametitle{Assumptions on the input programs} |
---|
132 | |
---|
133 | \begin{block}{} |
---|
134 | \begin{itemize} |
---|
135 | \item No recursive functions. |
---|
136 | |
---|
137 | \item Every loop must be annotated with a {\em variant}. |
---|
138 | |
---|
139 | \item The variants of `for' loops are automatically inferred. |
---|
140 | |
---|
141 | \end{itemize} |
---|
142 | \end{block} |
---|
143 | |
---|
144 | \end{frame} |
---|
145 | |
---|
146 | \begin{frame} |
---|
147 | \frametitle{Details on the plugin internals} |
---|
148 | |
---|
149 | \begin{block}{Main steps of the inference engine} |
---|
150 | \begin{enumerate} |
---|
151 | \item Traverse the callgraph following dependencies. |
---|
152 | \item For each function, traverse its control flow graph, bottom-up. |
---|
153 | \item The cost at a node is the maximum of the costs of the successors. |
---|
154 | \item Symbolically update the cost along the sequence of instructions. |
---|
155 | \end{enumerate} |
---|
156 | \end{block} |
---|
157 | |
---|
158 | \end{frame} |
---|
159 | |
---|
160 | \begin{frame} |
---|
161 | \frametitle{Details on the treatment of for-loops (1/2)} |
---|
162 | |
---|
163 | \begin{block}{\underline{Case 1}: body whose cost is constant for every step of the loop} |
---|
164 | The cost is the product of the cost of the body |
---|
165 | and of the variant taken at the start of the loop. |
---|
166 | \end{block} |
---|
167 | |
---|
168 | \end{frame} |
---|
169 | |
---|
170 | \begin{frame} |
---|
171 | \frametitle{Details on the treatment of for-loops (2/2)} |
---|
172 | |
---|
173 | \begin{block}{\underline{Case 2}: body whose cost depends on free variables} |
---|
174 | |
---|
175 | \begin{itemize} |
---|
176 | \item A fresh logic function $f$ represents the cost of the loop in the logic assertions. |
---|
177 | |
---|
178 | \item This logic function takes the variant as a first parameter. |
---|
179 | |
---|
180 | \item The other parameters of $f$ are the free variables of the body. |
---|
181 | |
---|
182 | \item An axiom denotes the accumulation of the cost at each step of the loop: |
---|
183 | \[ |
---|
184 | f(v, \vec x) = |
---|
185 | \textrm{if } v < 0 \textrm{ then } 0 \textrm{ else } (f(v-1, \phi(\vec x)) + \psi(\vec x)) |
---|
186 | \] |
---|
187 | \end{itemize} |
---|
188 | $\small\left\{ |
---|
189 | \begin{array}{l} |
---|
190 | \vec x \textrm{ are the free variables} \\ |
---|
191 | v \textrm{ is the variant} \\ |
---|
192 | \phi \textrm{ computes the modification of the variable at each step of the loop} \\ |
---|
193 | \psi \textrm{ is the cost of the body of the loop} |
---|
194 | \end{array} |
---|
195 | \right.$ |
---|
196 | \end{block} |
---|
197 | |
---|
198 | \end{frame} |
---|
199 | |
---|
200 | \begin{frame} |
---|
201 | \frametitle{Beyond the assumptions on the source programs} |
---|
202 | |
---|
203 | \begin{block}{} |
---|
204 | The user can influence the annotation by different means: |
---|
205 | \begin{itemize} |
---|
206 | \item By using more precise variants. |
---|
207 | \item By annotating function with cost specification. The plugin will |
---|
208 | use this cost for the function instead of computing it. |
---|
209 | \end{itemize} |
---|
210 | \end{block} |
---|
211 | |
---|
212 | \end{frame} |
---|
213 | |
---|
214 | \begin{frame} |
---|
215 | \begin{center} |
---|
216 | {\Large How to prove cost annotations using Frama-C?} |
---|
217 | \\\vspace{1cm} |
---|
218 | {\Huge {\textcolor{red}{Demo}}} |
---|
219 | \end{center} |
---|
220 | \end{frame} |
---|
221 | |
---|
222 | \begin{frame} |
---|
223 | \frametitle{Focus on an experiment} |
---|
224 | |
---|
225 | \begin{block}{} |
---|
226 | \begin{center} |
---|
227 | \large A certified bound on the \hili{reaction time} of a {\sc Lustre} program |
---|
228 | \end{center} |
---|
229 | \end{block} |
---|
230 | |
---|
231 | \- |
---|
232 | |
---|
233 | \begin{block}{The specificities of synchronous programs} |
---|
234 | \begin{itemize} |
---|
235 | \item {\sc Lustre} is a data-flow language to program synchronous systems. |
---|
236 | \item The language is usually compiled to {\sc C} as a \texttt{step} function. |
---|
237 | \item This function only has assignment and conditional statements. |
---|
238 | \item In that setting, the assertion inference is \hili{fully automatic}. |
---|
239 | \item Once this assertion is proved, we get a \hili{certified bound} on the reaction time of the system. |
---|
240 | \end{itemize} |
---|
241 | \end{block} |
---|
242 | |
---|
243 | \end{frame} |
---|
244 | |
---|
245 | |
---|
246 | \begin{frame} |
---|
247 | \frametitle{Experiments} |
---|
248 | |
---|
249 | {\footnotesize \begin{center} |
---|
250 | \begin{tabular}{|l|c|l|c|c|} |
---|
251 | \hline |
---|
252 | \multicolumn{1}{|c|}{File} & |
---|
253 | \multicolumn{1}{c|}{Type} & |
---|
254 | \multicolumn{1}{c|}{Description} & |
---|
255 | \multicolumn{1}{c|}{LOC} & |
---|
256 | \multicolumn{1}{c|}{VCs}\\ |
---|
257 | \hline |
---|
258 | \texttt{3-way.c} & C & Three way block cipher & 144 & 34\\ |
---|
259 | \hline |
---|
260 | \texttt{a5.c} & C & A5 stream cipher, used in GSM cellular & 226 & 18\\ |
---|
261 | \hline |
---|
262 | \texttt{array\_sum.c} & S & Sums the elements of an integer array & |
---|
263 | 15 & 9\\ |
---|
264 | \hline |
---|
265 | \texttt{fact.c} & S & Factorial function, imperative implementation & |
---|
266 | 12 & 9\\ |
---|
267 | \hline |
---|
268 | \texttt{is\_sorted.c} & S & Sorting verification of an array & 8 & |
---|
269 | 8\\ |
---|
270 | \hline |
---|
271 | \texttt{LFSR.c} & C & 32-bit linear-feedback shift register & 47 & 3\\ |
---|
272 | \hline |
---|
273 | \texttt{minus.c} & L & Two modes button & 193 & 8\\ |
---|
274 | \hline |
---|
275 | \texttt{mmb.c} & C & Modular multiplication-based block cipher & 124 & 6\\ |
---|
276 | \hline |
---|
277 | \texttt{parity.lus} & L & Parity bit of a boolean array & 359 & 12\\ |
---|
278 | \hline |
---|
279 | \texttt{random.c} & C & Random number generator & 146 & 3\\ |
---|
280 | \hline |
---|
281 | \multicolumn{5}{|c|}{S: standard algorithm \quad C: cryptographic |
---|
282 | function}\\ |
---|
283 | \multicolumn{5}{|c|}{L: $\C$ generated from a $\lustre$ file}\\ |
---|
284 | \hline |
---|
285 | \end{tabular} |
---|
286 | \end{center}} |
---|
287 | |
---|
288 | \end{frame} |
---|
289 | |
---|
290 | \begin{frame} |
---|
291 | \frametitle{About the trusted base of CerCo software} |
---|
292 | |
---|
293 | \begin{block}{What is trusted} |
---|
294 | \begin{itemize} |
---|
295 | \item The cost model provided by the manufacturer. |
---|
296 | \item The cost annotating compiler |
---|
297 | \item The deductive plugin {\sf Jessie} of {\sf Frama-C} |
---|
298 | \end{itemize} |
---|
299 | \end{block} |
---|
300 | |
---|
301 | \begin{block}{What is \textbf{not} trusted} |
---|
302 | \begin{itemize} |
---|
303 | \item The {\sf Frama-C} plugin that computes cost annotations. |
---|
304 | \end{itemize} |
---|
305 | \end{block} |
---|
306 | |
---|
307 | \end{frame} |
---|
308 | |
---|
309 | |
---|
310 | \begin{frame} |
---|
311 | \frametitle{} |
---|
312 | |
---|
313 | \begin{block}{} |
---|
314 | \begin{center} |
---|
315 | \Large Thanks for your attention! \\ |
---|
316 | Any questions? |
---|
317 | \end{center} |
---|
318 | \end{block} |
---|
319 | |
---|
320 | \end{frame} |
---|
321 | |
---|
322 | \end{document} |
---|