Linux Kernel Hardens Sound Drivers Against Spectre V1 Vulnerability

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

[ElectricPrism]

Thanks intel /s

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

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

[dungeon]

this is getting out of hand hand.

Tilde is getting out of arrow arrow.



Nope, this is the correct one one

[starshipeleven]

Don't worry , we got you covered covered.

this is getting out of hand hand.

[Leopard]

I quit as typo reporter for a few days until my ISP fixes a major connection problem within the area.

Don't worry , we got you covered covered.

[Leopard]

More is better better.

You are right indeed indeed.

[RSpliet]

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

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...
Second problem is that very few programmers think in terms of mathematics. Especially in kernel device drivers, we just want to execute a sequence of operations. Although this is not forbidden by functional languages, it's often more tedious to write such sequential bits of code. It will most likely result in less-readable and thus less maintainable code, in turn leading to fewer kernel contributors.

[cybertraveler]

A bit exaggerated, but not totally sarcastic. You do have a too low idea of the quality standards there.

You're mistaken. I expressed an absence of knowledge about how they implemented these fixes, an understanding that there is potential for low quality solutions to be implemented and a hope that the devs had implemented high quality solutions.

I appreciate the information you provided that demonstrated the Linux devs took a high quality approach to the problem.