X.Org Server Hit By New Local Privilege Escalation Vulnerability

[ryao]

Did you ignore that in Android 13, Google rewrote the low-level driver into Rust?
And cargo itself is production ready.

I don't think it's fair to say "almost and next to no".

It is fair to say that for any new language.

As for Android, Google is very clear that they are using Rust for new code:

https://security.googleblog.com/2022...ndroid-13.html

The same can be said about every project, including your mature software.
You don't know a bug is present until it's found, so lacks of bug report does not mean lacks of bug.

There are a number of bugs in any non-trivial software that is not formally verified, including OpenZFS. I am working on squashing as many as I can. Unlike new code, the OpenZFS source code at least has the benefit of having had years of validation and debugging, which separates it from freshly written code.

Because this is their proprietary software and it's part of their core business.
Would you expect Google to release its search engine code as open source?

It's already stated that this is a proprietary project by Cloudflare and they have no plan to open source it from day 0.

The fact that Cloudflare is using it where they get GB or TB level of data per second in their data center means they have confidence in it.

Cloudflare explicitly stated that they plan to open source Pingora from the beginning:

https://blog.cloudflare.com/how-we-b...-the-internet/

Cloudflare has an enormous amount of infrastructure. If I were one of their engineers, I would start by putting it into production on a fraction of the infrastructure, monitoring that and expanding from there. The monitoring will likely help to catch reliability bugs, but as far as security bugs go, those will not be caught by monitoring, since you need malicious packets being sent to the servers and until they open source it, outside of fuzzing, the black hat community will have no clue how to send malicious packets to their servers.

Rewrite is hard and it could be buggy at first, but not every rewrite produce more bugs.

Planning not to have any bugs is a recipe for disaster. Anything non-trivial will have many bugs and the first thing that compiles will undoubtedly have an even higher number of bugs. Mozilla, which invented Rust, did not take such an approach to Rust. They waited 5 years before introducing Rust to firefox, by reusing the "stable" portions of the Servo codebase that they had been developing for 5 years.

Just because people don't often rewrite software doesn't mean every rewrite produces more bugs, it's simply that rewrite is very hard and resource consuming.

Rewrites are hard and resource consuming in large part because you need to catch and fix all of the bugs that they introduce.

Getting to the same level as a mature solution takes time. To give a tangible example, we are seeing this right now with Intel's graphics drivers playing catch up with Nvidia's graphics drivers.

Rust do have a few ways of preventing high level logic bugs.
For example, rust has type builder https://www.reddit.com/r/rust/commen...ecked_builder/ which makes sure that you cannot pass invalid combination of values into the builder.

There's also NonZeroUsize, which guarantees that it contains a non-zero usize and creating an instance would check its value and returns an Option<NonZeroUsize>.
And often crates create their own newtype uphold the invariants.

This communicates the invariant explicitly to the user, though the programmer could obviously just ignore it and go head to pass an invalid one, but still using this pattern is much better than not.

A high level logic bug would be something where you cannot have a checker that will identify what is correct unless the checker is checking a proof of correctness for the software as part of formal verification. Here is an example of one of the more expensive ones:

http://edition.cnn.com/TECH/space/99...ars.metric.02/

Here is another example of a high level logic bug where they made a mistake transcribing mathematical equations:

https://medium.com/lessons-from-hist...n-23651aba474d

Interestingly, there are limits to Rust's guarantees even with "safe" Rust. If you use an out of bounds index in a way that the Rust compiler cannot detect in advance, it will terminate the program. Do that based on untrusted inputs in a daemon that provide a network service (e.g. as part of Pingora) and you have a DoS vulnerability. Rust being "memory safe" does not prevent out of bounds issues from being security problems, although it does change those security problems into DoS vulnerabilities. If such a bug exists in Pingora, then Cloudflare could see their CDN trivially disabled by a DDoS attack that operates by exploiting that bug rather than saturating bandwidth, but at least the Pingora code is memory safe.

That said, there is Clippy, which likely helps, provided that people use it:

https://github.com/rust-lang/rust-clippy

[NobodyXu]

I said almost and next to no. Firefox’s incorporation of code that was 5 years old from the servo project is not a counter example to that.

Did you ignore that in Android 13, Google rewrote the low-level driver into Rust?
And cargo itself is production ready.

I don't think it's fair to say "almost and next to no".

As for Pingora, they have fewer crashes, but there is no evidence that there are fewer bugs.

The same can be said about every project, including your mature software.
You don't know a bug is present until it's found, so lacks of bug report does not mean lacks of bug.

Not every bug involves a crash and those that do not involve things that Rust can prevent are the categories of bugs that are likely to be in abundance until the software matures.

They already use it in production.

I imagine that one reason that cloudflare has not released the source code to Pingora is that they have no confidence that they have done sufficient hardening against such bugs.

Because this is their proprietary software and it's part of their core business.
Would you expect Google to release its search engine code as open source?

It's already stated that this is a proprietary project by Cloudflare and they have no plan to open source it from day 0.

The fact that Cloudflare is using it where they get GB or TB level of data per second in their data center means they have confidence in it.

There is plenty of backing for that. It is the reason why people do not rewrite mature software from scratch very often. The result is always very buggy at first. The main problem common to both C and Rust is that getting high level logic right in non-trivial software is hard. Rust does not prevent bugs from issues in high level logic. Getting reliable software requires time for the software to mature such that those logic issues are identified and corrected, even without memory issues.

Rewrite is hard and it could be buggy at first, but not every rewrite produce more bugs.
Just because people don't often rewrite software doesn't mean every rewrite produces more bugs, it's simply that rewrite is very hard and resource consuming.

Rust do have a few ways of preventing high level logic bugs.
For example, rust has type builder https://www.reddit.com/r/rust/commen...ecked_builder/ which makes sure that you cannot pass invalid combination of values into the builder.

There's also NonZeroUsize, which guarantees that it contains a non-zero usize and creating an instance would check its value and returns an Option<NonZeroUsize>.
And often crates create their own newtype uphold the invariants.

This communicates the invariant explicitly to the user, though the programmer could obviously just ignore it and go head to pass an invalid one, but still using this pattern is much better than not.

[ryao]

There is, it's used in firefox, android 13 low-level driver wrote in Rust https://security.googleblog.com/2022...ndroid-13.html, cargo, and cloudflare recently rewrites its nginx + lua into rust called pingora https://www.phoronix.com/news/CloudF...ngora-No-Nginx.

I said almost and next to no. Firefox’s incorporation of code that was 5 years old from the servo project is not a counter example to that.

As for Pingora, they have fewer crashes, but there is no evidence that there are fewer bugs. Not every bug involves a crash and those that do not involve things that Rust can prevent are the categories of bugs that are likely to be in abundance until the software matures. I imagine that one reason that cloudflare has not released the source code to Pingora is that they have no confidence that they have done sufficient hardening against such bugs. Once they publish it, black hats will look for bugs in it and if they find any that they can exploit, they will attack cloudflare using them. If they want to sleep well after publication, they must gain very high confidence that the code is at least as secure as what it replaced. They are likely trying to identify and squash as many bugs as they can before they publish the source code.

And your claim that any software rewrite creates more bug is dubious, there is no backing to that.
Just stop and go back to OSS development, there seems to no point in continue arguing which just waste your time.

There is plenty of backing for that. It is the reason why people do not rewrite mature software from scratch very often. The result is always very buggy at first. The main problem common to both C and Rust is that getting high level logic right in non-trivial software is hard. Rust does not prevent bugs from issues in high level logic. Getting reliable software requires time for the software to mature such that those logic issues are identified and corrected, even without memory issues.

[NobodyXu]

There is almost no mature software written is rust. There is next to no widely deployed software written in rust (and a few tiny parts of Linux 6.1 and later do not count). There is no data to support such an idea (and Mozilla’s merger of the stable parts of a 5 year old code base into Firefox is consistent with the idea that code written in Rust needs time to mature, not the idea that Rust magically makes code reliable from day 1). Looking at a deficit of bugs that Rust can eliminate is not sufficient to suggest that the mere use of Rust produces reliable software without any time for it to mature.

There is, it's used in firefox, android 13 low-level driver wrote in Rust https://security.googleblog.com/2022...ndroid-13.html, cargo, and cloudflare recently rewrites its nginx + lua into rust called pingora https://www.phoronix.com/news/CloudF...ngora-No-Nginx.

As I said previously, those who do not remember history are doomed to repeat it. This is the same “it will fix everything” mentality we see every decade over the latest idea or language. While Rust does plenty of things right, you cannot just reinvent non-trivial software in Rust and have a production solution. Software development does not work that way, no matter how much the compiler does for you.

I don't think Rust can fix everything, but it can significantly reduce memory related bugs and guarantee that there is no memory bugs in safe code.

And your claim that any software rewrite creates more bug is dubious, there is no backing to that.
Just stop and go back to OSS development, there seems to no point in continue arguing which just waste your time.

I agree that OpenZFS is an awesome piece of software, but there is no need to get defensive for this.
It will be an awesome piece of software even if some technically-more-advanced alternatives come.

[ryao]

No it does not, no formal verification can do that its actually impossible and there is a proof of that, see https://en.wikipedia.org/wiki/G%C3%B...eness_theorems. Any form of formal verification is proving a set of properties out of all possible properties because practical speaking for any trivial program that isn't just adding 2 numbers, there are certain properties that you cannot prove.

I already addressed your misuse of Godel’s theorems.

Its quite clear you actually don't understand what you are talking about, formal verification or otherwise

Project as much as you want. That does not make it true.

The sound static analysis you are talking about with C or C++ only works with very specific subsets of those languages because otherwise its impossible to verify anything practical. Both of these languages let you point to any arbitrary address in memory, and the minute you are allowed to do that any kind of static analysis is thrown out of the window (thats just one example).

A number of them do, but astree no longer claims to have such limitations.

Case in point MISRA C (which is one of the common solutions for safety critical systems) is a subset of C and the static analysis tools that are part of that ecosystem only work if you code in that specific subset. If your argument is that you can take any C/C++ codebase and do static analysis on it to formal verify certain properties, well then all I can say is good luck because you will need it.

The documentation published by Absint suggests it is possible with their software, which was created by the team that invented abstract interpretation. I have not tried it yet, but given its creator, I am inclined to believe the claims.

The advantage of Rust here is that by design that limited subset is the default, and nothing is preventing additional static analysis ontop of Rust if you want to prove more properties.

It would need to be sound static analysis, since normal static analysis does not prove properties.

i am just pointing out you have no idea what you are talking about on topics like formal verification or type systems, whether you work on ZFS or not is irrelevant on that point. I studied this at university, and I know people both in academia and industry who specialize precisely in this field and the kind of comments that you state are typical of someone who only has a surface level understanding of some topic while also being overly conservative because of "experience".

Which university so I can consider it for my list of universities that issue worthless degrees?

Its also quite clear you didn't read any of the material I gave you

I do not waste my time reading things people regurgitating what they heard send me, since it does not make a difference. For what it is worth, I hold degrees in both CS and mathematics. I already know what Godel’s incompleteness theorems are.

Firstly, it’s not my realization, it’s yours. I have been saying this consistently for the entire time but for whatever reason you get defensive when someone points an inconvenient truth which causes you to either not read and/or not comprehend things correctly.

What is inconvenient is that for non-trivial software, you do not reach the same level of reliability merely by using rust. Instead, it takes years of development and testing to get to that level and while you can avoid a good number of bugs by using Rust, it does not avoid enough bugs for you to produce the same quality of software without time for it to mature.

Thats an assumption in your head, I have already stated that software is being rewritten in Rust as we speak and there is zero evidence that generally speaking such rewrites introduce new bugs to a significant degree (in fact there is evidence of the opposite). I provided evidence of this earlier, you completely ignored it.

There is almost no mature software written is rust. There is next to no widely deployed software written in rust (and a few tiny parts of Linux 6.1 and later do not count). There is no data to support such an idea (and Mozilla’s merger of the stable parts of a 5 year old code base into Firefox is consistent with the idea that code written in Rust needs time to mature, not the idea that Rust magically makes code reliable from day 1). Looking at a deficit of bugs that Rust can eliminate is not sufficient to suggest that the mere use of Rust produces reliable software without any time for it to mature.

I get it, you don't like that and it doesn't fit your world view but maybe instead of arguing for 5 pages you should actually spend 10 minutes understanding how type systems in the context of formal methods works, maybe you will learn something new.

I know how type systems work. I also know that they are not a silver bullet. Not every bug is a matter of getting the type correct.

As I said previously, those who do not remember history are doomed to repeat it. This is the same “it will fix everything” mentality we see every decade over the latest idea or language. While Rust does plenty of things right, you cannot just reinvent non-trivial software in Rust and have a production solution. Software development does not work that way, no matter how much the compiler does for you.

[mdedetrich]

You compared what the Rust compiler does to formal verification.

You are the one who compared what the Rust compiler does to formal verification. You demonstrated ignorance on this topic.

You compared what the Rust compiler does to formal verification. You might have worked with people who did formal verification, but you clearly did not.

Formal verification implies that all of the bugs are fixed, since bugs are only possible when the specification is violated and formal verification proves that the specification is not violated.

No it does not, no formal verification can do that its actually impossible and there is a proof of that, see https://en.wikipedia.org/wiki/G%C3%B...eness_theorems. Any form of formal verification is proving a set of properties out of all possible properties because practical speaking for any trivial program that isn't just adding 2 numbers, there are certain properties that you cannot prove.

Its quite clear you actually don't understand what you are talking about, formal verification or otherwise

Their achievements are not your achievements and those industries are using C or C++ with sound static analysis ti get stronger guarantees than Rust can give when unsafe rust is needed.

The sound static analysis you are talking about with C or C++ only works with very specific subsets of those languages because otherwise its impossible to verify anything practical. Both of these languages let you point to any arbitrary address in memory, and the minute you are allowed to do that any kind of static analysis is thrown out of the window (thats just one example).

Case in point MISRA C (which is one of the common solutions for safety critical systems) is a subset of C and the static analysis tools that are part of that ecosystem only work if you code in that specific subset. If your argument is that you can take any C/C++ codebase and do static analysis on it to formal verify certain properties, well then all I can say is good luck because you will need it.

The advantage of Rust here is that by design that limited subset is the default, and nothing is preventing additional static analysis ontop of Rust if you want to prove more properties.

ZFS is still more mission critical than anything you have developed. I had been being polite, but you decided to throw stones from your glass cave. Competence in a subject is a prerequisite for being able to recognize competence in a subject and if we are going to degenerate to accusing people of not knowing things (or having poor reading comprehension), then just comparing what the two of us have done would indicate that you are the clueless one.

I am just pointing out you have no idea what you are talking about on topics like formal verification or type systems, whether you work on ZFS or not is irrelevant on that point. I studied this at university, and I know people both in academia and industry who specialize precisely in this field and the kind of comments that you state are typical of someone who only has a surface level understanding of some topic while also being overly conservative because of "experience".

Its also quite clear you didn't read any of the material I gave you

If you realize that Rust’s borrow checker cannot check for everything

Firstly, its not my realization, its yours. I have been saying this consistently for the entire time but for whatever reason you get defensive when someone points an inconvenient truth which causes you to either not read and/or not comprehend things correctly.

then you should realize that new software written in Rust needs time to mature before it is reliable, such that a rewrite in Rust is a recipe for a period of time where things are less reliable.

Thats an assumption in your head, I have already stated that software is being rewritten in Rust as we speak and there is zero evidence that generally speaking such rewrites introduce new bugs to a significant degree (in fact there is evidence of the opposite). I provided evidence of this earlier, you completely ignored it.

I get it, you don't like that and it doesn't fit your world view but maybe instead of arguing for 5 pages you should actually spend 10 minutes understanding how type systems in the context of formal methods works, maybe you will learn something new.

[ryao]

For starters I never said that Rust's borrow checker can check for all possible bugs, thats impossible (see Gödel’s incompletness theorem), I said that a specific subset of memory access bugs can be formally verified and large set of that subset of errors are security issues (inclusive of the one mentioned in this thread).

You compared what the Rust compiler does to formal verification.

In the area of formal verification, Gödel’s incompletness theorems suggest at most the possibility that a subset of software exists that cannot be formally verified as being free of bugs, but for software outside of that subset, you can in theory prove the absence of bugs with formal verification, even if it is not feasible to do in practice.

Do you even know what formal verification is? Its a process, not some magic wand. There are many ways to do formal verification and it all depends on context. For example the formal verification of C would look completely different to the formal verification of a program written in Rust because the former is completely loosely typed.

You are the one who compared what the Rust compiler does to formal verification. You demonstrated ignorance on this topic.

Again you twisted my words and created a strawman. I know what formal verification is, I worked with colleagues at uni who developed the sel4 which is the only non trivial formally verified microkernel (see https://sel4.systems/). And somewhat similarly (but not exactly the same), that microkernel's specification is written in Haskell and uses Haskell's type system as part of the formal verification process (there are other steps onto of this as well).

You compared what the Rust compiler does to formal verification. You might have worked with people who did formal verification, but you clearly did not.

Again attacking a strawman, I never said that Rusts borrow checker will magically fix all bugs. I said there are a certain subset of bugs that it can prove won't happen which naturally means you have less bugs to worry about.

Formal verification implies that all of the bugs are fixed, since bugs are only possible when the specification is violated and formal verification proves that the specification that the code is supposed to match is not violated provided that the machine behaves as modeled.

As I said before, I know people that worked on sel4 which have even higher reliability guarantees than ZFS, we are talking about a kernel that is used in defence, medical industries, aviation and so on.

Their achievements are not your achievements and those industries are using C or C++ with sound static analysis to get stronger guarantees than Rust can give when unsafe rust is needed.

ZFS doesn't have a formal proof, it has empirical proof and that is not the same. sel4 does have formal verification/proof, but just like Rust's borrow checker it also cannot check for everything.

If you realize that Rust’s borrow checker cannot check for everything, then you should realize that new software written in Rust needs time to mature before it is reliable, such that a rewrite in Rust is a recipe for a period of time where things are less reliable.

As for checking for everything, formal verification implies that all of the bugs are fixed, since bugs are only possible when the specification that the code is supposed to match is violated and formal verification proves that the specification is not violated provided that the machine behaves as modeled. This goes well beyond what Rust’s compiler can check, even when ignoring unsafe rust.

That said, I had been being polite, but you decided to throw stones from your glass cave. ZFS’ lack of formal verification does not preclude it from being under higher reliability requirements than anything you have written. You can do plenty of background research on the topic of formal verification to regurgitate what you read to sound like you have a clue, but comparing the rust compiler to formal verification showed that you are clueless. Maybe you will learn something from doing research to pretend you know things, although I doubt you will admit it.

[mdedetrich]

Rust code can have CVEs too, especially since CVEs are not solely concerned with the classes of bugs that Rust is supposed to avoid. Make a big enough codebase in Rust that is really important and there will be no end to its CVEs.

You clearly have issues with reading comprehension.

For starters I never said that Rust's borrow checker can check for all possible bugs, thats impossible (see Gödel’s incompletness theorem), I said that a specific subset of memory access bugs can be formally verified and large set of that subset of errors are security issues (inclusive of the one mentioned in this thread).

You should have a read of https://dl.acm.org/doi/10.1145/1111037.1111056

The only way to avoid CVEs is to do formal verification, but that is too hard to do for large codebases.

Do you even know what formal verification is? Its a process, not some magic wand. There are many ways to do formal verification and it all depends on context. For example the formal verification of C would look completely different to the formal verification of a program written in Rust because the former is completely loosely typed.

You have no clue what formal verification is if you think it is only concerned with memory errors and other things that can be caught by static analysis. You can have bugs that do not involve memory errors and those bugs can be security issues. Here is a prominent example:

Again you twisted my words and created a strawman. I know what formal verification is, I worked with colleagues at uni who developed the sel4 which is the only non trivial formally verified microkernel (see https://sel4.systems/). And somewhat similarly (but not exactly the same), that microkernel's specification is written in Haskell and uses Haskell's type system as part of the formal verification process (there are other steps onto of this as well).

There are other ways of having bugs, such as high level logic issues that nothing Rust does will prevent, since those cannot be caught by static analysis. Formal verification, unlike a compiler, will catch such bugs. To elaborate on how much more intelligent formal verification is, let us say that you have a formally verified compiler (note that the only one that exists is for C) and you replace the source code with the source code for awk (to give an extreme example). The verifier will complain that it is not what it is supposed to be. If you replace valid source code with valid source code that does something completely different, the rust compiler will not tell you it is not what it is supposed to be. Formal verification catches all bugs in code, including high level logic bugs. Putting an entirely different codebase that does something completely different in place of the source code for your software would be an extreme example of a high level logic bug.

Again attacking a strawman, I never said that Rusts borrow checker will magically fix all bugs. I said there are a certain subset of bugs that it can prove won't happen which naturally means you have less bugs to worry about.

You seem to be arguing that has zero benefit.

[QUOTE=ryao;n1372619]
That said, since the conversation has degenerated to you saying that I do not know what I am “talking about”, let me end this. The reliability requirements for the filesystem code that I write are likely far higher than those for any of the code you write, so between the two of us, when we differ on how to write reliable software, you are the one who has no idea what he is saying. I already considered a rewrite in Rust and my conclusion was that it is a recipe for more problems for many years until it reaches maturity. It might have fewer problems after maturation than the C code has today, but the 5 to 7 year disruption that would involve would be better spent improving the existing C code and it is likely that the end result of continuing to improve the C code would be similar with much less disruption. It is not just me who says this. Everyone I know who is responsible for software reliability came to the same conclusion. Just about everyone responsible for the reliability of mature code bases is also saying that rewrites in Rust are not worthwhile. That is also why Linus Torvalds is not embarking on a journey to rewrite Linux in Rust, but is accepting it for new drivers/QUOTE]

As I said before, I know people that worked on sel4 which have even higher reliability guarantees than ZFS, we are talking about a kernel that is used in defence, medical industries, aviation and so on.

ZFS doesn't have a formal proof, it has empirical proof and that is not the same. sel4 does have formal verification/proof, but just like Rust's borrow checker it also cannot check for everything. sel4 happens to guarantee many more things then Rust's borrow check and its also in different domain, but that also makes it less practical to use.

[ryao]

Yet, Jolla (in 2014) decided to use Wayland.

There is no single way of doing things.

[Berniyh]

X11 works on smart phones (see OpenMoko) and on multi-monitor setups with different refresh rates. The thing that it cannot handle is a multi-monitor setup with monitors sharing the same X screen with VRR thrown into the mix. You need different X screens for that.

Saying “there was a lot of effort to fix it and it's well structured code now” means that it is mature code since that is basically the definition of mature code. Also, your link says “using it to drive your display hardware and multiplex your input devices is choosing to make your life worse”. We have direct rendering manager with kernel modesetting and libinput now, so those things have already been moved outside of the xorg server and the result works well.

Yet, Jolla (in 2014) decided to use Wayland.