{"guid":"81cba379-0eb6-4dbb-a48c-80feaea60939","title":"Verified Firewall Ruleset Verification","subtitle":"Math, Functional Programming, Theorem Proving, and an Introduction to Isabelle/HOL","slug":"32c3-7195-verified_firewall_ruleset_verification","link":"https://events.ccc.de/congress/2015/Fahrplan/events/7195.html","description":"We develop a tool to verify Linux netfilter/iptables firewalls rulesets. Then, we verify the verification tool itself.\n\nWarning: involves math!\n\nThis talk is also an introduction to interactive theorem proving and programming in Isabelle/HOL. We strongly suggest that audience members have some familiarity with functional programming. A strong mathematical background is NOT required.\n\nTL;DR: Math is cool again, we now have the tools for \"executable math\". Also: iptables!","original_language":"eng","persons":["Cornelius Diekmann"],"view_count":5006,"promoted":false,"date":"2015-12-28T17:30:00.000+01:00","release_date":"2015-12-28T01:00:00.000+01:00","updated_at":"2026-03-17T03:45:03.646+01:00","tags":["Science"],"length":1950,"duration":1950,"thumb_url":"https://static.media.ccc.de/media/congress/2015/7195-hd.jpg","poster_url":"https://static.media.ccc.de/media/congress/2015/7195-hd_preview.jpg","timeline_url":"https://static.media.ccc.de/media/congress/2015/81cba379-0eb6-4dbb-a48c-80feaea60939-timeline.jpg","thumbnails_url":"https://static.media.ccc.de/media/congress/2015/81cba379-0eb6-4dbb-a48c-80feaea60939-thumbnails.vtt","frontend_link":"https://media.ccc.de/v/32c3-7195-verified_firewall_ruleset_verification","url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_title":"32C3: gated communities","conference_url":"https://api.media.ccc.de/public/conferences/32c3","related":[{"event_id":677,"event_guid":"import-ea971d9a74241bb280","weight":1},{"event_id":1217,"event_guid":"import-92bdbf3754ee00fffc","weight":1},{"event_id":1398,"event_guid":"import-4cd820d77b40b4b492","weight":1},{"event_id":1405,"event_guid":"import-9a084512d1ad9e7a7a","weight":1},{"event_id":1719,"event_guid":"import-1975766c6d4f873c2c","weight":1},{"event_id":1828,"event_guid":"kkMSS4JoEJtzbF9jc2JJ4A","weight":1},{"event_id":1836,"event_guid":"SKDne_Zu6SPJc-ADxqiLnA","weight":1},{"event_id":1915,"event_guid":"_O_wClK0WXa9WWkjJ228GQ","weight":1},{"event_id":1918,"event_guid":"ix6eImcX7hzVSBSn6_CHdA","weight":1},{"event_id":2172,"event_guid":"ELK9-ZQeFcqKxBYW8eay8g","weight":1},{"event_id":2277,"event_guid":"ad722522-5817-4317-8f3d-bb443b4e6c77","weight":1},{"event_id":2378,"event_guid":"213f5667-d2b5-4f7c-b3f7-90ef3f6322a0","weight":1},{"event_id":2435,"event_guid":"d047bc73-a435-4f4b-9740-640a3da51a90","weight":1},{"event_id":2613,"event_guid":"c0ef160e-771a-433c-842b-5c7fd15928b6","weight":1},{"event_id":2705,"event_guid":"55fccc39-c1bb-4d05-aa95-7188ad229f56","weight":1},{"event_id":2813,"event_guid":"7d2e79be-5d42-425b-a335-c41fd18431fb","weight":1},{"event_id":2814,"event_guid":"3cb4101c-2042-4883-b6fb-6591994a70c0","weight":2},{"event_id":2816,"event_guid":"78ea005f-4ddb-44d1-82e5-a2825ddea4e1","weight":1},{"event_id":2825,"event_guid":"56721a59-30c0-4201-8744-5d2a9846ed28","weight":1},{"event_id":2836,"event_guid":"56e8d345-8c04-4281-9811-d4ed9da8603e","weight":1},{"event_id":2850,"event_guid":"4f1a0717-6931-4580-9e49-5d523be045df","weight":1},{"event_id":2851,"event_guid":"62290f8e-f515-416f-9c4a-b403474e94e6","weight":1},{"event_id":2855,"event_guid":"52706f90-a2f9-48be-a4c3-786257fce233","weight":1},{"event_id":2856,"event_guid":"012b9dea-7d42-4428-acd4-4f84fa41e729","weight":1},{"event_id":2858,"event_guid":"17259b49-65ef-4726-ae03-a0b90e45806a","weight":1},{"event_id":2861,"event_guid":"01da121b-bd49-4805-aaaf-a6ec1f4f941f","weight":1},{"event_id":2862,"event_guid":"2f4cd1ef-dd90-4145-a734-141e5c081940","weight":1},{"event_id":2871,"event_guid":"74515f8e-a752-4cbb-b407-3a70fca5b0b3","weight":1},{"event_id":2874,"event_guid":"5f57ffa9-631c-429d-a11b-5b51bebe0f0f","weight":1},{"event_id":2882,"event_guid":"df35c860-60fc-4df8-801c-b2f4f91b33b8","weight":1},{"event_id":2883,"event_guid":"1edc7ea3-0f06-4453-911f-f11b2a49e649","weight":1},{"event_id":2886,"event_guid":"088e3078-bab2-433d-8be2-f1a4b37b4d5c","weight":1},{"event_id":2890,"event_guid":"b7327513-182a-455a-932e-aab4791f5331","weight":1},{"event_id":2894,"event_guid":"9d3ce896-1ee6-47c5-b616-1ebcf6860690","weight":1},{"event_id":2899,"event_guid":"0c8f0e98-92ee-42ba-aa75-04fc50344904","weight":1},{"event_id":2903,"event_guid":"bfadd7de-3680-4766-a474-faa53c5f141f","weight":1},{"event_id":2904,"event_guid":"8b01d636-d39b-44b8-8d6f-fc03e47eae1b","weight":1},{"event_id":2906,"event_guid":"550b8e16-3394-40d2-b47c-7cfe0031945b","weight":1},{"event_id":2917,"event_guid":"16613345-4f8c-44f1-a065-b3fa1d7b51cc","weight":1},{"event_id":2918,"event_guid":"f4da28f8-1e28-45d4-9fab-d1d36d20ca7b","weight":1},{"event_id":2929,"event_guid":"d66db4df-49ed-4c9f-ada3-289d16786c8e","weight":2},{"event_id":2943,"event_guid":"969bee9e-d0bf-4d24-a649-15f93747d608","weight":1},{"event_id":2959,"event_guid":"83ab70a1-de38-42d3-993e-08024cac1ddg","weight":1},{"event_id":3007,"event_guid":"8d3d7bf7-7e45-4621-9da2-dd518609a45c","weight":1},{"event_id":3043,"event_guid":"79e60f58-b2e7-4910-be32-f0a8896569e0","weight":1},{"event_id":3058,"event_guid":"56846834-12f4-495f-b92f-8cae32b8f1c2","weight":1},{"event_id":3154,"event_guid":"axE0bWDwutJ5VgLbiJnqJQ","weight":1},{"event_id":3603,"event_guid":"798573a8-f544-48f0-abaf-ebc405f03f4a","weight":1},{"event_id":3656,"event_guid":"1a6657a2-b6c2-4acc-b8fc-5ec081c0877f","weight":1},{"event_id":3690,"event_guid":"8d0aed87-2484-4880-ae08-2dc3c7898959","weight":1},{"event_id":3692,"event_guid":"f21478d4-e8db-4f19-854c-2f74b5824706","weight":1},{"event_id":3702,"event_guid":"5fb5e620-383a-4679-b37a-beef20bcd4fe","weight":1},{"event_id":3703,"event_guid":"65833373-6cae-4f9d-947b-c93a83ff1ba1","weight":1},{"event_id":3712,"event_guid":"cb23378b-6db0-4e2f-a4c8-f5006a467ca3","weight":1},{"event_id":3863,"event_guid":"9d73617c-83e1-4457-ab0f-13a99ea57d0d","weight":1},{"event_id":3916,"event_guid":"d8e3c106-4f42-4a68-8d55-62f708f5bf89","weight":1},{"event_id":3950,"event_guid":"L0a92AY4MXdIRWubHJn0Jg","weight":1},{"event_id":4247,"event_guid":"2dd16bb3-657b-41b6-bdec-987ada3f285c","weight":1},{"event_id":4772,"event_guid":"0ff9c9c4-a561-4ec0-afa2-93647a740f26","weight":1},{"event_id":4775,"event_guid":"51f1fe0d-19df-406d-a313-befeab6ac1bb","weight":1},{"event_id":4825,"event_guid":"a39634b4-d220-4c84-bf5a-e52c375827c5","weight":1},{"event_id":4846,"event_guid":"832b8fb8-beb1-4d92-93d0-ba3b7568905a","weight":1},{"event_id":4860,"event_guid":"f552b4b5-7446-4cc4-836b-0aa3639b994f","weight":1},{"event_id":4893,"event_guid":"6c4b2648-3840-476c-b966-c008010bca66","weight":1},{"event_id":4969,"event_guid":"2f480a87-d595-4312-97c1-0a0f0fa0f75a","weight":1},{"event_id":5016,"event_guid":"b22bb12f-7bf1-4e5f-b3d5-7baf9bb3d18c","weight":1},{"event_id":5061,"event_guid":"f2fad80c-2d2f-4717-9a82-2406e7b23c77","weight":1},{"event_id":6005,"event_guid":"67dbfc12-f4ad-4a4d-8370-118f1c72e98b","weight":2},{"event_id":6029,"event_guid":"19767f93-f0df-477f-a534-aee61b4288a9","weight":1},{"event_id":6423,"event_guid":"ea7c532f-cc2d-4cb1-8f15-1933df7fd523","weight":1},{"event_id":6430,"event_guid":"462f9320-3a0e-4785-82de-15343803c2ba","weight":1},{"event_id":6603,"event_guid":"ea00d1e0-a580-415f-a8cf-f02883d939dc","weight":1},{"event_id":7106,"event_guid":"e5435c9d-3e16-5419-b326-391df1522988","weight":1},{"event_id":7133,"event_guid":"65da5605-4c79-57cc-8114-ab413d97189f","weight":1},{"event_id":7147,"event_guid":"5fe8bbbe-116b-5d42-ad17-90208755ce30","weight":1},{"event_id":7251,"event_guid":"b69c19ce-7c89-4afd-9396-ea664f80dba7 ","weight":1}],"recordings":[{"size":26,"length":1941,"mime_type":"audio/opus","language":"deu","filename":"32c3-7195-de-Verified_Firewall_Ruleset_Verification.opus","state":"downloaded","folder":"opus-translation","high_quality":true,"width":null,"height":null,"updated_at":"2016-01-02T17:39:50.395+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/opus-translation/32c3-7195-de-Verified_Firewall_Ruleset_Verification.opus","url":"https://api.media.ccc.de/public/recordings/9458","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"},{"size":29,"length":1941,"mime_type":"audio/mpeg","language":"deu","filename":"32c3-7195-de-Verified_Firewall_Ruleset_Verification.mp3","state":"downloaded","folder":"mp3-translated","high_quality":true,"width":null,"height":null,"updated_at":"2015-12-30T14:22:37.691+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/mp3-translated/32c3-7195-de-Verified_Firewall_Ruleset_Verification.mp3","url":"https://api.media.ccc.de/public/recordings/9266","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"},{"size":null,"length":null,"mime_type":"application/x-subrip","language":"eng","filename":"DRAFT_32c3-7195-en-de-Verified_Firewall_Ruleset_Verification.en_DRAFT.srt","state":"todo","folder":"","high_quality":true,"width":null,"height":null,"updated_at":"2022-01-15T18:12:46.450+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/DRAFT_32c3-7195-en-de-Verified_Firewall_Ruleset_Verification.en_DRAFT.srt","url":"https://api.media.ccc.de/public/recordings/50750","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"},{"size":101,"length":1950,"mime_type":"video/webm","language":"eng-deu","filename":"32c3-7195-en-de-Verified_Firewall_Ruleset_Verification_webm-sd.webm","state":"downloaded","folder":"webm-sd","high_quality":false,"width":720,"height":576,"updated_at":"2016-02-03T14:13:30.453+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/webm-sd/32c3-7195-en-de-Verified_Firewall_Ruleset_Verification_webm-sd.webm","url":"https://api.media.ccc.de/public/recordings/9456","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"},{"size":29,"length":1941,"mime_type":"audio/mpeg","language":"eng","filename":"32c3-7195-en-Verified_Firewall_Ruleset_Verification.mp3","state":"downloaded","folder":"mp3","high_quality":true,"width":null,"height":null,"updated_at":"2016-01-02T17:35:47.879+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/mp3/32c3-7195-en-Verified_Firewall_Ruleset_Verification.mp3","url":"https://api.media.ccc.de/public/recordings/9457","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"},{"size":24,"length":1941,"mime_type":"audio/opus","language":"eng","filename":"32c3-7195-en-Verified_Firewall_Ruleset_Verification.opus","state":"downloaded","folder":"opus","high_quality":true,"width":null,"height":null,"updated_at":"2016-01-02T17:41:04.690+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/opus/32c3-7195-en-Verified_Firewall_Ruleset_Verification.opus","url":"https://api.media.ccc.de/public/recordings/9459","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"},{"size":105,"length":1950,"mime_type":"video/mp4","language":"eng-deu","filename":"32c3-7195-en-de-Verified_Firewall_Ruleset_Verification_sd.mp4","state":"downloaded","folder":"h264-sd","high_quality":false,"width":720,"height":576,"updated_at":"2016-02-03T14:12:48.492+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/h264-sd/32c3-7195-en-de-Verified_Firewall_Ruleset_Verification_sd.mp4","url":"https://api.media.ccc.de/public/recordings/9188","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"},{"size":216,"length":1950,"mime_type":"video/mp4","language":"eng-deu","filename":"32c3-7195-en-de-Verified_Firewall_Ruleset_Verification_hd.mp4","state":"downloaded","folder":"h264-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2016-02-03T14:11:53.910+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/h264-hd/32c3-7195-en-de-Verified_Firewall_Ruleset_Verification_hd.mp4","url":"https://api.media.ccc.de/public/recordings/8664","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"},{"size":196,"length":1950,"mime_type":"video/mp4","language":"eng","filename":"32c3-7195-en-Verified_Firewall_Ruleset_Verification.mp4","state":"downloaded","folder":"h264-hd-web","high_quality":true,"width":1920,"height":1080,"updated_at":"2016-02-03T14:11:53.551+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/h264-hd-web/32c3-7195-en-Verified_Firewall_Ruleset_Verification.mp4","url":"https://api.media.ccc.de/public/recordings/8662","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"},{"size":195,"length":1950,"mime_type":"video/mp4","language":"deu","filename":"32c3-7195-de-Verified_Firewall_Ruleset_Verification.mp4","state":"downloaded","folder":"h264-hd-web","high_quality":true,"width":1920,"height":1080,"updated_at":"2016-02-03T14:11:53.736+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/h264-hd-web/32c3-7195-de-Verified_Firewall_Ruleset_Verification.mp4","url":"https://api.media.ccc.de/public/recordings/8663","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"},{"size":268,"length":1950,"mime_type":"video/webm","language":"eng-deu","filename":"32c3-7195-en-de-Verified_Firewall_Ruleset_Verification_webm-hd.webm","state":"downloaded","folder":"webm-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2016-02-03T21:01:46.105+01:00","recording_url":"https://cdn.media.ccc.de/congress/2015/webm-hd/32c3-7195-en-de-Verified_Firewall_Ruleset_Verification_webm-hd.webm","url":"https://api.media.ccc.de/public/recordings/9237","event_url":"https://api.media.ccc.de/public/events/81cba379-0eb6-4dbb-a48c-80feaea60939","conference_url":"https://api.media.ccc.de/public/conferences/32c3"}]}