Programm 30C3

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:

• iCalendar
• crypto-agda
• BREACH (security exploit)
• Agda

Dateien

• slides

Feedback

Uns interessiert deine Meinung! Wie fandest du diese Veranstaltung?