{"guid":"-zXtqISaAof8oPTr8SYyTQ","title":"BREACH in Agda","subtitle":"Security notions, proofs and attacks using dependently typed functional programming","slug":"30C3_-_5394_-_en_-_saal_g_-_201312281130_-_breach_in_agda_-_nicolas_pouillard","link":"http://events.ccc.de/congress/2013/Fahrplan/events/5394.html","description":"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.\n\nIn this talk I show our development of attacks and security notions within Agda, using the recent \u003ca href=\"https://en.wikipedia.org/wiki/BREACH_%28security_exploit%29\"\u003eBREACH\u003c/a\u003e exploit as an example. Our development is a constructive step towards verified software and bridges a gap between theory and practice.\nI will explain the details about the Curry-Howard correspondence.\nThe target audience are interested people with some programming experience.\n","original_language":"eng","persons":["Nicolas Pouillard"],"view_count":122,"promoted":false,"date":"2013-12-28T01:00:00.000+01:00","release_date":"2013-12-31T01:00:00.000+01:00","updated_at":"2024-08-03T21:30:01.727+02:00","tags":["30c3","Science \u0026 Engineering"],"length":2940,"duration":2940,"thumb_url":"https://static.media.ccc.de/media/congress/2013/5394-h264-iprod.jpg","poster_url":"https://static.media.ccc.de/media/congress/2013/5394-h264-iprod_preview.jpg","timeline_url":"https://static.media.ccc.de/media/congress/2013/x-zXtqISaAof8oPTr8SYyTQ-timeline.jpg","thumbnails_url":"https://static.media.ccc.de/media/congress/2013/x-zXtqISaAof8oPTr8SYyTQ-thumbnails.vtt","frontend_link":"https://media.ccc.de/v/30C3_-_5394_-_en_-_saal_g_-_201312281130_-_breach_in_agda_-_nicolas_pouillard","url":"https://api.media.ccc.de/public/events/-zXtqISaAof8oPTr8SYyTQ","conference_title":"30C3","conference_url":"https://api.media.ccc.de/public/conferences/30c3","related":[{"event_id":168,"event_guid":"import-007ef07bf3c6b624be","weight":1},{"event_id":1722,"event_guid":"RiskSjr33wsyUrC5oX80uw","weight":1},{"event_id":1763,"event_guid":"WbqegbTKG5YheKse8X4ZUw","weight":1},{"event_id":1772,"event_guid":"seTBwtIxwEedOMpITZG7EQ","weight":1},{"event_id":1801,"event_guid":"I1Wkt7x8Yy2ZnP2kOGAuXA","weight":1},{"event_id":1803,"event_guid":"c3Q-MbMX7FDXWv6rYj2bFw","weight":1},{"event_id":1839,"event_guid":"tnCge6rYmFPy9O0KjvtBAQ","weight":1},{"event_id":1853,"event_guid":"_PZbf5bEsVNq9q3vTxAazQ","weight":1},{"event_id":1854,"event_guid":"D27zQV1jKk88oKyXxGBGPQ","weight":1},{"event_id":2183,"event_guid":"yMuYr5eW4o9FpJMw-NwXrg","weight":1},{"event_id":2187,"event_guid":"JhCUm-jQqCMx_jDfrzH24Q","weight":2},{"event_id":2188,"event_guid":"oBQMMNfX5t-5TBIk3z6pOg","weight":1},{"event_id":2204,"event_guid":"78e2d419-0adc-43ff-989e-95a78ac9ddd4","weight":1},{"event_id":2208,"event_guid":"T7Ta13fUuQaAbv1JlO4-Qg","weight":1},{"event_id":2244,"event_guid":"a7cde3ca-46a8-4f0b-be61-f60e77f3418e","weight":1},{"event_id":2267,"event_guid":"9RncwfCW37x4dhs15BQqBQ","weight":1},{"event_id":2505,"event_guid":"b17ff452-d735-49b4-b91f-b8f7cd62dad2","weight":1},{"event_id":2868,"event_guid":"0549d204-604a-46c5-92a2-e64b85aa9892","weight":1},{"event_id":2884,"event_guid":"fb537cde-7f1d-484b-971b-1d30a543ecfb","weight":1},{"event_id":2890,"event_guid":"b7327513-182a-455a-932e-aab4791f5331","weight":1},{"event_id":3611,"event_guid":"f62fb3be-656f-4e7b-9619-11f3cdb2da26","weight":1},{"event_id":3667,"event_guid":"6347d122-daf0-4b30-851c-32cac06bf6bd","weight":1},{"event_id":3671,"event_guid":"4ef69e6a-026f-4b30-888d-af654b220a3d","weight":1},{"event_id":3692,"event_guid":"f21478d4-e8db-4f19-854c-2f74b5824706","weight":1},{"event_id":3719,"event_guid":"d851c029-9f83-41af-befd-a54209453d41","weight":1},{"event_id":3732,"event_guid":"8270c91a-d6e2-4f1c-9ebb-cdf10708d921","weight":1},{"event_id":3767,"event_guid":"0c197c9a-35eb-4780-a38d-9c53b7ff9bea","weight":1},{"event_id":4891,"event_guid":"2dd1ed02-2a4f-4c15-93e5-6d171fea74df","weight":1},{"event_id":6457,"event_guid":"74b9c748-970f-4693-ac7e-46fcc733d2b4","weight":1}],"recordings":[{"size":null,"length":null,"mime_type":"application/x-subrip","language":"eng","filename":"DRAFT_30c3-5394-BREACH_in_Agda.en_DRAFT.srt","state":"todo","folder":"","high_quality":true,"width":null,"height":null,"updated_at":"2022-01-24T22:40:43.715+01:00","recording_url":"https://cdn.media.ccc.de/congress/2013/DRAFT_30c3-5394-BREACH_in_Agda.en_DRAFT.srt","url":"https://api.media.ccc.de/public/recordings/52427","event_url":"https://api.media.ccc.de/public/events/-zXtqISaAof8oPTr8SYyTQ","conference_url":"https://api.media.ccc.de/public/conferences/30c3"},{"size":null,"length":2940,"mime_type":"audio/opus","language":"eng","filename":"30c3-5394-BREACH_in_Agda_opus.opus","state":"downloaded","folder":"opus","high_quality":true,"width":0,"height":0,"updated_at":"2014-11-11T12:42:54.733+01:00","recording_url":"https://cdn.media.ccc.de/congress/2013/opus/30c3-5394-BREACH_in_Agda_opus.opus","url":"https://api.media.ccc.de/public/recordings/4730","event_url":"https://api.media.ccc.de/public/events/-zXtqISaAof8oPTr8SYyTQ","conference_url":"https://api.media.ccc.de/public/conferences/30c3"},{"size":null,"length":2439,"mime_type":"audio/mpeg","language":"eng","filename":"30c3-5394-BREACH_in_Agda_mp3.mp3","state":"downloaded","folder":"mp3","high_quality":true,"width":640,"height":360,"updated_at":"2014-06-29T00:22:04.818+02:00","recording_url":"https://cdn.media.ccc.de/congress/2013/mp3/30c3-5394-BREACH_in_Agda_mp3.mp3","url":"https://api.media.ccc.de/public/recordings/3441","event_url":"https://api.media.ccc.de/public/events/-zXtqISaAof8oPTr8SYyTQ","conference_url":"https://api.media.ccc.de/public/conferences/30c3"},{"size":null,"length":2940,"mime_type":"video/mp4","language":"eng","filename":"30c3-5394-BREACH_in_Agda_h264-hq.mp4","state":"downloaded","folder":"mp4","high_quality":true,"width":640,"height":360,"updated_at":"2016-01-27T11:03:55.928+01:00","recording_url":"https://cdn.media.ccc.de/congress/2013/mp4/30c3-5394-BREACH_in_Agda_h264-hq.mp4","url":"https://api.media.ccc.de/public/recordings/3440","event_url":"https://api.media.ccc.de/public/events/-zXtqISaAof8oPTr8SYyTQ","conference_url":"https://api.media.ccc.de/public/conferences/30c3"},{"size":null,"length":2940,"mime_type":"video/webm","language":"eng","filename":"30c3-5394-BREACH_in_Agda_webm.webm","state":"downloaded","folder":"webm","high_quality":true,"width":640,"height":360,"updated_at":"2016-01-27T11:03:55.963+01:00","recording_url":"https://cdn.media.ccc.de/congress/2013/webm/30c3-5394-BREACH_in_Agda_webm.webm","url":"https://api.media.ccc.de/public/recordings/3439","event_url":"https://api.media.ccc.de/public/events/-zXtqISaAof8oPTr8SYyTQ","conference_url":"https://api.media.ccc.de/public/conferences/30c3"},{"size":null,"length":2940,"mime_type":"video/mp4","language":"eng","filename":"30c3-5394-BREACH_in_Agda_h264-iprod.mp4","state":"downloaded","folder":"mp4-lq","high_quality":false,"width":512,"height":288,"updated_at":"2016-01-26T08:07:13.638+01:00","recording_url":"https://cdn.media.ccc.de/congress/2013/mp4-lq/30c3-5394-BREACH_in_Agda_h264-iprod.mp4","url":"https://api.media.ccc.de/public/recordings/4593","event_url":"https://api.media.ccc.de/public/events/-zXtqISaAof8oPTr8SYyTQ","conference_url":"https://api.media.ccc.de/public/conferences/30c3"}]}