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.
| Name | Type | Role | |
|---|---|---|---|
| Nicolas Pouillard | Guest Star |