Scaling the Everest of software security with Dr. Jonathan Protzenko

Publié janvier 9, 2019

Partagez cette page

Researcher Jonathan Protzenko

Episode 58, January 9, 2019

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’s why Dr. Jonathan Protzenko, a researcher in the RiSE – or Research in Software Engineering – group at Microsoft Research, is working on designing better software tools in order to make our growing software ecosystem safer and more secure.

Today, Dr. Protzenko talks about what’s wrong with software (and why it’s vitally important to get it right), explains why there are so many programming languages (and tells us about a few he’s 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.

Microsoft Research Podcast: View more podcasts on Microsoft.com
iTunes: Subscribe and listen to new podcasts each week on iTunes
Email: Subscribe and listen by email
Android: Subscribe and listen on Android
Spotify: Listen on Spotify
RSS feed
Microsoft Research Newsletter: Sign up to receive the latest news from Microsoft Research

Transcript

Jonathan Protzenko: What we’re concerned with, in my day-to-day work these days, is the security of the internet. When you come to think of it, it’s absolutely everywhere. And it’s not just between you and a website. It’s also in the cloud. It’s 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’s so much at stake, that people are ready to try something different.

Host: You’re 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’m your host, Gretchen Huizinga.

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’s why Dr. Jonathan Protzenko, a researcher in the RiSE – or Research in Software Engineering – group at Microsoft Research, is working on designing better software tools in order to make our growing software ecosystem safer and more secure.

Host: Jonathan Protzenko, welcome to the podcast.

Jonathan Protzenko: Hi.

Host: You’re a researcher in the RiSE, or Research in Software Engineering group. What are the big problems you’re trying to solve? I usually ask my guests, what gets you up in the morning? But I can’t help myself: what makes you RiSE and shine?

Jonathan Protzenko: Well, RiSE is focused with many aspects of software engineering and the specific thing that I’m 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’s going to be a security failure. And soon enough, there will be videos of my cat all over the internet. That’s 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’m very concerned about the state of the software ecosystem. And in RiSE, what we’re trying to do is address problems related to software through research and trying to make software better in general.

Host: Before we plunge into the specific research you’re 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.

Jonathan Protzenko: Yes.

Host: And there wouldn’t be any big technical revolutions if there weren’t programming languages. That said, there are so many of them. They’re legion. Why are there so many?

Jonathan Protzenko: So, it’s actually a good question. There have been like hundreds, if not thousands, of programming languages being developed, and there’s always new ones popping up. I think one of the reasons is, there’s that “holy grail” of programming languages that you’re 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 programmer productivity that you want, and also zero bugs. And I don’t think we’ve attained that holy grail yet, so the quest continues. There’s always room for improvement.

Host: Yeah.

Jonathan Protzenko: You realize that there exists large ecosystems of software and that we’re 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.

Host: So, I usually frame my more general questions from what I like to call the 10,000-foot view. But since we’re going to land on Everest in this podcast, I’ll frame it from the 29,000-foot view.

Jonathan Protzenko: All right.

Host: Let’s talk about software verification and security writ large. These are the kind of reasons for being, or raisons d’etre, for you guys. Give us an overview of what’s wrong here, and why it’s important to get it right, and what you’re doing with the research to tackle this.

Jonathan Protzenko: So, it kind of ties into what we were mentioning earlier. There’s a lot of software that’s absolutely critical. Where either gigantic breaches of security are at stake, or human lives, or accidents, and there’s usually a large set of examples that you can draw from, ranging from DNA testing software, to planes, to nuclear software, medical devices, it’s a very large array. And there are, I think, a few of these areas where we’ve 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’re nearly getting there. There have been hackable pacemakers. There have been demonstrations that you can actually control someone’s 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’re concerned with, in my day-to-day work these days, is the security of the internet. When you come to think of it, it’s absolutely everywhere. And it’s not just between you and a website. It’s also in the cloud. It’s 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’s 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’t be a huge failure after all.

Host: This technology from the 70s you’re referring to…

Jonathan Protzenko: I’m thinking of the C programming language that remains the language that people use to write the majority of the software. And it’s extremely easy to shoot yourself in the foot with that language. So, what we’re trying to do, and we’re 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’s how we’re going to do it. What do you think?

Host: How much of an education curve is this requiring?

Jonathan Protzenko: It’s an extremely steep curve, and I think that’s also the big challenge in my field. Like, how can we make these tools usable by people outside of our field? There’s a reason why people stick with these well-established programming languages. It’s because they’re 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’s also a challenge for us, like, how can we make software verification more usable for someone that doesn’t have that background?

Host: Yeah, that tradeoff between power and ease of use…

Jonathan Protzenko: Absolutely, and that’s why new languages keep showing up. It’s because sometimes, you’re ready to have an expert that is going to use a language that will make them very productive, but maybe you can’t find 10,000 experts, or maybe your software is already written, and you can’t swap it out and rewrite everything from the ground up.

Host: Wow, my mind is just reeling, because I’ve had a couple of cryptographers in the booth here.

Jonathan Protzenko: Mm-hmm.

Host: And the revelation that things aren’t as secure as you think – I mean, even if you go to an http, not an https – most people don’t even know that there’s a difference there. And I’m talking about the vast majority of people that are using the software?

Jonathan Protzenko: Yes, and that’s why we need to help these people, because we can’t rely on the fact that people are going to check the padlock on their website. It’s just too much to ask from a regular user. So, we need to help them out. And there’s been really great initiatives. The number of people who use https is skyrocketing, in no small part due to an initiative called Let’s Encrypt from Mozilla that is nudging people to switch to https.

Host: Nice.

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.

Host: Or maybe even more than slightly. You’re being modest. Because like you said, software is pervasive, and we’re all just sort of onboarding it into our lives.

Jonathan Protzenko: The trend is that software is going to be everywhere, and we’re 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’s just frightening. And you see these videos on YouTube of people taking remote control of a car. And it’s not just cars. It’s absolutely everywhere. And we’re just putting an enormous amount of trust into it.

Host: And we will come back, in a while, to what keeps you up at night. But let’s get happy for a minute.

Jonathan Protzenko: Yes.

Host: Let’s talk about the cool projects you’re working on, or have worked on, and one of them is a language, a functional language called F*.

Jonathan Protzenko: Yes.

Host: And I keep looking at it going, F#. It’s a star… And it’s a general-purpose functional programming language with effects aimed at program verification.

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’re a functionally-trained programmer, and you’re comfortable with ML, maybe you’ve written a bunch of OCaml in your life, here’s 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’s trying to cater to an audience of people who want to write software first. It’s not a tool that you would use to do a massive mathematical proof about some theorem, but it’s a tool that you would use to write your software in.

Host: Mm-hmm. Who’s your audience for this?

Jonathan Protzenko: It’s actually a good question… A good way to think about that is to look at who’s 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’ 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’re hoping to land into some existing software. And I’m sure we’ll talk about that soon.

Host: Yeah.

Jonathan Protzenko: What we’re hoping our audience is, is the “enlightened programmer.” Someone who is functionally trained, realizes that it’s great, but that there’s also something beyond that, and who’s willing to learn more and go further and deeper to actually convince themselves that their software is doing the right thing.

(music plays)

Host: So, another thing you’re working on is called KreMLin. I’m going to spell this: big K, little r, little e, big M, big L, little i, little n.

Jonathan Protzenko: Yes.

Host: Why the change-up in lowercase-uppercase?

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’s K and R and ML. And it’s kind of, you know, Kernighan and Ritchie meets ML. KreMLin is a compiler from F* to C, and here I’m tying together two things that we’ve 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’s 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.

Host: Speaking of acronyms, there’s another program you’re 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’s cool about this particular project?

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’ve mentioned that there’s a lot of software disasters, and, in my opinion, cryptography is one of the biggest ones, because it’s the underpinning of almost every secure software.

Host: Yeah.

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’s a library of cryptographic code, verified in F*, that comes out as a bunch of C code that people want to use. It’s been designed in collaboration with INRIA, the French Institute for Computer Science, and it’s already being used by several people.

Host: What’s the Venn diagram overlap with cryptographers and programming language people? There’s a lot of layers…

Jonathan Protzenko: Yes.

Host: …of people working on different things and then needing to get together and make it usable.

Jonathan Protzenko: There’s the cryptographers that design algorithms, and for me, that’s not my job. I know that algorithms exist. I know how they’re done, but I would have a really hard time creating a new one, so, don’t let me do that. That would be a disaster. There’s 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’s the consumers.

Host: Right.

Jonathan Protzenko: People who know that they need cryptography and are going to make use of it in their own software. And we’re 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’t design new code. What we design is verification methodologies that will allow us to show that either the existing code was broken, and we’ve found broken code, or that the existing code, or our code, is fine, and that we’re 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.

Host: The question just in my head when you said that is, how hard is this?

Jonathan Protzenko: So, there’s 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’re going to make it. It’s just a matter of throwing enough energy at it.

Host: Sure.

Jonathan Protzenko: But then once you’ve done that, actually going to meet people in software, telling them that you have something new and that, really, they should use it, it’s a different problem. And you need to build trust. You need to show them that you’re serious. You need to show them that your code makes sense. They’re probably not going to trust your very exotic verification methodology, and they’re 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.

Host: So, let’s talk about miTLS, a verified reference implementation of TLS. Why don’t you give us a little bit of history of that project? Who’s involved in it, what are you doing with it, and why do we need other organizations involved in order to tackle this program?

Jonathan Protzenko: Yes. So maybe I can say a little word about TLS first?

Host: Please.

Nonathan Protzenko: TLS is the protocol that you’re using when you’re connecting to a website over https. And I was talking about the cryptography being at the bottom of the stack. It’s 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’s two key properties that you want to establish when you have a channel with a third party: integrity and confidentiality. If you’re going, I don’t know, to a web search, confidentiality is making sure that no one can see what you’re looking for. And integrity is making sure that no one can tamper with your search while you’re receiving the results. So, the protocol that does this is called TLS, it was previously known as SSL.

Host: Right.

Jonathan Protzenko: It’s from the early 90s, originated at Netscape, and it’s the one you use every time you go to an https website. And so, miTLS is our attempt at making TLS more secure. It’s a fairly old project that started as a joint collaboration between Microsoft and INRIA.

Host: Hence the m-i… mi…

Jonathan Protzenko: Hence the name mi, Microsoft/INRIA TLS. We’ve gone through successive languages. The first version of miTLS was using a precursor of F* called F7, and we’ve 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’s the best way to design a tool, is to use it yourself…

Host: Yeah.

Jonathan Protzenko: …realize where you have shortcomings, and just try to fix it and improve it. So, it’s 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.

Host: So how much time do you spend trying to break your stuff?

Jonathan Protzenko: Well, theoretically, because it’s “verified,” it should never be…

Host: Right.

Jonathan Protzenko: …you know, broken. So that’s the theory. The practice is, we also try to find flaws.

Host: Yeah.

Jonathan Protzenko: And it’s an interesting question. There’s 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’t 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.

(music plays)

Host: Now let’s climb the big one. Be our digital Sherpa on Project Everest. Your goal – I’ll tee this up by, by saying – your goal is to build and deploy a verified https stack. Tell us all about Everest.

Jonathan Protzenko: So, Everest is, as you mentioned, our answer to that very sorry state of the world, which is that there hasn’t been a secure TLS implementation since the beginning of TLS. It’s always broken. So, what we set out to do, a few years ago, is to say, all right, we’ve 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 – we want to verify the entire stack – and also, in terms of impact – 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’s people at Carnegie Mellon University. There’s people at University of Edinburgh. And, of course, there’s our very close collaborators at INRIA. And so, what we’re doing is that, it’s 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’s 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.

Host: Yeah. All right, so Everest is a “goal mountain” for a lot of people who climb. Would you frame this as a “goal mountain” to summit for software engineering?

Jonathan Protzenko: I would say that, for us, yes, there’s that theorem that I was alluding to earlier that you get integrity and confidentiality, and that’s 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’re hoping to get there. And for us, it will also be a summit, because it’s a very wide-ranging and ambitious verification effort. One thing to realize is that we’re aiming for a very comprehensive set of software.

Host: Yeah.

Jonathan Protzenko: Just looking at the cryptography, we’re aiming to verify not just one algorithm, but entire families. And we’re 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’s a lot of work and it’s a lot of software. So, I think for us, we’re 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.

Host: So, what’s the relationship of miTLS with project Everest?

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’re, 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.

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’t necessarily historically been the case in industry with IP and competitive advantage issues. But lately, it seems there’s been a bit of a shift towards an embrace of a more open source mentality. So why do you think we’re seeing more “sharing” in the open source community among industry researchers, and why is that a good thing?

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’s two aspects to consider. The first one is, we just work better when it’s in the open. I find that it fosters better collaborations, more productive ideas, and generally a better atmosphere. It’s more motivating to know that you’re 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’t see your code, they’re just going to have a hard time convincing themselves that you’re secure. It’s a hard claim, right, that your software is secure? And you usually want to provide evidence for that.

Host: Sure.

Jonathan Protzenko: And if your code is closed source, then you’re going to have a hard time convincing other people that, really, you have secure software. So, it’s just better to do it in the open. That way everyone can go and see for themselves.

Host: Do you feel like you’ve 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’s proprietary. We don’t want anyone to see the source code. We don’t, you know…

Jonathan Protzenko: I have seen like a big change at Microsoft in just the four years that I’ve been here. I think I came in just at the right time when the mentalities were changing. And it’s been just getting better and better. I’ve found that I can use a Linux computer to do my day-to-day work and I can post on GitHub. I don’t have to worry about anything. And I think it’s just a reality of software development now, that so much software that you depend on is open source, that you’re 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’s a bug in it, fine. I’ll go and fix it. And it’s just a better way to work.

Host: And maybe somebody else has found your bug and helped you out there?

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’ve never met, who just come in, out of the blue, and submit improvements. And for us, that’s just…

Host: Thank you very much.

Jonathan Protzenko: It’s… yeah, we’re 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.

Host: I wish that would happen to me. Not software, but, you know…

(music plays)

Host: Jonathan, you’re working on security and verification in software, and you know the realities. We’ve talked a little bit about how scary that world is. And you’re 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’t discussed already? And what should we be aware of?

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’s Christmas season. People are going to get gifts, and I’m being bombarded with smart appliances. Every time I see one of these, I’m wondering, what are the consequences? And so far, it’s 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’s going to happen to these devices? Who’s going to maintain the software? Who’s even going to look at the software before it’s released and sold in millions? And it’s actually happening faster than we realize. And that’s 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’m very worried about these things, but I’m 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’t want broken software, or maybe there’s a regulation that says you can’t put on the market something that is obviously broken and that’s going to be actually a threat.

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… and unverified?

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’re 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’t 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’re getting a smart appliance, also think twice.

Host: But the problem is the binary option, you know? Do you agree? If you don’t, you can’t have the app. So, I hit agree.

Jonathan Protzenko: Yes, and for me, that’s the big question. Like, how do we create the social and economic dynamic for better software? And for me, that’s a big open question, because I’m just like you. I click on “agree” all the time. I couldn’t, like, go into existential mode whenever I install an app. So yes, I do click on agree. But where’s the incentive going to come from? For internet security, the interesting bit is that there’s a big economic incentive. If you’re broken, people are going to have to be paged on a weekend. There’s going to be, like, an incident response, a crisis. So, this resonates very well with the people that we work with. And that’s why they’re ready for better software. What is the equivalent for all these devices and the security of that software? I think that’s 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.

Host: Jonathan, tell us a bit about yourself, academically and otherwise. What’s your story? How did you come to be working in software engineering research at MSR? What don’t people know about Jonathan Protzenko?

Jonathan Protzenko: I did my PhD in France, at INRIA. And, as oftentimes happens at the end of one’s PhD, I was pretty fed up by the end of my dissertation writing, and I wasn’t 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’s how I arrived here. I didn’t believe in it at first. I didn’t think I would make it. I remember chatting with my advisor about it, being like, come on, Francois, they’re 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’ve been here for four years now.

Host: Prior to that, you did your PhD in France. Did you grow up in France?

Jonathan Protzenko: Yes, I did grow up in the France. I’m a pure product of the French system.

Host: Because you keep talking about existential moments. And so, it’s like, oh, Jean-Paul Sartre…. Uhmmm… Where are you from in France?

Jonathan Protzenko: I grew up in near Bordeaux. I stayed in Bordeaux for high school, and then did my Masters’ degree in Lyon, and then my PhD program in Paris.

Host: Nice. What’s your future goal? Aside from conquering Everest, where do you see yourself in five years?

Jonathan Protzenko: Oh, that’s a tough question, and you didn’t give me a heads up for that one.

Host: I didn’t.

Jonathan Protzenko: Otherwise I would have thought about it. I’m 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 “software matters” 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’s where the incentive to have better software is going to come from, from better software literacy. You’re 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’s, actually, an essential skill in the modern world. And maybe, eventually, people are aware enough that they’re going to start demanding better software, and hopefully it will be there.

Host: As we close, give us an idea – this will sound like a large question, but you can scale it down if you like – what’s 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’re doing?

Jonathan Protzenko: One thing to keep in mind is that we’re 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’s perspective. But it’s a lot of hard work, and it’s 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’t 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’s an enormous challenge, and any help would be most welcome.

(music plays)

Host: Jonathan Protzenko, thanks for joining us today. It’s been really fun.

Jonathan Protzenko: It’s been a pleasure. Thanks for having me.

To learn more about Dr. Jonathan Protzenko, and how researchers are trying to summit the verification mountain so you don’t have to, visit Microsoft.com/research