{"id":557352,"date":"2019-01-09T08:00:53","date_gmt":"2019-01-09T16:00:53","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?p=557352"},"modified":"2020-06-08T10:20:21","modified_gmt":"2020-06-08T17:20:21","slug":"scaling-the-everest-of-software-security-with-dr-jonathan-protzenko","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/podcast\/scaling-the-everest-of-software-security-with-dr-jonathan-protzenko\/","title":{"rendered":"Scaling the Everest of software security with Dr. Jonathan Protzenko"},"content":{"rendered":"<div id=\"attachment_557358\" style=\"width: 1034px\" class=\"wp-caption aligncenter\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-557358\" class=\"size-large wp-image-557358\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-1024x576.png\" alt=\"Jonathan Protzenko standing outside\" width=\"1024\" height=\"576\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-1024x576.png 1024w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-300x169.png 300w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-768x432.png 768w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-1066x600.png 1066w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-655x368.png 655w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-343x193.png 343w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788.png 1400w\" sizes=\"(max-width: 1024px) 100vw, 1024px\" \/><p id=\"caption-attachment-557358\" class=\"wp-caption-text\">Researcher Jonathan Protzenko<\/p><\/div>\n<h3>Episode 58, January 9, 2019<\/h3>\n<p>When people first started making software, computers were relatively rare and there was no internet, so programming languages were designed to get the job done quickly and run efficiently, with little thought for security. But software is everywhere now, from our desktops to our cars, from the cloud to the internet of things. That\u2019s why <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/protz\/\">Dr. Jonathan Protzenko<\/a>, a researcher in the <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/group\/research-software-engineering-rise\/\">RiSE \u2013 or Research in Software Engineering<\/a> \u2013 group at Microsoft Research, is working on designing better software tools in order to make our growing software ecosystem safer and more secure.<\/p>\n<p>Today, Dr. Protzenko talks about what\u2019s wrong with software (and why it\u2019s vitally important to get it right), explains why there are so many programming languages (and tells us about a few he\u2019s been working on), and finally, acts as our digital Sherpa for <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/project-everest-verified-secure-implementations-https-ecosystem\/\">Project Everest<\/a>, an assault on software integrity and confidentiality that aims to build and deploy a verified HTTPS stack.<\/p>\n<h3>Related:<\/h3>\n<ul type=\"disc\">\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/podcast\">Microsoft Research Podcast<\/a>: View more podcasts on Microsoft.com<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/itunes.apple.com\/us\/podcast\/microsoft-research-a-podcast\/id1318021537?mt=2\">iTunes<\/a>: Subscribe and listen to new podcasts each week on iTunes<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/subscribebyemail.com\/www.blubrry.com\/feeds\/microsoftresearch.xml\">Email<\/a>: Subscribe and listen by email<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/subscribeonandroid.com\/www.blubrry.com\/feeds\/microsoftresearch.xml\">Android<\/a>: Subscribe and listen on Android<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/open.spotify.com\/show\/4ndjUXyL0hH1FXHgwIiTWU\">Spotify<\/a>: Listen on Spotify<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/www.blubrry.com\/feeds\/microsoftresearch.xml\">RSS feed<\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/note.microsoft.com\/ww-registration-microsoft-research-newsletter-s.html?wt.mc_id=S-webpage_podcast\">Microsoft Research Newsletter<\/a>: Sign up to receive the latest news from Microsoft Research<\/li>\n<\/ul>\n<hr \/>\n<h3>Transcript<\/h3>\n<p>Jonathan Protzenko: What we\u2019re concerned with, in my day-to-day work these days, is the security of the internet. When you come to think of it, it\u2019s absolutely everywhere. And it\u2019s not just between you and a website. It\u2019s also in the cloud. It\u2019s also in all sorts of software. And the big awakening is that, for the past twenty years, this has never been secure. And the consequences are so huge, there\u2019s so much at stake, that people are ready to try something different.<\/p>\n<p><strong>Host: You\u2019re listening to the Microsoft Research Podcast, a show that brings you closer to the cutting-edge of technology research and the scientists behind it. I\u2019m your host, Gretchen Huizinga.<\/strong><\/p>\n<p><strong>Host: When people first started making software, computers were relatively rare and there was no internet, so programming languages were designed to get the job done quickly and run efficiently, with little thought for security. But software is everywhere now, from our desktops to our cars, from the cloud to the internet of things. That\u2019s why Dr. Jonathan Protzenko, a researcher in the RiSE \u2013 or Research in Software Engineering \u2013 group at Microsoft Research, is working on designing better software tools in order to make our growing software ecosystem safer and more secure.<\/strong><\/p>\n<p><strong>Today, Dr. Protzenko talks about what\u2019s wrong with software (and why it\u2019s vitally important to get it right), explains why there are so many programming languages (and tells us about a few he\u2019s been working on), and finally, acts as our digital Sherpa for Project Everest, an assault on software integrity and confidentiality that aims to build and deploy a verified HTTPS stack. That and much more on this episode of the Microsoft Research Podcast.<\/strong><\/p>\n<p><strong>Host: Jonathan Protzenko, welcome to the podcast.<\/strong><\/p>\n<p>Jonathan Protzenko: Hi.<\/p>\n<p><strong>Host: You\u2019re a researcher in the RiSE, or Research in Software Engineering group. What are the big problems you\u2019re trying to solve? I usually ask my guests, what gets you up in the morning? But I can\u2019t help myself: what makes you RiSE and shine?<\/strong><\/p>\n<p>Jonathan Protzenko: Well, RiSE is focused with many aspects of software engineering and the specific thing that I\u2019m concerned with is programming languages. And what gets me up in the morning is the fact that there is a lot of software out there that needs us to intervene and do something about. I was recently seeing an ad for a pet feeder that has a camera and that can report to me on my smartphone. And the immediate thing that I thought about was, that\u2019s going to be a security failure. And soon enough, there will be videos of my cat all over the internet. That\u2019s not a huge deal, but when you think about the millions of devices that are out there and that are ready to be hacked, and that are ready to be covered by the New York Times in the next wave of cyber-attacks, I\u2019m very concerned about the state of the software ecosystem. And in RiSE, what we\u2019re trying to do is address problems related to software through research and trying to make software better in general.<\/p>\n<p><strong>Host: Before we plunge into the specific research you\u2019re doing, I do want to talk about programming languages, in general. To paraphrase a colleague of yours, Ben Zorn, from a software perspective, you build the things people build things with.<\/strong><\/p>\n<p>Jonathan Protzenko: Yes.<\/p>\n<p><strong>Host: And there wouldn\u2019t be any big technical revolutions if there weren\u2019t programming languages. That said, there are so many of them. They\u2019re legion. Why are there so many?<\/strong><\/p>\n<p>Jonathan Protzenko: So, it\u2019s actually a good question. There have been like hundreds, if not thousands, of programming languages being developed, and there\u2019s always new ones popping up. I think one of the reasons is, there\u2019s that \u201choly grail\u201d of programming languages that you\u2019re always seeking: the right programming language that will compromise on nothing, the one that will allow you to get the speed that you want, the <strong>programmer productivity that you want, and also zero bugs. And I don\u2019t think we\u2019ve attained that holy grail yet, so the quest continues. There\u2019s always room for improvement.<\/strong><\/p>\n<p><strong>Host: Yeah.<\/strong><\/p>\n<p>Jonathan Protzenko: You realize that there exists large ecosystems of software and that we\u2019re now reaching like millions, hundreds of millions of lines of code, and any improvement in the tool that you use every single day of your life is going to be an improvement over software in general. So, the responsibility is enormous, in a sense. We have to design the right tools that will make people write better tools for other people.<\/p>\n<p><strong>Host: So, I usually frame my more general questions from what I like to call the 10,000-foot view. But since we\u2019re going to land on Everest in this podcast, I\u2019ll frame it from the 29,000-foot view.<\/strong><\/p>\n<p>Jonathan Protzenko: All right.<\/p>\n<p><strong>Host: Let\u2019s talk about software verification and security writ large. These are the kind of reasons for being, or raisons d\u2019etre, for you guys. Give us an overview of what\u2019s wrong here, and why it\u2019s important to get it right, and what you\u2019re doing with the research to tackle this.<\/strong><\/p>\n<p>Jonathan Protzenko: So, it kind of ties into what we were mentioning earlier. There\u2019s a lot of software that\u2019s absolutely critical. Where either gigantic breaches of security are at stake, or human lives, or accidents, and there\u2019s usually a large set of examples that you can draw from, ranging from DNA testing software, to planes, to nuclear software, medical devices, it\u2019s a very large array. And there are, I think, a few of these areas where we\u2019ve hit the right spot. And by the right spot, I mean that the consequences are so dramatic, and the past incidents have been so wide-ranging and have had such an impact, that the people in the field are ready to try something different. I think, for instance, for medical devices, we\u2019re nearly getting there. There have been hackable pacemakers. There have been demonstrations that you can actually control someone\u2019s medical device at a distance. And I think, for instance, in this specific configuration, soon enough, people will realize that the previous approaches no longer work, that they need to try something different, and that they need to start from the ground up and actually think about how to write better software. And in our case, and what we\u2019re concerned with, in my day-to-day work these days, is the security of the internet. When you come to think of it, it\u2019s absolutely everywhere. And it\u2019s not just between you and a website. It\u2019s also in the cloud. It\u2019s also in all sorts of software. And the big awakening is that, for the past twenty years, this has never been secure. And the consequences are so huge, there\u2019s so much at stake, that people are ready to try something different. They might be willing to let go of the technology from the 70s that I was mentioning and try something a little strange, a little functional, but that might give them greater confidence that maybe there won\u2019t be a huge failure after all.<\/p>\n<p><strong>Host: This technology from the 70s you\u2019re referring to\u2026<\/strong><\/p>\n<p>Jonathan Protzenko: I\u2019m thinking of the C programming language that remains the language that people use to write the majority of the software. And it\u2019s extremely easy to shoot yourself in the foot with that language. So, what we\u2019re trying to do, and we\u2019re working with some great people, is to say, this has been so broken and so badly that we have a new methodology. Let us try to help you. Like, here\u2019s how we\u2019re going to do it. What do you think?<\/p>\n<p><strong>Host: How much of an education curve is this requiring?<\/strong><\/p>\n<p>Jonathan Protzenko: It\u2019s an extremely steep curve, and I think that\u2019s also the big challenge in my field. Like, how can we make these tools usable by people outside of our field? There\u2019s a reason why people stick with these well-established programming languages. It\u2019s because they\u2019re very usable, and I think the tools that we use to write more secure software are sometimes not so usable, or require, like, a very high degree of training. And that\u2019s also a challenge for us, like, how can we make software verification more usable for someone that doesn\u2019t have that background?<\/p>\n<p><strong>Host: Yeah, that tradeoff between power and ease of use\u2026<\/strong><\/p>\n<p>Jonathan Protzenko: Absolutely, and that\u2019s why new languages keep showing up. It\u2019s because sometimes, you\u2019re ready to have an expert that is going to use a language that will make them very productive, but maybe you can\u2019t find 10,000 experts, or maybe your software is already written, and you can\u2019t swap it out and rewrite everything from the ground up.<\/p>\n<p><strong>Host: Wow, my mind is just reeling, because I\u2019ve had a couple of cryptographers in the booth here.<\/strong><\/p>\n<p>Jonathan Protzenko: Mm-hmm.<\/p>\n<p><strong>Host: And the revelation that things aren\u2019t as secure as you think \u2013 I mean, even if you go to an http, not an https \u2013 most people don\u2019t even know that there\u2019s a difference there. And I\u2019m talking about the vast majority of people that are using the software?<\/strong><\/p>\n<p>Jonathan Protzenko: Yes, and that\u2019s why we need to help these people, because we can\u2019t rely on the fact that people are going to check the padlock on their website. It\u2019s just too much to ask from a regular user. So, we need to help them out. And there\u2019s been really great initiatives. The number of people who use https is skyrocketing, in no small part due to an initiative called Let\u2019s Encrypt from Mozilla that is nudging people to switch to https.<\/p>\n<p><strong>Host: Nice.<\/strong><\/p>\n<p>Jonathan Protzenko: And that has achieved really excellent results. And so, if on top of that, we hope to give them more secure software to perform https, then I think the world would be a slightly better place.<\/p>\n<p><strong>Host: Or maybe even more than slightly. You\u2019re being modest. Because like you said, software is pervasive, and we\u2019re all just sort of onboarding it into our lives.<\/strong><\/p>\n<p>Jonathan Protzenko: The trend is that software is going to be everywhere, and we\u2019re delegating extremely important decisions to software. When you think about cars, for instance, the millions, tens, maybe hundreds of millions of lines of code that are running in a car, it\u2019s just frightening. And you see these videos on YouTube of people taking remote control of a car. And it\u2019s not just cars. It\u2019s absolutely everywhere. And we\u2019re just putting an enormous amount of trust into it.<\/p>\n<p><strong>Host: And we will come back, in a while, to what keeps you up at night. But let\u2019s get happy for a minute.<\/strong><\/p>\n<p>Jonathan Protzenko: Yes.<\/p>\n<p><strong>Host: Let\u2019s talk about the cool projects you\u2019re working on, or have worked on, and one of them is a language, a functional language called F*.<\/strong><\/p>\n<p>Jonathan Protzenko: Yes.<\/p>\n<p><strong>Host: And I keep looking at it going, F#. It\u2019s a star\u2026 And it\u2019s a general-purpose functional programming language with effects aimed at program verification.<\/strong><\/p>\n<p>Jonathan Protzenko: Yes, so, F* draws inspiration from F#, hence the similar name and also the general, like, family of functional programming languages such as OCaml and the general ML family. But it adds verification on top of it. The idea is that, if you\u2019re a functionally-trained programmer, and you\u2019re comfortable with ML, maybe you\u2019ve written a bunch of OCaml in your life, here\u2019s a language that allows you to go further and to start thinking about what your programs do, what their specification is, to reason about them using and pre- and post-conditions, and to, generally, use the assistance of an SMT solver to scale up verification. So, in that sense, I think that F* is also at a very interesting point in the design space in that it\u2019s trying to cater to an audience of people who want to write software first. It\u2019s not a tool that you would use to do a massive mathematical proof about some theorem, but it\u2019s a tool that you would use to write your software in.<\/p>\n<p><strong>Host: Mm-hmm. Who\u2019s your audience for this?<\/strong><\/p>\n<p>Jonathan Protzenko: It\u2019s actually a good question\u2026 A good way to think about that is to look at who\u2019s been working on F*. F* is a large, joint project, the brainchild of Nik Swamy and a lot of his collaborators, including INRIA and many other institutions. And I would say that the audience is academics that are trying to write verified software. It can be both for learners, masters\u2019 students, PhD students, who are warming up to verification. It can be for people who want to write a verified piece of code that they\u2019re hoping to land into some existing software. And I\u2019m sure we\u2019ll talk about that soon.<\/p>\n<p><strong>Host: Yeah.<\/strong><\/p>\n<p>Jonathan Protzenko: What we\u2019re hoping our audience is, is the \u201cenlightened programmer.\u201d Someone who is functionally trained, realizes that it\u2019s great, but that there\u2019s also something beyond that, and who\u2019s willing to learn more and go further and deeper to actually convince themselves that their software is doing the right thing.<\/p>\n<p><strong>(music plays)<\/strong><\/p>\n<p><strong>Host: So, another thing you\u2019re working on is called KreMLin. I\u2019m going to spell this: big K, little r, little e, big M, big L, little i, little n.<\/strong><\/p>\n<p>Jonathan Protzenko: Yes.<\/p>\n<p><strong>Host: Why the change-up in lowercase-uppercase?<\/strong><\/p>\n<p>Jonathan Protzenko: I just wanted to highlight ML. I like puns. But all jokes aside, the interesting bit that you see in KreMLin is that there\u2019s K and R and ML. And it\u2019s kind of, you know, Kernighan and Ritchie meets ML. KreMLin is a compiler from F* to C, and here I\u2019m tying together two things that we\u2019ve talked about before, the fact that you want to use a high-end, sophisticated, advanced programming language to prove important things about your software, but also the fact that the majority of software these days is written in C, and that it\u2019s not going away anytime soon. And one interesting thing is that you need to meet software where it is. So, the idea behind my work these days is that we need to reconcile these two visions: the vision of the enlightened programmer that works in F* and does their very advanced verification result, and the fact that people want C code if you want your software to be used. And so, KreMLin is a compiler that will transform a subset of F* into C code that is ready to be integrated into existing software. And you can use all of F*. You can write code as you normally would. You can conduct proofs that are just like you would normally, except that, at the end of the tool chain, you get C code, and you can walk to people and say, hey, now I have code that you might want to use.<\/p>\n<p><strong>Host: Speaking of acronyms, there\u2019s another program you\u2019re working on called HACL*, H-A-C-L stands for high-assurance cryptographic library. What is that, and what does it allow you to do? What\u2019s cool about this particular project?<\/strong><\/p>\n<p>Jonathan Protzenko: So, we talked about how there exists the program language called F* and the companion compiler that will give you C code that people actually want to use. And once you have that tool chain, the question is, how do you make the best use of it? And I\u2019ve mentioned that there\u2019s a lot of software disasters, and, in my opinion, cryptography is one of the biggest ones, because it\u2019s the underpinning of almost every secure software.<\/p>\n<p><strong>Host: Yeah.<\/strong><\/p>\n<p>Jonathan Protzenko: And, if cryptography breaks, your whole scaffolding breaks and everything shatters, and so cryptography is perhaps the place where we have the right combination of factors that make people want to use different software, new software, verified software. And so HACL* is our answer to that. It\u2019s a library of cryptographic code, verified in F*, that comes out as a bunch of C code that people want to use. It\u2019s been designed in collaboration with INRIA, the French Institute for Computer Science, and it\u2019s already being used by several people.<\/p>\n<p><strong>Host: What\u2019s the Venn diagram overlap with cryptographers and programming language people? There\u2019s a lot of layers&#8230;<\/strong><\/p>\n<p>Jonathan Protzenko: Yes.<\/p>\n<p><strong>Host: &#8230;of people working on different things and then needing to get together and make it usable.<\/strong><\/p>\n<p>Jonathan Protzenko: There\u2019s the cryptographers that design algorithms, and for me, that\u2019s not my job. I know that algorithms exist. I know how they\u2019re done, but I would have a really hard time creating a new one, so, don\u2019t let me do that. That would be a disaster. There\u2019s us, the people who implement the cryptography, taking a reference or design or some math on a paper that describes the inner workings of an algorithm. We just transform it into actual software. And then there\u2019s the consumers.<\/p>\n<p><strong>Host: Right.<\/strong><\/p>\n<p>Jonathan Protzenko: People who know that they need cryptography and are going to make use of it in their own software. And we\u2019re kind of bridging the gap between the cryptographers and the consumers by taking existing implementations that have been done before, but reverifying them. So, we don\u2019t design new code. What we design is verification methodologies that will allow us to show that either the existing code was broken, and we\u2019ve found broken code, or that the existing code, or our code, is fine, and that we\u2019re ready to give it to consumers. And we work closely with our consumers, such as Firefox. And we spend a lot of time making sure that the C code that comes out of our tool chain is something that they actually want to use. And that turned out to be surprisingly difficult.<\/p>\n<p><strong>Host: The question just in my head when you said that is, how hard is this?<\/strong><\/p>\n<p>Jonathan Protzenko: So, there\u2019s two halves to the work, in a sense. Like first, you want to verify code. And that is tedious, difficult, but in a sense, we already know that we\u2019re going to make it. It\u2019s just a matter of throwing enough energy at it.<\/p>\n<p><strong>Host: Sure.<\/strong><\/p>\n<p>Jonathan Protzenko: But then once you\u2019ve done that, actually going to meet people in software, telling them that you have something new and that, really, they should use it, it\u2019s a different problem. And you need to build trust. You need to show them that you\u2019re serious. You need to show them that your code makes sense. They\u2019re probably not going to trust your very exotic verification methodology, and they\u2019re going to reread the C code that comes out of it just to convince themselves that it makes sense. So, we spend a lot of time and energy engaging with them, polishing what comes out of our verification suite, and making sure that it was something that looked solid to them.<\/p>\n<p><strong>Host: So, let\u2019s talk about miTLS, a verified reference implementation of TLS. Why don\u2019t you give us a little bit of history of that project? Who\u2019s involved in it, what are you doing with it, and why do we need other organizations involved in order to tackle this program?<\/strong><\/p>\n<p>Jonathan Protzenko: Yes. So maybe I can say a little word about TLS first?<\/p>\n<p><strong>Host: Please.<\/strong><\/p>\n<p>Nonathan Protzenko: TLS is the protocol that you\u2019re using when you\u2019re connecting to a website over https. And I was talking about the cryptography being at the bottom of the stack. It\u2019s the base building-block. But on top of the cryptography, you can work out a protocol that will allow you to negotiate keys, parameters, sessions, and then establish a secure channel between you a third party. So, there\u2019s two key properties that you want to establish when you have a channel with a third party: integrity and confidentiality. If you\u2019re going, I don&#8217;t know, to a web search, confidentiality is making sure that no one can see what you\u2019re looking for. And integrity is making sure that no one can tamper with your search while you\u2019re receiving the results. So, the protocol that does this is called TLS, it was previously known as SSL.<\/p>\n<p><strong>Host: Right.<\/strong><\/p>\n<p>Jonathan Protzenko: It\u2019s from the early 90s, originated at Netscape, and it\u2019s the one you use every time you go to an https website. And so, miTLS is our attempt at making TLS more secure. It\u2019s a fairly old project that started as a joint collaboration between Microsoft and INRIA.<\/p>\n<p><strong>Host: Hence the m-i&#8230; mi\u2026<\/strong><\/p>\n<p>Jonathan Protzenko: Hence the name mi, Microsoft\/INRIA TLS. We\u2019ve gone through successive languages. The first version of miTLS was using a precursor of F* called F7, and we\u2019ve just evolved both the verification artifact and the language that enables us to verify the software. So, the two go hand in hand. We both design the tools that enable verification and take it upon ourselves to actually use them to perform verification. And I would say that that\u2019s the best way to design a tool, is to use it yourself\u2026<\/p>\n<p><strong>Host: Yeah.<\/strong><\/p>\n<p>Jonathan Protzenko: \u2026realize where you have shortcomings, and just try to fix it and improve it. So, it\u2019s actually a continuous back-and-forth process where you try to verify something, realize that the tool could help you better, or could do something more easily for you, and then you fix the tool, and the tool keeps improving, driven by the needs of the verification.<\/p>\n<p><strong>Host: So how much time do you spend trying to break your stuff?<\/strong><\/p>\n<p>Jonathan Protzenko: Well, theoretically, because it\u2019s \u201cverified,\u201d it should never be&#8230;<\/p>\n<p><strong>Host: Right.<\/strong><\/p>\n<p>Jonathan Protzenko: &#8230;you know, broken. So that\u2019s the theory. The practice is, we also try to find flaws.<\/p>\n<p><strong>Host: Yeah.<\/strong><\/p>\n<p>Jonathan Protzenko: And it\u2019s an interesting question. There\u2019s occasionally flaws in our tools, and we need to either fix the tools, improve the tools, or, ideally, verify the tools themselves to show that our tools have no flaws. And also, sometimes, we don\u2019t cover everything. For instance, you can always write a very secure implementation of TLS that just declines to connect to any website. And you get the property that every connection is secure. So, we also need to make sure that we can actually interoperate with the rest of world.<\/p>\n<p><strong>(music plays)<\/strong><\/p>\n<p><strong>Host: Now let\u2019s climb the big one. Be our digital Sherpa on Project Everest. Your goal \u2013 I\u2019ll tee this up by, by saying \u2013 your goal is to build and deploy a verified https stack. Tell us all about Everest.<\/strong><\/p>\n<p>Jonathan Protzenko: So, Everest is, as you mentioned, our answer to that very sorry state of the world, which is that there hasn\u2019t been a secure TLS implementation since the beginning of TLS. It\u2019s always broken. So, what we set out to do, a few years ago, is to say, all right, we\u2019ve been working on that miTLS technology. Can we push it next level, verify the entire stack, and also get people to use it? So, it was an ambitious effort that we set out, both in terms of breadth \u2013 we want to verify the entire stack \u2013 and also, in terms of impact \u2013 we want people to use it. And so for that, we got together people at several institutions. There was Microsoft Research here in Redmond, but also Cambridge and Bangalore. There\u2019s people at Carnegie Mellon University. There\u2019s people at University of Edinburgh. And, of course, there\u2019s our very close collaborators at INRIA. And so, what we\u2019re doing is that, it\u2019s so wide and big that we have different people working on different things. INRIA, as I mentioned, is mostly concerned with the base building-blocks, the cryptography. We have another tool that we use to verify assembly code for those bits that really need absolute performance. And that\u2019s between say, CMU and here. We have, in Cambridge, our expert cryptographers and protocol experts that find the flaws and try to fix the standard by submitting feedback whenever they find a conceptual flaw in TLS. And we try to bring all these people together behind that effort.<\/p>\n<p><strong>Host: Yeah. All right, so Everest is a \u201cgoal mountain\u201d for a lot of people who climb. Would you frame this as a \u201cgoal mountain\u201d to summit for software engineering?<\/strong><\/p>\n<p>Jonathan Protzenko: I would say that, for us, yes, there\u2019s that theorem that I was alluding to earlier that you get integrity and confidentiality, and that\u2019s kind of the top of the pyramid, the summit of the mountain. Once we get that theorem, our entire stack will be verified. So, we\u2019re hoping to get there. And for us, it will also be a summit, because it\u2019s a very wide-ranging and ambitious verification effort. One thing to realize is that we\u2019re aiming for a very comprehensive set of software.<\/p>\n<p><strong>Host: Yeah.<\/strong><\/p>\n<p>Jonathan Protzenko: Just looking at the cryptography, we\u2019re aiming to verify not just one algorithm, but entire families. And we\u2019re aiming to offer a comprehensive cryptographic library that has everything you need to do crypto, and that covers all the popular algorithms that you might need. So, it\u2019s a lot of work and it\u2019s a lot of software. So, I think for us, we\u2019re hoping that, by the time we reach that final theorem, we will have advanced both what we are capable of doing in terms of size, and also like the state of the art in terms of verification tools.<\/p>\n<p><strong>Host: So, what\u2019s the relationship of miTLS with project Everest?<\/strong><\/p>\n<p>Jonathan Protzenko: miTLS is, so far, the main component of Project Everest, and the one that depends on almost everything else, and the one that will be our implementation of TLS. I think there will be other things afterwards. Depends on what you see at the top of the mountain. The top of the mountain could be miTLS and C, but it could also be, say, a verified web server that uses miTLS, and then we\u2019re, you know, setting another goal. So, I guess that remains to be determined, but yeah, the v.1 would be miTLS and the TLS library. And maybe the v.2 will have other things, such as a small server or even other components of the stack.<\/p>\n<p><strong>Host: Academics by nature are open source people. You do some work, you share it with everybody. You build off the work of others, and they build off your work. But that hasn\u2019t necessarily historically been the case in industry with IP and competitive advantage issues. But lately, it seems there\u2019s been a bit of a shift towards an embrace of a more open source mentality. So why do you think we\u2019re seeing more \u201csharing\u201d in the open source community among industry researchers, and why is that a good thing?<\/strong><\/p>\n<p>Jonathan Protzenko: So, yes, one thing that I should have mentioned is that all of our work is open source, and we work completely in the open with academics and universities. All of our code is on GitHub and we have public discussion channels. And I think there\u2019s two aspects to consider. The first one is, we just work better when it\u2019s in the open. I find that it fosters better collaborations, more productive ideas, and generally a better atmosphere. It\u2019s more motivating to know that you\u2019re doing software for the general good that will benefit a lot of other people than just software for a small subset of the planet. So, that is something that motivates me personally. And I very much believe in the societal value of having code that is for everyone to use. And the other, more pragmatic reason perhaps, is that in security, if people can\u2019t see your code, they\u2019re just going to have a hard time convincing themselves that you\u2019re secure. It\u2019s a hard claim, right, that your software is secure? And you usually want to provide evidence for that.<\/p>\n<p><strong>Host: Sure.<\/strong><\/p>\n<p>Jonathan Protzenko: And if your code is closed source, then you\u2019re going to have a hard time convincing other people that, really, you have secure software. So, it\u2019s just better to do it in the open. That way everyone can go and see for themselves.<\/p>\n<p><strong>Host: Do you feel like you\u2019ve noticed a sea change in this area? I know that, you know, in certain decades prior, a lot of companies kept their cards really close to their chest. It\u2019s proprietary. We don\u2019t want anyone to see the source code. We don\u2019t, you know&#8230;<\/strong><\/p>\n<p>Jonathan Protzenko: I have seen like a big change at Microsoft in just the four years that I\u2019ve been here. I think I came in just at the right time when the mentalities were changing. And it\u2019s been just getting better and better. I\u2019ve found that I can use a Linux computer to do my day-to-day work and I can post on GitHub. I don\u2019t have to worry about anything. And I think it\u2019s just a reality of software development now, that so much software that you depend on is open source, that you\u2019re just more productive if you can contribute back. And we have done that, occasionally, in my day-to-day work. I use an open source project, there\u2019s a bug in it, fine. I\u2019ll go and fix it. And it\u2019s just a better way to work.<\/p>\n<p><strong>Host: And maybe somebody else has found your bug and helped you out there?<\/strong><\/p>\n<p>Jonathan Protzenko: Oh, yeah. And people can come and sometimes report bugs on our stuff. If you look at F* for instance, we have contributors, people we\u2019ve never met, who just come in, out of the blue, and submit improvements. And for us, that\u2019s just&#8230;<\/p>\n<p><strong>Host: Thank you very much.<\/strong><\/p>\n<p>Jonathan Protzenko: It\u2019s\u2026 yeah, we\u2019re very happy with that, and it just makes you feel better when you wake up in the morning and you have someone who just fixed one of your bugs.<\/p>\n<p><strong>Host: I wish that would happen to me. Not software, but, you know\u2026<\/strong><\/p>\n<p><strong>(music plays)<\/strong><\/p>\n<p><strong>Host: Jonathan, you\u2019re working on security and verification in software, and you know the realities. We\u2019ve talked a little bit about how scary that world is. And you\u2019re working on it every day. Is there anything that keeps you up at night, particularly as it pertains to the state of software that you haven\u2019t discussed already? And what should we be aware of?<\/strong><\/p>\n<p>Jonathan Protzenko: I think the general awareness of the fragility of software is not as it should be. What I mean by that is, there seems to be, in my opinion, too much of an enthusiasm for software without the awareness of what this entails. It\u2019s Christmas season. People are going to get gifts, and I\u2019m being bombarded with smart appliances. Every time I see one of these, I\u2019m wondering, what are the consequences? And so far, it\u2019s kind of the wild west. If you think about all of the IoT things that are going to be spread out all across the world, what\u2019s going to happen to these devices? Who\u2019s going to maintain the software? Who\u2019s even going to look at the software before it\u2019s released and sold in millions? And it\u2019s actually happening faster than we realize. And that\u2019s something that keeps me up at night. I see everyone getting smart light bulbs. What if your light bulb is being taken over by someone else? I\u2019m very worried about these things, but I\u2019m also hoping that, soon enough, there will be a change, both in terms of the software, and also in terms of expectations. And that could be, you know, people just don\u2019t want broken software, or maybe there\u2019s a regulation that says you can\u2019t put on the market something that is obviously broken and that\u2019s going to be actually a threat.<\/p>\n<p><strong>Host: When I talked to Ben, it was actually a year ago, we talked about the Internet of Things and how many devices get put out in the world. And the key is verification, and that was when he alluded to Everest. How is that project informing this world of devices that are quote-unquote smart\u2026 and unverified?<\/strong><\/p>\n<p>Jonathan Protzenko: What I would hope for, at least, is that by the time we manage to get a working version of miTLS, that it can become a viable option. Say you\u2019re doing a smart security camera. And of course, you need to upload in the cloud on the server. Well, hopefully, miTLS can be a viable option for people who want to establish a secure channel between their little device and the cloud. That won\u2019t solve every problem, far from it, but I really, firmly believe in one brick at a time, and one step at a time. And my hope is that we have, at least, a better brick in that big software ecosystem. One way to sum it up is, software has consequences, and everyone needs to be aware of it. Software is not benign. Software could do all sorts of terrible things. And it hardly ever does, but we need to be cognizant of the fact that it could, and we need to exercise caution. You install an app, think twice. You\u2019re getting a smart appliance, also think twice.<\/p>\n<p><strong>Host: But the problem is the binary option, you know? Do you agree? If you don\u2019t, you can\u2019t have the app. So, I hit agree.<\/strong><\/p>\n<p>Jonathan Protzenko: Yes, and for me, that\u2019s the big question. Like, how do we create the social and economic dynamic for better software? And for me, that\u2019s a big open question, because I\u2019m just like you. I click on \u201cagree\u201d all the time. I couldn\u2019t, like, go into existential mode whenever I install an app. So yes, I do click on agree. But where\u2019s the incentive going to come from? For internet security, the interesting bit is that there\u2019s a big economic incentive. If you\u2019re broken, people are going to have to be paged on a weekend. There\u2019s going to be, like, an incident response, a crisis. So, this resonates very well with the people that we work with. And that\u2019s why they\u2019re ready for better software. What is the equivalent for all these devices and the security of that software? I think that\u2019s something we need to figure out, and it can come from many different places. But my hope is that, ultimately, yes, there is an incentive to make software, in general, more secure.<\/p>\n<p><strong>Host: Jonathan, tell us a bit about yourself, academically and otherwise. What\u2019s your story? How did you come to be working in software engineering research at MSR? What don\u2019t people know about Jonathan Protzenko?<\/strong><\/p>\n<p>Jonathan Protzenko: I did my PhD in France, at INRIA. And, as oftentimes happens at the end of one\u2019s PhD, I was pretty fed up by the end of my dissertation writing, and I wasn\u2019t sure what I wanted to do with my life. I had a lot of existential moments, and I was ready to quit, you know, research and go work in software, because I thought research was too hard. And then my PhD advisor really nudged me and said, well, Jonathan, at least try Microsoft Research. You know, you might find a good vibe there. So, I did, and that\u2019s how I arrived here. I didn\u2019t believe in it at first. I didn\u2019t think I would make it. I remember chatting with my advisor about it, being like, come on, Francois, they\u2019re never going to take me. But I tried, and yes, they did take me, so that was good. And I started out as a post-doc here. I worked on a variety of projects, and then I became a researcher after a year and a half, I think. And I\u2019ve been here for four years now.<\/p>\n<p><strong>Host: Prior to that, you did your PhD in France. Did you grow up in France?<\/strong><\/p>\n<p>Jonathan Protzenko: Yes, I did grow up in the France. I\u2019m a pure product of the French system.<\/p>\n<p><strong>Host: Because you keep talking about existential moments. And so, it\u2019s like, oh, Jean-Paul Sartre\u2026. Uhmmm\u2026 Where are you from in France?<\/strong><\/p>\n<p>Jonathan Protzenko: I grew up in near Bordeaux. I stayed in Bordeaux for high school, and then did my Masters\u2019 degree in Lyon, and then my PhD program in Paris.<\/p>\n<p><strong>Host: Nice. What\u2019s your future goal? Aside from conquering Everest, where do you see yourself in five years?<\/strong><\/p>\n<p>Jonathan Protzenko: Oh, that\u2019s a tough question, and you didn\u2019t give me a heads up for that one.<\/p>\n<p><strong>Host: I didn\u2019t.<\/strong><\/p>\n<p>Jonathan Protzenko: Otherwise I would have thought about it. I\u2019m hoping that in five years, I can start tackling more fundamental questions about software, about the things that we were talking about, social consequences of software and that I can bring greater awareness of, what is software? What happens with it? And that we can bring the message of \u201csoftware matters\u201d beyond just the niche areas where people have come to that conclusion already and make people more aware of what software entails. And maybe that\u2019s where the incentive to have better software is going to come from, from better software literacy. You\u2019re likely going to be dealing with computers almost every single day of your life, so you need a little bit of computer literacy. You need people to understand how software works, because that\u2019s, actually, an essential skill in the modern world. And maybe, eventually, people are aware enough that they\u2019re going to start demanding better software, and hopefully it will be there.<\/p>\n<p><strong>Host: As we close, give us an idea \u2013 this will sound like a large question, but you can scale it down if you like \u2013 what\u2019s left to discover, or solve, in the field of research in software engineering? What advice or encouragement would you give to listeners who might be interested or inspired by the work you\u2019re doing?<\/strong><\/p>\n<p>Jonathan Protzenko: One thing to keep in mind is that we\u2019re getting a lot of people to use our software. Our software runs in Firefox. Our software runs in Windows. This is great, and hopefully, soon, it will run in Linux. So, it all seems wonderful from an outsider\u2019s perspective. But it\u2019s a lot of hard work, and it\u2019s not as easy as it sometimes seems. So, we need a lot of help. And I think the next frontier is, how can we make this more usable? How can we make it more accessible to people who don\u2019t have the luxury of spending, you know, almost a decade training in computer science and who will still be writing software for a living? How can we bring the technology to the masses of programmers that are out there? And I think that\u2019s an enormous challenge, and any help would be most welcome.<\/p>\n<p><strong>(music plays)<\/strong><\/p>\n<p><strong>Host: Jonathan Protzenko, thanks for joining us today. It\u2019s been really fun.<\/strong><\/p>\n<p>Jonathan Protzenko: It\u2019s been a pleasure. Thanks for having me.<\/p>\n<p><strong>To learn more about Dr. Jonathan Protzenko, and how researchers are trying to summit the verification mountain so you don\u2019t have to, visit <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/\">Microsoft.com\/research<\/a><\/strong><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Episode 58, January 9, 2019 &#8211; Dr. Protzenko talks about what\u2019s wrong with software (and why it\u2019s vitally important to get it right), explains why there are so many programming languages (and tells us about a few he\u2019s been working on), and finally, acts as our digital Sherpa for Project Everest, an assault on software integrity and confidentiality that aims to build and deploy a verified HTTPS stack.<\/p>\n","protected":false},"author":37074,"featured_media":557358,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"https:\/\/player.blubrry.com\/id\/40321313","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"categories":[240054],"tags":[],"research-area":[13560],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-557352","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-msr-podcast","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"https:\/\/player.blubrry.com\/id\/40321313","podcast_episode":"","msr_research_lab":[199565],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[663087,144812],"related-projects":[235367],"related-events":[558255],"related-researchers":[],"msr_type":"Post","featured_image_thumbnail":"<img width=\"960\" height=\"540\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788.png\" class=\"img-object-cover\" alt=\"Jonathan Protzenko standing outside\" decoding=\"async\" loading=\"lazy\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788.png 1400w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-300x169.png 300w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-768x432.png 768w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-1024x576.png 1024w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-1066x600.png 1066w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-655x368.png 655w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/12\/Jonathan-Protzenko_POD_Site_11_2018_1400x788-343x193.png 343w\" sizes=\"(max-width: 960px) 100vw, 960px\" \/>","byline":"","formattedDate":"January 9, 2019","formattedExcerpt":"Episode 58, January 9, 2019 - Dr. Protzenko talks about what\u2019s wrong with software (and why it\u2019s vitally important to get it right), explains why there are so many programming languages (and tells us about a few he\u2019s been working on), and finally, acts as&hellip;","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/557352"}],"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\/37074"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=557352"}],"version-history":[{"count":4,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/557352\/revisions"}],"predecessor-version":[{"id":557481,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/557352\/revisions\/557481"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/557358"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=557352"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=557352"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=557352"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=557352"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=557352"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=557352"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=557352"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=557352"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=557352"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=557352"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=557352"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}