Chaos Communication Congress

BREACH in Agda (#5394) (30x41)

: 28, 2013

Speaker: Nicolas Pouillard 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.