Version 1.5.9e last one standing

## Vortrag: BREACH in Agda

### Security notions, proofs and attacks using dependently typed functional programming

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 BREACH 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.

Using the recent BREACH exploit as an example, I will present how to represent attacks and security notions within the Type Theory of Agda.

Using security notions such as semantic security (`IND-CPA`

, `IND-CCA`

), 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 Agda.

A note on Agda: 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.

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!

### Info

**Tag:**
28.12.2013
**Anfang:**
11:30 Uhr
**Dauer:**
01:00
**Room:**
Saal G
**Track:**
Science & Engineering
**Sprache:**
en

### Links:

### Dateien

### Feedback

Uns interessiert deine Meinung! Wie fandest du diese Veranstaltung?

### Concurrent events

- Saal 1
- The Gospel of IRMA
- Saal 6
- We only have one earth
- Saal 2
- Hello World!

### Referenten

Nicolas Pouillard |