{"id":1099821,"date":"2024-11-05T11:30:00","date_gmt":"2024-11-05T19:30:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?p=1099821"},"modified":"2024-11-05T11:24:38","modified_gmt":"2024-11-05T19:24:38","slug":"abstracts-november-5-2024","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/podcast\/abstracts-november-5-2024\/","title":{"rendered":"Abstracts: November 5, 2024"},"content":{"rendered":"\n<figure class=\"wp-block-image size-full\"><img loading=\"lazy\" decoding=\"async\" width=\"1400\" height=\"788\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788.jpg\" alt=\"Outlined illustrations of Chris Hawblitzel and Jay Lorch for the Microsoft Research Podcast, Abstracts series.\" class=\"wp-image-1099833\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788.jpg 1400w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-300x169.jpg 300w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-1024x576.jpg 1024w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-768x432.jpg 768w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-1066x600.jpg 1066w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-655x368.jpg 655w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-240x135.jpg 240w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-640x360.jpg 640w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-960x540.jpg 960w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-1280x720.jpg 1280w\" sizes=\"(max-width: 1400px) 100vw, 1400px\" \/><\/figure>\n\n\n<div class=\"wp-block-msr-podcast-container my-4\">\n\t<iframe loading=\"lazy\" src=\"https:\/\/player.blubrry.com\/?podcast_id=138212589&modern=1\" class=\"podcast-player\" frameborder=\"0\" height=\"164px\" width=\"100%\" scrolling=\"no\" title=\"Podcast Player\"><\/iframe>\n<\/div>\n\n\n\n<p>Members of the research community at Microsoft work continuously to advance their respective fields.\u202f<em>Abstracts<\/em>\u202fbrings its audience to the cutting edge with them through short, compelling conversations about new and noteworthy achievements.\u202f<\/p>\n\n\n\n<p>In this episode, Microsoft senior principal researchers <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/chrishaw\/\">Chris Hawblitzel<\/a> and <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/lorch\/\">Jay Lorch<\/a> join host Amber Tingle to discuss <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/verus-a-practical-foundation-for-systems-verification\/\">\u201cVerus: A Practical Foundation for Systems Verification,\u201d<\/a> which received the Distinguished Artifact Award at this year\u2019s Symposium on Operating Systems Principles, or SOSP. In their research, Hawblitzel, Lorch, and their coauthors leverage advances in programming languages and formal verification with two aims. The first aim is to help make software verification more accessible for systems developers so they can demonstrate their code will behave as intended. The second aim is to provide the research community with sound groundwork to tackle the application of formal verification to large, complex systems.\u00a0<\/p>\n\n\n\n<div class=\"wp-block-buttons is-layout-flex wp-block-buttons-is-layout-flex\">\n<div class=\"wp-block-button\"><a data-bi-type=\"button\" class=\"wp-block-button__link wp-element-button\" href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/verus-a-practical-foundation-for-systems-verification\/\">Read the paper<\/a><\/div>\n<\/div>\n\n\n\n<section class=\"wp-block-msr-subscribe-to-podcast subscribe-to-podcast\">\n\t<div class=\"subscribe-to-podcast__inner border-top border-bottom border-width-2\">\n\t\t<h2 class=\"h5 subscribe-to-podcast__heading\">\n\t\t\tSubscribe to the <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/podcast\">Microsoft Research Podcast<\/a>:\t\t<\/h2>\n\t\t<ul class=\"subscribe-to-podcast__list list-unstyled\">\n\t\t\t\t\t\t\t<li class=\"subscribe-to-podcast__list-item\">\n\t\t\t\t\t<a class=\"subscribe-to-podcast__link\" href=\"https:\/\/itunes.apple.com\/us\/podcast\/microsoft-research-a-podcast\/id1318021537?mt=2\" target=\"_blank\" rel=\"noreferrer noopener\">\n\t\t\t\t\t\t<svg class=\"subscribe-to-podcast__svg\" xmlns=\"http:\/\/www.w3.org\/2000\/svg\" fill=\"black\" viewBox=\"0 0 32 32\">  <path d=\"M7.12 0c-3.937-0.011-7.131 3.183-7.12 7.12v17.76c-0.011 3.937 3.183 7.131 7.12 7.12h17.76c3.937 0.011 7.131-3.183 7.12-7.12v-17.76c0.011-3.937-3.183-7.131-7.12-7.12zM15.817 3.421c3.115 0 5.932 1.204 8.079 3.453 1.631 1.693 2.547 3.489 3.016 5.855 0.161 0.787 0.161 2.932 0.009 3.817-0.5 2.817-2.041 5.339-4.317 7.063-0.812 0.615-2.797 1.683-3.115 1.683-0.12 0-0.129-0.12-0.077-0.615 0.099-0.792 0.192-0.953 0.64-1.141 0.713-0.296 1.932-1.167 2.677-1.911 1.301-1.303 2.229-2.932 2.677-4.719 0.281-1.1 0.244-3.543-0.063-4.672-0.969-3.595-3.907-6.385-7.5-7.136-1.041-0.213-2.943-0.213-4 0-3.636 0.751-6.647 3.683-7.563 7.371-0.245 1.004-0.245 3.448 0 4.448 0.609 2.443 2.188 4.681 4.255 6.015 0.407 0.271 0.896 0.547 1.1 0.631 0.447 0.192 0.547 0.355 0.629 1.14 0.052 0.485 0.041 0.62-0.072 0.62-0.073 0-0.62-0.235-1.199-0.511l-0.052-0.041c-3.297-1.62-5.407-4.364-6.177-8.016-0.187-0.943-0.224-3.187-0.036-4.052 0.479-2.323 1.396-4.135 2.921-5.739 2.199-2.319 5.027-3.543 8.172-3.543zM16 7.172c0.541 0.005 1.068 0.052 1.473 0.14 3.715 0.828 6.344 4.543 5.833 8.229-0.203 1.489-0.713 2.709-1.619 3.844-0.448 0.573-1.537 1.532-1.729 1.532-0.032 0-0.063-0.365-0.063-0.803v-0.808l0.552-0.661c2.093-2.505 1.943-6.005-0.339-8.296-0.885-0.896-1.912-1.423-3.235-1.661-0.853-0.161-1.031-0.161-1.927-0.011-1.364 0.219-2.417 0.744-3.355 1.672-2.291 2.271-2.443 5.791-0.348 8.296l0.552 0.661v0.813c0 0.448-0.037 0.807-0.084 0.807-0.036 0-0.349-0.213-0.683-0.479l-0.047-0.016c-1.109-0.885-2.088-2.453-2.495-3.995-0.244-0.932-0.244-2.697 0.011-3.625 0.672-2.505 2.521-4.448 5.079-5.359 0.547-0.193 1.509-0.297 2.416-0.281zM15.823 11.156c0.417 0 0.828 0.084 1.131 0.24 0.645 0.339 1.183 0.989 1.385 1.677 0.62 2.104-1.609 3.948-3.631 3.005h-0.015c-0.953-0.443-1.464-1.276-1.475-2.36 0-0.979 0.541-1.828 1.484-2.328 0.297-0.156 0.709-0.235 1.125-0.235zM15.812 17.464c1.319-0.005 2.271 0.463 2.625 1.291 0.265 0.62 0.167 2.573-0.292 5.735-0.307 2.208-0.479 2.765-0.905 3.141-0.589 0.52-1.417 0.667-2.209 0.385h-0.004c-0.953-0.344-1.157-0.808-1.553-3.527-0.452-3.161-0.552-5.115-0.285-5.735 0.348-0.823 1.296-1.285 2.624-1.291z\"\/><\/svg>\n\t\t\t\t\t\t<span class=\"subscribe-to-podcast__link-text\">Apple Podcasts<\/span>\n\t\t\t\t\t<\/a>\n\t\t\t\t<\/li>\n\t\t\t\n\t\t\t\t\t\t\t<li class=\"subscribe-to-podcast__list-item\">\n\t\t\t\t\t<a class=\"subscribe-to-podcast__link\" href=\"https:\/\/subscribebyemail.com\/www.blubrry.com\/feeds\/microsoftresearch.xml\" target=\"_blank\" rel=\"noreferrer noopener\">\n\t\t\t\t\t\t<svg class=\"subscribe-to-podcast__svg\" xmlns=\"http:\/\/www.w3.org\/2000\/svg\" fill=\"none\" viewBox=\"0 0 32 32\"><path fill=\"currentColor\" d=\"M6.4 6a2.392 2.392 0 00-2.372 2.119L16 15.6l11.972-7.481A2.392 2.392 0 0025.6 6H6.4zM4 10.502V22.8a2.4 2.4 0 002.4 2.4h19.2a2.4 2.4 0 002.4-2.4V10.502l-11.365 7.102a1.2 1.2 0 01-1.27 0L4 10.502z\"\/><\/svg>\n\t\t\t\t\t\t<span class=\"subscribe-to-podcast__link-text\">Email<\/span>\n\t\t\t\t\t<\/a>\n\t\t\t\t<\/li>\n\t\t\t\n\t\t\t\t\t\t\t<li class=\"subscribe-to-podcast__list-item\">\n\t\t\t\t\t<a class=\"subscribe-to-podcast__link\" href=\"https:\/\/subscribeonandroid.com\/www.blubrry.com\/feeds\/microsoftresearch.xml\" target=\"_blank\" rel=\"noreferrer noopener\">\n\t\t\t\t\t\t<svg class=\"subscribe-to-podcast__svg\" xmlns=\"http:\/\/www.w3.org\/2000\/svg\" fill=\"none\" viewBox=\"0 0 32 32\"><path fill=\"currentColor\" d=\"M12.414 4.02c-.062.012-.126.023-.18.06a.489.489 0 00-.12.675L13.149 6.3c-1.6.847-2.792 2.255-3.18 3.944h13.257c-.388-1.69-1.58-3.097-3.179-3.944l1.035-1.545a.489.489 0 00-.12-.675.492.492 0 00-.675.135l-1.14 1.68a7.423 7.423 0 00-2.55-.45c-.899 0-1.758.161-2.549.45l-1.14-1.68a.482.482 0 00-.494-.195zm1.545 3.824a.72.72 0 110 1.44.72.72 0 010-1.44zm5.278 0a.719.719 0 110 1.44.719.719 0 110-1.44zM8.44 11.204A1.44 1.44 0 007 12.644v6.718c0 .795.645 1.44 1.44 1.44.168 0 .33-.036.48-.09v-9.418a1.406 1.406 0 00-.48-.09zm1.44 0V21.76c0 .793.646 1.44 1.44 1.44h10.557c.793 0 1.44-.647 1.44-1.44V11.204H9.878zm14.876 0c-.169 0-.33.035-.48.09v9.418c.15.052.311.09.48.09a1.44 1.44 0 001.44-1.44v-6.719a1.44 1.44 0 00-1.44-1.44zM11.8 24.16v1.92a1.92 1.92 0 003.84 0v-1.92h-3.84zm5.759 0v1.92a1.92 1.92 0 003.84 0v-1.92h-3.84z\"\/><\/svg>\n\t\t\t\t\t\t<span class=\"subscribe-to-podcast__link-text\">Android<\/span>\n\t\t\t\t\t<\/a>\n\t\t\t\t<\/li>\n\t\t\t\n\t\t\t\t\t\t\t<li class=\"subscribe-to-podcast__list-item\">\n\t\t\t\t\t<a class=\"subscribe-to-podcast__link\" href=\"https:\/\/open.spotify.com\/show\/4ndjUXyL0hH1FXHgwIiTWU\" target=\"_blank\" rel=\"noreferrer noopener\">\n\t\t\t\t\t\t<svg class=\"subscribe-to-podcast__svg\" xmlns=\"http:\/\/www.w3.org\/2000\/svg\" fill=\"none\" viewBox=\"0 0 32 32\"><path fill=\"currentColor\" d=\"M16 4C9.383 4 4 9.383 4 16s5.383 12 12 12 12-5.383 12-12S22.617 4 16 4zm5.08 17.394a.781.781 0 01-1.086.217c-1.29-.86-3.477-1.434-5.303-1.434-1.937.002-3.389.477-3.403.482a.782.782 0 11-.494-1.484c.068-.023 1.71-.56 3.897-.562 1.826 0 4.365.492 6.171 1.696.36.24.457.725.217 1.085zm1.56-3.202a.895.895 0 01-1.234.286c-2.338-1.457-4.742-1.766-6.812-1.747-2.338.02-4.207.466-4.239.476a.895.895 0 11-.488-1.723c.145-.041 2.01-.5 4.564-.521 2.329-.02 5.23.318 7.923 1.995.419.26.547.814.286 1.234zm1.556-3.745a1.043 1.043 0 01-1.428.371c-2.725-1.6-6.039-1.94-8.339-1.942h-.033c-2.781 0-4.923.489-4.944.494a1.044 1.044 0 01-.474-2.031c.096-.023 2.385-.55 5.418-.55h.036c2.558.004 6.264.393 9.393 2.23.497.292.663.931.371 1.428z\"\/><\/svg>\n\t\t\t\t\t\t<span class=\"subscribe-to-podcast__link-text\">Spotify<\/span>\n\t\t\t\t\t<\/a>\n\t\t\t\t<\/li>\n\t\t\t\n\t\t\t\t\t\t\t<li class=\"subscribe-to-podcast__list-item\">\n\t\t\t\t\t<a class=\"subscribe-to-podcast__link\" href=\"https:\/\/www.blubrry.com\/feeds\/microsoftresearch.xml\" target=\"_blank\" rel=\"noreferrer noopener\">\n\t\t\t\t\t\t<svg class=\"subscribe-to-podcast__svg\" xmlns=\"http:\/\/www.w3.org\/2000\/svg\" fill=\"none\" viewBox=\"0 0 32 32\"><path fill=\"currentColor\" d=\"M6.667 4a2.676 2.676 0 00-2.612 2.13v.003c-.036.172-.055.35-.055.534v18.666c0 .183.019.362.055.534v.003a2.676 2.676 0 002.076 2.075h.002c.172.036.35.055.534.055h18.666A2.676 2.676 0 0028 25.333V6.667a2.676 2.676 0 00-2.13-2.612h-.003A2.623 2.623 0 0025.333 4H6.667zM8 8h1.333C17.42 8 24 14.58 24 22.667V24h-2.667v-1.333c0-6.618-5.382-12-12-12H8V8zm0 5.333h1.333c5.146 0 9.334 4.188 9.334 9.334V24H16v-1.333A6.674 6.674 0 009.333 16H8v-2.667zM10 20a2 2 0 11-.001 4.001A2 2 0 0110 20z\"\/><\/svg>\n\t\t\t\t\t\t<span class=\"subscribe-to-podcast__link-text\">RSS Feed<\/span>\n\t\t\t\t\t<\/a>\n\t\t\t\t<\/li>\n\t\t\t\t\t<\/ul>\n\t<\/div>\n<\/section>\n\n\n<div class=\"wp-block-msr-show-more\">\n\t<div class=\"bg-neutral-100 p-5\">\n\t\t<div class=\"show-more-show-less\" data-mount=\"show-more-show-less\">\n\t\t\t<div>\n\t\t\t\t<span>\n\t\t\t\t\t\n\n<h2 class=\"wp-block-heading\" id=\"transcript\">Transcript&nbsp;<\/h2>\n\n\n\n<p>[MUSIC]&nbsp;<\/p>\n\n\n\n<p><strong>AMBER TINGLE: <\/strong>Welcome to <em>Abstracts<\/em>, a Microsoft Research Podcast that puts the spotlight on world-class research <em>in brief<\/em>. I\u2019m Amber Tingle. In this series, members of the research community at Microsoft give us a quick snapshot\u2014or a <em>podcast abstract<\/em>\u2014of their new and noteworthy papers.&nbsp;<\/p>\n\n\n\n<p>[MUSIC FADES]&nbsp;<\/p>\n\n\n\n<p>Our guests today are Chris Hawblitzel and Jay Lorch. They are both senior principal researchers at Microsoft and two of the coauthors on a paper called \u201cVerus: A Practical Foundation for Systems Verification.\u201d This work received the Distinguished Artifact Award at the 30th Symposium on Operating Systems Principles, also known as <em>SOSP<\/em>, which is happening right now in Austin, Texas. Chris and Jay, thank you for joining us today for <em>Abstracts<\/em> and congratulations!<\/p>\n\n\n\n<p><strong>JAY LORCH: <\/strong>Thank you for having us.&nbsp;<\/p>\n\n\n\n<p><strong>CHRIS HAWBLITZEL: <\/strong>Glad to be here.&nbsp;<\/p>\n\n\n\n<p><strong>TINGLE: <\/strong>Chris, let&#8217;s start with an overview. What problem does this research address, and why is Verus something that the broader research community should know about?&nbsp;<\/p>\n\n\n\n\t\t\t\t<\/span>\n\t\t\t\t<span id=\"show-more-show-less-toggle-1\" class=\"show-more-show-less-toggleable-content\">\n\t\t\t\t\t\n\n\n\n<p><strong>HAWBLITZEL: <\/strong>So what we&#8217;re trying to address is a very simple problem where we&#8217;re trying to help developers write software that doesn&#8217;t have bugs in it. And we&#8217;re trying to provide a tool with Verus that will help developers show that their code actually behaves the way it&#8217;s supposed to; it obeys some sort of specification for what the program is supposed to do.&nbsp;<\/p>\n\n\n\n<p><strong>TINGLE: <\/strong>How does this publication build on or differ from other research in this field, including your previous Verus-related work?&nbsp;<\/p>\n\n\n\n<p><strong>HAWBLITZEL: <\/strong>So formal verification is a process where you write down what it is that you want your program to do in mathematical terms. So if you&#8217;re writing an algorithm to sort a list, for example, you might say that the output of this algorithm should be a new list that is a rearrangement of the elements of the old list, but now this rearrangement should be in sorted order. So you can write that down using standard mathematics. And now given that mathematical specification, the challenge is to prove that your piece of software written in a particular language, like Java or C# or Rust, actually generates an output that meets that mathematical specification. So this idea of using verification to prove that your software obeys some sort of specification, this has been around for a long time, so, you know, even Alan Turing talked about ways of doing this many, many decades ago. The challenge has always been that it&#8217;s really hard to develop these proofs for any large piece of software. It simply takes a long time for a human being to write down a proof of correctness of their software. And so what we&#8217;re trying to do is to build on earlier work in verification and recent developments in programming languages to try to make this as easy as possible and to try to make it as accessible to ordinary software developers as possible. So we&#8217;ve been using existing tools. There are automated theorem provers\u2014one of them from Microsoft Research called Z3\u2014where you give it a mathematical formula and ask it to prove that the formula is valid. We&#8217;re building on that. And we&#8217;re also taking a lot of inspiration from tools developed at Microsoft Research and elsewhere, like Dafny and F* and so on, that we&#8217;ve used in the past for our previous verification projects. And we&#8217;re trying to take ideas from those and make them accessible to developers who are using common programming languages. In this case, the Rust programming language is what we&#8217;re focusing on.&nbsp;<\/p>\n\n\n\n<p><strong>TINGLE: <\/strong>Jay, could you describe your methodology for us and maybe share a bit about how you and your coauthors tested the robustness of Verus.<\/p>\n\n\n\n<p><strong>LORCH: <\/strong>So the question we really want to answer is, <em>is<\/em> Verus suitable for systems programming? So that means a variety of things. Is it amenable to a variety of kinds of software that you want to build as part of a system? Is it usable by developers? Can they produce compact proofs? <em>And<\/em> can they get timely feedback about those proofs? Can the verifier tell you quickly that your proof is correct or, if it&#8217;s wrong, that it&#8217;s wrong and guide you to fix it? So the main two methodological techniques we used were millibenchmarks and full systems. So the millibenchmarks are small pieces of programs that have been verified by other tools in the past, and we built them in Verus and compared to what other tools would do to find whether we could improve usability. And we found generally that we could verify the same things but with more compact proofs and proofs that would give much snappier feedback. The difference between one second and 10 seconds might not seem a lot, but when you&#8217;re writing code and working with the verifier, it&#8217;s much nicer to get immediate feedback about what is wrong with your proof so you can say, oh, what about this? And it can say, oh, well, I still see a problem there. And you could say, OK, let me fix that. As opposed to waiting 10, 20 seconds between each such query<strong> <\/strong>to the verifier. So the millibenchmarks helped us evaluate that. And the <em>macro<\/em>benchmarks, the building entire systems, we built a couple of distributed systems that had been verified before\u2014a key value store and a node replication system\u2014to show that you could do them more effectively and with less verification time. We also built some new systems, a verified OS page table, a memory allocator, and a persistent memory append-only log.&nbsp;<\/p>\n\n\n\n<p><strong>TINGLE: <\/strong>Chris, the paper mentions that successfully verifying system software has required\u2014you actually use the word <em>heroic<\/em> to describe the developer effort. Thinking of those heroes in the developer community and perhaps others, what real-world impact do you expect Verus to have? What kind of gains are we talking about here?&nbsp;<\/p>\n\n\n\n<p><strong>HAWBLITZEL: <\/strong>Yeah, so I think, you know, traditionally verification or this formal software verification that we&#8217;re doing has been considered a little bit of a pie-in-the-sky research agenda. Something that people have applied to small research problems but has not necessarily had a real-world impact before. And so I think it&#8217;s just, you know, recently, in the last 10 or 15 years, that we started to see a change in this and started to see verified software actually deployed in practice. So on one of our previous projects, we worked on verifying the cryptographic primitives that people use when, say, they browse the web or something and their data is encrypted. So in these cryptographic primitives, there&#8217;s a very clear specification for exactly what bytes you&#8217;re supposed to produce when you encrypt some data. And the challenge is just writing software that actually performs those operations and does so efficiently. So in one of our previous projects that we worked on called HACL* and EverCrypt, we verified some of the most commonly used and efficient cryptographic primitives for things like encryption and hashing and so on. And these are things that are actually used on a day-to-day basis. So we, kind of, took from that experience that the tools that we&#8217;re building are getting ready for prime time here. We can actually verify software that is security critical, reliability critical, and is in use. So some of the things that Jay just mentioned, like verifying, you know, persistent memory storage systems and so on, those are the things that we&#8217;re looking at next for software that would really benefit from reliability and where we can formally prove that your data that&#8217;s written to disk is read correctly back from disk and not lost during a crash, for example. So that&#8217;s the kind of software that we&#8217;re looking to verify to try to have a real-world impact.&nbsp;<\/p>\n\n\n\n<p><strong>LORCH: <\/strong>The way I see the real-world impact, is it going to enable Microsoft to deal with a couple of challenges that are severe and increasing in scale? So the first challenge is attackers, and the second challenge is the vast scale at which we operate. There&#8217;s a lot of hackers out there with a lot of resources that are trying to get through our defenses, and every bug that we have offers them purchase, and techniques like this, that can get rid of bugs, allow us to deal with that increasing attacker capability. The other challenge we have is scale. We have billions of customers. We have vast amounts of data and compute power. And when you have a bug that you&#8217;ve <em>thoroughly<\/em> tested but then you run it on millions of computers over decades, those rare bugs eventually crop up. So they become a problem, and traditional testing has a lot of difficulty finding those. And this technology, which enables us to reason about the <em>infinite<\/em> possibilities in a finite amount of time and observe all possible ways that the system can go wrong and make sure that it can deal with them, that enables us to deal with the vast scale that Microsoft operates on today.<\/p>\n\n\n\n<p><strong>HAWBLITZEL: <\/strong>Yeah, and I think this is an important point that differentiates us from testing. Traditionally, you find a bug when you <em>see<\/em> that bug happen in running software. With formal verification, we&#8217;re catching the bugs <em>before<\/em> you run the software at all. We&#8217;re trying to prove that on all possible inputs, on all possible executions of the software, these bugs will not happen, and it&#8217;s much cheaper to fix bugs before you&#8217;ve deployed the software that has bugs, before attackers have tried to exploit those bugs.&nbsp;<\/p>\n\n\n\n<p><strong>TINGLE: <\/strong>So, Jay, ideally, what would you like our listeners and your fellow SOSP conference attendees to tell their colleagues about Verus? What&#8217;s the key takeaway here?&nbsp;<\/p>\n\n\n\n<p><strong>LORCH: <\/strong>I<strong> <\/strong>think the key takeaway is that it is possible now to build software without bugs, to build systems code that is going to obey its specification on all possible inputs <em>always<\/em>. We have that technology. And this is possible <em>now<\/em> because a lot of technology has advanced to the point where we can use it. So for one thing, there&#8217;s advances in programming languages. People are moving from C to Rust. They&#8217;ve discovered that you can get the high performance that you want for systems code without having to sacrifice the ability to reason about ownership and lifetimes, concurrency. The other thing that we build on is advances in computer-aided theorem proving. So we can really make compact and quick-to-verify mathematical descriptions of all possible behaviors of a program and get fast answers that allow us to rapidly turn around proof challenges from developers.&nbsp;<\/p>\n\n\n\n<p><strong>TINGLE: <\/strong>Well, finally, Chris, what are some of the open questions or future opportunities for formal software verification research, and what might you and your collaborators tackle next? I heard a few of the things earlier.&nbsp;<\/p>\n\n\n\n<p><strong>HAWBLITZEL: <\/strong>Yes, I think despite, you know, the effort that we and many other researchers have put into trying to make these tools more accessible, trying to make them easier to use, there still is a lot of work to prove a piece of software correct, even with advanced state-of-the-art tools. And so we&#8217;re still going to keep trying to push to make that easier. Trying to figure out how to automate the process better. There&#8217;s a lot of interest right now in artificial intelligence for trying to help with this, especially if you think about artificial intelligence actually <em>writing<\/em> software. You ask it to write a piece of software to do a particular task, and it generates some C code or some Rust code or some Java code, and then you hope that that&#8217;s correct because it could have generated any sort of code that performs the right thing or does total nonsense. So it would be really great going forward if when we ask AI to develop software, we also expect it to create a proof that the software is correct and does what the user asked for. We\u2019ve started working on some projects, and we found that the AI is not quite there yet for realistic code. It can do small examples this way. But I think this is still a very large challenge going forward that could have a large payoff in the future if we can get AI to develop software <em>and<\/em> prove that the software is correct.&nbsp;<\/p>\n\n\n\n<p><strong>LORCH: <\/strong>Yeah, I see there&#8217;s a lot of synergy between\u2014<em>potential<\/em> synergy\u2014between AI and verification. Artificial intelligence can solve one of the key challenges of verification, namely making it easy for developers to write that code. And verification can solve one of the key challenges of AI, which is hallucinations, synthesizing code that is not correct, and Verus can verify that that code actually is correct.&nbsp;<\/p>\n\n\n\n<p><strong>TINGLE: <\/strong>Well, Chris Hawblitzel and Jay Lorch, thank you so much for joining us today on the Microsoft Research Podcast to discuss your work on Verus.&nbsp;<\/p>\n\n\n\n<p>[MUSIC]&nbsp;<\/p>\n\n\n\n<p><strong>HAWBLITZEL: <\/strong>Thanks for having us.&nbsp;<\/p>\n\n\n\n<p><strong>LORCH: <\/strong>Thank you.&nbsp;<\/p>\n\n\n\n<p><strong>TINGLE: <\/strong>And to our listeners, we appreciate you, too. If you&#8217;d like to learn more about Verus, you&#8217;ll find a link to the paper at aka.ms\/abstracts or you can read it on the SOSP website. Thanks for tuning in. I&#8217;m Amber Tingle, and we hope you&#8217;ll join us again for <em>Abstracts<\/em>.<\/p>\n\n\n\n<p>[MUSIC FADES]&nbsp;<\/p>\n\n\t\t\t\t<\/span>\n\t\t\t<\/div>\n\t\t\t<button\n\t\t\t\tclass=\"action-trigger glyph-prepend mt-2 mb-0 show-more-show-less-toggle\"\n\t\t\t\taria-expanded=\"false\"\n\t\t\t\tdata-show-less-text=\"Show less\"\n\t\t\t\ttype=\"button\"\n\t\t\t\taria-controls=\"show-more-show-less-toggle-1\"\n\t\t\t\taria-label=\"Show more content\"\n\t\t\t\tdata-alternate-aria-label=\"Show less content\">\n\t\t\t\tShow more\t\t\t<\/button>\n\t\t<\/div>\n\t<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Researchers Chris Hawblitzel and Jay Lorch share how progress in programming languages and verification approaches are bringing bug-free software within reach. Their work on the Rust verification tool Verus won the Distinguished Artifact Award at SOSP \u201924.<\/p>\n","protected":false},"author":43518,"featured_media":1099833,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"https:\/\/player.blubrry.com\/id\/138212589","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"categories":[240054],"tags":[],"research-area":[13560,13547],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[269148,269142,243990],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[268128],"class_list":["post-1099821","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-msr-podcast","msr-research-area-programming-languages-software-engineering","msr-research-area-systems-and-networking","msr-locale-en_us","msr-post-option-approved-for-river","msr-post-option-include-in-river","msr-post-option-podcast-featured","msr-podcast-series-abstracts"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"https:\/\/player.blubrry.com\/id\/138212589","podcast_episode":"","msr_research_lab":[199565],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[1097610],"related-events":[],"related-researchers":[{"type":"user_nicename","value":"Amber Tingle","user_id":42681,"display_name":"Amber Tingle","author_link":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/ambertingle\/\" aria-label=\"Visit the profile page for Amber Tingle\">Amber Tingle<\/a>","is_active":false,"last_first":"Tingle, Amber","people_section":0,"alias":"ambertingle"},{"type":"user_nicename","value":"Chris Hawblitzel","user_id":31425,"display_name":"Chris Hawblitzel","author_link":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/chrishaw\/\" aria-label=\"Visit the profile page for Chris Hawblitzel\">Chris Hawblitzel<\/a>","is_active":false,"last_first":"Hawblitzel, Chris","people_section":0,"alias":"chrishaw"},{"type":"user_nicename","value":"Jay Lorch","user_id":32732,"display_name":"Jay Lorch","author_link":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/lorch\/\" aria-label=\"Visit the profile page for Jay Lorch\">Jay Lorch<\/a>","is_active":false,"last_first":"Lorch, Jay","people_section":0,"alias":"lorch"}],"msr_type":"Post","featured_image_thumbnail":"<img width=\"960\" height=\"540\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-960x540.jpg\" class=\"img-object-cover\" alt=\"Outlined illustrations of Chris Hawblitzel and Jay Lorch for the Microsoft Research Podcast, Abstracts series.\" decoding=\"async\" loading=\"lazy\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-960x540.jpg 960w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-300x169.jpg 300w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-1024x576.jpg 1024w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-768x432.jpg 768w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-1066x600.jpg 1066w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-655x368.jpg 655w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-240x135.jpg 240w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-640x360.jpg 640w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788-1280x720.jpg 1280w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2024\/11\/Chris-and-Jay_Abstracts_Hero_Feature_No_Text_1400x788.jpg 1400w\" sizes=\"(max-width: 960px) 100vw, 960px\" \/>","byline":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/ambertingle\/\" title=\"Go to researcher profile for Amber Tingle\" aria-label=\"Go to researcher profile for Amber Tingle\" data-bi-type=\"byline author\" data-bi-cN=\"Amber Tingle\">Amber Tingle<\/a>, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/chrishaw\/\" title=\"Go to researcher profile for Chris Hawblitzel\" aria-label=\"Go to researcher profile for Chris Hawblitzel\" data-bi-type=\"byline author\" data-bi-cN=\"Chris Hawblitzel\">Chris Hawblitzel<\/a>, and <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/lorch\/\" title=\"Go to researcher profile for Jay Lorch\" aria-label=\"Go to researcher profile for Jay Lorch\" data-bi-type=\"byline author\" data-bi-cN=\"Jay Lorch\">Jay Lorch<\/a>","formattedDate":"November 5, 2024","formattedExcerpt":"Researchers Chris Hawblitzel and Jay Lorch share how progress in programming languages and verification approaches are bringing bug-free software within reach. Their work on the Rust verification tool Verus won the Distinguished Artifact Award at SOSP \u201924.","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/1099821"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/users\/43518"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=1099821"}],"version-history":[{"count":13,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/1099821\/revisions"}],"predecessor-version":[{"id":1101081,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/1099821\/revisions\/1101081"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/1099833"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=1099821"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=1099821"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=1099821"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=1099821"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=1099821"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=1099821"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=1099821"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=1099821"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=1099821"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=1099821"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=1099821"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}