source: Deliverables/Dissemination/final-review/wp5/main.tex @ 3282

Last change on this file since 3282 was 3282, checked in by regisgia, 7 years ago
  • WP5 slides for the final review.
File size: 8.8 KB
Line 
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
39This work was (partially) supported by the Information and
40Communication Technologies (ICT) Programme as Project
41FP7-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
74cost of executing the C functions of the program as a function of the value of their
75parameters.
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}{}
204The 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! \\
316Any questions?
317\end{center}
318\end{block}
319
320\end{frame}
321
322\end{document}
Note: See TracBrowser for help on using the repository browser.