Linux 5.15 Working Towards Comprehensive Compile-Time & Run-Time Detection Of Buffer Overflows

[darkonix]

language for incremental replacement of c is called c++.

If you are talking about programming in general it may true that C++ replaces C. But for low level and systems development C++ features are usually not a good match. In Linux Kernel development in particular, it will never happen. Linus Torvalds has expressed a strong opposition to C++. On the other hand he kind of supported adding the infrastructure for Rust modules in the kernel.

rust is language for bankrupting mozilla[

If Mozilla bankrupts there are more likely other reasons than Rust. The interest in Rust by many companies (Amazon, Microsoft, Google, Dropbox, Facebook, etc) shows that its usage is thriving.

[darkonix]

Some people need their perspective widened a little.
C and its derivatives require the developer to manage. The original CPUs and OSs did not do any of this, therefore the coder had to.
Modern languages are nice and all, but that type of automatic memory safety just wasn't available when C was created.
It's really a different environment in computing these days and the advent if Virtual Memory spaces on a per program basis, really are what allows things like Rust and Java to exist. Only truly low level things like OS kernels really need the explicit memory management that C provides. Otherwise, everybody should be using the newer memory safe code paths instead.

I'm not sure why you put Rust in the same level as Java. Rust is a low level, systems language, like C. It uses abstractions and restrictions at compile time to provide some guarantees. Your comment seems to suggest it uses automatic garbage collection like Java. I'm not sure if that was your intention. You can do manual memory management in Rust, it is just that it is not required if you follow the rules. Java is a completely language and environment where the memory is automatically managed by the garbage collector.

[darkonix]

Rust can be just as fast or faster.

Rust can be as fast as C or C++, but I'm not sure why it would be faster. Do you have any benchmarks to support that comment?

[oiaohm]

Yes, yes it does. C is not fixable. Full stop. Open up a list of CVEs that are language/compile time issues and see for yourself.

That is in fact not true. SeL4 in fact demoed that C is in fact fixable long time back but the process was not well optimised. There is ways to make static analysers as Sel4 demoed that remove all the C problems. sparse in the Linux kernel is a important read.

https://sparse.docs.kernel.org/en/latest/types.html

This extends the types and other information static analysers can use to work out if a code is correct or incorrect. C language standard type system is way too limited.

Rust isn't perfect but it's in a different league when it comes to security constraint enforcement.

The horrible part here is rust is second rate to what sel4 did for security constraint enforcement while keep core code C. The sel4 work really did set a benchmark we should be aiming to get to be you using rust or c. C++ is may not be fixable(there are particular things coded in the C++ language define that ruin your day)

Sparse shows that we can extend the metadata of C a hell of a lot. Of course some of the problem for developers coming to Linux kernel work is getting use to the extra meta data they have to put in their code to get it mainline. Linux kernel C is not the normal C that most CVE issue use.

The reality here is fixing the C language will result in having to code C different in future. There have been breaking changes in C code over the years.

Almindor the reality here the Linux kernel code base is huge. Having to recode it all in rust would be a pure nightmare. If sparse way of inserted meta can be used add what is need so rust for detect faults can be put on top of C the conversion will have a lighter workload.

https://www.cylab.cmu.edu/news/2021/07/09-SyRust.html

Also rust is not that far used and we are already seeing memory issues like buffer overflow issues. Yes it the unsafe memory areas rust language lacks proper validation in the unsafe areas.

There is more than 1 way to solve this problem. Extending the C language again is a option of course this time the Extend to the C language be focused on being secure not another C++.

Sel4 extend off C with mathematical based proof that horrible because its a mess development process result in you have the C source file and 3 other files matching up to it. So Sel4 demoed that C was fixable but their method was horrible. Sparse in the Linux demos that C is still truly extendable. Sel4 work + the Linux kernel sparce work = the possibility of extending C to have single source files with greater safety than rust.

[arQon]

C is just old and clunky and not designed around being memory safe. It just wasnt a concern at the time. Most early architectures didn't even have protected memory in the first place.

Few things are more amusing to me than watching an idiot try to pretend he has any clue at all of what he's talking about, and man do you fail hard on that. That comment is Hall Of Fame levels of stupidity.

Fun fact for you: even in the absence of "protected memory", overrunning an array still tramples on other bits of memory, and that almost never ends well.

"wasn't a concern" my ass. The difference is that "at the time", programmers were Real Men who actually studied the craft, not randos who minored in it for one semester and only got jobs in software because they flunked their EE courses or it paid better. Do you think trading systems etc were written in BASIC or something 30+ years ago?!
jfc...

[mdedetrich]

That is in fact not true. SeL4 in fact demoed that C is in fact fixable long time back but the process was not well optimised. There is ways to make static analysers as Sel4 demoed that remove all the C problems. sparse in the Linux kernel is a important read.

https://sparse.docs.kernel.org/en/latest/types.html

This extends the types and other information static analysers can use to work out if a code is correct or incorrect. C language standard type system is way too limited.


The horrible part here is rust is second rate to what sel4 did for security constraint enforcement while keep core code C. The sel4 work really did set a benchmark we should be aiming to get to be you using rust or c. C++ is may not be fixable(there are particular things coded in the C++ language define that ruin your day)

Sparse shows that we can extend the metadata of C a hell of a lot. Of course some of the problem for developers coming to Linux kernel work is getting use to the extra meta data they have to put in their code to get it mainline. Linux kernel C is not the normal C that most CVE issue use.

The reality here is fixing the C language will result in having to code C different in future. There have been breaking changes in C code over the years.

Almindor the reality here the Linux kernel code base is huge. Having to recode it all in rust would be a pure nightmare. If sparse way of inserted meta can be used add what is need so rust for detect faults can be put on top of C the conversion will have a lighter workload.

https://www.cylab.cmu.edu/news/2021/07/09-SyRust.html

Also rust is not that far used and we are already seeing memory issues like buffer overflow issues. Yes it the unsafe memory areas rust language lacks proper validation in the unsafe areas.

There is more than 1 way to solve this problem. Extending the C language again is a option of course this time the Extend to the C language be focused on being secure not another C++.

Sel4 extend off C with mathematical based proof that horrible because its a mess development process result in you have the C source file and 3 other files matching up to it. So Sel4 demoed that C was fixable but their method was horrible. Sparse in the Linux demos that C is still truly extendable. Sel4 work + the Linux kernel sparce work = the possibility of extending C to have single source files with greater safety than rust.

Sel4 isn't really written in C, its written in HOL/Isabel which is a formally verified abstract language that is a refinement ontop of C along with other theorem provers like Isabel (see part 3.1 in https://sel4.systems/About/seL4-whitepaper.pdf). Ontop of that the produced C is a subset of the C standard. Sel4 also has to formally verify that the produced binary is correct (since compilers can also be wrong) and to do this it has disassembles the binary again in HOL to prove that its correct.

In other words its misdealing to say that Sel4 is written in C, its not. Sel4 just treats C as a high level assembler and they don't directly write in C.

Furthermore developing Sel4 is not that easy, you have to use capabilities for pretty much everything (including hardware address spaces). Sel4 also has limitations, i.e. multicore is only on Arm (and has a very trivial lock implementation that doesn't scale well, and its also not formally verified). Also if its not obvious, Sel4 is a microkernel which means that it simply doesn't implement a lot of things which a Linux equivalent would, they intentionally made their problem space smaller.

For something like Linux, Rust is really the best candidate, although its true there are memory buffer overflows with things like unsafe one thing to note is that Rust's borrow checker has also been formally verified, the problem of course is with the compiler. Sel4 is too extreme on one end of the spectrum, its very difficult to develop with (any changes to the sel4 kernel need a formal proof, because again you are not directly writing C in Sel4 but rather in Isabell/HOL).

Rust has a nice middlegroud which is appropriate for Linux's target audience/demographic.

[krzyzowiec]

Rust can be as fast as C or C++, but I'm not sure why it would be faster. Do you have any benchmarks to support that comment?

Rust has more information than C or C++. In particular, the aliasing guarantees, which could lead to performance optimizations. I know there was some work on llvm in that regard but I have no idea what the status is.

[mdedetrich]

Rust has more information than C or C++. In particular, the aliasing guarantees, which could lead to performance optimizations. I know there was some work on llvm in that regard but I have no idea what the status is.

iirc They finally ended up enabling it (for those who were unaware, it was actually a bug in LLVM)

[oiaohm]

Sel4 isn't really written in C, its written in HOL/Isabel which is a formally verified abstract language that is a refinement ontop of C along with other theorem provers like Isabel (see part 3.1 in https://sel4.systems/About/seL4-whitepaper.pdf).

Go back and read 3.1 again.

C is not a formal language; in order to allow reasoning about a C program in the theorem prover (we use Isabelle/HOL), it has to be transformed into mathematicallogic (HOL). This is done by a C parser written in Isabelle. The parser defines thesemantics of the C program, and gives it meaning in HOL according to this seman-tics. It is this formalisation which we prove to be a refinement of the mathematical(abstract) model.

SeL4 is in fact written in C. There is a parser that turns C into HOL for mathematical validation. The HOL does not generate the C program just yells at you if you have it coded wrong. Yes look at page 10 you start at the C code for both the compiler and the validator.

For something like Linux, Rust is really the best candidate, although its true there are memory buffer overflows with things like unsafe one thing to note is that Rust's borrow checker has also been formally verified, the problem of course is with the compiler.

This is something that Sel4 proved could be done with C. Yes you would need processing engine on top of C. This is the comprehensive Comple-Time buffer overflow detection that is now being implement.

Does gcc and llvm have a theorem prover the answer is in fact yes. Working out how to get from Isabel into gcc and llvm version of a theorem prover. How does gcc and llvm optimise code by covering what very language you code in to a internal language that it can run provers on for optimisation and validation.

So gcc case C comes into gets turned into gimple and that is what the provers are using.

SeL4 like it or not demoed that you could still code C and have validation tool on top and produce solid code. This of course can be change to integrate validator into C compiler so doing the same thing with 1 tool.

mdedetrich yes your claim that Sel4 is written in HOL/Isabel is invalid. SeL4 is written it self in C being a limited subset with its validator written in HOL/Isabel that cannot generate C code itself only error if you have something coded wrong.

So there is two ways to solve this problem. SeL4 demos that the C compiler can be improved and with gcc and llvm based tools adding extra meta data to C by __attribute__( stuff they are limit themselves to only C standard. Yes sparse demos that this can be pushed even more than what it currently is.

mdedetrich parties like you don't want to admit to the possibility that C could be fixed. Yes this will most likely result in feature of C being disabled from use. There are already a list of C things you are not allowed to submit to the Linux that are allowed under the C standard. Yes the issue they talked about with C not having enough information this is also being addressed as compilers catch up in validation to what the sel4 validation can do by extending C with features like __attribute( that are not part of the C standard.

There could come the day where the sales pitch that rust will fix buffer overflow issues and other memory issues will mean nothing to the Linux kernel because the version of C the Linux kernel will accept will not have these issues. "Rust's borrow checker" like it or not SeL4 implemented equal as a static analyzation tool on top of project written C with C functionality restricted. Nothing says that the Linux kernel code base has to use every C feature..

[xhustler]

This is where C doesn't shine. It is a very simple language and allows compilation to nearly every computer architecture out there, but memory management is a total mess and there are absolutely no checks, which makes the language hard to master.

Prepare for the Rust comments...

I don't claim to be a master Jedi programmer but all this railing against C is bogus in my book - learn to write better code. STOP being lazy, once you allocate memory, clean it up. All this Java and Rust BS (pardon the language) simply encourages lazy programmers.