WEBVTT 00:00.000 --> 00:25.100 Thank you. 00:25.100 --> 00:26.100 Yes. 00:26.100 --> 00:27.100 Thank you. 00:27.100 --> 00:35.260 So I will start with a quick summary and also a motivation for this project. 00:35.260 --> 00:41.740 So yeah, as you all may well be aware, like any larger project, the box in the Linux 00:41.740 --> 00:43.700 certifier. 00:43.700 --> 00:45.620 And there are existing solutions to this. 00:45.620 --> 00:52.660 For example, the fuzzling has found a lot of box and some were resolved using formal verification. 00:52.660 --> 00:58.500 And also there are hardware-based approaches to kind of put the program into another 00:58.500 --> 01:00.980 sandbox inside the kernel. 01:00.980 --> 01:06.660 But unfortunately, these all either involves runtime overheads to some extent or they are 01:06.660 --> 01:09.340 where you hard and complicated to implement. 01:09.340 --> 01:12.540 So they take time to cover the whole verifier. 01:12.540 --> 01:19.900 And in this talk, I'm going to talk about an alternative idea to solving this problem 01:19.900 --> 01:24.140 using layouts using a layout security approach. 01:24.140 --> 01:29.900 So basically the idea was that you verify the program twice once maybe in user space, 01:29.900 --> 01:34.820 for example, using prevail or based on the Rust compiler compiler. 01:34.820 --> 01:38.220 And then in the kernel, you verify it again. 01:38.220 --> 01:42.900 And if there are box in any of those algorithms, you hope that the box in one algorithm 01:42.900 --> 01:46.820 are caught by the other algorithm. 01:46.820 --> 01:52.700 And I did two case studies, one based on the Rust compiler and one based on prevail. 01:52.700 --> 01:56.860 And unfortunately, you're found that this kind of design doesn't really work, at least 01:56.860 --> 02:02.780 to me, it appears it is still exploitable, even though writing exploits certainly sometimes 02:02.780 --> 02:06.100 becomes smaller tedious. 02:06.100 --> 02:11.700 So sticking to the rough-based design, here's how it would look in detail. 02:11.700 --> 02:18.100 So we get the source code from some untrusted Rust program. 02:18.100 --> 02:21.100 And we compile this using a modified Rust compiler. 02:21.100 --> 02:25.300 I will get to the modifications you would have to make in a second. 02:25.300 --> 02:30.140 And then this generates some byte code, which in theory should already be safe, because 02:30.140 --> 02:35.420 you restricted the Rust compiler and also the libraries the programs used in a way such 02:35.420 --> 02:40.380 that this program can only do memory safe and type safe behavior. 02:40.380 --> 02:46.020 And then you verify that again using the Linux verifier, and hopefully you get even safe 02:46.020 --> 02:47.820 a byte code. 02:47.820 --> 02:52.940 And so the implementations of the two verifiers should obviously be as different as possible 02:52.940 --> 02:57.420 because then it is you are more unlikely to have the same bug. 02:57.420 --> 03:01.660 If you have code we use between the verifiers, then you could end up with the same bug 03:01.660 --> 03:03.940 in the two systems. 03:03.940 --> 03:07.860 And the obvious benefits are that you basically have no runtime overheads, you just have 03:07.860 --> 03:13.620 a verification time overheads, and you can reuse existing tools and libraries, so it's relatively 03:13.620 --> 03:17.140 easy to implement. 03:17.140 --> 03:21.700 And the two case studies are, and so one based on the Rust compiler already talked about the 03:21.700 --> 03:27.860 other design would be based on pvail, and prevail already verifies ppf object files, so you 03:27.860 --> 03:33.820 can directly feed those into the prevail verifier and then do a second pass with the Linux 03:33.820 --> 03:35.420 verifier. 03:35.420 --> 03:39.700 And in my analysis, I focused on the changes you would have to make to those systems 03:39.700 --> 03:44.860 to make this kind of approach work, whether there are any bugs in those systems, so in the 03:44.860 --> 03:50.300 prevail verifier and the Rust compiler, and whether the resulting layer verification approach 03:50.300 --> 03:52.820 would be exploitable. 03:52.820 --> 04:00.540 So first, looking at the Rust based design in more detail, so I previously thought about 04:00.540 --> 04:05.740 that we have to make some changes to the Rust compiler, and likely we also have some kind 04:05.740 --> 04:12.060 of trusted Rust library which can be used by the ppf program, so this would, for example, 04:12.060 --> 04:18.940 allow the program to call bpf helpers in a safe way, and then this produces the bytecode 04:18.940 --> 04:22.780 which can be verified by Linux. 04:22.780 --> 04:27.820 So regarding changes, we would have to make to the Rust compiler, and you obviously have 04:27.820 --> 04:32.860 to disable unsafe, but there's also a bunch of other features, for example, there are 04:32.860 --> 04:38.220 procedure macros in the Rust compiler, which basically allow you to rewrite the whole program 04:38.220 --> 04:40.500 source code to something else. 04:40.500 --> 04:45.860 This also has to be disabled, and in the appendix, I also look at a few other features, for 04:45.860 --> 04:52.500 example, ppf and some other, for example, unions, they also would likely allow you to introduce 04:52.500 --> 04:58.620 unsound behavior or there will that relative in you and therefore likely background. 04:58.620 --> 05:04.260 Another thing where the Rust compiler currently for short is termination checks, these are 05:04.260 --> 05:10.220 obviously not needed for user space applications, so it doesn't provide those, and you could 05:10.220 --> 05:16.860 likely implement something like this using procedural macros, but a more exhaustive check would 05:16.860 --> 05:20.820 likely be better put into the compiler directly. 05:20.820 --> 05:26.180 So these are the compiler related changes you would have to make, and second, and there's 05:26.180 --> 05:32.540 also a bunch of changes that would have to be made to the Rust library that is used 05:32.540 --> 05:40.060 by the bpf program, and so there's already a Rust library which allows you to write 05:40.060 --> 05:47.580 bpf code in Rust, that's IA, also in the next talk, so you could likely extend this, and 05:47.660 --> 05:54.700 looking at the examples I've looked at, you can already write where we complex programs 05:54.700 --> 06:00.060 only using save code, and the places where they still use unsafe at least to me looked, 06:00.060 --> 06:07.540 as if they could be likely easily removed using more interfaces. 06:07.540 --> 06:13.220 Another thing is a problem in the Rust standard library, and also how safety is commonly 06:13.300 --> 06:18.660 perceived in Rust is that it does not guarantee non-static destructors, so that's the reason 06:18.660 --> 06:26.660 people commonly refer to Rust as not guaranteeing memory safety, however this could be changed, 06:26.660 --> 06:32.180 I believe, so it was basically a design decision that was made for the Rust standard library 06:32.180 --> 06:39.940 in 1.0 of the Rust compiler, but in the compiler I think it's not half-coded, so it's 06:39.940 --> 06:45.860 only something, it's basically a definition of what safety means for the Rust standard library, 06:45.860 --> 06:52.740 and it's not built into Rust. Yeah, so this concludes the changes you would have to make 06:52.740 --> 06:57.700 to the Rust compiler, and now looking at the box in the compiler that would likely be relevant 06:57.700 --> 07:04.740 to such a design, so all the compiler box reported, so the last one is the issue, so there's 07:04.820 --> 07:14.980 roughly 10,000 issues open, around 4,000 bucks, and there are two kinds of bucks which are 07:14.980 --> 07:20.980 relevant to such a system. First, you have arbitrary code execution, but the someone can 07:20.980 --> 07:26.340 write a Rust program which can take over the compiler, they can obviously generate any ebps, 07:26.340 --> 07:32.260 but they want to generate, and this can then be some exploit for the ebps verify. 07:33.220 --> 07:39.460 However, at least I've not found any reports of our repository code execution box for the Rust 07:39.460 --> 07:47.780 compiler directly, however there are 104 compiler crashes reported, and these indicate that there's 07:47.780 --> 07:54.260 some kind of memory unsafe to the compiler that could probably lead to our repository code execution 07:54.260 --> 08:00.740 down the line, or it doesn't seem that anybody tried to exploit those for our repository code execution, 08:01.700 --> 08:06.980 they exist further potential for hardening, for example, memory sanitizers, I think they are 08:06.980 --> 08:13.940 usually not applied to the compiler, and the second kind of box is an unsoundless box, of course, 08:13.940 --> 08:19.380 or you basically have safe code, and it produces an unsafe binary, so it's basically at 08:19.380 --> 08:28.180 back in the checks from Rust that for safe Rust, and they are around 100 of those open, 08:28.180 --> 08:36.740 so that's already much better than the 4000 box overall, and then the following I will assume that 08:37.860 --> 08:42.740 basically there are unfoundless box and assume that there are no arbitrary code execution 08:42.740 --> 08:47.460 box, and I analyzed whether the system would be exploitable if we make this assumption. 08:49.780 --> 08:56.580 Unfortunately, it appears to be exploitable, so the two box I have looked at as an example 08:56.660 --> 09:05.380 are a Rust unsoundless, unsoundless issue, which is called implied bounds on nested references, 09:05.380 --> 09:12.660 plus variance equals a sound as whole, and this is apparently relatively complex to fix because 09:12.660 --> 09:18.980 they basically decided to redesign a whole part of the compiler to fix it, and that also explains 09:18.980 --> 09:28.020 why it takes so much time. The other box I looked at was a Linux or a firebox, a TVE from 2022, 09:28.420 --> 09:32.900 and that's basically a case where a pointer arithmetic is correct incorrectly. 09:34.580 --> 09:41.300 So looking at the unsoundless box, there's proof of concepts online where you can look at how 09:41.300 --> 09:45.700 you can exploit this unsoundless box in the verify, and it basically gives you a function, 09:46.660 --> 09:50.260 you don't have to read this code, I just want to show it that it's a lot of code, 09:51.540 --> 09:56.900 it basically gives you a function that allows you to cast one type into another type. 09:59.540 --> 10:07.220 So this then basically gives you an unsave task primitive, which can be compared using only 10:07.300 --> 10:14.980 safe code. And the idea to then build an exploit for this layered approach is to basically use this 10:14.980 --> 10:22.740 unsoundless box for type unsave, if you have type unsave, you can, for example, cast a scalar 10:22.740 --> 10:27.860 into a pointer, and this gives you a out of funds pointer, and the harder part of the exploit 10:27.860 --> 10:33.940 is then finding a Rust program that generates the unsave EBPF bytecode that is also misbite 10:34.020 --> 10:43.220 verify. So that's basically this compilation. And it takes some times, but you can certainly do it. 10:43.220 --> 10:50.260 So you can use this transmute primitive to construct the out of bounds pointer, and the interesting 10:50.260 --> 10:56.740 thing here is maybe that all this code I just showed you in Rust gets compiled basically down to a 10:56.740 --> 11:02.260 single, register silent in the EBPF bytecode, because the compiler does the optimizations, 11:03.060 --> 11:08.740 and therefore the EBPF verify has no way of kind of double checking whether the Rust compiler 11:08.740 --> 11:16.580 did any error here. When you have optimizations, you don't want in the bytecode you can 11:16.580 --> 11:23.060 avoid them using data dependencies. What is a little bit more tedious is to get the register usage 11:23.060 --> 11:28.420 in the exploit right, because the Rust compiler doesn't really care whether it's at a 11:28.420 --> 11:35.060 it adds a scarlet to a pointer or the other way around, and this can get more tedious to kind of 11:35.060 --> 11:40.260 make it do the right thing, but yeah it's possible. And you can find the proof of concept in the 11:40.260 --> 11:48.740 GitHub repo. Yeah, so this concludes the part on the Rust compiler, and I also looked into the 11:48.820 --> 11:57.140 prevailed EBPF verify, and the good news is first it looks like it does not reuse any 11:57.140 --> 12:04.740 kernel code, which should also be the case as it uses the MIT license. So if there are any bugs in 12:04.740 --> 12:11.940 the prevail verify, which I will assume they are likely to be different from the bugs in the Linux 12:12.020 --> 12:20.100 verify. There are currently around four the issues open. One is a one is tagged as a bug that 12:20.100 --> 12:26.340 would be potentially relevant for this kind of thing, but I did not look into it specifically 12:26.340 --> 12:33.380 I just assumed that there is some bytecode, which is incorrectly analyzed by the prevailed verify, 12:33.380 --> 12:40.980 and then asked whether it can be exploited. As so the ideas we have two functions. One is 12:40.980 --> 12:47.540 incorrectly abstracted by the Linux verify, one is incorrectly abstracted by prevailed, and we now 12:47.540 --> 12:53.060 will try to combine these functions, and then kind of use the result of this combination to 12:53.060 --> 13:00.180 construct a hidden out of bounds read all right, which is then native kernel exploit. And unfortunately 13:00.180 --> 13:08.260 such a combination exists, and it's also very simple actually. So you basically, you assume 13:08.260 --> 13:15.220 at one and at two are some complex sequences of bytecode, which are incorrectly abstracted by one 13:15.220 --> 13:23.700 of the verifiers, and you see that both for air one and air two, at least one of the verifiers 13:23.700 --> 13:29.460 still matches the actual execution, or ever if you of course, and these results together you 13:30.100 --> 13:37.460 basically have a result, which where none of the verifiers is correct anymore, and then in the second 13:37.460 --> 13:43.700 part you can basically just use this incorrectly track register to construct an out of bounds 13:43.700 --> 13:52.900 point and use it. So this concludes my talk. Unfortunately, layer verification seems to have limited 13:52.900 --> 13:58.820 potential. You can usually combine the exploits, it roughly doubles the exploitation effort, 13:58.820 --> 14:04.340 because you need one exploit for one system and one for the other, and then you have to combine those. 14:04.900 --> 14:10.580 Of course, marks in the runtime, for example, the helpers, but in any case, not be covered by it. 14:11.940 --> 14:17.140 The effort, at least for a rest, it seems to be a little bit more tedious, however, I also 14:17.140 --> 14:24.580 not look at whether there are any reliable tools, which give you a rest program for a certain 14:24.580 --> 14:30.020 ebbed bytecode. I'm not sure if something like this exists. For prevail, it's certainly very easy, 14:30.020 --> 14:37.780 because you can just use the generic consumption. Thank you very much, and I'm happy to take questions. 14:44.340 --> 14:49.860 Yes? For the rest of the exploits, what you're not doing, technically, right, unsafe, 14:49.860 --> 14:56.580 or a very code that is equitable, we have to intentionally make the exploit out of it. 14:57.300 --> 15:03.060 Yes, the question is whether you have to make the exploit happen intentionally. Yes, that's the case for sure. 15:03.060 --> 15:09.700 So I think, I guess someone stumbled upon this issue in the rest compile at some point by mistake, 15:09.700 --> 15:15.540 I guess, or maybe through fuzzling or something like that, but it's very complex code, and I guess 15:15.540 --> 15:20.580 you would never kind of write this kind of unsafe, safe code by mistake. 15:20.580 --> 15:29.380 But it's like if you build a ebbed program, assuming you've done everything correctly according 15:29.380 --> 15:38.980 to the rest centers and the compiler said, somebody else can't exploit your ebbed code. Or is that possible? 15:41.380 --> 15:45.860 You mean that there are memory safety box in the ebbed program? 15:46.740 --> 15:53.940 Would there be? I think if you do not make a mistake on purpose, it would be like, yeah, I think. 16:01.620 --> 16:02.980 Yes? 16:02.980 --> 16:11.140 More like the background for this topic, what's the extent behind using graphs to write ebbed over 16:11.700 --> 16:14.500 So why we do that? 16:14.500 --> 16:21.700 I think the question is better as we do for the next talk, but we can also talk offline.