Presented at
30C3 (2013),
Dec. 28, 2013, 11:30 a.m.
(60 minutes).
Software engineering is in a unsustainable state: software is mainly developed in a trial and error fashion, which always leads to vulnerable systems. Several decades ago the correspondence between logics and programming (Curry-Howard) was found. This correspondence is now being used in modern programming languages using dependent types, such as Agda, Coq, and Idris.
In this talk I show our development of attacks and security notions within Agda, using the recent <a href="https://en.wikipedia.org/wiki/BREACH_%28security_exploit%29">BREACH</a> exploit as an example. Our development is a constructive step towards verified software and bridges a gap between theory and practice.
I will explain the details about the Curry-Howard correspondence.
The target audience are interested people with some programming experience.
<p>Using the recent <a href="https://en.wikipedia.org/wiki/BREACH_%28security_exploit%29">BREACH</a> exploit as an example, I will present how to represent attacks and security notions within the Type Theory of <a href="http://wiki.portal.chalmers.se/agda/">Agda</a>.</p>
<p>Using security notions such as semantic security (<code>IND-CPA</code>, <code>IND-CCA</code>), it is intuitive to show how the use of compression leads to a not semantically secure encryption, and thus potential issues. Indeed the length of the ciphertext can now be controlled by the adversary who can control the plaintext. I will show how this intuitive result can be formalized using <a href="http://wiki.portal.chalmers.se/agda/">Agda</a>.</p>
<p>A note on <a href="http://wiki.portal.chalmers.se/agda/">Agda</a>: It is both a programming language and a proof system. The programming language features pure, exhaustive, and terminating functions over rich user defined data types (inductive and co-inductive). This powerful λ-calculus is equipped with a rich type-system featuring dependent-types. Through the Curry-Howard correspondence this programming language can also be used as a proof system. With such a combined system it becomes possible to write programs and proofs about these programs in a unified way. Additionally using this approach, one can start proving properties starting only with programming skills and gradually learn more proof techniques by exploring the type system.</p>
<p>I claim that functional programming and dependent types can be of a great help to formalize cryptography and thus privacy enhancing tools. I will present how functions are convenient at describing these games and adversaries. I will also give an overview of the crypto-agda project: how type-isomorphisms can ease probabilistic reasoning; how circuits can help capturing the requirements on the complexity bounds; and how all of these aspects can fit together thanks to polymorphism!</p>
Presenters:
-
Nicolas Pouillard
Type Theory Hacker
<p>
My current areas of research are a mixture of Type Theory and Cryptography/Security.
I'm currently postdoc researcher with the Demtech project at IT Univeristy of Copenhagen.
<p/>
<p>
Previously I was an engineer and then a PhD student in the Gallium research team at INRIA Paris Rocquencourt. At that time I was mainly focused on the design of programming languages and in particular meta-programming.
</p>
<p>
I learned programming and computer science at the engineering school of EPITA in Paris.
<p/>
Links:
Similar Presentations: