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.