[00:00.000 --> 00:02.540]  I didn't realize the previous talk was going to be about jet engines.
[00:02.680 --> 00:03.540]  That's a nice lineup.
[00:05.400 --> 00:14.400]  There's this story about a rocket spaceship that exploded 30 seconds after launch because of a software bug.
[00:15.120 --> 00:17.280]  And I found that very, very interesting.
[00:17.460 --> 00:18.980]  I've been thinking about that a lot.
[00:18.980 --> 00:23.100]  And I realized there's a lot of lessons to learn from that story.
[00:24.060 --> 00:28.880]  So we're going to talk about the story and we're going to talk about some of the lessons from it.
[00:30.720 --> 00:34.720]  First, a little bit of context to how I got to that story.
[00:37.320 --> 00:38.960]  I used to work as a pen tester.
[00:39.240 --> 00:45.520]  So you use tools like Nmap, Burp Suite, to find bugs in software, mostly web applications.
[00:46.060 --> 00:48.040]  So my background is finding bugs.
[00:49.020 --> 00:52.740]  Which really means you're generating PDFs.
[00:52.880 --> 00:56.720]  You work at the PDF factory and you're delivering PDFs over and over every year.
[00:56.720 --> 00:59.300]  And that gets a little bit repetitive.
[00:59.800 --> 01:03.640]  Especially when you work for a company, you give them your pen test report.
[01:03.800 --> 01:06.340]  The next year come, it's the same findings.
[01:06.760 --> 01:07.480]  Nothing changed.
[01:07.820 --> 01:08.380]  No one cares.
[01:09.160 --> 01:14.460]  So I thought there's probably more to security than just finding bugs or writing PDFs.
[01:15.860 --> 01:20.760]  So I started realizing there's like many different fields.
[01:21.360 --> 01:25.720]  Like this tweet shows like there's a whole aspect to just even detection, right?
[01:25.800 --> 01:29.480]  Like you can find the bugs, but can you really detect intrusion real time?
[01:30.060 --> 01:32.120]  The whole logging by itself was a whole field.
[01:32.280 --> 01:33.500]  Like there's a lot to security.
[01:35.320 --> 01:39.560]  So I started trying to learn about software security in theory.
[01:40.640 --> 01:42.420]  And there's this...
[01:43.440 --> 01:45.900]  Well, I mean, when someone says let's make a product more secure.
[01:46.020 --> 01:46.920]  What does that mean?
[01:47.080 --> 01:48.800]  That's kind of broad.
[01:49.000 --> 01:49.260]  That's vague.
[01:49.420 --> 01:50.620]  There's a lot that goes into it.
[01:50.700 --> 01:52.920]  And there's this really interesting book by Kelly Shortridge.
[01:53.180 --> 01:56.540]  Some of the themes here are going to recur over the presentation.
[01:57.440 --> 02:02.540]  But the main idea is that security is a subset of resilience.
[02:03.580 --> 02:07.020]  And resilience is an emergent property of the system as a whole.
[02:07.220 --> 02:10.580]  So it's not just about specific components that you're assessing, right?
[02:10.720 --> 02:11.880]  All of it comes together.
[02:13.500 --> 02:18.680]  And that, you know, systems can be complex and just hard to think and communicate about software.
[02:19.760 --> 02:23.020]  So as a start at a very high level, you have standards, right?
[02:23.600 --> 02:24.780]  That just shows intent.
[02:25.640 --> 02:31.640]  Every standard and procedure and guideline, like, it's lessons from different failures.
[02:31.840 --> 02:34.180]  There's a reason we do things in standards.
[02:36.200 --> 02:38.160]  It started decades ago, right?
[02:38.220 --> 02:39.840]  Like, there's the orange book from the DOD.
[02:39.980 --> 02:42.440]  I've been trying to find a physical copy of it, if anyone has one.
[02:44.040 --> 02:49.160]  And another interesting aspect that I learned is that I used to think that security was a technical problem.
[02:49.200 --> 02:53.340]  But then I realized, you know, actually, the human part of it is very important as well, right?
[02:53.340 --> 02:57.120]  When you're trying to make software more secure, you're working with engineers.
[02:57.360 --> 02:58.740]  And they have their own preferences.
[03:00.020 --> 03:01.320]  Psychological safety is important.
[03:01.560 --> 03:04.960]  Making sure that they're all comfortable with the decisions we're making.
[03:04.960 --> 03:07.060]  All of that really important.
[03:07.620 --> 03:08.740]  Otherwise, they just ignore you.
[03:11.660 --> 03:15.100]  So some of the things that go into security engineering, there's many tools.
[03:15.300 --> 03:16.280]  There's, like, static analysis.
[03:16.440 --> 03:18.020]  You look at the code line by line.
[03:18.120 --> 03:18.880]  That's one aspect of it.
[03:18.940 --> 03:20.080]  There's dynamic analysis.
[03:20.080 --> 03:22.100]  You're testing something that's running.
[03:23.020 --> 03:25.000]  You're trying to find secrets in code.
[03:25.400 --> 03:27.640]  Secure coding trainings is also a part of it.
[03:27.900 --> 03:28.600]  Threat modeling.
[03:29.300 --> 03:30.400]  Many different aspects.
[03:30.580 --> 03:33.980]  So something happened February this year.
[03:36.240 --> 03:42.060]  So early this year, I had made this image for a blog post I wrote.
[03:42.060 --> 03:43.220]  I'm not gonna explain all of it.
[03:43.340 --> 03:52.800]  But basically, what happened early this year is the White House released a white paper about software security, basically.
[03:54.020 --> 03:56.300]  And the outline is interesting to me.
[03:56.960 --> 04:10.060]  So, first, the reason they released it or, like, part of it was that they said that the current ecosystem did not sufficiently incentivize the investments required to secure cyberspace.
[04:11.220 --> 04:11.780]  Interesting.
[04:12.220 --> 04:26.280]  And I was impressed that the, like, official government communications was using the word cyberspace, a word coined in science fiction by, like, this is the okay.
[04:26.300 --> 04:28.060]  The opening of Neuromancer, William Gibson.
[04:28.980 --> 04:33.280]  But the outline of the paper was that these three points.
[04:33.420 --> 04:34.660]  One, they talk about hardware.
[04:34.920 --> 04:37.240]  So hardware is not that interesting to me personally.
[04:37.440 --> 04:38.620]  And I'll tell you why.
[04:39.160 --> 04:42.420]  When you talk about, like, spaceships, yes, you own the hardware.
[04:42.960 --> 04:44.640]  So it's perfectly valid.
[04:45.380 --> 04:52.700]  But a lot of us work in securing consumer software, which runs on hardware you don't own, right?
[04:53.320 --> 04:56.440]  Sure, you might own, like, the warehouse or something.
[04:56.640 --> 05:03.780]  But, like, if you're writing a password manager or a video game, usually it's running on software, on hardware you don't own.
[05:03.780 --> 05:07.080]  And you want to support a broad range of hardware.
[05:07.340 --> 05:09.280]  So I'm not going to talk about this too much.
[05:09.540 --> 05:11.480]  The other one is formal methods.
[05:11.780 --> 05:13.080]  That's very interesting to me.
[05:15.400 --> 05:20.460]  Of which, specifically, formal verification is an interesting recommendation for them to make.
[05:21.160 --> 05:27.760]  So, formal verification, like, we're mathematically proving that that program behaves as intended, as we wanted to design it.
[05:28.580 --> 05:32.900]  And I'm curious, who here uses formal verification in a production environment?
[05:35.200 --> 05:36.320]  More than I expected.
[05:36.980 --> 05:39.040]  Do you work at Amazon or Microsoft?
[05:39.040 --> 05:39.800]  No?
[05:39.980 --> 05:40.860]  Okay, okay, okay.
[05:41.020 --> 05:41.760]  That's interesting.
[05:42.060 --> 05:43.440]  Maybe I'll talk to you after.
[05:43.880 --> 05:48.560]  So it's rare to find people that actually use formal verification in a production environment.
[05:49.580 --> 05:50.400]  Because it's hard.
[05:51.680 --> 05:53.960]  So when I was looking into it, like, who actually uses it?
[05:54.080 --> 05:57.860]  Amazon does it for their TLS implementation called S2N.
[05:58.520 --> 06:03.420]  They have this interesting paper where they simplify the aspects of it and verify some components.
[06:03.420 --> 06:06.020]  And they have, like, a verification that runs in CI-CD.
[06:07.100 --> 06:08.660]  So it's possible to do.
[06:09.020 --> 06:10.200]  It's very interesting to do.
[06:10.360 --> 06:11.320]  But it's very hard.
[06:11.340 --> 06:12.100]  And it's very costly.
[06:12.240 --> 06:16.180]  Like, there was a team working for a year to get this up and running.
[06:18.760 --> 06:20.280]  And there's limits to formal verification.
[06:20.440 --> 06:22.200]  We're going to talk about the limits at the end of it.
[06:22.260 --> 06:24.700]  But basically, you're proving that the binary is correct.
[06:25.780 --> 06:29.720]  And one of my favorite security papers is Ken Thompson's Reflections on Trusting Trust.
[06:29.720 --> 06:32.420]  Basically, he's like, what if the compiler is backdoored?
[06:32.700 --> 06:33.120]  Right?
[06:33.200 --> 06:34.880]  Like, your own code could be perfect.
[06:35.020 --> 06:35.080]  Right?
[06:35.160 --> 06:38.040]  But the compiler itself could have issues that you're not aware of.
[06:39.340 --> 06:41.920]  The third part is memory-safe programming languages.
[06:42.180 --> 06:45.060]  So the language war is classic.
[06:45.240 --> 06:45.300]  Right?
[06:45.380 --> 06:50.180]  Like, I know every one of you has an opinion on which language is good.
[06:51.100 --> 06:54.140]  But essentially, Joe Biden made C++ illegal.
[06:54.660 --> 06:55.140]  Right?
[06:55.360 --> 06:56.720]  Because it's not memory-safe.
[06:56.720 --> 07:03.240]  So that's going to be something I talk about throughout this talk.
[07:05.580 --> 07:07.720]  One aspect is interoperability.
[07:08.600 --> 07:14.040]  So they recommend to write code in memory-safe languages.
[07:14.360 --> 07:15.980]  They mentioned Rust as an example.
[07:16.460 --> 07:17.540]  Any Rust fans?
[07:18.760 --> 07:19.660]  There's a few.
[07:19.820 --> 07:19.980]  Okay.
[07:21.200 --> 07:25.380]  So obviously, it's hard to rewrite the whole thing in a new language.
[07:25.380 --> 07:27.900]  So what they recommend is you can start writing a few components.
[07:28.220 --> 07:32.880]  And when you write a few components, let's say your code base is in C++, you rewrite one critical component in Rust.
[07:33.020 --> 07:36.080]  So you want interoperability between Rust and C++.
[07:37.600 --> 07:38.400]  Android does that.
[07:38.600 --> 07:46.460]  The Android team, they already use interoperability between different languages, and they also support the Rust Foundation in that.
[07:48.280 --> 07:51.280]  So let's go into the story of the rocket for a bit.
[07:53.200 --> 07:55.320]  So we're in 1996.
[07:56.820 --> 07:57.980]  That's a long time ago.
[07:58.100 --> 08:02.680]  That's when Francis McDormand did a killer performance in the movie Fargo.
[08:03.720 --> 08:05.980]  That's when Tupac was still alive.
[08:06.380 --> 08:09.100]  Only for a few months, but he doesn't know that.
[08:10.160 --> 08:14.560]  So we're in Kourou, which is a fishing town in French Guyana.
[08:17.600 --> 08:20.600]  French Guyana is French territory.
[08:20.900 --> 08:28.740]  And this rocket is the Ariane 5, which is launched by the European Space Agency, mostly a French company.
[08:30.980 --> 08:37.580]  And I learned that we launched rockets from the equator, because things are faster at the equator.
[08:37.720 --> 08:42.600]  Like if you're in the North Pole, you're just like spinning in place really fast, but you're not actually going...
[08:42.600 --> 08:45.420]  But if you're at the equator because of the Earth's diameter, you're actually going faster.
[08:45.560 --> 08:46.400]  So it just helps.
[08:47.820 --> 08:49.560]  And we're launching the Ariane 5 today.
[08:49.720 --> 08:52.720]  So there was rockets before it.
[08:52.860 --> 08:54.740]  There was Ariane 4, which was pretty successful.
[08:55.640 --> 08:57.080]  Today's Ariane 5, a new version.
[08:57.260 --> 08:58.740]  It's the first launch of that rocket.
[08:59.300 --> 09:03.160]  So the main reason of the explosion was self-destruction.
[09:03.380 --> 09:04.200]  We already know that.
[09:04.280 --> 09:07.480]  And so they know that because we mentioned logging is important.
[09:07.700 --> 09:09.200]  So they had logging.
[09:09.620 --> 09:12.680]  After it exploded, French Guyana is like swamp plant.
[09:12.860 --> 09:20.620]  So they fished out the black box and they got all of the interesting data and they realized, okay, it was a self-destruction for a good reason.
[09:20.760 --> 09:22.900]  But what caused it to self-destruct?
[09:25.100 --> 09:31.500]  So there's this module on the ship, on the rocket, called the inertial reference system.
[09:32.760 --> 09:35.340]  It calibrates the trajectory before launch.
[09:35.520 --> 09:36.900]  So before you launch, it's just calculating.
[09:37.740 --> 09:38.500]  It's using some sensors.
[09:38.640 --> 09:41.360]  It's seeing like, do I need to calibrate anything in my trajectory?
[09:41.500 --> 09:42.440]  Do I need to change my speed?
[09:43.640 --> 09:46.400]  It was created and used by the Ariane 4 successfully.
[09:46.600 --> 09:47.560]  It never had any issues.
[09:48.260 --> 09:53.320]  And so they moved it as it is from the Ariane 4 into the new rocket, the Ariane 5, which is launching today.
[09:54.600 --> 09:56.800]  And this is a diagram from them.
[09:56.960 --> 10:01.240]  Like they... you can see that it uses sensors like a gyro and an accelerometer.
[10:01.600 --> 10:09.360]  And it uses it to do calculations and then feeds angles and velocity increments into the onboard computer or the flight controller.
[10:09.360 --> 10:13.000]  So it's like, oh, you need to increase your speed if it determines that you need to.
[10:15.300 --> 10:20.700]  So, looking more at the logs, you realize, oh, actually there was an integer overflow at some point.
[10:21.400 --> 10:21.840]  Okay?
[10:22.920 --> 10:23.800]  That's interesting.
[10:25.060 --> 10:25.900]  Why did that happen?
[10:26.000 --> 10:33.380]  So basically, the buffer that held the speed was only 16 bit signed integer, but the velocity was supposed to be a 64 bit float.
[10:34.240 --> 10:40.500]  Real quick, what is buffer overflow or integer overflow or buffer uberlab?
[10:41.300 --> 10:47.320]  So essentially you have a fixed part in memory and you're trying to stuff a number that's larger than what the memory holds.
[10:47.480 --> 10:48.660]  And so you overwrite other things.
[10:48.900 --> 10:58.820]  That's generally buffer overflow, which also in 1996 was popularized by the Phrack article, smashing the stack for fun and profit.
[11:00.460 --> 11:06.400]  But in this case was integer overflow, which is slightly different in that, like, this is probably the best illustration.
[11:06.580 --> 11:09.820]  Like, you have a long number and you add one, but it's more than the buffer can hold.
[11:09.860 --> 11:12.420]  And so it wraps around, which can cause issues.
[11:13.900 --> 11:20.460]  And in some cases that can cause undefined behavior, which is common in C++.
[11:21.600 --> 11:25.640]  And undefined behavior is loss of flow, loss of control flow in the output.
[11:25.640 --> 11:27.380]  Like, I don't know what happens, right?
[11:27.420 --> 11:29.700]  It's not defined what, how the program should behave.
[11:30.300 --> 11:31.700]  There are ways to catch it.
[11:33.060 --> 11:34.540]  But it's still something that occurs.
[11:35.780 --> 11:39.900]  Now, in C++, that can be an issue.
[11:40.020 --> 11:44.180]  Now, luckily, the Arian 5 was not using C++, actually was using Ada.
[11:45.940 --> 11:48.600]  Great language, way ahead of its time.
[11:49.420 --> 11:53.580]  Instead of, like, it references a historical genius instead of being, like, the third letter of the alphabet.
[11:55.120 --> 11:58.420]  And it has a lot of security guarantees that we like to see today.
[12:00.300 --> 12:05.760]  So in this case, signed integer in C++, it would have caused undefined behavior.
[12:05.760 --> 12:08.720]  But we're using Ada, so instead it just raises an exception.
[12:08.920 --> 12:11.060]  It raises a constraint error exception.
[12:11.640 --> 12:13.180]  That's fine, we can handle exceptions.
[12:13.180 --> 12:13.940]  That's not a problem.
[12:16.100 --> 12:21.720]  So the reason for the overflow was that the Arian 4 was slow and the Arian 5 was way, way, way faster.
[12:21.880 --> 12:25.260]  Faster than the engineers could have ever imagined while designing the Arian 4.
[12:25.440 --> 12:27.880]  Because then we copied the system over as it is.
[12:28.900 --> 12:35.540]  So the initial reference system detected the operand error because that integer overflowed.
[12:35.620 --> 12:40.140]  We have an integer overflowed because it was so much faster than what we expected.
[12:40.140 --> 12:49.140]  And so the way it was designed is when you detect an overflow, you shut the system down because they assume it's a random hardware failure.
[12:49.580 --> 12:50.620]  Valid assumption at the time.
[12:51.780 --> 12:56.840]  And you trigger the backup, or you start talking to the backup system.
[12:56.980 --> 12:59.160]  So you shut this one down, you go to the backup.
[12:59.300 --> 13:01.160]  Now the backup, it's the same system.
[13:01.500 --> 13:03.300]  You're giving it exactly the same input.
[13:03.620 --> 13:06.080]  It's gonna do the exact same output, right?
[13:06.140 --> 13:08.320]  It's gonna say, like, operand error, time for it, and shut it down.
[13:08.320 --> 13:10.780]  So now you have your two IRS shut down.
[13:12.600 --> 13:14.620]  Still nothing that will cause an explosion.
[13:16.500 --> 13:24.620]  So once these two systems shut down, they're gonna talk to the flight control system, and they're gonna raise the operand error, saying, like, hey, I detected something wrong.
[13:25.040 --> 13:25.300]  Error.
[13:25.420 --> 13:26.240]  Catch the exception.
[13:27.640 --> 13:34.980]  Now the flight control system, and that's the core part of the issue, was that it assumed that it was getting flight data.
[13:35.220 --> 13:37.580]  In this case, the speed velocity.
[13:38.620 --> 13:47.760]  And so instead of catching the exception and handling it properly, it just assumed that it was getting, like, a number.
[13:47.980 --> 13:55.380]  And so it basically converted the error into ASCII values, which made, like, a really long number.
[13:55.380 --> 13:58.420]  And that didn't overflow.
[13:58.680 --> 14:02.380]  But instead, it felt like, oh, I am actually going really, really fast.
[14:02.900 --> 14:04.560]  Like, unbelievably fast.
[14:05.340 --> 14:09.960]  So to compensate for that, I just have to tilt the rocket by 90 degrees.
[14:12.680 --> 14:21.540]  So when you're launching a rocket, and you do this, like, that, like, that starts, like, ripping the hull apart.
[14:22.140 --> 14:25.840]  And it starts turning into a ballistic missile going down.
[14:26.220 --> 14:32.300]  And so the self-destruct program, the self-destruct program works incredibly well.
[14:32.440 --> 14:33.780]  Like, it works perfectly well.
[14:33.900 --> 14:34.880]  No problem at all.
[14:34.960 --> 14:36.580]  It just blows up the rocket, right?
[14:38.320 --> 14:40.700]  So technically, this was a safety mechanism, right?
[14:40.860 --> 14:44.280]  It blew up so it doesn't cause, like, more damage by landing in someone's house.
[14:47.340 --> 14:48.420]  So why did that happen?
[14:48.560 --> 14:50.300]  Like, we were talking about the European Space Agency.
[14:50.480 --> 14:51.760]  It's, like, some of the smartest people in the world.
[14:51.880 --> 14:52.900]  Like, they know what they're doing.
[14:55.180 --> 14:57.560]  Seven billion dollars in funding versus one operand error.
[14:57.660 --> 14:58.600]  Why did that happen?
[14:58.680 --> 15:00.580]  So you can say, like, oh, did they not catch the errors?
[15:00.600 --> 15:01.800]  Did they not use the static analysis?
[15:02.000 --> 15:02.820]  Like, all the things we talk about.
[15:03.180 --> 15:03.660]  They did.
[15:03.660 --> 15:06.320]  They used static analysis tools.
[15:06.660 --> 15:07.820]  And they caught errors.
[15:08.480 --> 15:10.660]  They caught, like, buffer overflows, integer overflows.
[15:10.900 --> 15:11.800]  They saw them.
[15:12.620 --> 15:17.220]  Now, in software engineering, you always have constraints.
[15:17.540 --> 15:19.020]  They were operating under some constraints.
[15:19.220 --> 15:21.940]  And so one of their goals was to...
[15:21.940 --> 15:24.460]  The target max CPU utilization was 80%.
[15:25.080 --> 15:26.500]  They read their documentation.
[15:26.500 --> 15:28.940]  They knew that they were writing ADA, not C++.
[15:30.740 --> 15:31.980]  Met work with partners.
[15:32.200 --> 15:32.720]  Check their assumptions.
[15:32.940 --> 15:33.500]  All of that.
[15:33.740 --> 15:38.740]  And after studying everything, well, they fixed four of the potential issues.
[15:40.260 --> 15:43.700]  Because with their assumptions, the three remaining ones would never overflow.
[15:43.860 --> 15:44.720]  There would never be a problem.
[15:45.760 --> 15:47.540]  One of them was the one that overflowed.
[15:48.420 --> 15:49.900]  And you might say, like, what?
[15:49.980 --> 15:51.200]  Like, why do they care about CPU?
[15:51.380 --> 15:52.920]  So, like, it's a rocket.
[15:53.060 --> 15:53.660]  Like, that's fine.
[15:53.660 --> 15:55.440]  We're talking about one if statement.
[15:55.640 --> 15:56.920]  Just add one if statement and fix it.
[15:57.060 --> 16:02.660]  Well, actually, your phone is 100 times more powerful than the CPU that was on the rocket.
[16:03.680 --> 16:05.300]  1996, it wasn't that fast.
[16:05.500 --> 16:07.880]  So every single check actually did matter a lot.
[16:08.720 --> 16:12.540]  Another part of it is, like, arguably, they tested in production a bit.
[16:13.140 --> 16:15.220]  And basically, they could have tested more.
[16:15.220 --> 16:18.880]  But it is very expensive to build a proper testing harness for rockets.
[16:19.060 --> 16:21.300]  So some of them, they did some light testing.
[16:21.300 --> 16:24.960]  In a way, the first launch was a test in itself.
[16:25.180 --> 16:26.320]  So that's fine.
[16:26.960 --> 16:33.380]  So some of the assumptions they took was that one exception handling is you just store the exception in memory.
[16:33.900 --> 16:34.240]  Log it.
[16:34.460 --> 16:35.680]  And then you shut the hardware down.
[16:35.880 --> 16:40.520]  Because the assumption was that any failure would be from a random hardware failure.
[16:40.600 --> 16:42.120]  Because the software is correct.
[16:43.680 --> 16:55.540]  The other assumption is when they were porting things from the old rocket to the new one, they thought that unless proven necessary, if something works, don't change it.
[16:55.640 --> 16:55.860]  It's fine.
[16:56.000 --> 16:56.700]  We know it works.
[16:56.920 --> 16:57.860]  Why would you make any changes?
[16:58.080 --> 16:58.340]  Keep it.
[17:00.780 --> 17:08.360]  The most tragic part is that the IRS, that system, it calibrated the trajectory before takeoff.
[17:08.360 --> 17:10.300]  So why was it working during takeoff?
[17:10.520 --> 17:21.000]  So another thing from the previous rocket, the IRN-4, you needed to continue running because if anything went wrong right before takeoff and you needed to reset the system, it took a long time to reset.
[17:21.140 --> 17:23.420]  So they were like, oh, let's just keep it running for like 40 seconds.
[17:24.160 --> 17:26.780]  And in case something went wrong, you can just reset it more quickly.
[17:27.860 --> 17:29.340]  The IRN-5 did not have this issue.
[17:29.440 --> 17:32.280]  So technically, the IRN-5 did not need the system to be running at all.
[17:32.380 --> 17:33.500]  It was completely useless.
[17:34.700 --> 17:36.360]  And that caused all these issues.
[17:40.160 --> 17:40.880]  When they...
[17:40.880 --> 17:47.680]  After this incident happened, they had a really, really interesting investigation and they tested a lot of things.
[17:47.800 --> 17:48.820]  They wrote a really interesting report.
[17:48.960 --> 17:50.700]  But they also just retested.
[17:50.860 --> 17:52.260]  They built a proper testing harness.
[17:53.600 --> 17:57.560]  They inputted like the actual trajectory details, not just like a generic, like I'll just try to lift off.
[17:57.700 --> 17:59.000]  And it caught the bug.
[17:59.420 --> 18:01.220]  It would have caught it if they did it before.
[18:03.320 --> 18:04.660]  This could have been avoided.
[18:04.840 --> 18:06.200]  So what triggered the failure?
[18:06.380 --> 18:07.200]  It's not just one thing.
[18:07.320 --> 18:18.160]  It's actually wrong design assumptions, undocumented assumptions, reusing old software, legacy code, lack of testing, mishandled exception, and an integer overflow.
[18:18.220 --> 18:21.700]  All of these together caused this explosion.
[18:22.360 --> 18:27.160]  So in the report, very interesting report, they mentioned that...
[18:27.160 --> 18:29.980]  They admit it was due to specification and design errors.
[18:30.920 --> 18:35.140]  And a combination of like lack of testing and analysis.
[18:38.100 --> 18:46.000]  They admit that they had considered before that their view was that things are correct until you prove that they're false.
[18:48.420 --> 18:49.880]  They decided to correct that.
[18:50.000 --> 18:58.880]  They're like, now we're in favor of the opposite view that software should be assumed to be faulty until you can demonstrate that it's correct.
[19:00.280 --> 19:01.580]  That's really interesting to me.
[19:02.260 --> 19:03.780]  1996, we've learned nothing.
[19:04.500 --> 19:05.180]  No, okay.
[19:05.260 --> 19:07.140]  We have learned a lot.
[19:07.140 --> 19:12.700]  But the interesting part of this statement is that what...
[19:12.700 --> 19:13.040]  How?
[19:13.320 --> 19:15.320]  What does it mean to demonstrate that software is correct?
[19:15.840 --> 19:17.240]  That's not very easy to do.
[19:17.880 --> 19:21.520]  So we're going to talk about that for the rest of this presentation.
[19:23.120 --> 19:28.340]  But overall, the RN5, the first launch was a failure because of software.
[19:28.660 --> 19:30.400]  It was actually one of the most successful rockets ever.
[19:30.600 --> 19:31.420]  It did great.
[19:31.560 --> 19:34.940]  It even launched the James Webb Space Telescope last year.
[19:36.840 --> 19:43.000]  And just two days ago was the first launch of the Ariane 6, the successor.
[19:43.260 --> 19:46.080]  And it was a success.
[19:46.240 --> 19:47.760]  It was perfectly fine.
[19:47.760 --> 19:51.280]  And it resulted in these great images.
[19:55.340 --> 19:56.900]  There's both in the image.
[19:57.140 --> 19:58.780]  There's one plane and one rocket.
[20:03.200 --> 20:03.720]  So...
[20:07.730 --> 20:09.070]  Does anyone get this reference?
[20:09.670 --> 20:09.810]  Yeah.
[20:10.170 --> 20:11.170]  So it's an inter-overflow.
[20:11.630 --> 20:12.150]  Exactly.
[20:12.330 --> 20:12.410]  Exactly.
[20:12.630 --> 20:18.290]  So Civilization video game, if you play against Gandhi, he's the most peaceful leader.
[20:18.550 --> 20:21.930]  When you discover nuclear weapons, he nukes everyone.
[20:23.050 --> 20:29.470]  And the rumor was that it was an integer underflow because he's supposed to have an aggression level of zero.
[20:29.630 --> 20:32.510]  And then when you discover nuclear weapons, your aggression level gets minus one.
[20:32.670 --> 20:34.230]  And so it overalls the maximum aggression level.
[20:34.430 --> 20:36.870]  But actually, they said it was a rumor.
[20:36.990 --> 20:37.730]  It was a myth.
[20:38.030 --> 20:42.230]  Apparently Sid Meier and the team said there was not actually a real integer underflow.
[20:42.230 --> 20:45.150]  But I still think that's the perfect example for an integer overflow.
[20:48.790 --> 20:49.270]  Another...
[20:50.310 --> 20:53.090]  So that's a radiation therapy machine.
[20:53.690 --> 20:55.070]  And it had...
[20:55.070 --> 20:57.390]  In the 80s, it had a lot of the same issues we just talked about.
[20:57.670 --> 21:00.950]  Overflows, but also ported legacy code, untested modules.
[21:02.090 --> 21:04.490]  But most importantly, bad UI and UX.
[21:04.790 --> 21:10.410]  So it actually encouraged the operators to just keep clicking next in the same button.
[21:10.490 --> 21:11.350]  Next, next, next, next, next.
[21:11.350 --> 21:14.290]  And if it ever throw an error saying, like, oh, this is terrible, something...
[21:14.290 --> 21:15.270]  You're just clicking next.
[21:15.370 --> 21:15.910]  You're not even reading.
[21:16.150 --> 21:16.510]  Right?
[21:16.630 --> 21:22.330]  So the bad UI, I think, is a great point in that the UI of our software also matters for security.
[21:26.380 --> 21:26.820]  So...
[21:27.840 --> 21:31.440]  That made me think, how can we prove that software is correct?
[21:32.980 --> 21:38.200]  And in 1931, this man...
[21:39.360 --> 21:40.680]  Did some interesting research.
[21:40.680 --> 21:44.800]  So that's Kurt Gödel and his incompleteness theorems.
[21:46.720 --> 21:47.680]  And essentially...
[21:47.680 --> 21:50.860]  Let's say you had to program Pinocchio, right?
[21:51.440 --> 21:54.720]  And if Pinocchio says, my nose will now grow...
[21:55.280 --> 21:56.160]  Well, if it...
[21:56.680 --> 21:59.340]  If it doesn't grow, then he's lying, then it will grow.
[21:59.480 --> 22:01.860]  But then he wouldn't be lying, so it would not have to...
[22:01.860 --> 22:03.140]  So it's a paradox, right?
[22:04.900 --> 22:07.920]  I personally think it will just grow and shrink repeatedly very quickly.
[22:08.140 --> 22:14.300]  But in general, this example of a paradox shows that...
[22:15.720 --> 22:22.600]  Or in Gödel's incompleteness theorems, there are statements that are neither provable nor refutable within the system.
[22:23.180 --> 22:28.060]  Which means that, like, some things I just can't really demonstrate that they are correct.
[22:29.980 --> 22:32.060]  And there's this interesting book that shows...
[22:33.020 --> 22:34.140]  That talks a lot about this stuff.
[22:34.300 --> 22:38.480]  But essentially, it also says, like, it's the self-reference that causes the paradox.
[22:38.720 --> 22:40.380]  Because, like, Pinocchio says, like, my nose will...
[22:40.380 --> 22:41.800]  Like, Pinocchio was talking about external things.
[22:41.920 --> 22:44.460]  Like, you can easily, like, prove if they're correct or not.
[22:44.540 --> 22:45.880]  But because he's referring to himself.
[22:47.420 --> 22:53.200]  Alan Turing came up with this halting problem based on the incompleteness theorems, right?
[22:54.160 --> 22:58.160]  So, for a given program and its input, can I prove if it's correct...
[22:58.160 --> 22:59.620]  Sorry, if it halts or not.
[23:00.860 --> 23:13.900]  And so, the way he proved that it's not possible to determine if a program halts or not is that assume you have a program that tells if another program halts or not, then get it to always say the opposite.
[23:14.120 --> 23:16.820]  Like, if it has an infinite loop, say that it halts.
[23:16.900 --> 23:18.600]  And if it halts, say that it has an infinite loop.
[23:18.720 --> 23:20.820]  And feed it to the program that tells if something halts or not.
[23:20.820 --> 23:25.840]  And it's, again, it's that self-reference system that creates a paradox and, like, I can't tell if something halts or not.
[23:28.000 --> 23:29.460]  Essentially, does the program halt?
[23:29.680 --> 23:30.360]  I don't know.
[23:30.700 --> 23:34.580]  Assume that the program doesn't halt, it's not secure, denial of service, just an example.
[23:35.220 --> 23:36.360]  Then is the program secure?
[23:36.500 --> 23:37.540]  I can't tell.
[23:37.800 --> 23:40.220]  That's kind of like a half-cooked thought I've been thinking of.
[23:40.380 --> 23:42.660]  If you have thoughts on it, we'll talk.
[23:42.880 --> 23:47.420]  But does that mean, like, we just can't prove that the software is correct?
[23:50.880 --> 23:58.140]  So these two theorems also contribute to limits of formal verification, right?
[23:59.260 --> 24:04.560]  Given these constraints, how can I provably demonstrate that software is running correctly?
[24:04.860 --> 24:06.180]  It just makes it even harder.
[24:07.240 --> 24:10.760]  Now, back to the language wars.
[24:11.860 --> 24:12.900]  Memory-safe programming language.
[24:13.080 --> 24:16.520]  There's a few things to say about that.
[24:18.820 --> 24:21.220]  So, yeah, Rust is what they recommended.
[24:21.500 --> 24:22.820]  C++ already in use.
[24:22.940 --> 24:23.760]  Lots of people hate C++.
[24:23.960 --> 24:24.720]  Lots of people love C++.
[24:24.920 --> 24:26.300]  Lots of people love Rust, right?
[24:26.440 --> 24:30.740]  So, who here prefers C++ over Rust?
[24:32.000 --> 24:33.340]  There's a few people.
[24:33.960 --> 24:36.000]  Does anyone else prefer Rust over C++?
[24:37.700 --> 24:38.680]  Also a few people.
[24:41.320 --> 24:42.840]  We'll go back to the example of ADA.
[24:43.220 --> 24:49.420]  So, when you're thinking about language wars, like, oh, Rust is supposed to give memory guarantees, guarantees for memory safety that C++ doesn't have.
[24:49.600 --> 24:50.980]  Well, ADA already had these.
[24:51.060 --> 25:01.780]  In fact, ADA in the 90s, the Department of Defense had a mandate that all critical weapon systems would use the ADA programming language for these same guarantees.
[25:01.780 --> 25:03.360]  So, we've been through this before.
[25:05.100 --> 25:14.940]  And even with that, eventually, that stopped applying because people just wanted to use C++ anyway, right?
[25:15.080 --> 25:19.540]  So, even though we had that mandate of, like, oh, you should use ADA, people were like, no, you know what?
[25:19.620 --> 25:19.960]  Never mind.
[25:20.120 --> 25:21.400]  We're just going to go back to using C++.
[25:21.600 --> 25:25.180]  And, like, for example, this fighter jet was made mostly in C++, right?
[25:25.900 --> 25:27.620]  No JavaScript, no Rust either.
[25:28.940 --> 25:32.560]  But that shows that you can use C++ well.
[25:33.520 --> 25:34.420]  It's feasible.
[25:36.120 --> 25:43.480]  Now, given that my background is turning bugs into PDFs, how can we list bugs in our code?
[25:44.660 --> 25:46.800]  Static analysis helps.
[25:47.040 --> 25:48.900]  So, I'm going to talk a little bit about that.
[25:49.060 --> 25:50.340]  It's not a comprehensive review.
[25:50.340 --> 25:56.580]  It's just one aspect of the many things you can do to check the security of your code.
[25:57.620 --> 26:00.200]  As we talk about, these are other things.
[26:01.820 --> 26:08.580]  So, static analysis, you're incorporating it into your pipeline.
[26:08.880 --> 26:10.860]  You're empowering developers to address these findings.
[26:12.880 --> 26:15.040]  It just looks at your code line by line.
[26:16.280 --> 26:18.220]  And it's basically pattern matching.
[26:18.400 --> 26:22.420]  So, because it's pattern matching, there is an example of cryptography.
[26:22.820 --> 26:23.660]  A good example.
[26:23.800 --> 26:25.400]  Like, how are we configuring your ciphers?
[26:25.520 --> 26:26.360]  Like, ECB is bad.
[26:27.080 --> 26:27.840]  AESGCM is better.
[26:29.080 --> 26:33.260]  But what static analysis doesn't catch is, like, maybe I shouldn't be encrypting at all in this case.
[26:33.360 --> 26:35.240]  Maybe I should just be hashing instead.
[26:36.360 --> 26:38.420]  That context is missing from static analysis.
[26:38.700 --> 26:42.980]  But it's still a good pattern matching to help with surfacing some findings.
[26:44.280 --> 26:48.820]  So, generally, on a security engineering team, you're running variant analysis.
[26:49.060 --> 26:50.060]  You're trying to surface trends.
[26:50.300 --> 26:52.740]  You're trying to recommend guidelines.
[26:53.020 --> 26:54.940]  And it depends on the language.
[26:55.120 --> 26:56.720]  So, languages do matter to a certain extent.
[26:56.860 --> 27:00.220]  Like, for example, I like to give the example of Ruby on Rails because it has amazing tooling.
[27:00.560 --> 27:00.920]  Right?
[27:00.940 --> 27:02.420]  You have Brakeman, Rubocop, RSpec.
[27:02.560 --> 27:03.660]  You have RubyGems for dependencies.
[27:03.940 --> 27:05.660]  And Brakeman is the static analysis tool.
[27:05.980 --> 27:12.200]  Brakeman is so good that even if you buy commercial static analysis tools, most of them just run Brakeman under the hood.
[27:14.660 --> 27:18.740]  Now, it's not as... Like, the tooling differs.
[27:19.060 --> 27:20.700]  The quality of tooling differs from a language to language.
[27:20.880 --> 27:22.660]  And, for example, like, I like to use Semgrep a lot.
[27:23.320 --> 27:28.780]  And with tools like Semgrep, it's just looking line by line.
[27:28.900 --> 27:30.420]  But C++ has complex grammar.
[27:30.600 --> 27:33.860]  Usually, you want to generate the AST before you have accurate scanning.
[27:34.020 --> 27:42.420]  But even in the domain of static analysis without wrapping around the compiler, even then, there's been some developments over the last few years.
[27:42.520 --> 27:49.700]  Like, even just earlier this year, Semgrep improved the way they scan C++ code using TreeSister.
[27:52.000 --> 27:55.360]  So tooling has been improving for all languages.
[27:57.100 --> 28:09.480]  I think the biggest mistake people do in static analysis is you just run the code, run the tool, and it generates 84,000 findings, and you just give them to the developers, and you know, good luck, and you leave, and they usually ignore you.
[28:09.620 --> 28:11.380]  Because why are you going to fix all of them?
[28:11.540 --> 28:13.500]  So usually, you want to, like, triage it for them.
[28:13.620 --> 28:20.940]  You want to list, like, the... remove false positives, prioritize the findings, and work with them on remediation.
[28:23.880 --> 28:25.140]  So, last part.
[28:25.300 --> 28:26.780]  Can C++ even be secure?
[28:27.900 --> 28:30.100]  Since Joe Biden made it illegal.
[28:30.460 --> 28:34.160]  I added this image because apparently the SpaceX rockets are C++.
[28:36.460 --> 28:39.200]  So there's been a few interesting things that happened recently.
[28:42.340 --> 28:46.620]  Bjorn Srautstrup had a very interesting talk on CPPCon last year.
[28:46.840 --> 28:50.520]  And he made two really good points that I hadn't thought about before.
[28:50.660 --> 28:55.700]  One was that we should be writing contemporary C++, not C slash C++.
[28:56.060 --> 28:58.920]  A lot of people learn C++ from books from, like, 2003.
[28:59.500 --> 29:01.940]  But, like, we... like, C++ evolves a lot, right?
[29:02.000 --> 29:04.600]  Like, we have C++ 23, right?
[29:04.600 --> 29:10.180]  Like, there's a lot of modern features at C++ that we ignore because of legacy code.
[29:11.180 --> 29:21.440]  Another interesting point he made is that with languages like Rust, it's usually... you usually have enthusiasts, people who are, like, writing code for passion projects.
[29:21.600 --> 29:24.060]  They really care about the quality of their code.
[29:24.960 --> 29:27.540]  They're spending a lot of time writing code.
[29:28.160 --> 29:39.360]  But with more established programming languages, you just have, like, a mid-dev that, like, hates their job, and has to write code with, like, 10,000 other people on, like, enterprise software for, like, a shopping cart.
[29:39.440 --> 29:40.260]  Like, no one cares about...
[29:40.260 --> 29:43.780]  So, not caring about it, like, it just makes it harder to write good code, right?
[29:44.200 --> 29:48.240]  And so, in any language, like, just make it very enterprise-y with, like, many people writing it.
[29:48.540 --> 29:51.100]  And you're gonna have... the quality of the code is gonna be less.
[29:54.140 --> 30:00.260]  Herb Sutter is on the ISO committee for C++, and he has some also really good research.
[30:00.440 --> 30:07.720]  He has this excellent blog post that goes into so much detail, like, the future of, like, how to make C++ more secure in terms of memory safety.
[30:08.180 --> 30:10.520]  He also has CppFront, which is, like, a compiler.
[30:10.760 --> 30:17.740]  Also, Herb Sutter did a similar thing with Circle, like, a compiler that ports a lot of the modern features you get with Rust.
[30:18.540 --> 30:20.160]  He's porting them to C++.
[30:20.740 --> 30:22.280]  He has also some iconic tweets.
[30:22.460 --> 30:25.500]  Like, people on Reddit were comparing him to overthrowing the government.
[30:26.100 --> 30:29.080]  Also, he's like, oh, why is no one else pursuing memory safety?
[30:29.080 --> 30:30.380]  And then, like, 83 comments later.
[30:30.520 --> 30:31.500]  He was like, well, that's depressing.
[30:31.800 --> 30:33.560]  But I think he's very funny.
[30:33.640 --> 30:35.340]  But also, like, excellent research.
[30:35.580 --> 30:36.060]  Really smart.
[30:37.840 --> 30:42.340]  Like, lots of things that he's doing that are worth looking at.
[30:43.920 --> 30:47.500]  So, all of these are showing that recent developments are happening.
[30:47.700 --> 30:50.060]  Like, all of these things were from the last, like, couple of years.
[30:52.500 --> 30:54.140]  And that's an interesting one here.
[30:54.280 --> 31:00.680]  So, one thing that causes undefined behavior is uninitialized variables in C++.
[31:01.100 --> 31:05.000]  And so, you can't actually do default initialization, right?
[31:05.060 --> 31:13.180]  Like, you can tell your compiler whenever someone declares a variable, if I don't actually explicitly initialize it, just, like, set it to zero, right?
[31:14.480 --> 31:22.920]  I was talking to some people, and one person made a really good argument that, like, maybe that's not what I want, because maybe it's wrong for the variable to be zero, right?
[31:23.100 --> 31:30.300]  So, I can't just assume, like, oh, just set it to zero, because that can cause other issues that are even harder to bug down the line, because it's a decision that the compiler took.
[31:31.340 --> 31:45.780]  So, some people proposed, also, last year, there was this paper, interesting paper about how we can define erroneous behavior instead of undefined behavior.
[31:45.780 --> 31:53.660]  So, whenever there's a variable that wasn't initialized explicitly, you just throw in an erroneous behavior error, and that's something you can catch and deal with later.
[31:54.020 --> 31:58.760]  So, bottom line is, like, you have many languages that people want to write, right?
[31:59.040 --> 32:00.980]  And do you have to port everything to C++?
[32:01.720 --> 32:05.340]  Do you have to keep using... do you have to port everything to Rust?
[32:05.960 --> 32:06.980]  It doesn't matter.
[32:07.200 --> 32:08.620]  You can do it whatever you want.
[32:10.380 --> 32:14.200]  Sorry, Ruby, not Ruby, Rust.
[32:14.540 --> 32:15.640]  I was going to talk about Ruby next.
[32:15.720 --> 32:16.440]  Rust is great.
[32:16.740 --> 32:21.960]  It has a lot of features, like the compiler will flag things immediately.
[32:24.120 --> 32:31.460]  But the idea is, like, if someone hires you to fix memory safety issues, and you say, like, oh, let's just rewrite everything in Rust, maybe that's not feasible for them.
[32:31.620 --> 32:33.020]  Maybe there's so much code.
[32:33.020 --> 32:36.640]  It's easy to say, like, oh, I like to rewrite and Rust.
[32:36.780 --> 32:40.820]  But, like, practically, it just takes a tremendous amount of effort.
[32:40.940 --> 32:46.980]  And if you're going to suspend the effort anyway, well, maybe just update your C++ code, right?
[32:49.100 --> 32:53.900]  There's also Zig, there's also, like, Ruby, whatever.
[32:54.140 --> 32:56.140]  You can make it all secure if you really wanted to.
[32:56.200 --> 32:56.980]  It's the same amount of effort.
[32:58.480 --> 32:59.160]  Software is hard.
[32:59.200 --> 33:00.980]  Sometimes they explode, but it's okay.
[33:00.980 --> 33:03.300]  If something explodes, you'll be fine.
[33:03.760 --> 33:04.720]  That's the end of the talk.
[33:04.840 --> 33:05.060]  Thank you.
[33:12.040 --> 33:15.440]  We have plenty of time left, so if anyone has questions or...
[33:15.440 --> 33:19.960]  If you want to talk about formal verification there, I would be interested in hearing.
[33:24.440 --> 33:25.220]  Oh, yeah, sorry.
[33:25.280 --> 33:25.480]  Go ahead.
[33:25.800 --> 33:26.620]  Are you familiar?
[33:30.240 --> 33:31.340]  No, tell us about it.
[33:34.900 --> 33:41.300]  SCL4 is a microkernel in the L4 pattern, but it was formally verified, which means they write...
[33:42.480 --> 33:48.740]  The actual code's in C, but it's got formal groups for everything properly.
[33:50.960 --> 33:52.520]  That's the whole story.
[33:52.980 --> 33:53.780]  Okay, so, yeah.
[33:54.380 --> 33:55.520]  Kernel, that's been formally verified.
[33:55.740 --> 33:58.080]  And was that safe?
[33:58.320 --> 34:00.040]  Like, did they have any issues with it?
[34:00.100 --> 34:01.180]  Was it, like, good forever?
[34:01.460 --> 34:02.240]  So the thing...
[34:02.240 --> 34:03.340]  I mean, it's a microkernel.
[34:03.340 --> 34:04.000]  Okay.
[34:04.000 --> 34:06.260]  So, you don't have drivers there.
[34:06.720 --> 34:08.200]  It's mostly with a scheduling.
[34:08.960 --> 34:11.460]  And so, they end up using it for...
[34:12.000 --> 34:20.240]  You end up attaching, like, a run kernel for the drivers, or you use it as a hypervisor to run, like, a network of a Linux kernel inside of.
[34:20.660 --> 34:24.320]  So, the problem is, it's not a solution by itself.
[34:24.500 --> 34:27.600]  You have to add components, and also the components aren't fully verified.
[34:27.880 --> 34:28.060]  Right.
[34:28.300 --> 34:30.640]  The kernel that isolates between the components...
[34:30.640 --> 34:32.440]  That's a good point, yeah.
[34:32.640 --> 34:43.220]  And you just remind me, with formal verification, things like a microcontroller, or anything you want to formally verify, you're formally verifying it according to the spec, right?
[34:43.380 --> 34:46.920]  And so, you generally assume that the spec is correct.
[34:47.160 --> 34:51.840]  But there's been instances of, like, the spec itself could have issues, or, like, bad design issues.
[34:53.160 --> 34:57.420]  Like, the rocket we saw, some of the issues were just bad assumptions on the design phase.
[34:59.620 --> 35:00.700]  So, I don't know.
[35:00.760 --> 35:04.700]  I can't think of any examples of, like, something that was formally verified, but still had the bug.
[35:04.820 --> 35:06.820]  But that's still certainly possible.
[35:08.140 --> 35:14.800]  So, I guess, formal verification can help address some subset of issues in that component itself.
[35:15.640 --> 35:18.380]  But still, things can still go wrong.
[35:18.560 --> 35:22.320]  And it's important to remember that this is a relatively small piece of code.
[35:22.500 --> 35:25.060]  It's technically an OS, because it's a micro kernel.
[35:25.380 --> 35:26.260]  There's not much to it.
[35:26.540 --> 35:27.320]  It's small.
[35:27.760 --> 35:28.980]  Yeah, that's a good point.
[35:29.060 --> 35:33.960]  I think the Amazon S2N library, like, the TLS library that they formally verified, they also...
[35:33.960 --> 35:45.960]  I remember something, like, they took a small subset of the code and was, like, generally, like, a small spec, well-defined, like, contained, like, the code isn't too large, and that makes it easier to verify.
[35:47.180 --> 35:48.160]  So, that's interesting.
[35:48.440 --> 35:55.180]  But then, yeah, like, let's say someone asks you, like, hey, verify all of Linux, the whole kernel, or, like, all of Microsoft Windows.
[35:55.340 --> 35:58.460]  I feel like that's overwhelmingly difficult.
[35:59.040 --> 36:03.620]  And to be clear, though, 90-plus percent of Linux is a driver.
[36:04.040 --> 36:04.820]  It's a driver.
[36:05.080 --> 36:05.900]  Yeah, yeah.
[36:06.080 --> 36:06.740]  That's interesting.
[36:09.840 --> 36:12.200]  As written, you couldn't formally verify it.
[36:12.280 --> 36:14.140]  You'd have to rewrite it to be able to verify it.
[36:14.380 --> 36:15.320]  You would have to rewrite?
[36:15.420 --> 36:15.540]  Why?
[36:16.100 --> 36:21.100]  Because a lot of things are heuristically written, and so they don't have an abstract model to verify directly.
[36:21.320 --> 36:28.320]  The verification process requires creating a mathematical proof that is an independent entity that has an isomorphism to the existing code.
[36:28.540 --> 36:32.880]  Because that requires it to have the structure that can do formal verification stuff.
[36:33.180 --> 36:45.160]  And so, like, unless you have a formal verifier that can run across C, in general, arbitrarily, which is not a thing that a human is going to create like an 800-page document formally verified in the course schedule.
[36:45.520 --> 36:47.480]  You're going to leave that schedule to be verifiable.
[36:47.660 --> 36:48.340]  Right, right.
[36:48.340 --> 37:00.420]  For the people online, I guess, he was saying, it'll be very difficult to formally verify something like C kernel, because you're not going to rewrite all of the components and define them well, and...
[37:02.180 --> 37:05.420]  Yeah, that's like the three-sentence summary of...
[37:06.920 --> 37:08.580]  Chat DVD, write me A.
[37:10.020 --> 37:11.460]  I'm sure that'll be fine, yeah.
[37:17.360 --> 37:35.100]  So, you touched on it a little bit, but with C, C++, which I write it in C, there are a lot of tools with a lot of the compiler stack, so there's the static, you touched on the static analysis, but just the compilers alone, the CLAN and the GCC, have
[37:35.100 --> 37:37.860]  a really large set of...
[37:37.860 --> 37:40.560]  Sanifies this, Sanifies that, Sanifies everything.
[37:41.100 --> 37:48.140]  Sanifies their family from C-Lounge, and a bunch of stuff that's been added to GCC from decades ago.
[37:48.360 --> 37:49.560]  They're not really...
[37:51.020 --> 37:52.380]  comparable to the GCC.
[37:57.700 --> 37:59.680]  Like that uninitialized variable thing.
[38:00.200 --> 38:01.020]  I'm pretty sure that's in there.
[38:01.780 --> 38:02.940]  Yeah, you can...
[38:02.940 --> 38:05.740]  I think it was one of the earlier slides.
[38:05.860 --> 38:09.560]  You can tell the compiler to detect...
[38:10.440 --> 38:13.680]  undefined behavior, but also uninitialized variables, for sure.
[38:13.960 --> 38:15.720]  And I think...
[38:15.720 --> 38:17.980]  I was recently reading on...
[38:17.980 --> 38:18.900]  about ZIG.
[38:19.980 --> 38:23.280]  I barely know anything about it, but it was something like...
[38:23.280 --> 38:30.560]  you can use it to compile C code, and it adds some of the checks and features that...
[38:31.480 --> 38:35.160]  So yeah, to your point, the compilers themselves are also improving.
[38:37.080 --> 38:37.960]  You can...
[38:37.960 --> 38:39.760]  use a lot of good sanitizers.
[38:41.120 --> 38:42.620]  And I hope that...
[38:42.620 --> 38:44.280]  people would start using those more.
[38:44.400 --> 38:50.500]  I think one of the challenges is when you have a huge code base with legacy parts of it, enabling some of these...
[38:50.500 --> 38:53.440]  just flags too many things, and people are like...
[38:53.440 --> 38:58.360]  it's like, oh, it's gonna take me months to go over all of this, and so they just avoid it.
[39:00.580 --> 39:01.920]  But I guess the key is...
[39:02.460 --> 39:11.660]  you're just gonna have to put in effort to... if you want to add the sanitizer, if you want to initialize all of your variables, all of those are good to do, but it's gonna take effort.
[39:12.020 --> 39:18.720]  And so that's why I thought when the White House saying, oh, rewrite components in Rust, that's fine.
[39:18.820 --> 39:19.420]  You can do that.
[39:19.500 --> 39:25.160]  But also, if you're gonna put in effort anyway, you can just put in effort to improve your current code base.
[39:30.160 --> 39:30.780]  Anything else?
[39:34.800 --> 39:37.200]  Are you familiar with antithesis?
[39:37.800 --> 39:38.480]  Antithesis?
[39:38.800 --> 39:39.920]  No, what is that?
[39:40.120 --> 39:45.180]  It's kinda like a cutting edge in the space of finding bugs.
[39:45.520 --> 39:48.100]  It's not quite formal verification, but...
[39:48.100 --> 39:50.320]  Yeah, it's a very cool fuzzer.
[39:50.660 --> 39:51.320]  It's a fuzzer?
[39:51.700 --> 39:52.800]  So, okay.
[39:53.300 --> 40:02.040]  A fuzzer randomly explores the state space, but many possible states are very unlikely to happen.
[40:02.040 --> 40:07.700]  So, if you have a time out of five seconds, you will not hit the something-something that happens after ten seconds.
[40:08.320 --> 40:08.340]  Mm-hmm.
[40:08.600 --> 40:13.420]  So, it's a smart fuzzer that systematically searches your state space.
[40:13.660 --> 40:17.500]  And so you can find bugs that are extremely unlikely.
[40:17.640 --> 40:21.980]  Those one in a million bugs that you only see in production can reproduce them in a few minutes.
[40:22.260 --> 40:25.400]  So, it's a smart fuzzer within your state space.
[40:25.400 --> 40:26.240]  Yeah.
[40:26.680 --> 40:26.880]  Interesting.
[40:26.880 --> 40:27.540]  What's the name of it?
[40:28.200 --> 40:28.740]  Antithesis.
[40:29.320 --> 40:29.860]  Antithesis?
[40:31.000 --> 40:31.260]  Does it...
[40:31.260 --> 40:33.960]  What languages does it?
[40:34.120 --> 40:37.900]  It actually works with many languages because it doesn't...
[40:37.900 --> 40:39.340]  It's not a language at this level.
[40:39.340 --> 40:45.340]  So, fundamentally, they took KVM and they modified it so it was replayable.
[40:46.140 --> 40:49.600]  So, they can replay an arbitrary Linux VM session.
[40:49.720 --> 40:50.180]  Oh, wow.
[40:50.480 --> 40:50.520]  Wow.
[40:50.620 --> 40:56.560]  You throw your Linux distribution plus kernel or whatever you want for your program to run.
[40:57.420 --> 41:02.940]  And a full trace of the effective failure and they can replay it.
[41:03.160 --> 41:03.680]  And then they...
[41:03.680 --> 41:05.200]  Oh, that's why it's a fuzzer.
[41:05.420 --> 41:05.640]  Okay.
[41:05.820 --> 41:07.840]  It's really just re-running your...
[41:07.840 --> 41:09.180]  everything on a VM, basically.
[41:09.460 --> 41:09.700]  Right.
[41:09.880 --> 41:23.440]  And then on top of that, they do like modern ML-based stochastic optimization for finding bugs in the first place and then can do functional replay with the idea for distributed software.
[41:23.740 --> 41:30.320]  So, if you have distributed database, you can have a whole bunch of these antithesis instances running against each other and you can inject faults.
[41:30.500 --> 41:30.840]  Yeah.
[41:31.180 --> 41:31.680]  That's interesting.
[41:31.860 --> 41:35.240]  I mean, that's interesting because the whole domain of fuzzing is an interesting one.
[41:35.340 --> 41:42.920]  I mean, lots of bugs have been found through fuzzing, which I find a bit depressing is like just like throwing random data actually works.
[41:44.580 --> 41:49.560]  But I think Google, they find a lot of their bugs through fuzzing.
[41:49.700 --> 41:51.920]  I guess partly because they have unlimited resources.
[41:52.180 --> 41:53.840]  Google has a lot to fuzzing.
[41:54.980 --> 41:57.040]  Google donates a lot to fuzzing open-source projects.
[41:57.120 --> 41:59.040]  Donates a lot to fuzzing open-source projects.
[41:59.220 --> 41:59.260]  Yeah.
[41:59.480 --> 41:59.580]  Yeah.
[42:00.860 --> 42:01.960]  I'm glad it works.
[42:03.100 --> 42:03.500]  Yeah.
[42:03.600 --> 42:04.640]  That's the whole other field.
[42:05.040 --> 42:08.520]  You say it's depressing that fuzzing works but I kind of look at it the other way.
[42:08.780 --> 42:14.960]  You put the effort in to either fix the code or write new code and you're going to have to fuzz it either way.
[42:15.340 --> 42:15.360]  Yeah.
[42:15.580 --> 42:20.280]  Sometimes you can think a little less about things and what the fuzzing do to heavy lifting for you.
[42:20.860 --> 42:21.260]  Yeah.
[42:21.460 --> 42:21.920]  No, you're right.
[42:22.040 --> 42:22.360]  I'm joking.
[42:22.460 --> 42:23.260]  It's not depressing at all.
[42:23.380 --> 42:24.040]  It's incredible.
[42:26.100 --> 42:26.600]  You're right.
[42:26.740 --> 42:27.440]  I have a question.
[42:27.680 --> 42:27.800]  Yeah.
[42:28.180 --> 42:32.620]  What's your primary reason for using the support plus versus Rust?
[42:32.860 --> 42:34.140]  Is there some kind of security?
[42:35.620 --> 42:36.020]  Sure.
[42:36.860 --> 42:37.260]  Yeah.
[42:37.500 --> 42:37.640]  Yeah.
[42:37.880 --> 42:39.300]  Rust is memory safe.
[42:39.500 --> 42:41.980]  Well, it's supposed to be a memory safe by default.
[42:41.980 --> 42:48.080]  Now, to do certain things, you add the unsafe, what do you call it?
[42:48.220 --> 42:48.960]  Like declaration, I guess.
[42:49.160 --> 42:52.520]  And you could still write unsafe code within Rust.
[42:52.740 --> 42:58.720]  But by default, it has a lot of guarantees to avoid memory safety issues.
[42:58.880 --> 43:03.300]  And the compiler itself also is good at flagging issues on compile time.
[43:04.000 --> 43:07.560]  Whereas C++, things cause undefined behavior.
[43:07.740 --> 43:15.140]  C++ generally was made with the philosophy of like it's the programmers' responsibility to avoid any issues.
[43:15.680 --> 43:24.980]  Whereas Rust and a lot of the modern tooling, they try to flag things and they don't assume you're gonna write perfect code because it's, you know, you're gonna make, everyone makes mistakes.
[43:27.740 --> 43:35.900]  So, yeah, I mean, the White House, I mean, the same thing, they recommended Rust now, which is the same reason they recommended Ada before, right?
[43:36.060 --> 43:44.560]  It's like a tool that has more guarantees that will make it easier for someone to not have security issues in their code.
[43:46.580 --> 43:47.020]  Yeah.
[43:47.740 --> 43:48.940]  Which is like the old-fashioned way?
[43:50.620 --> 43:51.600]  No, no, no.
[43:51.740 --> 43:53.360]  To be fair, I don't, I don't care.
[43:53.560 --> 43:55.960]  Like, you can, you can use whatever programming language you want.
[43:56.320 --> 44:07.800]  But the reality is, it's often not up to us because it's often, like, like, often you're a security engineer that's gonna be onboarded to a company and you just, yeah, yeah, there's a lot of code there.
[44:07.800 --> 44:08.020]  Exactly.
[44:08.220 --> 44:13.000]  It's whatever they're using, it's hard to be like, hey, rewrite everything, right?
[44:13.140 --> 44:15.880]  Like, there's, that's not, often not feasible, right?
[44:16.080 --> 44:21.040]  So, so that's why sometimes you have to stick with what you already have.
[44:21.260 --> 44:44.740]  Now, if you have a vision and standards have to play, examples are C++ core guidelines and M, I, S, or A.
[44:45.420 --> 44:47.720]  Yeah, that's an excellent point.
[44:47.820 --> 44:48.580]  That's an excellent point.
[44:48.740 --> 44:51.080]  That kind of goes back to one of the first slides.
[44:51.220 --> 45:06.160]  But coding, when you, when you join a company, so, it's, it's one thing to, to write secure code yourself, but it's more challenging when you have, like, thousands of employees in a company and you want them all to write secure code.
[45:06.280 --> 45:11.680]  And so, automated tooling that's run in CI, CD, like, that's one way to surface findings.
[45:12.320 --> 45:23.180]  But, guidelines, to your point, is another way to, to, to encourage good behaviors and good patterns before the code even gets compiled.
[45:23.460 --> 45:26.640]  And so, you have standard template libraries.
[45:26.800 --> 45:32.180]  You have, you can just have, like, secure coding trainings that, you can have modules.
[45:32.440 --> 45:39.100]  Like, if there's something you have to do over and over again, just use the library that we've already vetted, that we know is good.
[45:41.220 --> 45:46.520]  You can also have some tooling to enforce those good patterns within your code.
[45:46.740 --> 45:58.560]  And the idea is that by having standards and, like, secure coding standards, it's, the developer has to make less decisions or, like, it's, the default decisions are often the, the secure ones.
[45:58.780 --> 46:00.440]  And it encourages good behavior.
[46:00.660 --> 46:01.280]  It avoids issues.
[46:02.980 --> 46:04.920]  Yeah, it's generally a good idea.
[46:07.640 --> 46:08.020]  Cool.
[46:09.280 --> 46:10.340]  We will end here.
[46:10.460 --> 46:10.760]  Thank you.
[46:10.920 --> 46:12.100]  I will be outside if you want to talk.
[46:12.400 --> 46:12.660]  Thank you.
[46:12.680 --> 46:13.520]  Thank you.