CppCast - Formal Verification

Episode Date: August 31, 2018

Rob and Jason are joined by Matt Fernandez from Intel Labs to discuss Formal Verification. Matthew Fernandez is a Research Scientist with Intel Labs. Matt began his programming career building Windows GUI applications and designing databases, before moving into operating system architecture and security. He has a PhD in formal verification of operating systems from the University of New South Wales in Australia, and worked with the Australian research group Data61. In the past, he has worked on compilers, device drivers and hypervisors, and now spends his days exploring new tools and techniques for functional correctness and verification of security properties. On the weekends, you can usually find Matt in a park with a good book, hunting for good coffee or helping a newbie debug their code. He hopes to avoid saying “monad” on this podcast. News C++17 in Detail now available Cross-language interfaces between C and C++ Spaceship Operator Matt Fernandez @wattsamata Links The sel4 Microkernel Isabelle - Generic Proof Assistant The Coq Proof Assistant Dafny - Microsoft language and program verifier Z3 Theorem Prover Sponsors Backtrace Patreon CppCast Patreon Hosts @robwirving @lefticus

Episode 165 of CppCast with guest Matt Fernandez, recorded August 29th, 2018. This episode of CppCast is sponsored by Backtrace, the turnkey debugging platform that helps you spend less time debugging and more time building. Get to the root cause quickly with detailed information at your fingertips. Start your free trial at backtrace.io slash cppcast. In this episode, we discuss potential issues with compiling C as C++. Then we talk to Matt Fernandez. Matt talks to us about formal verification of code. Welcome to episode 165 of CppCast, the first podcast for C++ developers by C++ developers. I'm your host, Rob Irving, joined by my co-host, Jason Turner.

Jason, how are you doing today? I'm doing pretty well, Rob. How are you doing? I'm doing okay. Getting closer and closer to CppCon. Any other news with you? Are you ready for your talks? Yeah, mostly. I ended up doing a bunch of research and programming for my second talk,

and it keeps being one of these things where I'm like, well, I have to stop working on the project for a couple of days so I can finish the talk. But we'll get there. And I think aside from that, we should probably mention there is some construction happening in your office right now. So if some noises come through, that's the problem today. Yeah, I apologize. I'm at my office today, and a new tenant is moving in downstairs, so they're doing a bunch of work. They're hanging up drywall and stuff down there. Hopefully it won't be too noisy.

Right. Yeah. Okay. Well, time for episode three to piece of feedback. This week we got a tweet from – actually, I think this was from Facebook. A post from Christopher saying, awesome, perfect timing. I'm currently teaching myself OpenGL and Vulkan, so I keep coming into contact with OpenCL and SQL. And some of these lectures I'm watching by Kronos.

Can't wait to listen in. Yeah, so I'm glad to hear he enjoyed the show. And we haven't talked much about Vulkan or OpenGL either. Maybe that would be a good topic for the show sometime. Yeah, perhaps. It's so far outside of my world. There was a graphics programming class that I didn't take at my university where I would have learned OpenGL.

And that's the last time I had any direct exposure to it was with a friend taking the class, basically. Right. I have some interaction with OpenGL, but I don't know a lot about it myself. I kind of just use a library that uses OpenGL. From what I understand, it's low-level enough that that's the preferable way of doing things. Pretty much, yeah. Well, we'd love to hear your thoughts about the show as well.

You can always reach out to us on facebook twitter or email us at feedback at speakcast.com and don't forget to leave us a review on itunes joining us today is matt fernandez matt is a research scientist with intel labs matt began his programming career building windows gui applications and design databases before moving into operating system architecture and security he has has a PhD in formal verification of operating systems from the University of New South Wales in Australia and worked with the Australian research group Data61. In the past, he has worked on compilers, device drivers, and hypervisors, and now spends his days exploring new tools and techniques for functional correctness and verification of security properties.

On the weekends, you can usually find Matt in a park with a good book, hunting for good coffee, or helping a newbie debug their code. He hopes to avoid saying monad on this podcast. Matt, welcome to the show. Thanks for having me. I guess you could say I'm a long-time listener, first-time caller. Very glad to be on. So I kind of want to ask you about Intel Labs,

but maybe I'll wait until the actual interview portion to do that. But I have to ask, hunting for good coffee, are you like a coffee snob, or do you just like drinking all of the coffee and you're just hunting for a cup of coffee that happens to be good? I think I was, amongst my social circle in Australia. I was sort of at the low end of the coffee drinkers. And that has translated when I moved to the U.S. to people thinking I'm obsessed with coffee, apparently.

So, yeah, I've been sort of trying to find good coffee in my area. And I found some places. Well, so I would not have assumed you were obsessed with coffee if you had not made a point of putting it in your bio. I think that's just from the reaction I've had from people around me that apparently I drink a lot of coffee. Oh, okay. So, okay, this is completely off topic for the podcast,

but I'm still just going to go ahead and ask it. What makes a good cup of coffee versus an average cup of coffee? Well, I think, like, to me, the coffee, there's no such thing as non-espresso coffee, really. I don't accept these other variants of coffee. So that already cuts out a whole swath of things that other people will class as coffee so uh espresso referring to the brewing process right yes so that's uh super hot water injected through tightly packed grounds yes then do you let's if i'm only just vague vaguely versed on coffee terminology but i think an americano is where you take that and add water to it to get it back to the consistency of what I would consider to be coffee. Yes.

Okay. So does an Americano qualify as coffee to you? Depending on how you make it, I guess so. But I would usually have just like a single shot of espresso in the morning and then maybe something like a latte in the afternoon. Okay. You're making me feel really bad for sipping a cup of, uh,

Keurig brewed coffee right now. Lowest common denominator of coffee, I guess. Well, I just did a bunch of training in Europe and every office that I went in had these machines that completely blew my mind that you could press a button and say, I want whatever an espresso.

And it was all one contained machine, which I'd never seen outside of Europe, where it ground the coffee beans and made the espresso and poured it right there for you and then ejected the beans into the next batch. And so I drank like four cups of coffee a day because I tried all of the different things that were possible, which is far too much coffee for me personally. Okay, well, Matt, we got a couple of news articles to discuss. Feel free to comment on any of these, and we'll start talking more about formal verification, okay?

Rob's done with the coffee conversation. Okay. So this first thing we have to discuss is about, I think I looked it up, and it was 20 episodes ago. We had Bartwamy Flipek. Hopefully I pronounced that close to correct. And he just released a book, self-publishing via LeanPub, and it's called C++17 in Detail.

I haven't had a chance to look at it myself, but I know we had a great conversation with him, and I know he's got a very, very good blog, so I'm sure there's a lot of great stuff in this book and uh he actually put together a discount code that i will be putting into the show notes for listeners do we know what the details of that discount code are i think it's like 20 off okay cool yeah yeah so uh definitely check out bartrami's book like i said c++ 17 in detail learn exciting features of the new standard sounds good yeah uh next thing we have is this article from yen's gustez blog and this is cross-language interfaces between c and c++ and i thought this was kind of interesting and he kind

of opens up the article saying how you should be very wary if you ever see some C code being compiled with the C++ compiler, which I know I've seen plenty of times. Plenty of times. Yes. And I didn't realize it was necessarily something to be wary of. But he highlights several things where the C and C++ standard are different. So there are reasons to be wary of that type of thing. This was quite interesting to me in that I've had to work in situations where I've had to write code compatible with C and C++,

and I think I've just defaulted to some common safe subset, but nothing that I've ever seen documented anywhere. I've just kind of guessed, oh, this thing is probably interpreted the same way. Yeah. And this article is also interesting to me, but I'm reading this like, you know, people say, well, I like C because it's so much more simple than C++. But you read this blog and I'm like,

wait, wait, what is this complex thing? How is that even allowed in C? So I go and look it up. Oh, that's a macro that refers to the underscore capital C complex keyword that was added at some point in C to allow complex data types. Like what? Like this language is not simple anymore it's got all kinds of random keywords built into it and it has ways of doing overloads that are weird extensions to the language like generics yeah the underscore generic thing that is come on now just allow overloads yeah i was surprised by a lot of this too i guess most of the times that i've seen c code you know being compiled with c++ it's probably an older c library that's not necessarily

keeping up to date with the changes within c which i guess is for the better because it's more portable i don't know yeah okay uh next thing i had is a article from simon brand on the spaceship operator and i thought this was a really good post that goes into some examples of you know kind of what makes the spaceship operator different from just implementing the old, you know, less than, greater than, and equal operators, and some of the neat things you can do with it. This has been quite a long time coming, right? Like, I've heard tales of the spaceship operator for, feels like years now.

Yeah, I think it was, I think, I think Herb presented on it one year ago at CBPCon. I don't know how long it's been in the works, though. But either way, I didn't realize that there were so many options for the return type that you could specify partial ordering, weak ordering, strong, weak equality, etc. I did not know that either. That actually surprised me that the compare three-way example they have is actually very verbose to actually write that out to implement one of those oh when you need to do the common comparison category aspect is that what you're referring to yeah well fortunately i i at least expect for most of my code where this would

come up i'll just do the equals default thing and let the compiler take care of the details. It's a little surprising that it has taken till C++20 to get this when I think several other languages have this already and have had it for a while. And I know it's like a pain point I have regularly implementing many different comparators. I think in most non-compiled languages, it's easy to do because you can just do a runtime lookup to see what kind of comparison is available. And this might have just taken maybe just to have that threshold where we finally agreed, okay, there's enough pain here, and we now know how we can do it in a way that the compiler can do something efficient with it at compile time. I don't know, honestly. I don't know if it will make you happy to hear, but I think Haskell has had this for quite a while.

Right, and Haskell is a compiled language. Right. Right. Garbage-collected compiled language, I think. Yeah, that might give them some more leeway in terms of, I mean, they don't necessarily want the blazing fast efficiency yeah honestly i i don't know i i i find personally like i occasionally implement a less than when i want something that can be put into an ordered container but otherwise for just the type of programming i've ended up doing it hasn't come up very often for me so So I haven't spent a lot of time thinking about it. Okay. Well, let's start talking about, uh, formal verification, Matt, you know,

we've been making the show for, what is it, Jason, like over three years now. And we've probably been asked maybe a half dozen times or so to, uh, talk about formal verification. And Jason, I know absolutely nothing about it, but,'s why we have you to explain what formal verification is. Yeah, so I can kind of start at a very high level of broad description of what it is. So it's basically using logic to prove properties about systems. So this isn't necessarily related to computers or software. You might be proving a property about some abstract math system. But the area that C++ programmers are probably most interested in is the use of C++ to do

formal verification as well as proving properties about a C++ program, which is sort of two different sides of a coin here. And so a kind of rising area now is using computers as an assistant when you're doing proofs about an artifact. So the idea is you have some piece of software that acts as some sort of verification framework where you are explaining to that tool why your system has the properties it has. And that tool is doing this checking for you, saying like, yes, the argument you've given me does actually hold. So typical way you would do this is to construct an abstract model or a specification of your system. So some kind of limited, restricted view of what your program or other system that you're attempting to model is actually doing. And then you want to do two different things.

You want to convince yourself that certain properties hold about that system and convince yourself that your abstraction actually matches the real world, what's going on there. And so this is where computer-aided verification comes in, where there are a lot of automated tools that have been improving dramatically over the past few years to aid with this. And you can kind of think about this process of abstraction and modeling your system as kind of similar to object-oriented programming.

Like you might build a class to represent a person or something. You build some class that is some abstraction of an object in the real world, and you want certain things to be true of that class that are also true of the real-world object. So in theory, you're going through the same kind of patterns of thinking when doing object-oriented software. The overall goal of the whole exercise when doing it with a piece of software or hardware

is to give some sort of convincing evidence for its correctness and absence of bugs involved. Okay. You look more confused than ever. Oh, I'm just thinking. So you want to prove the properties of a system to make sure that it matches your expectations, assumptions, and what the real world, perhaps if you're doing real world modeling of an object.

Okay. My first thought when hearing you describe this was I'm thinking there has to be a piece to this, bringing it to my world, for how C++ or for how optimizers work, optimizing compilers work. If it can prove that a certain range of values is the only thing that's going to be passed into this function, then it can do something different. Yes. So they're effectively doing a class of these problems internally to do the kind of transformations you do with the compiler optimization. The compiler needs to do some sort of, it's effectively like a limited proof internally that the transformation they're doing is valid.

And they might even do this ahead of time statically. If you have some rule for what that transformation does and you can prove that's always safe, then you know you can apply it. And there's also, I was going to talk about this a bit later, but part of this also involves type checking within the compiler, particularly in the face of things like auto now. You're supplying the compiler with something where you're saying, I'm sure you can figure out the types for me. And your compiler has to do some, in the worst case, quite complicated reasoning to figure out what the types are of the variables you've given it um so are you familiar with partially typed languages like typescript as well uh not so much okay i was just thinking if i was wondering how partial typing might fall into your uh description that the type system itself is related. Does it work similarly to something like Python with dynamic types? With partial typing, you can be dynamic up to a point and then say,

except this function, this actually takes a double. I actually care here. And then wherever you use typing, it has to prove things about the system to make sure that you are using the correct types, you know, below a certain point or whatever. So that would most likely be doing something like this internally as well, constructing some sort of chain of evidence for why this is the case, why we can guarantee that this is not going to cause some sort of runtime type mismatch. Okay. So would you mind giving like a specific example outside of the compiler world like maybe how the requirements are specified and how this tool actually or how this concept actually

works as you described as an assistant uh when working on proofs in terms of verifying a piece of software i don't know like what's the best example that you could, like, what's the first example that comes to mind, I guess, whether software verification or a mathematical proof verification or something? For programmers, I think the most relatable thing, if you've been through some sort of computer science course, is the idea of pre- and post-conditions for a function, which is sort of informally what you're thinking

about when you're writing code typically. Like, this is what I'm assuming when I enter this function. This is what I'm actually guaranteeing at the end of it. And so you might try and state that kind of property to one of these computer-aided tools. And then you try and reason over that function's body and explain to the tool this is why this thing holds which there are various ways of doing this and sort of a spectrum from automated and not very expressive through to a lot of manual work but quite a lot of power in what you can prove okay so the kind of um the example you gave before of what the compiler is doing internally is a very automated process, right? Like your compiler never comes back to you and says, tell me why these types are okay.

It basically compiles your code or says, I failed. So this might be skipping ahead a little bit, but what you were just describing, it sounds a lot like C++ contracts. Is that right? The pre-imposed conditions? Yeah, to some extent. I haven't closely monitored contracts, but they're actually intended to be checked at compile time, right?

The contracts? They can be checked at compile time, or if it's all purely runtime values, then it would have to do runtime instrumentation. Right, that's what I was wondering, that you would be able to write a contract that's impossible to check at compile time. I believe that would be true, yes. Do you get some, I mean, I don't know if they've been completely finalized yet, but it almost seems like you would want some constexpr equivalent of saying, sometimes here's a contract that I want you to fail if you can't do it compile time. Yeah, as far as I know, that's not an option, but I do know that the final wording is still being worked on as well. And I also know that I don't fully understand every aspect of what's gone into the contracts proposal so far. Yeah, I haven't really, I was kind of hoping to just sort of learn about it thoroughly once it

stabilized, rather than tracking it closely. I feel like if I could maybe try to relate contracts, what I know of contracts from what I have understood about what you have said so far, that perhaps if you had a function that had a post condition saying the result expect a value that is always less than three that perhaps the compiler could prove something about that function that result going to the other function call and be able to do some sort of optimization or proof or something give you a warning if they don't match or something like right by chaining these things together yeah and that's sort of in practice what a compiler is doing internally. It has, I think you mentioned before, these kind of range-based optimizations where it knows some subset of values of a type that your variable can actually take on at that point, and it can use that to do certain optimizations.

So outside of the programming world, then, you have used formal verification. If I got your degree right, you actually have a PhD with formal verification of operating systems. That's still within the computing world. So what kind of work did you do with your PhD research? So that was proving the correctness of a collection of systems level C code, basically. So that was very much this style of verification, reasoning about pre and post conditions and the way you can chain these things together. And a lot of what I worked on was a code generator for part of this system as well. So it was not only writing these proofs of this code, but also teaching this generator how to generate proofs alongside the code it was

generating. So the kind of verification we were doing there was with a tool called an interactive theorem prover. And it's a much more, I guess you could say much less automated environment in some ways, but much more powerful in what you can prove. So it looks more like an IDE when you're using it. And what you're writing is almost like a program explaining to this kind of core of the theorem prover why you believe this property to be true. And so what you write is actually much more like a math proof, like a set of steps of kind of inferences you're taking. And at each step, the interactive theorem prover is saying, yes,

that step holds, like you've made a step that's valid here. So you can sort of get to the bottom of one of these. And what you've done is essentially similar to a pencil and paper proof, but you have this piece of software assisting you at be evaluated on each release of the operating system to prove that you are still meeting the requirements you thought you were? Yeah, so you can sort of rerun these proofs through this interactive theorem prover to confirm they still hold. And we actually had some infrastructure for importing C code into this environment as well. So if you change the C code, you wouldn't have to sort of transliterate that into something in the theorem prover.

The theorem prover would just see the new C code, and if the old proof you'd written didn't hold on the new code, it would say, hey, this doesn't work. You need to fix this up. So... No, sorry, go ahead. Oh, sorry. So at a high level,

the properties we were trying to prove were often um security related uh properties about the system so things like um separation between two processes that run on top of the system so uh confidentiality and integrity guarantees between two different processes okay trying to think what that would actually look like, and I realize I don't have enough experience with operating systems to have a good example in my mind. I think it's kind of doubly counterintuitive in that the process is very foreign for a lot of programmers and it's also um a lot of the properties we were looking at were things that people just sort of assume are true of common

operating systems so like people assume because they're running in a different address space they're nicely isolated from another process on the system right that isn't necessarily the case there are are other avenues you have. I mean, sometimes you explicitly have something like shared memory where you can communicate with another process. But often, even if you think you're isolated from somebody else, you're not exactly. And there's all sorts of subtle information flows there as well, like the timing of when you're scheduled versus somebody else. How would that come into play?

So if you're running on a system in isolation and you can observe some source of time, like the timestamp counter or something, if you're reading that, you can tell if the operating system context switched away from you to somebody else and then back to you. And based on those switches and the timing, sometimes you can conclude what the other person was doing as well. Interesting. So for the most part, you actually don't care about this in a desktop environment, right?

Like if Word can learn what your email client is doing, who cares, really? But in other more restricted environments so you might have like some secure military computer or something where you're running like software where you really want to keep isolated isolated to the extent that it would be as if it was on two physically separate computers providing those kind of guarantees on a single computer is actually pretty complicated. So were you able to, since this is the specific example you brought up, were you able to prove that in this operating system example that you're doing research on, that the two processes were in

fact running in isolated environments? Yeah, so this is actually getting a bit beyond the work I did to some other colleagues at the Research Institute I was at. This was Data61. And I should mention that the operating system I'm talking about is SEL4, which people might have heard of. Okay. And so it has some very strong properties proven about it, but it's also an operating system that's designed quite differently

to most desktop operating systems because it's sort of built from the ground up based on this foundation of strong isolation between different processes executing on top. Okay. Well, is there anything from that research that you thought was true that you then ended up with the tools being able to prove was in fact false and you needed to fix or they needed to fix all the time okay was there looking for a good story here for how the how the tools helped you with your work in this regard yeah sure

um so an interesting facet of this when working in a language like c is that there are a lot of just generic properties you want to know about a c program that aren't specific to an operating system or to that case so like for example you want to know you never dereference a null pointer or you never cause some kind of undefined behavior. And it turns out the categories of undefined behavior are pretty hard for a human to keep in their head at once. So I would say the number of times I wrote something that I thought was acceptable

and it turned out to have some subtle undefined behavior, which the theorem prover then revealed to me were countless this uh all sorts of um when I was early on in this project one of the things I stumbled across was uh shifting one uh left by 31 on a 32-bit platform because you end up shifting it into the sign bit, which is technically undefined. And then once I realized rules like that, I was like, oh, okay, that's so obvious. Don't do that. And then I started looking around at other code bases

and the number of C and C++ code bases that do that idiom are countless. Um, so you start, I think it's almost a very, uh, demoralizing exercise in some ways that, uh, when you're trying to prove the correctness of a C program,

it's quite hard. And for good reasons, because you, you're suddenly all your own mistakes are revealed to you. And then you start looking around and you realize, oh, almost every C program is broken. Really? It's one of those moments where you realize, ah, the whole world is on fire all the time. That's great. Yeah, that's definitely demoralizing. So the tool is able to tell you, you put in some sort of assumption or something, you say, well, I know that I am not invoking signed integer math undivined behavior here. And the tool says, well, actually, you might be doing a left shift by 31, and your assumption is false.

Yeah, so part of that was actually some previous work another researcher had done there, which was basically teaching the theorem prover all the rules of C, according to, I think this was C99 at the time. So basically teaching it what is allowed within the standard. And when you tried to do a proof about some C code, the theorem prover would say, okay, justify to me why you didn't trigger these cases of undefined behavior, which it looks like your code might. So you would have to say, okay, this is why I know this pointer isn't null before I dereference it. This is why I know this pointer isn't null before I dereference it.

This is why I know this pointer arithmetic doesn't go out of bounds, etc., etc. Wow. All right. I wanted to interrupt this discussion for just a moment to bring you a word from our sponsors. Backtrace is a debugging platform that improves software quality, reliability, and support by bringing deep introspection and automation throughout the software error lifecycle. Spend less time debugging and reduce your mean time to resolution by using the first and only platform to combine symbolic debugging, error aggregation, and state analysis. At the time of error, Bactres jumps into action, capturing detailed dumps of application and environmental state. Bactres then performs automated analysis on

process memory and executable code to classify errors and highlight important signals such as heap corruption, malware, and much more. This data is aggregated and archived in a centralized object store, providing your team a single system to investigate errors across your environments. Join industry leaders like Fastly,

Message Systems, and AppNexus that use Backtrace to modernize their debugging infrastructure. It's free to try, minutes to set up, fully featured with no commitment necessary. Check them out at backtrace.io.cppcast. Can you tell us a little bit more about the tools that are used for formal verification?

Are these tools accessible to average developers? Yeah, sure. We sort of dived in at the deep end there in that an interactive theorem prover is probably, like on that spectrum I mentioned, from automation to expressiveness. A theorem prover is right up in terms, like a low level of automation,

but highly expressive in terms of what you can do. And it has a very steep learning curve, I would say, because of that. But stepping back from that, there's a lot of automated constraint solvers, essentially, which are similar to what Jason was talking about with what a compiler is doing internally. In fact, a lot of compilers these days don't actually contain any logic to solve these problems internally. They form some description of a problem

describing the optimization they're trying to make, and they hand it off to one of these constraint solvers. And these are like completely automated tools, basically. You plug in some formula and you say, here is something that I believe you either can find variables to satisfy this formula, like to make this true, or you cannot find values and variables to make this true. And the solver will sort of churn away and come back to you and say either you were correct or or you were false and here's a counter example of the situation

and these tools have actually gained a lot of adoption in different areas and it's a little bit surprising because the problem they're working on is np complete or like worse in some cases and so for a long time people intuitively thought well there's no point looking at that area like that problem is just not something we can computationally tackle but it turns out when you try and build these systems it's very rare that anyone actually hits one of these like really computationally intractable situations. So in practice, these solvers are actually very successful at solving a class of problems

that we shouldn't be able to address this way theoretically. Interesting. So some people have done, I think there's some Microsoft work on integrating these into program annotations for C sharp, I think, where you can work in an environment where you write properties about your functions and about other state in your program within your IDE itself. And your IDE calls out to one of these solvers to try and satisfy these properties you've written. Do you know of any tools that work with C++ like this,

or know the rules of C++ like you explained the interactive theorem solver? There's been some efforts to kind of formalize the rules of C++, but I think people have sort of shied away from that a little bit because C++ feels vastly more complicated than most other languages. It's just, it's really like, it has taken a superset of every other language's features. So formalizing exactly, like even writing just a C++ parser

is an undertaking that most of us don't want to do. And particularly once you get into things like some complicated template instantiations and SphinI or SphinI, however you pronounce that, these kinds of tricks where you, uh, get a particular template instantiation by some sort of resolution, formalizing the rules for that are, it's a pretty complicated task.

Um, and I think there's also a mindset thing going on there that a lot of the people doing this work are, um, mindset thing going on there that a lot of the people doing this work are much more in the camp of functional programming languages than these low-level imperative languages. On the flip side of that, though, a lot of these tools are written in C++ for performance. So allow them to have nice C++is to interact with them as a library and um even some of the higher level tools they are written in nice pretty uh mathematically

pure languages and the deeper you go down the stack you eventually hit c++ us so how do they prove that their theorem provers are correct ah good question yes i think that's like the deeper somebody goes into this they always come to that question eventually who proves the prover um so most of them that i'm aware of are based around this idea of having this sort of minimal trusted core. Um, so there is some, there's some code that's trusted to judge whether the steps you make in a proof are correctly justified or not. And that code, if it has bugs could let you prove something incorrect, but that code is sort of kept as small as possible so that it could be manually audited. And then the verification environment as a whole is probably quite a lot of code, but a lot of it is, all it does is kind of call in to this kernel which makes these critical

decisions. So in theory you only have to trust a small, minimal core. Okay. Which is sort of the same way we do a lot of other systems, right? Like the principle of least privilege and trying to keep things small and simple. Right. So we talked a lot about your background with this and operating systems. What other industries are you aware of that heavily make use of formal verification tools? These days, it's getting broader and broader.

So traditionally, it has been a lot of safety and security-critical industries, so like aviation and military systems have used it a lot. In more recent times, communications vendors have started using verification. So there's some interest in using verification for embedded systems like mobile phones and other similar, these days, things that we call the Internet of Things. And the pull there, I mean, stepping back, the demand from aviation and the military in those kind of environments,

it's because if the thing goes wrong, people die. Like it's a very easy argument why you want to apply all the techniques you have to guarantee correctness. When it comes to something like an embedded device, often it's because you have no path to servicing that thing. So a bug in the field is going to brick the device or put somebody's security at risk, potentially. So in that case, it's more about that lack of serviceability.

And then lately, what we're seeing as well is a lot of automotive companies as well, particularly as we move into these advanced driving assistance systems and self-driving cars and whatnot. The consensus basically seems to be we will never be able to simulate enough hours of driving in a lab and in controlled circumstances to actually be a representative fraction of the real world driving that one of these cars will get so some people are pushing for verification being the only way to guarantee that these things won't kill people on the roads um and then i mean it's basically the same motivation as for aviation right that if one of these things goes wrong in a systematic way that's like lives being lost it seems like like i'm having a problem with the

mental leap of well i've proven that this code doesn't have any memory leaks because I know that anything that is allocated is freed from, I prove that this code can accurately assess whether or not there's a human in front of the car. Yeah, that's again a very precise interesting question there so you're getting into the distinction of things like functional correctness and safety

properties in these situations where a sort of correct memory management and a lack of seg faults in these things is sort of like table stakes for this, right? Like, if you prove that that's something you want, but that really doesn't get you to the property you actually want,

which is the car's visual recognition system actually recognizes a person. Right. But if you can't show these properties, anything else you're trying to prove can be invalidated by the fact that you screwed up memory somehow. Okay, yeah, that's a good point. So as a first step, you're sort of trying to prove functional correctness about these systems,

which is often just, I don't do anything obviously wrong, that I don't violate the language standards. And I don't have some bug in there that is like objectively a bug as opposed to a bug of something where we mismatch the specification and then beyond that um because a lot of these driving systems now are also based on neural networks and machine learning there's a pretty active area of research which i wouldn't say there's really agreement on how to do this yet but a big open problem is if we have a trained neural network how do you verify that it actually learned what it was supposed to like there's very it's very new sort of area of how do we how do we extract what it was that network has actually learned wow okay so i

feel like at some point i should tell you a happy story rather than all this the whole world is going to burn yes go ahead do you have a happy story i'm hoping yeah didn't sorry um oh well people are working on these things. Oh, that's good. That makes me feel better. Okay, I actually want to come back to maybe, I think, a smaller example, because self-driving cars, I feel like that's just a huge problem. But you said proving the status of Internet of Things devices. And, you know, I have, for example, my nephew visits and comments how,

oh, other people in his family have, like, smart light bulbs throughout their house. And I'm like, you know, I'm just not interested in my light bulb participating in a botnet trying to take down, you know, the New York Times website, which then is, you know,

a 30-minute discussion about why that would even be possible. If there are people actually selling smart light bulbs that are provably secure in some way, then I might be interested in actually buying one of those. So do you have any good stories about how formal verification is helping Internet of Things, since you mentioned Internet of Things? I don't know anyone selling a verified light bulb.

But I think it's sort of an area that companies are waking up to now, where for a long time it's been sort of like almost ship this and forget. Like, get it working, don't really think about security, sell this thing. And now, as you said, we see all these things being taken over by botnets. And I think what it's really going to take is some sort of liability for the companies. Like you need to have some consequences for the fact that you sold this insecure device that is now DDoSing whoever. And people are sort of thinking about this area. Like, the people I talk to are sort of exploring, can verification help us here?

But I think to see, like, some real movement on it, we basically need consequences for companies who sell known insecure or not even known insecure devices but just something where they didn't do due diligence on what they should have. So after all the lawsuits come, the tools are there waiting and ready?

Yes. Okay, that's good. It's a great marketing campaign. Just wait for the next big attack. Over the past decade or so, unit testing has become a lot more widespread. It seems like maybe this is going to be the next step in having even more trust in our software. Do you think that's an accurate statement? Yeah, I think it's, I mean, the people who are usually asking me about verification are

people who are testing pretty heavily already. Like to get to the level of thinking about doing verification, you've usually explored a lot of the low hanging fruit of how do I get some correctness guarantees? And the first question they always ask is, can I stop testing if I do this? And the answer is, well, no. Testing still demonstrates your system actually can do the specific things you want it to do.

Right. And it definitely, there's kind of one part of verification which has seen a pretty good uptake in that sense. A lot of static analysis tools are now pretty easy to use. So there's quite a few of those actually that understand C and C++ and are very good at doing a sort of ahead-of-time interpretation of what would this code do if I ran it, what would be the problems here. So they're getting to the point where you can pretty easily integrate those into continuous integration or whatever other testing environment

you have set up. So you put static analysis tools in the same realm as formal verification. Yeah, I mean, it's kind of on the edge there where I don't think there's really a hard boundary of what is verification and what isn't. I think most people probably wouldn who are interested in applying verification. And that's sort of their first foray into the area. I feel like my takeaway from our conversation, which we're kind of starting to run out of time here, is contracts and their ability for them to cooperate nicely with static analysis which is a great step in this direction for c++ yeah um if they kill it a nice synergy yeah i think so but i'd have to get more familiar with contracts to right to come into think yeah well at the moment contracts being the only mechanism that we will have for specifying requirements right yeah if it's that

or nothing then contracts do look pretty good right i actually wanted to ask you something else about the direction of c++. Jason, you're always on with constexpr, all the things, and the trend with compilers is to notice more and more oh, I can execute this thing at compile time, I'm going to do this aggressively. So a couple of verification tools I work on, they work by analyzing a model and generating a C++ program

that is your checker that you then run, and so the program it generates is this piece of C++ code that doesn't really do any relevant I.O. or anything. It basically does computation, and I really don't want that to run at compile time do any relevant I.O. or anything, it basically does computation. And I really don't want that to run at compile time because it's very runtime and memory intensive. So if my compiler gets clever enough to spot, oh, I can interpret this code at

compile time, that would not be good for me. So I almost want the opposite of constexpr to say, I know you think you can run this at compile time, but this is expensive. Trust me, don't run it right now. loops, something that would have already unrolled the loop because of your optimization flags. And now that the loop is unrolled, it says, oh, I can do constant folding and fold the stuff away, and it just goes away. If you actually use constexpr, then they all have escape patches that say, well, I have executed so many statements, I am going to give up and say this can't be done at constexpr time and effectively trying to detect that it doesn't terminate. So you could still use constexpr, but set those thresholds very low manually if you wanted to. But I will say for the sake of our conversation

about formal verification, constexpr does not does not well anything that happens at compile time is not allowed to invoke undefined behavior so you can actually find very interesting things about your program when you get a compile time failure because you did something like a signed integer overflow at compile time and your constexpr code so it will actually sort of instrument its interpretation of your code with checks for whether you're doing anything undefined and the what exactly exactly each compiler detects and actually aborts at compile time because it detected undefined behavior is definitely dependent on the compiler but both both Clang and GCC will do interesting things if you try to force something like an integer overflow

at compile time, constexpr, to actually see the error that you get back from the compiler. It's pretty cool. That is quite interesting because a not very well-maintained compiler I was using recently, I discovered if you divide by the literal zero, the compiler would do that and fault.

It would constant fault. That probably shouldn't happen. I can't honestly say I'm shocked, but, you know, yeah. I've never tried that actually I'll have to give that a go and see what what happens anyhow okay well Matt is there anything else you

wanted to go over before we let you go today I think I'd be remiss without mentioning that there's a formally verified C compiler that's available it's called CompCert is it written in Haskell or one verified C compiler that's available. It's called CompCert. Okay. Is it written in Haskell or one of the languages that's easier to verify?

It's actually written in a theorem prover. Okay. There's this theorem prover COQ. So they've written basically the logic and the proofs about the code in this theorem prover, and then that theorem prover has a mechanism to extract that code to OCaml, I think. And then they compile that. But yeah, it's a very impressive piece of work.

And I think there have been some studies on compiler fuzzing since then, which have looked at a whole range of compilers and it's the only one they can't find bugs in. Yeah, I don't know. I expect most compilers would fall down pretty quick if you fuzzed the input into them. I mean, I'm sure they try not to, but at the same time I've seen enough segfaults from compilers,

particularly unreleased versions of them, you know, like if I'm running Trunk or whatever. But anyhow. Okay, well we'll have to put a link to that in the show notes. Thanks for mentioning it. No problem. Okay, well it's been great having you on the show today, Matt.

It's been great being here. Thank you for having me. Thanks for the opportunity. Thanks for coming on, it's great. Thanks so much for listening in as we chat about C++. We'd love to hear what you think of the podcast. Please let us know if we're discussing the stuff you're interested in, or if you have a suggestion for a topic, we'd love to hear about that too. You can email all your thoughts to feedback at cppcast.com.

We'd also appreciate if you can like CppCast on Facebook and follow CppCast on Twitter. You can also follow me at Rob W. Irving and Jason at Lefticus on Twitter. We'd also like to thank all our patrons who help support the show through Patreon. If you'd like to support us on Patreon, you can do so at patreon.com slash cppcast. And of course, you can find all that info and the show notes on the podcast website at cppcast.com. Theme music for this episode is provided by podcastthemes.com.