Announcement

Collapse
No announcement yet.

X.Org Server Hit By New Local Privilege Escalation Vulnerability

Collapse
X
 
  • Filter
  • Time
  • Show
Clear All
new posts

  • NobodyXu
    replied
    ryao Thank you for the kind words!
    I will look into it by first doing some toy projects.

    Leave a comment:


  • ryao
    replied
    Originally posted by NobodyXu View Post

    Yeah, I can see making static analyzer is very hard, same for compiler and optimizer.
    Making a static analyzer is easy. You can do it easily by modifying a compiler such as LLVM/Clang to implement a check and that would give you a static analyzer. You can also just make a coccinelle check and that itself would be a static analyzer. There is a very low bar for making a static analyzer since it only requires you to be able to check for a bug without executing the program.

    Making a sound static analyzer is hard. A sound static analyzer is one where the absence of reports proves an absence of the kinds of bugs that it is designed to catch. Also, writing a compiler is easy in comparison to writing a compiler that is formally verified to produce correct code.

    Note that easy and hard here are relative things. I wrote a toy compiler in college and it was challenging, but doable. Writing a C to x86 compiler would have been a few steps above that in difficulty. Adding formal verification to verify the compiler output is always correct is a level of difficulty so great that few would be willing to attempt it.
    Last edited by ryao; 24 April 2023, 11:12 AM.

    Leave a comment:


  • NobodyXu
    replied
    Originally posted by ryao View Post
    Maybe if the idea had mainstream mindshare, we would see some corporate backed OSS projects to make them appear, although the biggest impact would be in making them for C, so getting them made for Rust would be an uphill battle. If you are interested in having them for Rust, perhaps you could start developing your own. It could very well be the hardest intellectual undertaking you will ever make and I am not saying that to belittle you. Hard is simply not enough to describe the development of these tools. Such an endeavor is too mathematical for most programmers and too much of a programming problem for most mathematicians. That is the main reason the rest of the industry pursues half measures rather than the development of sound static analysis tools.
    Yeah, I can see making static analyzer is very hard, same for compiler and optimizer.

    I certainly want to help here, but I would have to take my time to learn more about them first.

    Originally posted by ryao View Post
    The only reason we have them is because a few computer scientists, such as the guy who invented the theory that enables their creation, were stubborn and kept moving forward with it despite everyone else in the field pursuing easier things. They took decades of work by multiple people to make and the early versions only worked on subsets of languages since handling things like recursion, dynamic memory allocations and concurrency made a hard problem even harder.

    That said, if you are interested in this, the following might be a decent starting point for developing a sound static analyzer for Rust:

    A library for building abstract interpretation-based analyses - GitHub - seahorn/crab: A library for building abstract interpretation-based analyses


    I also read about one for Rust in the academic paper that I linked in a previous post, but it was made for the sake of writing a paper and is likely far from a production ready solution.
    Thank you, I appreciate the information you've provided.

    Originally posted by ryao View Post

    You might incorrectly think that evaluating all of those possibilities is impossible, but it is often possible to reduce things to a number of cases. That is how the proof of the 4 color theorem, a fact that applies to the infinite number of possible maps, was achieved:



    If I recall correctly, they reduced the infinite set of possible maps down to a less than 2 thousand (and later a few hundred) cases. Sound static analysis tools similarly reduce the number of things that they must consider to something manageable while still covering all possible program inputs.
    I will look into that, thanks.

    Originally posted by ryao View Post

    Lastly, Rust really is just the next iteration in the cycle of people inventing new languages to solve perceived problems, only for the new languages to have problems too. Here is a list:

    * Programming is too slow. Let’s make FORTRAN.
    * FORTRAN is a pain to read. Let’s make COBOL.
    * Both of those are not great. let’s make ALGOL.
    * None of that is portable, let’s make C.
    * C has problems because it is too simple. Let’s make C++ to solve all of the problems from the simplicity.
    * C++ has too many problems from complexity. Let’s make Java.
    * All of those others have problems, Let’s make Rust.

    We are here. I guarantee that the future holds:

    * Rust has problems. Let’s make …
    There sure will be new PLs to solve problems, especially when such problem too hard to fix in the original PL without breaking most if not all code.

    There are already new PL out there that uses a different way to solve memory safety while claiming to make writing code easier with less unsafe, especially for self-reference structure using an arena-like allocator.

    It sounds interesting, but it takes time to mature.

    There are also interpreter and other PLs with a GC that adopts some Rust features, enough to say that new PLs will eventually come out that will be even better,

    Leave a comment:


  • NobodyXu
    replied
    [QUOTE=ryao;n1382550]
    Sound static analysis is from the domain of formal verification, where you can prove such properties against a model. The main limitation is whether the model and reality truly match. If you get a “memory safety issue” in a program proven to have no memory safety issues because of a bad sys call implementation, then it is not a bug in the program. The program has perfect memory safety, so debugging a “memory safety issue” in it means you would be looking at layers beneath the program such as the toolchain, kernel or the hardware.

    If you use a library that is not verified by astree (and raw assembly would fall into this category), then you can have issues from that, but I would not be concerned about the glue assembly used to make syscalls. It is literally just putting arguments into the correct registers and executing an instruction to tell the CPU to invoke an interrupt service routine. That is so simple that it does not have room for subtle bugs, so if something were wrong in it, everything would be broken.


    I was not referring to that kinds of bugs that are external, which is not the program's fault.

    Imagine you are using file backed mmap and you mapped the same region twice but without using volatile, the it's clearly going to have UB which compiler assumes the memory is immutable and never changes between different reads that even static analyzer has a hard time detecting.

    The unsafe about assembly is not just about mistakes in these assemblies themselves, but also the power they bring.
    E.g. you can use them to configure memory sharing for external GPUs, DMA and etc, it's easy to introduce UB where immutability is broken or having multiple mutations.

    Originally posted by ryao View Post
    Anyway, Astree does not make guarantees about the kernel, hardware or tool chain. Those are out of scope for whether a program has memory safety. If you are concerned about them, then your only real choice would be C since C is the only language with a formally verified compiler that will never introduce bugs that do not exist in the source code:



    Also, the seL4 kernel has a proof of correctness:



    You can use those to build a highly reliable system as far as the software running on the cpu is concerned. As for hardware, it is primarily a two factor problem. One factor is whether the hardware behaves according to the verilog. There are techniques such as radiation hardening that can be applied to gain assurance of that:



    The second factor is whether the verilog is correct. It is possible in theory to formally verify the verilog, although I am not aware of anyone that has fully done that. Intel began to use formal methods to semi-formally verify their verilog after the fdiv bug, although they reportedly became more lax after 2015 (or was it 2016?). They still have a number of CPU errata since they have not fully verified all of the properties of their CPUs. Hence why what they do is semi-formal verification.

    A third factor might be power delivery, and you would want to talk to an electrical engineer about how to gain assurances of that, although redundant PSUs and other things used in datacenters likely help there.
    Thanks, I will look into seL4.

    For verified optimization, cranelift is working on formal verification and added a lot of fuzzing https://bytecodealliance.org/article...-progress-2022

    They also put a lot of work into Correctness in Register Allocation by building a symbolic checker and use it as a fuzzing oracle:



    Originally posted by ryao View Post
    Anyway, that is the state of the art in terms of having a reliable machine. It would be wrong to claim that verification of no runtime issues in high level source code leaves memory safety issues. Any remaining “memory safety issues” are in a different layer and that layer needs attention independently of the program on top. This fixation with memory safety issues itself is somewhat odd since if you are going to start nitpicking, there is always the elephant in the room of whether the software is fit for its purpose. To illustrate that:

    http://blog.branchpoint.net/wp-conte...lly_wanted.png
    I agree that there are other bugs that need to be solved, what I was saying that it is still possible to have UB despite using static analyzer.

    Leave a comment:


  • NobodyXu
    replied
    Then you will see people similar to yourself saying to rewrite everything to solve all of the problems in mature Rust code.
    ryao Just to clarif, I never said this

    I'm only saying that Rusr is a much better designed PL and all new projects should use Rust right now.
    I've never said something that every project should get rewritten to Rust nor will it solve all the problems

    I did question on whether all rewrites introduce more bugs, but that is another topic.

    ryao Weasel Please do not make assumptions about words I never said.
    Maybe you somehow imply that if I support Rust that much, support rewrite and argue Rust is a better PL, that I would support all projects to be rewritten in Rust.

    No I absolutely do not support that and did not say or imply that, it's reasonable for some projects to just keep using their existing tools, especially legacy projects that are under maintenance or does not add any new feature or only add small new feature once a while.

    For the rest, whether to rewrite is a hard question depending on the project itself, their resource and etc, so I will not make any claim for them at all since they have to be evaluated per-project.

    Leave a comment:


  • ryao
    replied
    Originally posted by NobodyXu View Post
    And there are tools to address that out-of-bound abort issue, like no-panic https://github.com/dtolnay/no-panic/ , which rustc should pick up, to prevent any assertion failure, plus you can also disable indexing by using #[forbid(clippy::indexing_slicing)] and force the programmer to use the slice::get API which returns Option<T> and you must check the return value manually.

    You can also disable unwrapping Option/Result using #![deny(clippy::unwrap_used)] and #![deny(clippy::expect_used)] to prevent such abortion.
    While that helps, these tools are not sound tools and they do not address the additional issues in unsafe Rust. Rust needs sound tools that apply to the entire language to reach the same level as C verified by a sound tool such as astree, but making sound tools is hard, especially for more complex languages. C++ only gained them as extensions of the ones for C. The result is that those who want high assurance software would just use C/C++. That produces a chicken and egg problem for other languages since people will not use languages that do not have such tools for high assurance software development, but without high assurance software development being done in other languages, there is no financial incentive to develop sound tools for them.

    Maybe if the idea had mainstream mindshare, we would see some corporate backed OSS projects to make them appear, although the biggest impact would be in making them for C, so getting them made for Rust would be an uphill battle. If you are interested in having them for Rust, perhaps you could start developing your own. It could very well be the hardest intellectual undertaking you will ever make and I am not saying that to belittle you. Hard is simply not enough to describe the development of these tools. Such an endeavor is too mathematical for most programmers and too much of a programming problem for most mathematicians. That is the main reason the rest of the industry pursues half measures rather than the development of sound static analysis tools.

    The only reason we have them is because a few computer scientists, such as the guy who invented the theory that enables their creation, were stubborn and kept moving forward with it despite everyone else in the field pursuing easier things. They took decades of work by multiple people to make and the early versions only worked on subsets of languages since handling things like recursion, dynamic memory allocations and concurrency made a hard problem even harder.

    That said, if you are interested in this, the following might be a decent starting point for developing a sound static analyzer for Rust:

    A library for building abstract interpretation-based analyses - GitHub - seahorn/crab: A library for building abstract interpretation-based analyses


    I also read about one for Rust in the academic paper that I linked in a previous post, but it was made for the sake of writing a paper and is likely far from a production ready solution.

    Also, it is rather fashionable to invent a new language to try to address problems rather than fixing the actual problems, so I expect someone to invent yet another language that is incorrectly billed as the solution to all woes before anyone can finish developing a production quality sound static analysis tool for Rust. Then you will see people similar to yourself saying to rewrite everything to solve all of the problems in mature Rust code. A rewrite will undoubtably introduce more problems than the existing code had until the new code has had sufficient time to mature. Of course, those people will deny it. However, the truth is that it will be worse than the existing code. The reason is the same reason why we have software bugs in the first place, which is that the space of states and state transitions are too big for humans to consider without formal methods. Just 1MB has over 10^300000 different possible states and the potential transitions between those states are even more numerous. Mature software has had many of the common problems in the huge state transition space ironed out, but new software will have them simply because the humans writing the software will not realize the problems are there as they create them. :/

    You might incorrectly think that evaluating all of those possibilities is impossible, but it is often possible to reduce things to a number of cases. That is how the proof of the 4 color theorem, a fact that applies to the infinite number of possible maps, was achieved:



    If I recall correctly, they reduced the infinite set of possible maps down to a less than 2 thousand (and later a few hundred) cases. Sound static analysis tools similarly reduce the number of things that they must consider to something manageable while still covering all possible program inputs.

    Lastly, Rust really is just the next iteration in the cycle of people inventing new languages to solve perceived problems, only for the new languages to have problems too. Here is a list:

    * Programming is too slow. Let’s make FORTRAN.
    * FORTRAN is a pain to read. Let’s make COBOL.
    * Both of those are not great. let’s make ALGOL.
    * None of that is portable, let’s make C.
    * C has problems because it is too simple. Let’s make C++ to solve all of the problems from the simplicity.
    * C++ has too many problems from complexity. Let’s make Java.
    * All of those others have problems, Let’s make Rust.

    We are here. I guarantee that the future holds:

    * Rust has problems. Let’s make …
    Last edited by ryao; 12 April 2023, 12:21 PM.

    Leave a comment:


  • Weasel
    replied
    Originally posted by NobodyXu View Post
    That is exactly what I said, no tool can achieve perfect memory safety.
    You have to have an escape patch.
    No static analyzer, borrow checker, etc can completely eliminate memory bugs.
    Yeah, but you're missing the point. It's about the code it can verify itself.

    For example, even if it literally verified ALL the code, including kernel and everything, and guaranteed it to be "safe", your computer could still crash or corrupt memory due to... faulty hardware or random bit flips from cosmic rays and so on.

    That doesn't say anything about the tool. The code itself is correct. The fault lies somewhere else.

    You can't even be 100% sure no corruption will happen. That's besides the point of the tool. Such tools are intended for you to correct your code. Not someone else's code. Not the hardware or the laws of physics.

    Leave a comment:


  • ryao
    replied
    Originally posted by NobodyXu View Post
    No tool can achive perfect memory safety at compile time, all they can do is to prove a subset of the program to be safe at compile time unless that program does not involve any assembly, syscall, external I/O or memory sharing using page table or whatever.

    I bring it up because ryao said that Astree can achieve 100% memory safety, but I know for sure no tool can achieve that, not static analyzer that checks every path or borrow checker, or mir's stack borrower or the new tree borrower model or Java's GC.
    Sound static analysis is from the domain of formal verification, where you can prove such properties against a model. The main limitation is whether the model and reality truly match. If you get a “memory safety issue” in a program proven to have no memory safety issues because of a bad sys call implementation, then it is not a bug in the program. The program has perfect memory safety, so debugging a “memory safety issue” in it means you would be looking at layers beneath the program such as the toolchain, kernel or the hardware.

    If you use a library that is not verified by astree (and raw assembly would fall into this category), then you can have issues from that, but I would not be concerned about the glue assembly used to make syscalls. It is literally just putting arguments into the correct registers and executing an instruction to tell the CPU to invoke an interrupt service routine. That is so simple that it does not have room for subtle bugs, so if something were wrong in it, everything would be broken.

    Anyway, Astree does not make guarantees about the kernel, hardware or tool chain. Those are out of scope for whether a program has memory safety. If you are concerned about them, then your only real choice would be C since C is the only language with a formally verified compiler that will never introduce bugs that do not exist in the source code:



    Also, the seL4 kernel has a proof of correctness:



    You can use those to build a highly reliable system as far as the software running on the cpu is concerned. As for hardware, it is primarily a two factor problem. One factor is whether the hardware behaves according to the verilog. There are techniques such as radiation hardening that can be applied to gain assurance of that:



    The second factor is whether the verilog is correct. It is possible in theory to formally verify the verilog, although I am not aware of anyone that has fully done that. Intel began to use formal methods to semi-formally verify their verilog after the fdiv bug, although they reportedly became more lax after 2015 (or was it 2016?). They still have a number of CPU errata since they have not fully verified all of the properties of their CPUs. Hence why what they do is semi-formal verification.

    A third factor might be power delivery, and you would want to talk to an electrical engineer about how to gain assurances of that, although redundant PSUs and other things used in datacenters likely help there.

    Anyway, that is the state of the art in terms of having a reliable machine. It would be wrong to claim that verification of no runtime issues in high level source code leaves memory safety issues. Any remaining “memory safety issues” are in a different layer and that layer needs attention independently of the program on top. This fixation with memory safety issues itself is somewhat odd since if you are going to start nitpicking, there is always the elephant in the room of whether the software is fit for its purpose. To illustrate that:

    Last edited by ryao; 12 April 2023, 09:24 AM.

    Leave a comment:


  • NobodyXu
    replied
    ryao Weasel Let's take a step back here and let me clarify my stands:

    No tool can achive perfect memory safety at compile time, all they can do is to prove a subset of the program to be safe at compile time unless that program does not involve any assembly, syscall, external I/O or memory sharing using page table or whatever.

    I bring it up because ryao said that Astree can achieve 100% memory safety, but I know for sure no tool can achieve that, not static analyzer that checks every path or borrow checker, or mir's stack borrower or the new tree borrower model or Java's GC.

    In fact, you could have race condition in Java, so memory safety in Java means no use-after-free, out-of-bound and etc but does not include thread safety.

    I totally agree on the fact that borrow checker cannot prove the entire program to be safe, only a subset, and that its out-of-bounds checking isn't good enough for critical program, that's why I've found the claim that Astree is 100% memory safe quite confusing and plainly wrong.

    Though I do think using Rust in web browser, Linux kernel, web servers, etc and anything not critical like avaiation is fine, since it's not like they cannot tolerate abort, in fact abortion on out-of-bound or an internal critical assertion failure is better for them than silently corrupt and taking over by attackers.

    Leave a comment:


  • NobodyXu
    replied
    Originally posted by ryao View Post
    Designing these tools requires having a very accurate model of how those operations work. It is proven within the model. Every remark you make here can be used against Rust, so I am not sure how this helps your “Rust is the answer” argument. Rust gives much weaker guarantees than Astree does across the board.
    I didn't say that Rust is better, I'm just saying that no tool can achieve perfect memory safety.

    And I never claim Rust is the answer for every single project.
    What I'd claim is that Rust is a better PL than C.

    As for the memory safety guarantees, I agree that Astree guarantees is stronger than Rust's default in terms of out-of-bound access, but I still consider Rust to be a much better pl than C, not just because of additional features, but also because the default behavior of panic on out-of-bound is strictly better than silent corruption anyway and one branch for bound checking is quite cheap in a lot of situations.

    And there are tools to address that out-of-bound abort issue, like no-panic https://github.com/dtolnay/no-panic/ , which rustc should pick up, to prevent any assertion failure, plus you can also disable indexing by using #[forbid(clippy::indexing_slicing)] and force the programmer to use the slice::get API which returns Option<T> and you must check the return value manually.

    You can also disable unwrapping Option/Result using #![deny(clippy::unwrap_used)] and #![deny(clippy::expect_used)] to prevent such abortion.

    Leave a comment:

Working...
X