Linux Kernel Hardens Sound Drivers Against Spectre V1 Vulnerability

[caligula]

It's not constructive calling people stupid and retarded. Please try and be polite; doing so will make this place a nicer place to have discussions.

The thing is, obviously he doesn't understand the situation for one reason or another. Type system is the basis of language semantics. A good analogy in real life would be neo-liberal capitalism, mercantilism, communism etc. Sometimes you can't "fix" one system to become another. For example, adding lambdas might benefit from a GC, which then would lead into a different pointer model when a more performant moving GC can change absolute pointer values. If you add a way to construct tagged unions, you'd need a way to also deconstruct them, that is, pattern matching. I was actually arguing that C could change into this direction, but these features can't be added with the precompiler. They either require frontend changes or a fairly complex macro system (not the one in C). When it comes to types, you can't have unsafe C style types with voids simultaneously with a automatic type check/deduction system which is also formally proven. This is a huge change, something that can't be just retrofitted.

[cybertraveler]

The thing is, obviously he doesn't understand the situation for one reason or another. Type system is the basis of language semantics. A good analogy in real life would be neo-liberal capitalism, mercantilism, communism etc. Sometimes you can't "fix" one system to become another. For example, adding lambdas might benefit from a GC, which then would lead into a different pointer model when a more performant moving GC can change absolute pointer values. If you add a way to construct tagged unions, you'd need a way to also deconstruct them, that is, pattern matching. I was actually arguing that C could change into this direction, but these features can't be added with the precompiler. They either require frontend changes or a fairly complex macro system (not the one in C). When it comes to types, you can't have unsafe C style types with voids simultaneously with a automatic type check/deduction system which is also formally proven. This is a huge change, something that can't be just retrofitted.

Thanks for your polite and informative reply

I'm not knowledgeable enough to suggest a path forward for C. In my amateur opinion, I think any further changes to the C standard should be small and conservative in order to main backwards compatibility, keep language complexity low and ensure existing use cases of C are not broken. I think the kind of enhancements you've just mentioned are best implemented in new languages.

[oiaohm]

When it comes to types, you can't have unsafe C style types with voids simultaneously with a automatic type check/deduction system which is also formally proven. This is a huge change, something that can't be just retrofitted.

Really this shows how little you know.

https://sel4.systems/

sel4 core is written in C.

http://ts.data61.csiro.au//projects/TS/l4.verified/approach.pml

Sel4 does not alter C. It has insanely effective lint system. Yes it has usage of unsafe C style types with voids and simultaneously achieves formally proven status.

Sorry sel4 absolutely proves that it can be retrofitted as it started with a C based l4 implementation then made it formally proven.

Do note the double way arrows. Using the tools developed for sel4 you can take C code in and produce a execution specification and abstract specification then processed to run full formal proof on that.

Something remember GC and tagged pointers consume performance and neither is required to make formally proven code.

I guess caligula you had never seen sel4 before.

[caligula]

Really this shows how little you know.

https://sel4.systems/

sel4 core is written in C.

http://ts.data61.csiro.au//projects/TS/l4.verified/approach.pml

Sel4 does not alter C. It has insanely effective lint system. Yes it has usage of unsafe C style types with voids and simultaneously achieves formally proven status.

Sorry sel4 absolutely proves that it can be retrofitted as it started with a C based l4 implementation then made it formally proven.

Do note the double way arrows. Using the tools developed for sel4 you can take C code in and produce a execution specification and abstract specification then processed to run full formal proof on that.

Something remember GC and tagged pointers consume performance and neither is required to make formally proven code.

I guess caligula you had never seen sel4 before.

No, sorry, you didn't understand what I said. I said nothing about proving programs, nothing about transpiling shit into C. I'm very familiar with seL4. I commented on using C as the implementation language. What you said is that using a larger framework with multiple languages, formal proofs and lots of transforms between languages, you can achieve things. That's basically admitting that C is not sufficient and you need other tools to achieve the goals. C is the only dispensable part in this figure you linked to. It's just something you have to deal with because the most used toolchains are C/C++ and people expect good performance and wide arch support. If there were more mature tools for any other systems programming language (mostly optimization passes and wide range of supported targets), they'd use those instead.

[oiaohm]

No, sorry, you didn't understand what I said. I said nothing about proving programs, nothing about transpiling shit into C. I'm very familiar with seL4. I commented on using C as the implementation language. What you said is that using a larger framework with multiple languages, formal proofs and lots of transforms between languages, you can achieve things. That's basically admitting that C is not sufficient and you need other tools to achieve the goals. C is the only dispensable part in this figure you linked to. It's just something you have to deal with because the most used toolchains are C/C++ and people expect good performance and wide arch support. If there were more mature tools for any other systems programming language (mostly optimization passes and wide range of supported targets), they'd use those instead.

The problem you have got here is transforming between languages is normal operation for a modern C compiler. Both Gcc and LLVM have a internal representation(IR) both take plugins to extend. https://github.com/torvalds/linux/bl...cc-plugins.txt

Yes the Linux kernel does not only extend the C standard for their code with sparse as a front end they also extend C language with compiler plugins.

What you have missed is what is the difference between optimization processing and proof processing. Turns out to be not much difference at all. Working out how to tool the internal representations of compilers with these features to proof quality and what would have to be added to C so this can be done would allow other languages by gcc and llvm also to be made safer.

Like you have to just look at address sanitiser in LLVM and GCC to see that these tool on tracking of memory allocations and that pointers are not going to stupid locations.

You have to remember when sel4 was done plugins into c compilers was not an option. The fact LLVM and GCC take plugins how much from the internal representation of these compilers can be extracted to fill out a proof and how much would have to added to the languages these compilers support to run a solid proof.

I am not saying you might not need a extra language. But you have to remember you already in a C compiler have at least 3 languages. 1 is C 2 is asm/machine code. 3 is what ever the compiler uses as internal representation for optimising and detecting errors/warning about code.

Of course as you said C and C++ already has wide platform support most of this is covered by just 2 compilers being LLVM and GCC.

It a surprise to most people when they looking inside a c compiler and see that just after the pre processor the compiler is converting the code into another language. C is like a short hand version of english.

Reality is no one who know C compilers that C is sufficient alone to achieve nicely optimised code let alone proofed code. A quality C compiler is going to have a internal representation. I currently don't think C source provides enough information so the internal representation inside a C compiler has enough information to proof the code but this does not have to stay this way with modern compilers supporting plugins.

The big thing is since we now have compilers with plugins to make highly secure programs does not have to mean write a new language. Instead you can extend existing languages and use compiler plugins to pickup those new features. Yes compiler plugins are not like the pre processor.

[cybertraveler]

^ I'm enjoying this discussion