{"guid":"b272476e-c7bb-4350-8371-f67f565a51f6","title":"Keynote: RustBelt: Securing the Foundations of the Rust Programming Language","subtitle":null,"slug":"bob2022-rustbelt-securing-the-foundations-dreyer","link":"https://bobkonf.de/2022/dreyer.html","description":"The Rust systems programming language promises to\n\tovercome the seemingly fundamental tradeoff in language design\n\tbetween high-level safety guarantees and low-level control\n\tover resource management. Unfortunately, none of Rust’s safety\n\tclaims have been formally proven, and there is good reason to\n\tquestion whether they actually hold. Specifically, Rust\n\temploys a strong, ownership-based type system, but then\n\textends the expressive power of this core type system through\n\tlibraries that internally use unsafe features.\n\nIn this talk, I will present RustBelt, the first formal (and\nmachine-checked) safety proof for a language representing a realistic\nsubset of Rust. Our proof is extensible in the sense that, for each\nnew Rust library that uses unsafe features, we can say what\nverification condition it must satisfy in order for it to be deemed a\nsafe extension to the language.\n\nWe have carried out this verification for some of the most important\nlibraries that are used throughout the Rust ecosystem. The secret\nweapon that makes RustBelt possible is the Iris framework for\nhigher-order concurrent separation logic in Coq.\n\nThe talk will not assume any prior familiarity with concurrent separation logic or Rust.\n\n\n\t","original_language":"eng","persons":["Derek Dreyer"],"tags":["bob2022","999","2022","Talk","BOB","BOBKonferenz"],"view_count":181,"promoted":false,"date":"2022-03-11T09:00:00.000+01:00","release_date":"2022-09-06T00:00:00.000+02:00","updated_at":"2026-02-18T19:45:06.993+01:00","length":3609,"duration":3609,"thumb_url":"https://static.media.ccc.de/media/events/bobkonf/2022/999-b272476e-c7bb-4350-8371-f67f565a51f6.jpg","poster_url":"https://static.media.ccc.de/media/events/bobkonf/2022/999-b272476e-c7bb-4350-8371-f67f565a51f6_preview.jpg","timeline_url":"https://static.media.ccc.de/media/events/bobkonf/2022/999-b272476e-c7bb-4350-8371-f67f565a51f6.timeline.jpg","thumbnails_url":"https://static.media.ccc.de/media/events/bobkonf/2022/999-b272476e-c7bb-4350-8371-f67f565a51f6.thumbnails.vtt","frontend_link":"https://media.ccc.de/v/bob2022-rustbelt-securing-the-foundations-dreyer","url":"https://api.media.ccc.de/public/events/b272476e-c7bb-4350-8371-f67f565a51f6","conference_title":"BOB Konferenz 2022","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2022","related":[],"recordings":[{"size":226,"length":3609,"mime_type":"video/webm","language":"eng","filename":"bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_webm-hd.webm","state":"new","folder":"webm-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2022-09-06T16:33:33.471+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2022/webm-hd/bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_webm-hd.webm","url":"https://api.media.ccc.de/public/recordings/61550","event_url":"https://api.media.ccc.de/public/events/b272476e-c7bb-4350-8371-f67f565a51f6","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2022"},{"size":103,"length":3609,"mime_type":"video/webm","language":"eng","filename":"bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_webm-sd.webm","state":"new","folder":"webm-sd","high_quality":false,"width":720,"height":576,"updated_at":"2022-09-06T16:11:05.341+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2022/webm-sd/bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_webm-sd.webm","url":"https://api.media.ccc.de/public/recordings/61549","event_url":"https://api.media.ccc.de/public/events/b272476e-c7bb-4350-8371-f67f565a51f6","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2022"},{"size":81,"length":3609,"mime_type":"video/mp4","language":"eng","filename":"bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_sd.mp4","state":"new","folder":"h264-sd","high_quality":false,"width":720,"height":576,"updated_at":"2022-09-06T15:56:57.845+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2022/h264-sd/bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_sd.mp4","url":"https://api.media.ccc.de/public/recordings/61548","event_url":"https://api.media.ccc.de/public/events/b272476e-c7bb-4350-8371-f67f565a51f6","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2022"},{"size":37,"length":3609,"mime_type":"audio/opus","language":"eng","filename":"bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_opus.opus","state":"new","folder":"opus","high_quality":false,"width":0,"height":0,"updated_at":"2022-09-06T15:55:16.199+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2022/opus/bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_opus.opus","url":"https://api.media.ccc.de/public/recordings/61547","event_url":"https://api.media.ccc.de/public/events/b272476e-c7bb-4350-8371-f67f565a51f6","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2022"},{"size":55,"length":3609,"mime_type":"audio/mpeg","language":"eng","filename":"bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_mp3.mp3","state":"new","folder":"mp3","high_quality":false,"width":0,"height":0,"updated_at":"2022-09-06T15:54:52.538+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2022/mp3/bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_mp3.mp3","url":"https://api.media.ccc.de/public/recordings/61546","event_url":"https://api.media.ccc.de/public/events/b272476e-c7bb-4350-8371-f67f565a51f6","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2022"},{"size":136,"length":3609,"mime_type":"video/mp4","language":"eng","filename":"bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_hd.mp4","state":"new","folder":"h264-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2022-09-06T15:54:48.979+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2022/h264-hd/bob2022-999-eng-Keynote_RustBelt_Securing_the_Foundations_of_the_Rust_Programming_Language_hd.mp4","url":"https://api.media.ccc.de/public/recordings/61545","event_url":"https://api.media.ccc.de/public/events/b272476e-c7bb-4350-8371-f67f565a51f6","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2022"}]}