Linux Kernel Hardens Sound Drivers Against Spectre V1 Vulnerability

[cybertraveler]

^ I'm enjoying this discussion

[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.

[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]

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.

[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.

[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.

[oiaohm]

What the heck should this do? C already has types, although very weak ones. I'm not one of those __feature__ folks, I'm not magically impressed every time you suggest replacing 'feature' with '__feature__' macros.

https://gcc.gnu.org/onlinedocs/gcc/Attribute-Syntax.html

__attribute__ in gcc is not a Macro instead is a core compiler processed feature. But can be removed by macros on compilers that don't support it.

Something here when a C person says feature is not a macro. Its a feature added to the core compiler. Maybe hide-able by macro.

C users seem to think that adding new features with underscore prefixed names somehow won't add bloat and don't belong to the core language. This school of taught is pretty retarded. How about just fixing the core syntax. Pre-processor is the one that should be axed. It's a constant source of problems.

The pre-processor is why you can add new compiler supported features to c compiler while still having the source code build on compiler that don't support that feature.

C can be expanded, yet support for tagged sum types hasn't landed yet in the standard. I'm not expecting this miracle to happen in the next 10-20 years.

The history of C standard development is features appear in compilers first then get made standard. So until someone start making modified versions of C compilers with the extra features of course is not going to happen in the standard. _Bool took 10+ years to get into the C standard after it had been in different compilers for that long.

C types are very generic and weak.

https://www.kernel.org/doc/html/v4.11/dev-tools/sparse.html#using-sparse-for-typechecking

Yes C type checking is too weak for the Linux kernel. The reason why the Linux kernel has by sparse __force.
PM_SUSPEND = (__force pm_request_t) 1, That means that PM_SUSPEND can only be used on something that is type pm_request_t. Of course under normal C without sparse you don't have this restriction. Of course (__force pm_request_t) on a standard C compiler with pre-processor macros disappears as a no operation. caligula there have been a lot of C lint systems over the years that have expanded what you can audit in C. Also the reality is Linux kernel is not restrict it self to the feature standard c offers instead uses sparse to expand the feature set so more issues can be detected. Of course the features like __force would be nice to be a generic C standard feature. Yes something use __force in the Linux kernel when you run sparse if you have recast type will be error.

Linux kernel is using an extended C. Now how many features of these other languages could be added to sparse or attempt to upstream into gcc.

[cybertraveler]

C users seem to think that adding new features with underscore prefixed names somehow won't add bloat and don't belong to the core language. This school of taught is pretty retarded. How about just fixing the core syntax. Pre-processor is the one that should be axed. It's a constant source of problems.

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.

Regarding your quoted point: the purpose of adding underscores isn't to do with optionality. In C, names with a leading underscore followed by an uppercase letter are reserved for use by the C standard (and maybe the compiler too; I'm not sure). When new versions of the C standard are brought out, they deliberately expose those features using this underscore prefix naming to ensure that existing, valid, C programs will still compile under the new standard. These new features with an underscore prefix may or may not be optional: that's completely unrelated to the underscore prefixing.

One example of this is C99 introduced a required built-in data type, _Bool (note the underscore followed by an upper case letter). You can optionally #include <stdbool.h> to get access to the macros bool, true and false (which map to _Bool, 1 and 0 respectively).

[caligula]

https://en.wikipedia.org/wiki/C11_(C_standard_revision)

Seriously, comparing C11 features with Rust, Haskell, or Coq? You must be stupid.

C is not as resistant to change as it first appears. Also you have to remember there are a lot of features in C compilers that have nothing to do with the C standard. Like __attribute__ in gcc.

C users seem to think that adding new features with underscore prefixed names somehow won't add bloat and don't belong to the core language. This school of taught is pretty retarded. How about just fixing the core syntax. Pre-processor is the one that should be axed. It's a constant source of problems.

Really there could be a __type__ feature added to compilers or any of the other functional programming features.

What the heck should this do? C already has types, although very weak ones. I'm not one of those __feature__ folks, I'm not magically impressed every time you suggest replacing 'feature' with '__feature__' macros. Obviously you don't realize how type systems work. As a bare minimum, learn System F.

You also have to remember items like gcc warnings and features like address sanitiser are not part of the C standard either. So this is why I ask why do we need a new language when its fully possible with C to expand C. Sparse with the Linux kernel proves it possible. Lets not rewrite the complete universe when it possible to fix the compiler.

C can be expanded, yet support for tagged sum types hasn't landed yet in the standard. I'm not expecting this miracle to happen in the next 10-20 years. Standardizing even the alignment features took over 40 years. Great job pals. After 40 years of OS/systems programming (where alignment control is basic bread and butter programming idiom), let's standardize alignments. Seriously, wtf.

[oiaohm]

Well, functional programming might not protect from Spectre, BUT it can eliminate thousands or millions of other kinds of bugs - both reveal existing ones in the codebase and prevent new ones from appearing. Also, instead of writing everything in Coq, we could instead try to improve C as a language. Improving the type safety of C. Perhaps we could even add few productivity features. It's funny (actually not funny) how eager people are at shotting down ideas that would help. It's like if it was better to do nothing and come up with naive excuses than gradually trying to do something. I do programming in C, Rust, Scala, F#, Haskell. I could come up with a list of pet peeves in C. However the language seems very resistant to change which is kind of sad. It's not like C was based on some state of the art in 1970 when it appeared. It was actually shittier than ALGOL, which appeared around 15 years earlier. Few improvements, lots of worse decisions. The syntax is shorter. Is that good? Depends.

https://en.wikipedia.org/wiki/C11_(C_standard_revision)

C is not as resistant to change as it first appears. Also you have to remember there are a lot of features in C compilers that have nothing to do with the C standard. Like __attribute__ in gcc.

http://flyingfrogblog.blogspot.com.au/2016/05/disadvantages-of-purely-functional.html

The problem is there is no such thing as pure functional programming.

Really there could be a __type__ feature added to compilers or any of the other functional programming features.

You also have to remember items like gcc warnings and features like address sanitiser are not part of the C standard either. So this is why I ask why do we need a new language when its fully possible with C to expand C. Sparse with the Linux kernel proves it possible. Lets not rewrite the complete universe when it possible to fix the compiler.