232 |
120 |
233 \normalsize |
121 \normalsize |
234 \begin{center} |
122 \begin{center} |
235 \begin{tabular}{ll} |
123 \begin{tabular}{ll} |
236 Email: & christian.urban at kcl.ac.uk\\ |
124 Email: & christian.urban at kcl.ac.uk\\ |
237 Of$\!$fice: & S1.27 (1st floor Strand Building)\\ |
125 Office: & S1.27 (1st floor Strand Building)\\ |
238 Slides: & KEATS (also homework is there)\\ |
126 Slides: & KEATS (also homework is there)\\ |
239 \end{tabular} |
127 \end{tabular} |
240 \end{center} |
128 \end{center} |
241 |
129 |
242 |
130 |
243 \end{frame}} |
131 \end{frame}} |
244 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
132 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
245 |
133 |
246 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
134 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
247 \mode<presentation>{ |
135 \mode<presentation>{ |
248 \begin{frame}[c] |
136 \begin{frame}[c] |
249 \frametitle{Judgements} |
137 \frametitle{} |
|
138 |
|
139 Recall the following scenario: |
|
140 |
|
141 \begin{itemize} |
|
142 \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file}} |
|
143 should be deleted, then this file must be deleted. |
|
144 \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether |
|
145 \textcolor{blue}{\isa{file}} should be deleted (delegation). |
|
146 \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file}}. |
|
147 \end{itemize}\bigskip |
|
148 |
|
149 \small |
|
150 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
|
151 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}},\\ |
|
152 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\ |
|
153 \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\ |
|
154 \end{tabular}}\medskip |
|
155 |
|
156 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}} |
|
157 \end{frame}} |
|
158 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
159 |
|
160 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
161 \mode<presentation>{ |
|
162 \begin{frame}[c] |
|
163 \frametitle{\begin{tabular}{@ {\hspace{-2mm}}c@ {}}The Access Control Problem\end{tabular}} |
|
164 |
250 |
165 |
251 \begin{center} |
166 \begin{center} |
252 \begin{tikzpicture}[scale=1] |
167 \begin{tikzpicture}[scale=1] |
253 |
168 |
254 \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}}; |
169 \draw[line width=1mm] (-.3, -0.5) rectangle (1.5,2); |
255 \onslide<2->{ |
170 \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}}; |
256 \draw (-1,-0.3) node (X) {}; |
171 \draw (4.2,1) node {\begin{tabular}{l}provable/\\not provable\end{tabular}}; |
257 \draw (-2.0,-2.0) node (Y) {}; |
172 \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\end{tabular}}; |
258 \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}}; |
|
259 \draw[red, ->, line width = 2mm] (Y) -- (X); |
|
260 |
173 |
261 \draw (1.2,-0.1) node (X1) {}; |
174 \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); |
262 \draw (2.8,-0.1) node (Y1) {}; |
175 \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1); |
263 \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}}; |
176 \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); |
264 \draw[red, ->, line width = 2mm] (Y1) -- (X1); |
177 |
265 |
178 \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\boldmath\bl{$\Gamma$})\end{tabular}}; |
266 \draw (-0.1,0.1) node (X2) {}; |
179 |
267 \draw (0.5,1.5) node (Y2) {}; |
|
268 \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}}; |
|
269 \draw[red, ->, line width = 2mm] (Y2) -- (X2);} |
|
270 |
|
271 \end{tikzpicture} |
180 \end{tikzpicture} |
272 \end{center} |
181 \end{center} |
273 |
182 |
274 \pause\pause |
183 \end{frame}} |
275 \footnotesize Gimel (Phoenician), Gamma (Greek), C and G (Latin), Gim (Arabic),\\[-2mm] ?? (Indian), Ge (Cyrillic) |
184 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
276 \end{frame}} |
185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
186 \mode<presentation>{ |
278 |
187 \begin{frame}[c] |
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
188 |
280 \mode<presentation>{ |
189 \begin{itemize} |
281 \begin{frame}[c] |
190 \item \bl{$P \,\text{says}\, F$} means \bl{$P$} can send a ``signal'' \bl{$F$} through a wire, or |
282 \frametitle{Inference Rules} |
191 can make a ``statement'' \bl{$F$}\bigskip\pause |
|
192 |
|
193 \item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\ |
|
194 \bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip |
283 |
195 |
284 \begin{center} |
196 \begin{center} |
285 \begin{tikzpicture}[scale=1] |
197 \bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}} |
286 |
|
287 \draw (0.0,0.0) node |
|
288 {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}}; |
|
289 |
|
290 \draw (-0.1,-0.7) node (X) {}; |
|
291 \draw (-0.1,-1.9) node (Y) {}; |
|
292 \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}}; |
|
293 \draw[red, ->, line width = 2mm] (Y) -- (X); |
|
294 |
|
295 \draw (-1,0.6) node (X2) {}; |
|
296 \draw (0.0,1.6) node (Y2) {}; |
|
297 \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}}; |
|
298 \draw[red, ->, line width = 2mm] (Y2) -- (X2); |
|
299 \draw (1,0.6) node (X3) {}; |
|
300 \draw (0.0,1.6) node (Y3) {}; |
|
301 \draw[red, ->, line width = 2mm] (Y3) -- (X3); |
|
302 \end{tikzpicture} |
|
303 \end{center} |
198 \end{center} |
304 |
199 |
305 \only<2>{ |
200 |
306 \begin{textblock}{11}(1,13) |
201 \end{itemize} |
307 \small |
202 |
308 \bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $} |
203 \end{frame}} |
309 \end{textblock}} |
204 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
310 \only<3>{ |
205 |
311 \begin{textblock}{11}(1,13) |
206 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
312 \small |
207 \mode<presentation>{ |
313 \bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge |
208 \begin{frame}[c] |
314 \underbrace{P \,\text{says}\, G}_{F_2} $} |
209 \frametitle{Security Levels} |
315 \end{textblock}} |
210 \small |
316 |
211 |
317 \end{frame}} |
212 \begin{itemize} |
318 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
213 \item Top secret (\bl{$T\!S$}) |
319 |
214 \item Secret (\bl{$S$}) |
320 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
215 \item Public (\bl{$P$}) |
321 \mode<presentation>{ |
216 \end{itemize} |
322 \begin{frame}[c] |
217 |
323 |
218 \begin{center} |
324 \begin{center} |
219 \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause |
325 \Large |
220 \end{center} |
326 \bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1\Rightarrow F_2 & \Gamma \vdash F_1}}\bigskip\bigskip\bigskip |
221 |
327 |
222 \begin{itemize} |
328 \bl{\infer{\Gamma\vdash P\,\text{says}\, F}{\Gamma \vdash F}} |
223 \item Bob has a clearance for ``secret'' |
329 \end{center} |
224 \item Bob can read documents that are public or sectret, but not top secret |
330 |
225 \end{itemize} |
331 \end{frame}} |
226 |
332 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
227 \end{frame}} |
333 |
228 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
334 |
229 % |
335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
230 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
336 \mode<presentation>{ |
231 \mode<presentation>{ |
337 \begin{frame}[t] |
232 \begin{frame}[c] |
338 |
233 \frametitle{Reading a File} |
339 We want to prove |
234 |
340 |
235 \bl{\begin{center} |
341 \begin{center} |
236 \begin{tabular}{c} |
342 \bl{$\Gamma \vdash \text{del\_file}$} |
237 \begin{tabular}{@ {}l@ {}} |
343 \end{center}\pause |
238 \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\ |
344 |
239 \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\ |
345 There is an inference rule |
240 Bob says Permitted $($File, read$)$\only<2->{\\} |
346 |
241 \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}% |
347 \begin{center} |
242 \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}% |
348 \bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} |
243 \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}% |
349 \end{center}\pause |
244 \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}% |
350 |
245 \end{tabular}\\ |
351 So we can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause |
246 \hline |
352 |
247 Permitted $($File, read$)$ |
353 \bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\ |
248 \end{tabular} |
354 So we can use the rule |
249 \end{center}} |
355 |
250 |
356 \begin{center} |
251 \end{frame}} |
357 \bl{\infer{\Gamma, F \vdash F}{}} |
252 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
358 \end{center} |
253 % |
359 |
254 |
360 \onslide<5>{\bf\alert{What is wrong with this?}} |
255 |
361 \hfill{\bf Done. Qed.} |
256 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
362 |
257 \mode<presentation>{ |
363 \end{frame}} |
258 \begin{frame}[c] |
364 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
259 \frametitle{Substitution Rule} |
365 |
260 \small |
366 |
261 |
367 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
262 \bl{\begin{center} |
368 \mode<presentation>{ |
263 \begin{tabular}{c} |
369 \begin{frame}[c] |
264 $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$ |
370 \frametitle{Digression: Proofs in CS} |
265 \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline |
371 |
266 $\Gamma \vdash slev(P) < slev(Q)$ |
372 Formal proofs in CS sound like science fiction? Completely irrelevant! |
267 \end{tabular} |
373 Lecturers gone mad!\pause |
268 \end{center}}\bigskip\pause |
374 |
269 |
375 \begin{itemize} |
270 \begin{itemize} |
376 \item in 2008, verification of a small C-compiler |
271 \item \bl{$slev($Bob$)$ $=$ $S$} |
377 \begin{itemize} |
272 \item \bl{$slev($File$)$ $=$ $P$} |
378 \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' |
273 \item \bl{$slev(P) < slev(S)$} |
379 \item is as good as \texttt{gcc -O1}, but less buggy |
274 \end{itemize} |
380 \end{itemize} |
275 |
381 \medskip |
276 \end{frame}} |
382 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc) |
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
383 \begin{itemize} |
278 % |
384 \item 200k loc of proof |
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
385 \item 25 - 30 person years |
280 \mode<presentation>{ |
386 \item found 160 bugs in the C code (144 by the proof) |
281 \begin{frame}[c] |
387 \end{itemize} |
282 \frametitle{Reading a File} |
388 \end{itemize} |
283 |
389 |
284 \bl{\begin{center} |
390 \end{frame}} |
285 \begin{tabular}{c} |
391 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
286 \begin{tabular}{@ {}l@ {}} |
392 |
287 $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\ |
|
288 \hspace{3cm}Bob controls Permitted $($File, read$)$\\ |
|
289 Bob says Permitted $($File, read$)$\\ |
|
290 $slev($File$)$ $=$ $P$\\ |
|
291 $slev($Bob$)$ $=$ $T\!S$\\ |
|
292 \only<1>{\textcolor{red}{$?$}}% |
|
293 \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}% |
|
294 \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}% |
|
295 \end{tabular}\\ |
|
296 \hline |
|
297 Permitted $($File, read$)$ |
|
298 \end{tabular} |
|
299 \end{center}} |
|
300 |
|
301 \end{frame}} |
|
302 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
303 % |
|
304 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
305 \mode<presentation>{ |
|
306 \begin{frame}[c] |
|
307 \frametitle{Transitivity Rule} |
|
308 \small |
|
309 |
|
310 \bl{\begin{center} |
|
311 \begin{tabular}{c} |
|
312 $\Gamma \vdash l_1 < l_2$ |
|
313 \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline |
|
314 $\Gamma \vdash l_1 < l_3$ |
|
315 \end{tabular} |
|
316 \end{center}}\bigskip |
|
317 |
|
318 \begin{itemize} |
|
319 \item \bl{$slev(P) < slev (S)$} |
|
320 \item \bl{$slev(S) < slev (T\!S)$} |
|
321 \item[] \bl{$slev(P) < slev (T\!S)$} |
|
322 \end{itemize} |
|
323 |
|
324 \end{frame}} |
|
325 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
326 % |
|
327 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
328 \mode<presentation>{ |
|
329 \begin{frame}[c] |
|
330 \frametitle{Reading Files} |
|
331 |
|
332 \begin{itemize} |
|
333 \item Access policy for Bob for reading |
|
334 \end{itemize} |
|
335 |
|
336 \bl{\begin{center} |
|
337 \begin{tabular}{c} |
|
338 \begin{tabular}{@ {}l@ {}} |
|
339 $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\ |
|
340 \hspace{3cm}Bob controls Permitted $(f$, read$)$\\ |
|
341 Bob says Permitted $($File, read$)$\\ |
|
342 $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\ |
|
343 $slev($Bob$)$ $=$ $T\!S$\\ |
|
344 $slev(P) < slev(S)$\\ |
|
345 $slev(S) < slev(T\!S)$ |
|
346 \end{tabular}\\ |
|
347 \hline |
|
348 Permitted $($File, read$)$ |
|
349 \end{tabular} |
|
350 \end{center}} |
|
351 |
|
352 \end{frame}} |
|
353 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
354 % |
|
355 |
|
356 |
|
357 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
358 \mode<presentation>{ |
|
359 \begin{frame}[c] |
|
360 \frametitle{Writing Files} |
|
361 |
|
362 \begin{itemize} |
|
363 \item Access policy for Bob for {\bf writing} |
|
364 \end{itemize} |
|
365 |
|
366 \bl{\begin{center} |
|
367 \begin{tabular}{c} |
|
368 \begin{tabular}{@ {}l@ {}} |
|
369 $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\ |
|
370 \hspace{3cm}Bob controls Permitted $(f$, write$)$\\ |
|
371 Bob says Permitted $($File, write$)$\\ |
|
372 $slev($File$)$ $=$ $T\!S$\\ |
|
373 $slev($Bob$)$ $=$ $S$\\ |
|
374 $slev(P) < slev(S)$\\ |
|
375 $slev(S) < slev(T\!S)$ |
|
376 \end{tabular}\\ |
|
377 \hline |
|
378 Permitted $($File, write$)$ |
|
379 \end{tabular} |
|
380 \end{center}} |
|
381 |
|
382 \end{frame}} |
|
383 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
384 % |
|
385 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
386 \mode<presentation>{ |
|
387 \begin{frame}[c] |
|
388 \frametitle{Encrypted Messages} |
|
389 |
|
390 \begin{itemize} |
|
391 \item Alice sends a message \bl{$m$} |
|
392 \begin{center} |
|
393 \bl{Alice says $m$} |
|
394 \end{center}\medskip\pause |
|
395 |
|
396 \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$}) |
|
397 \begin{center} |
|
398 \bl{Alice says $\{m\}_K$} |
|
399 \end{center}\medskip\pause |
|
400 |
|
401 \item Decryption of Alice's message\smallskip |
|
402 \begin{center} |
|
403 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} |
|
404 {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
|
405 \end{center} |
|
406 \end{itemize} |
|
407 |
|
408 \end{frame}} |
|
409 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
410 |
393 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
411 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
394 \mode<presentation>{ |
412 \mode<presentation>{ |
395 \begin{frame}[c] |
413 \begin{frame}[c] |
396 \frametitle{} |
414 \frametitle{Encryption} |
397 |
415 |
398 \begin{tabular}{c@ {\hspace{2mm}}c} |
416 \begin{itemize} |
399 \\[6mm] |
417 \item Encryption of a message\smallskip |
400 \begin{tabular}{c} |
418 \begin{center} |
401 \includegraphics[scale=0.11]{harper.jpg}\\[-2mm] |
419 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K} |
402 {\footnotesize Bob Harper}\\[-2.5mm] |
420 {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
403 {\footnotesize (CMU)} |
421 \end{center} |
404 \end{tabular} |
422 \end{itemize} |
405 \begin{tabular}{c} |
|
406 \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm] |
|
407 {\footnotesize Frank Pfenning}\\[-2.5mm] |
|
408 {\footnotesize (CMU)} |
|
409 \end{tabular} & |
|
410 |
|
411 \begin{tabular}{p{6cm}} |
|
412 \raggedright |
|
413 \color{gray}{published a proof about a specification in a journal (2005), |
|
414 $\sim$31pages} |
|
415 \end{tabular}\\ |
|
416 |
|
417 \pause |
|
418 \\[0mm] |
|
419 |
|
420 \begin{tabular}{c} |
|
421 \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] |
|
422 {\footnotesize Andrew Appel}\\[-2.5mm] |
|
423 {\footnotesize (Princeton)} |
|
424 \end{tabular} & |
|
425 |
|
426 \begin{tabular}{p{6cm}} |
|
427 \raggedright |
|
428 \color{gray}{relied on their proof in a\\ {\bf security} critical application} |
|
429 \end{tabular} |
|
430 \end{tabular} |
|
431 |
423 |
432 \end{frame}} |
424 \end{frame}} |
433 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
425 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
434 |
|
435 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
436 \mode<presentation>{ |
|
437 \begin{frame} |
|
438 \frametitle{Proof-Carrying Code} |
|
439 |
|
440 \begin{textblock}{10}(2.5,2.2) |
|
441 \begin{block}{Idea:} |
|
442 \begin{center} |
|
443 \begin{tikzpicture} |
|
444 \draw[help lines,cream] (0,0.2) grid (8,4); |
|
445 |
|
446 \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4); |
|
447 \node[anchor=base] at (6.5,2.8) |
|
448 {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering user: untrusted code\end{tabular}}; |
|
449 |
|
450 \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4); |
|
451 \node[anchor=base] at (1.5,2.3) |
|
452 {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering developer ---\\ web server\end{tabular}}; |
|
453 |
|
454 \onslide<3->{ |
|
455 \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8); |
|
456 \node[anchor=base,white] at (6.5,1.1) |
|
457 {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};} |
|
458 |
|
459 \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code}; |
|
460 \onslide<2->{ |
|
461 \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf certificate}; |
|
462 \node at (3.8,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof}}; |
|
463 } |
|
464 |
|
465 |
|
466 \end{tikzpicture} |
|
467 \end{center} |
|
468 \end{block} |
|
469 \end{textblock} |
|
470 |
|
471 %\begin{textblock}{15}(2,12) |
|
472 %\small |
|
473 %\begin{itemize} |
|
474 %\item<4-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; |
|
475 %803 loc in C including 2 library functions)\\[-3mm] |
|
476 %\item<5-> 167 loc in C implement a type-checker |
|
477 %\end{itemize} |
|
478 %\end{textblock} |
|
479 |
|
480 \end{frame}} |
|
481 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
482 |
|
483 \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex] |
|
484 \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, |
|
485 draw=black!50, top color=white, bottom color=black!20] |
|
486 \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, |
|
487 draw=red!70, top color=white, bottom color=red!50!black!20] |
|
488 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
489 \mode<presentation>{ |
|
490 \begin{frame}<2->[squeeze] |
|
491 \frametitle{} |
|
492 |
|
493 \begin{columns} |
|
494 |
|
495 \begin{column}{0.8\textwidth} |
|
496 \begin{textblock}{0}(1,2) |
|
497 |
|
498 \begin{tikzpicture} |
|
499 \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm] |
|
500 { \&[-10mm] |
|
501 \node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \& |
|
502 \node (proof1) [node1] {\large Proof}; \& |
|
503 \node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\ |
|
504 |
|
505 \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \& |
|
506 \onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \& |
|
507 \onslide<4->{\node (proof2) [node1] {\large Proof};} \& |
|
508 \onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\ |
|
509 |
|
510 \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \& |
|
511 \onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \& |
|
512 \onslide<5->{\node (proof3) [node1] {\large Proof};} \& |
|
513 \onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\ |
|
514 |
|
515 \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \& |
|
516 \onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \& |
|
517 \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \& |
|
518 \onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\ |
|
519 }; |
|
520 |
|
521 \draw[->,black!50,line width=2mm] (proof1) -- (def1); |
|
522 \draw[->,black!50,line width=2mm] (proof1) -- (alg1); |
|
523 |
|
524 \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);} |
|
525 \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);} |
|
526 |
|
527 \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);} |
|
528 \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);} |
|
529 |
|
530 \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);} |
|
531 \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);} |
|
532 |
|
533 \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} |
|
534 \end{tikzpicture} |
|
535 |
|
536 \end{textblock} |
|
537 \end{column} |
|
538 \end{columns} |
|
539 |
|
540 |
|
541 \begin{textblock}{3}(12,3.6) |
|
542 \onslide<4->{ |
|
543 \begin{tikzpicture} |
|
544 \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h}; |
|
545 \end{tikzpicture}} |
|
546 \end{textblock} |
|
547 |
|
548 \end{frame}} |
|
549 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
550 |
|
551 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
552 \mode<presentation>{ |
|
553 \begin{frame}[c] |
|
554 \frametitle{Mars Pathfinder Mission 1997} |
|
555 |
|
556 \begin{center} |
|
557 \includegraphics[scale=0.15]{marspath1.png} |
|
558 \includegraphics[scale=0.16]{marspath3.png} |
|
559 \includegraphics[scale=0.3]{marsrover.png} |
|
560 \end{center} |
|
561 |
|
562 \begin{itemize} |
|
563 \item despite NASA's famous testing procedure, the lander crashed frequently on Mars |
|
564 \item problem was an algorithm not used in the OS |
|
565 \end{itemize} |
|
566 |
|
567 \end{frame}} |
|
568 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
569 |
|
570 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
571 \mode<presentation>{ |
|
572 \begin{frame}[c] |
|
573 \frametitle{Priority Inheritance Protocol} |
|
574 |
|
575 \begin{itemize} |
|
576 \item \ldots a scheduling algorithm that is widely used in real-time operating systems |
|
577 \item has been ``proved'' correct by hand in a paper in 1983 |
|
578 \item \ldots but the first algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause |
|
579 |
|
580 \item we specified the algorithm and then proved that the specification makes |
|
581 ``sense'' |
|
582 \item we implemented our specification in C on top of PINTOS (used for teaching at Stanford) |
|
583 \item our implementation was much more efficient than their reference implementation |
|
584 \end{itemize} |
|
585 |
|
586 \end{frame}} |
|
587 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
588 |
|
589 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
590 \mode<presentation>{ |
|
591 \begin{frame}[c] |
|
592 \frametitle{Regular Expression Matching} |
|
593 \tiny |
|
594 |
|
595 \begin{tabular}{@ {\hspace{-6mm}}cc} |
|
596 \begin{tikzpicture}[y=.1cm, x=.15cm] |
|
597 %axis |
|
598 \draw (0,0) -- coordinate (x axis mid) (30,0); |
|
599 \draw (0,0) -- coordinate (y axis mid) (0,30); |
|
600 %ticks |
|
601 \foreach \x in {0,5,...,30} |
|
602 \draw (\x,1pt) -- (\x,-3pt) |
|
603 node[anchor=north] {\x}; |
|
604 \foreach \y in {0,5,...,30} |
|
605 \draw (1pt,\y) -- (-3pt,\y) |
|
606 node[anchor=east] {\y}; |
|
607 %labels |
|
608 \node[below=0.3cm] at (x axis mid) {\bl{a}s}; |
|
609 \node[rotate=90, left=0.6cm] at (y axis mid) {secs}; |
|
610 |
|
611 %plots |
|
612 \draw[color=blue] plot[mark=*, mark options={fill=white}] |
|
613 file {re-python.data}; |
|
614 \only<1->{ |
|
615 \draw[color=red] plot[mark=triangle*, mark options={fill=white} ] |
|
616 file {re1.data};} |
|
617 \only<1->{ |
|
618 \draw[color=green] plot[mark=square*, mark options={fill=white} ] |
|
619 file {re2.data};} |
|
620 |
|
621 %legend |
|
622 \begin{scope}[shift={(4,20)}] |
|
623 \draw[color=blue] (0,0) -- |
|
624 plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
625 node[right]{\footnotesize Python}; |
|
626 \only<1->{\draw[yshift=6mm, color=red] (0,0) -- |
|
627 plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
628 node[right]{\footnotesize Scala V1};} |
|
629 \only<1->{ |
|
630 \draw[yshift=12mm, color=green] (0,0) -- |
|
631 plot[mark=square*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
632 node[right]{\footnotesize Scala V2 with simplifications};} |
|
633 \end{scope} |
|
634 \end{tikzpicture} & |
|
635 |
|
636 \begin{tikzpicture}[y=.35cm, x=.00045cm] |
|
637 %axis |
|
638 \draw (0,0) -- coordinate (x axis mid) (10000,0); |
|
639 \draw (0,0) -- coordinate (y axis mid) (0,6); |
|
640 %ticks |
|
641 \foreach \x in {0,2000,...,10000} |
|
642 \draw (\x,1pt) -- (\x,-3pt) |
|
643 node[anchor=north] {\x}; |
|
644 \foreach \y in {0,1,...,6} |
|
645 \draw (1pt,\y) -- (-3pt,\y) |
|
646 node[anchor=east] {\y}; |
|
647 %labels |
|
648 \node[below=0.3cm] at (x axis mid) {\bl{a}s}; |
|
649 \node[rotate=90, left=0.6cm] at (y axis mid) {secs}; |
|
650 |
|
651 %plots |
|
652 \draw[color=blue] plot[mark=*, mark options={fill=white}] |
|
653 file {re-internal.data}; |
|
654 \only<1->{ |
|
655 \draw[color=red] plot[mark=triangle*, mark options={fill=white} ] |
|
656 file {re3.data};} |
|
657 |
|
658 %legend |
|
659 \begin{scope}[shift={(2000,4)}] |
|
660 \draw[color=blue] (0,0) -- |
|
661 plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
662 node[right]{\footnotesize Scala Internal}; |
|
663 \only<1->{ |
|
664 \draw[yshift=6mm, color=red] (0,0) -- |
|
665 plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
666 node[right]{\footnotesize Scala V3};} |
|
667 \end{scope} |
|
668 \end{tikzpicture} |
|
669 \end{tabular}\bigskip\pause |
|
670 \normalsize |
|
671 \begin{itemize} |
|
672 \item I needed a proof in order to make sure my program is correct |
|
673 \end{itemize}\pause |
|
674 |
|
675 \begin{center} |
|
676 \bl{End Digression.\\ (Our small proof is 0.0005\% of the OS-proof.)} |
|
677 \end{center} |
|
678 |
|
679 \end{frame}} |
|
680 |
|
681 |
|
682 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
683 |
|
684 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
685 \mode<presentation>{ |
|
686 \begin{frame}[c] |
|
687 \frametitle{One More Thing} |
|
688 |
|
689 \begin{itemize} |
|
690 \item I arrived at King's last year |
|
691 \item Maxime Crochemore told me about a string algorithm (suffix sorting) that appeared at a |
|
692 conference in 2007 (ICALP) |
|
693 \item ``horribly incomprehensible'', no implementation, but claims to be the best \bl{$O(n + k)$} algorithm\bigskip\pause |
|
694 |
|
695 \item Jian Jiang found 1 error and 1 superfluous step in this algorithm |
|
696 \item he received 88\% for the project and won the prize for the best 7CCSMPRJ project in the department |
|
697 \item no proof \ldots{} yet |
|
698 \end{itemize} |
|
699 |
|
700 \end{frame}} |
|
701 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
702 |
|
703 |
426 |
704 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
427 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
705 \mode<presentation>{ |
428 \mode<presentation>{ |
706 \begin{frame}[c] |
429 \begin{frame}[c] |
707 \frametitle{Trusted Third Party} |
430 \frametitle{Trusted Third Party} |
907 |
628 |
908 \end{frame}} |
629 \end{frame}} |
909 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
630 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
910 |
631 |
911 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
632 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
912 \mode<presentation>{ |
633 \mode<presentation>{ |
913 \begin{frame}[c] |
634 \begin{frame}[c] |
914 \frametitle{Another Challenge-Response} |
635 |
915 |
636 A Man-in-the-middle attack in real life: |
916 \bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to identify |
637 |
917 each other\bigskip |
638 \begin{itemize} |
918 |
639 \item the card only says yes or no to the terminal if the PIN is correct |
919 \begin{itemize} |
640 \item trick the card in thinking transaction is verified by signature |
920 \item \bl{$A \,\text{sends}\, B : A, N_A$} |
641 \item trick the terminal in thinking the transaction was verified by PIN |
921 \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$} |
642 \end{itemize} |
922 \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$} |
643 |
923 \end{itemize} |
644 \begin{minipage}{1.1\textwidth} |
924 \end{frame}} |
645 \begin{center} |
925 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
646 \mbox{}\hspace{-6mm}\includegraphics[scale=0.5]{pics/chip-attack.png} |
|
647 \includegraphics[scale=0.3]{pics/chipnpinflaw.png} |
|
648 \end{center} |
|
649 \end{minipage} |
|
650 |
|
651 \end{frame}} |
|
652 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
653 |
|
654 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
655 \mode<presentation>{ |
|
656 \begin{frame}[c] |
|
657 \frametitle{Problems with EMV} |
|
658 |
|
659 \begin{itemize} |
|
660 \item it is a wrapper for many protocols |
|
661 \item specification by consensus (resulted unmanageable complexity) |
|
662 \item its specification is 700 pages in English plus 2000+ pages for testing, additionally some |
|
663 further parts are secret |
|
664 \item other attacks have been found |
|
665 |
|
666 \item one solution might be to require always online verification of the PIN with the bank |
|
667 \end{itemize} |
|
668 |
|
669 \end{frame}} |
|
670 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
671 |
|
672 |
|
673 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
674 \mode<presentation>{ |
|
675 \begin{frame}[c] |
|
676 \frametitle{\begin{tabular}{c}Problems with WEP (Wifi)\end{tabular}} |
|
677 |
|
678 \begin{itemize} |
|
679 \item a standard ratified in 1999 |
|
680 \item the protocol was designed by a committee not including cryptographers |
|
681 \item it used the RC4 encryption algorithm which is a stream cipher requiring a unique nonce |
|
682 \item WEP did not allocate enough bits for the nonce |
|
683 \item for authenticating packets it used CRC checksum which can be easily broken |
|
684 \item the network password was used to directly encrypt packages (instead of a key negotiation protocol)\bigskip |
|
685 \item encryption was turned off by default |
|
686 \end{itemize} |
|
687 |
|
688 \end{frame}} |
|
689 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
690 |
|
691 |
|
692 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
693 \mode<presentation>{ |
|
694 \begin{frame}[c] |
|
695 \frametitle{Protocols are Difficult} |
|
696 |
|
697 \begin{itemize} |
|
698 \item even the systems designed by experts regularly fail\medskip |
|
699 \item try to make everything explicit (you need to authenticate all data you might rely on)\medskip |
|
700 \item the one who can fix a system should also be liable for the losses\medskip |
|
701 \item cryptography is often not {\bf the} answer\bigskip\bigskip |
|
702 \end{itemize} |
|
703 |
|
704 logic is one way protocols are studied in academia |
|
705 (you can use computers to search for attacks) |
|
706 |
|
707 \end{frame}} |
|
708 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
709 |
|
710 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
711 \mode<presentation>{ |
|
712 \begin{frame}[c] |
|
713 \frametitle{Public-Key Infrastructure} |
|
714 |
|
715 \begin{itemize} |
|
716 \item the idea is to have a certificate authority (CA) |
|
717 \item you go to the CA to identify yourself |
|
718 \item CA: ``I, the CA, have verified that public key \bl{$P^{pub}_{Bob}$} belongs to Bob''\bigskip |
|
719 \item CA must be trusted by everybody |
|
720 \item What happens if CA issues a false certificate? Who pays in case of loss? (VeriSign |
|
721 explicitly limits liability to \$100.) |
|
722 \end{itemize} |
|
723 |
|
724 \end{frame}} |
|
725 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
726 |
|
727 |
|
728 |
|
729 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
730 \mode<presentation>{ |
|
731 \begin{frame}[c] |
|
732 \frametitle{Privacy, Anonymity et al} |
|
733 |
|
734 Some terminology: |
|
735 |
|
736 \begin{itemize} |
|
737 \item \alert{secrecy} is the mechanism used to limit the number of |
|
738 principals with access to information (eg, cryptography or access controls) |
|
739 |
|
740 \item \alert{confidentiality} is the obligation to protect the secrets of other people |
|
741 or organizations (secrecy for the benefit of an organisation) |
|
742 |
|
743 \item \alert{anonymity} is the ability to leave no evidence of an activity (eg, sharing a secret) |
|
744 |
|
745 \item \alert{privacy} is the ability or right to protect your personal secrets |
|
746 (secrecy for the benefit of an individual) |
|
747 |
|
748 \end{itemize} |
|
749 |
|
750 \end{frame}} |
|
751 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
752 |
|
753 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
754 \mode<presentation>{ |
|
755 \begin{frame}[t] |
|
756 \frametitle{Privacy vs Anonymity} |
|
757 |
|
758 \begin{itemize} |
|
759 \item everybody agrees that anonymity has its uses (e.g., voting, whistleblowers, peer-review) |
|
760 \end{itemize}\bigskip\bigskip\pause |
|
761 |
|
762 |
|
763 But privacy?\bigskip\bigskip |
|
764 |
|
765 ``You have zero privacy anyway. Get over it.''\\ |
|
766 \hfill{}Scott Mcnealy (CEO of Sun)\bigskip\\ |
|
767 |
|
768 |
|
769 If you have nothing to hide, you have nothing to fear. |
|
770 |
|
771 \end{frame}} |
|
772 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
773 |
|
774 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
775 \mode<presentation>{ |
|
776 \begin{frame}[t] |
|
777 \frametitle{Privacy} |
|
778 |
|
779 private data can be often used against me |
|
780 |
|
781 \begin{itemize} |
|
782 \item if my location data becomes public, thieves will switch off their phones and help themselves in my home |
|
783 \item if supermarkets can build a profile of what I buy, they can use it to their advantage (banks - mortgages) |
|
784 \item my employer might not like my opinions\bigskip\pause |
|
785 |
|
786 \item one the other hand, Freedom-of-Information Act |
|
787 \item medical data should be private, but medical research needs data |
|
788 \end{itemize} |
|
789 |
|
790 \end{frame}} |
|
791 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
792 |
|
793 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
794 \mode<presentation>{ |
|
795 \begin{frame}[t] |
|
796 \frametitle{Privacy Problems} |
|
797 |
|
798 \begin{itemize} |
|
799 \item Apple takes note of every dictation (send over the Internet to Apple) |
|
800 \item markets often only work, if data is restricted (to build trust) |
|
801 \item Social network can reveal data about you |
|
802 \item have you tried the collusion extension for FireFox? |
|
803 \item I do use Dropbox and store cards\bigskip |
|
804 \item next week: anonymising data |
|
805 \end{itemize} |
|
806 |
|
807 \begin{textblock}{5}(12,9.8) |
|
808 \includegraphics[scale=0.2]{pics/gattaca.jpg}\\ |
|
809 \small Gattaca (1997) |
|
810 \end{textblock} |
|
811 |
|
812 \end{frame}} |
|
813 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
814 |
|
815 |
|
816 |
|
817 |
|
818 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
819 \mode<presentation>{ |
|
820 \begin{frame}[t] |
|
821 \frametitle{Privacy} |
|
822 |
|
823 \begin{minipage}{1.05\textwidth} |
|
824 \begin{itemize} |
|
825 \item we \alert{do} want that government data is made public (free maps for example) |
|
826 \item we \alert{do not} want that medical data becomes public (similarly tax data, school |
|
827 records, job offers)\bigskip |
|
828 \item personal information can potentially lead to fraud |
|
829 (identity theft) |
|
830 \end{itemize}\pause |
|
831 |
|
832 {\bf ``The reality'':} |
|
833 \only<2>{\begin{itemize} |
|
834 \item London Health Programmes lost in June last year unencrypted details of more than 8 million people |
|
835 (no names, but postcodes and details such as gender, age and ethnic origin) |
|
836 \end{itemize}} |
|
837 \only<3>{\begin{itemize} |
|
838 \item also in June last year, Sony got hacked: over 1M users' personal information, including passwords, email addresses, home addresses, dates of birth, and all Sony opt-in data associated with their accounts. |
|
839 \end{itemize}} |
|
840 \end{minipage} |
|
841 |
|
842 \end{frame}} |
|
843 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
844 |
|
845 |
|
846 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
847 \mode<presentation>{ |
|
848 \begin{frame}[c] |
|
849 \frametitle{Privacy and Big Data} |
|
850 |
|
851 Selected sources of ``Big Data'':\smallskip{} |
|
852 |
|
853 \begin{itemize} |
|
854 \item Facebook |
|
855 \begin{itemize} |
|
856 \item 40+ Billion photos (100 PB) |
|
857 \item 6 Billion messages daily (5 - 10 TB) |
|
858 \item 900 Million users |
|
859 \end{itemize} |
|
860 \item Common Crawl |
|
861 \begin{itemize} |
|
862 \item covers 3.8 Billion webpages (2012 dataset) |
|
863 \item 50 TB of data |
|
864 \end{itemize} |
|
865 \item Google |
|
866 \begin{itemize} |
|
867 \item 20 PB daily (2008) |
|
868 \end{itemize} |
|
869 \item Twitter |
|
870 \begin{itemize} |
|
871 \item 7 Million users in the UK |
|
872 \item a company called Datasift is allowed to mine all tweets since 2010 |
|
873 \item they charge 10k per month for other companies to target advertisement |
|
874 \end{itemize} |
|
875 \end{itemize}\pause |
|
876 |
|
877 |
|
878 \end{frame}} |
|
879 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
880 |
|
881 |
|
882 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
883 \mode<presentation>{ |
|
884 \begin{frame}[c] |
|
885 \frametitle{Cookies\ldots} |
|
886 |
|
887 ``We have published a new cookie policy. It explains what cookies are |
|
888 and how we use them on our site. To learn more about cookies and |
|
889 their benefits, please view our cookie policy.\medskip |
|
890 |
|
891 If you'd like to disable cookies on this device, please view our information |
|
892 pages on 'How to manage cookies'. Please be aware that parts of the |
|
893 site will not function correctly if you disable cookies. \medskip |
|
894 |
|
895 By closing this |
|
896 message, you consent to our use of cookies on this device in accordance |
|
897 with our cookie policy unless you have disabled them.'' |
|
898 |
|
899 |
|
900 \end{frame}} |
|
901 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
902 |
|
903 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
904 \mode<presentation>{ |
|
905 \begin{frame}[c] |
|
906 \frametitle{Scare Tactics} |
|
907 |
|
908 The actual policy reads:\bigskip |
|
909 |
|
910 ``As we explain in our Cookie Policy, cookies help you to get the most |
|
911 out of our websites.\medskip |
|
912 |
|
913 If you do disable our cookies you may find that certain sections of our |
|
914 website do not work. For example, you may have difficulties logging in |
|
915 or viewing articles.'' |
|
916 |
|
917 |
|
918 |
|
919 |
|
920 \end{frame}} |
|
921 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
922 |
|
923 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
924 \mode<presentation>{ |
|
925 \begin{frame}[c] |
|
926 \frametitle{Netflix Prize} |
|
927 |
|
928 Anonymity is \alert{necessary} for privacy, but \alert{not} enough!\bigskip |
|
929 |
|
930 \begin{itemize} |
|
931 \item Netflix offered in 2006 (and every year until 2010) a 1 Mio \$ prize for improving their movie rating algorithm |
|
932 \item dataset contained 10\% of all Netflix users (appr.~500K) |
|
933 \item names were removed, but included numerical ratings as well as times of rating |
|
934 \item some information was \alert{perturbed} (i.e., slightly modified) |
|
935 \end{itemize} |
|
936 |
|
937 \hfill{\bf\alert{All OK?}} |
|
938 |
|
939 \end{frame}} |
|
940 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
941 |
|
942 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
943 \mode<presentation>{ |
|
944 \begin{frame}[c] |
|
945 \frametitle{Re-identification Attack} |
|
946 |
|
947 Two researchers analysed the data: |
|
948 |
|
949 \begin{itemize} |
|
950 \item with 8 ratings (2 of them can be wrong) and corresponding dates that can have a margin 14-day error, 98\% of the |
|
951 records can be identified |
|
952 \item for 68\% only two ratings and dates are sufficient (for movie ratings outside the top 500)\bigskip\pause |
|
953 \item they took 50 samples from IMDb (where people can reveal their identity) |
|
954 \item 2 of them uniquely identified entries in the Netflix database (either by movie rating or by dates) |
|
955 \end{itemize} |
|
956 |
|
957 \end{frame}} |
|
958 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
959 |
|
960 |
|
961 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
962 \mode<presentation>{ |
|
963 \begin{frame}[c] |
|
964 \frametitle{} |
|
965 |
|
966 \begin{itemize} |
|
967 \item Birth data, postcode and gender (unique for\\ 87\% of the US population) |
|
968 \item Preferences in movies (99\% of 500K for 8 ratings) |
|
969 \end{itemize}\bigskip |
|
970 |
|
971 Therefore best practices / or even law (HIPAA, EU): |
|
972 |
|
973 \begin{itemize} |
|
974 \item only year dates (age group for 90 years or over), |
|
975 \item no postcodes (sector data is OK, similarly in the US)\\ |
|
976 \textcolor{gray}{no names, addresses, account numbers, licence plates} |
|
977 \item disclosure information needs to be retained for 5 years |
|
978 \end{itemize} |
|
979 |
|
980 \end{frame}} |
|
981 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
982 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
983 \mode<presentation>{ |
|
984 \begin{frame}<2>[c] |
|
985 \frametitle{How to Safely Disclose Information?} |
|
986 |
|
987 \only<1>{ |
|
988 \begin{itemize} |
|
989 \item Assume you make a survey of 100 randomly chosen people. |
|
990 \item Say 99\% of the surveyed people in the 10 - 40 age group have seen the |
|
991 Gangnam video on youtube.\bigskip |
|
992 |
|
993 \item What can you infer about the rest of the population? |
|
994 \end{itemize}} |
|
995 \only<2>{ |
|
996 \begin{itemize} |
|
997 \item Is it possible to re-identify data later, if more data is released. \bigskip\bigskip\pause |
|
998 |
|
999 \item Not even releasing only aggregate information prevents re-identification attacks. |
|
1000 (GWAS was a public database of gene-frequency studies linked to diseases; |
|
1001 you only needed partial DNA information in order |
|
1002 to identify whether an individual was part of the study --- DB closed in 2008) |
|
1003 \end{itemize}} |
|
1004 |
|
1005 \end{frame}} |
|
1006 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
926 |
1007 |
927 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1008 |
928 \mode<presentation>{ |
1009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
929 \begin{frame}[c] |
1010 \mode<presentation>{ |
930 \frametitle{Another Challenge-Response} |
1011 \begin{frame}[c] |
931 |
1012 \frametitle{Differential Privacy} |
932 \bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to identify |
|
933 each other\bigskip |
|
934 |
|
935 \begin{itemize} |
|
936 \item \bl{$A \,\text{sends}\, B : A, N_A$} |
|
937 \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$} |
|
938 \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$} |
|
939 \end{itemize} |
|
940 \end{frame}} |
|
941 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
942 |
|
943 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
944 \mode<presentation>{ |
|
945 \begin{frame}[c] |
|
946 \frametitle{Another Challenge-Response} |
|
947 |
|
948 Unfortunately, an intruder \bl{$I$} can impersonate \bl{$B$}. |
|
949 |
1013 |
950 \begin{center} |
1014 \begin{center} |
951 \begin{tabular}{@{\hspace{-7mm}}c@{\hspace{1mm}}c@{}} |
1015 User\;\;\;\; |
952 \begin{tabular}{@{}l@{}} |
1016 \begin{tabular}{c} |
953 \onslide<1->{\bl{$A \,\text{sends}\, I : A, N_A$}}\\ |
1017 tell me \bl{$f(x)$} $\Rightarrow$\\ |
954 \onslide<4->{\bl{$I \,\text{sends}\, A : \{N_A,\!K'_{\!AB}\}_{K_{\!AB}}$}}\\ |
1018 $\Leftarrow$ \bl{$f(x) + \text{noise}$} |
955 \onslide<5->{\bl{$A \,\text{sends}\, I : \{N_A\}_{K'_{AB}}$}}\\ |
|
956 \end{tabular} |
1019 \end{tabular} |
957 & |
1020 \;\;\;\;\begin{tabular}{@{}c} |
958 \begin{tabular}{@{}l@{}} |
1021 Database\\ |
959 \onslide<2->{\bl{$I \,\text{sends}\, A : B, N_A$}}\\ |
1022 \bl{$x_1, \ldots, x_n$} |
960 \onslide<3->{\bl{$A \,\text{sends}\, I : \{N_A,\!K'_{\!AB}\}_{K_{\!AB}}$}}\\ |
|
961 \onslide<6->{\bl{$I \,\text{sends}\, A : \{N_A\}_{K'_{AB}}$}}\\ |
|
962 \end{tabular} |
|
963 \end{tabular} |
1023 \end{tabular} |
964 \end{center} |
1024 \end{center} |
965 |
1025 |
966 \end{frame}} |
1026 |
967 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1027 \begin{itemize} |
|
1028 \item \bl{$f(x)$} can be released, if \bl{$f$} is insensitive to |
|
1029 individual entries \bl{$x_1, \ldots, x_n$}\\ |
|
1030 \item Intuition: whatever is learned from the dataset would be learned regardless of whether |
|
1031 \bl{$x_i$} participates\bigskip\pause |
|
1032 |
|
1033 \item Noised needed in order to prevent queries:\\ Christian's salary $=$ |
|
1034 \begin{center} |
|
1035 \bl{\large$\Sigma$} all staff $-$ \bl{\large$\Sigma$} all staff $\backslash$ Christian |
|
1036 \end{center} |
|
1037 \end{itemize} |
|
1038 |
|
1039 \end{frame}} |
|
1040 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1041 |
|
1042 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1043 \mode<presentation>{ |
|
1044 \begin{frame}[c] |
|
1045 \frametitle{Adding Noise} |
|
1046 |
|
1047 Adding noise is not as trivial as one would wish: |
|
1048 |
|
1049 \begin{itemize} |
|
1050 \item If I ask how many of three have seen the Gangnam video and get a result |
|
1051 as follows |
|
1052 |
|
1053 \begin{center} |
|
1054 \begin{tabular}{l|c} |
|
1055 Alice & yes\\ |
|
1056 Bob & no\\ |
|
1057 Charlie & yes\\ |
|
1058 \end{tabular} |
|
1059 \end{center} |
|
1060 |
|
1061 then I have to add a noise of \bl{$1$}. So answers would be in the |
|
1062 range of \bl{$1$} to \bl{$3$} |
|
1063 |
|
1064 \bigskip |
|
1065 \item But if I ask five questions for all the dataset (has seen Gangnam video, is male, below 30, \ldots), |
|
1066 then one individual can change the dataset by \bl{$5$} |
|
1067 \end{itemize} |
|
1068 |
|
1069 \end{frame}} |
|
1070 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
968 |
1071 |
|
1072 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1073 \mode<presentation>{ |
|
1074 \begin{frame}[c] |
|
1075 \frametitle{\begin{tabular}{@{}c@{}}Take Home Point\end{tabular}} |
|
1076 |
|
1077 According to Ross Anderson: \bigskip |
|
1078 \begin{itemize} |
|
1079 \item Privacy in a big hospital is just about doable.\medskip |
|
1080 \item How do you enforce privacy in something as big as Google |
|
1081 or complex as Facebook? No body knows.\bigskip |
|
1082 |
|
1083 Similarly, big databases imposed by government |
|
1084 \end{itemize} |
|
1085 |
|
1086 |
|
1087 \end{frame}} |
|
1088 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
969 |
1089 |
970 \end{document} |
1090 \end{document} |
971 |
1091 |
972 %%% Local Variables: |
1092 %%% Local Variables: |
973 %%% mode: latex |
1093 %%% mode: latex |