Linux Kernel Hardens Sound Drivers Against Spectre V1 Vulnerability

[starshipeleven]

Don't worry , we got you covered covered.

this is getting out of hand hand.

[dungeon]

this is getting out of hand hand.

Tilde is getting out of arrow arrow.



Nope, this is the correct one one

[oiaohm]

The kernel needs to be gradually rewritten in a language like this:

The answer would changing language not what need to happen.

https://en.wikipedia.org/wiki/Sparse...el_definitions The Linux kernel is not pure C to start off with and sparse already allows adding extra information for code sanity checking. The ideas out of ATS could go into sparse so expanding what faults sparse will find. Of Course while trying to keep syntax simple and common sense for kernel space.

https://lwn.net/Articles/718628/

The Linux kernel does have fairly formal memory model that does need to be expanded to be more useful for locating multi threading issues memory.

The fact there is a formal memory model for the Linux kernel means for lots of type things the Linux kernel does not need generic solution instead need the Linux kernel memory model solution. The Linux kernel memory model has odd behaviours different platforms can do due to out of order execution and other things.

https://www.kernel.org/doc/Documentation/locking/lockdep-design.txt

Its not like the Linux kernel had to change to a new language to get mathematically provable lock safety. Its require tooling yes but not a new language.

This is always the same thing we need to write a new language to be safe?? Then they go out and write a new language that people have to learn and rewrite the code completely. Please note rewriting the code completely creates room for creating a new set of bugs. The other option is don't change the program language but add tooling like sparse and lockdep. Do note sparse is using flags that are not part of the C language and due to the way they are added they are ignored by the C compiler. So added features to sparse to have it audited is adding extra bits to existing code no full rewriting. Its how marking pointers as user or kernel space and detect if they would be used wrong is done in sparse.

Yes it cool to write a new language its not a cool to add tools to existing languages.

[xiando]

fun isn't over yet! 8 new security vulnerabilities found in Intel processors. Xorg server security is beginning to look like an armed fortress in comparison to CPUs.[/URL]

And the first Happening is in Two Days (May 8th) when the first of these are made public. Intel/AMD/Microsoft and other players are supposedly told already yet I have seen nothing about spectre-ng on the kernel mailing list.

[ElectricPrism]

Thanks intel /s

[caligula]

Well, academics are interested in this idea, but I personally think there's two problems with such an approach. Firstly, a functional language wouldn't've helped against Spectre, as program checkers don't formally model details required to catch timing-based side-channel attacks on architectures. That tends to be way too much detail needed for validating *program* correctness...

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.

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

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

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

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