Towards Linux Kernel Memory Safety
arxiv.org
arxiv.org
I'm kind of surprised that the authors went with compare-and-exchange for their ref count, rather than get-and-increment. Even if the counter does overflow, it's usually detectable, and reversible. This is true even in the face of concurrent updates. The benefit is that there is only one atomic operation in the fast path.
Huh. Even MSVC supports it (currently experimental though): https://blogs.msdn.microsoft.com/vcblog/2016/01/20/visual-st...
So it would only happen with a binary Ada library in two ways:
- the binary was manipulated and thus does not map to the original source code
- the code was compiled with permission for Uncheked packages enabled
In C, 100% of the source code is unsafe, specially when compiled with -O3.
This project is adding protection to the linux kernel. Now, this bounds checking could be added to a kernel build with 100% of the source code available, in which case all is good. Or, it could be added to a kernel build where some of the drivers are available only in a 'binary blob' form. In which case, rewriting the kernel in Ada (or whatever) would not help you with the binary blobs, since they are out of your control. So, as I understand it, your point of 'only working properly if 100% of the source code is available' would seem to be just as true for a code rewrite as it is for the paper's approach to the problem.
http://phrack.org/issues/64/6.html
"- separated kernel and process address space (both can use the whole address space). Such an implementation, to be efficient, requires a dedicated support from the underlaining architecture. It is the case of the primary and secondary context register used in conjunction with the ASI identifiers on the UltraSPARC (sun4u/sun4v) architecture.
The only limitation to kernel (and processes) virtual space on systems implementing an userland/kerneland separated address space is given by the architecture (UltraSPARC I and II can reference only 44bit of the whole 64bit addressable space. This VA-hole is placed among 0x0000080000000000 and 0xFFFFF7FFFFFFFFFF).
This memory model makes explotation indeed harder, because we can't directly dereference the userspace. The previously cited NULL pointer dereferences are pretty much un-exploitable. Moreover, we can't rely on "valid" userland addresses as a place to store our shellcode (or any other kernel emulation data), neither we can "return to userspace"."
This already exists on x86_64 Linux in the form of SMEP and SMAP.
> With SMEP enabled, it’s no longer possible to map exploit payloads in userland, as the CPU will trigger a fault if it attempts to execute those user pages in kernel mode
http://vulnfactory.org/blog/2011/06/05/smep-what-is-it-and-h...
> SMEP can be used to prevent supervisor-mode code from unintentionally executing user-space code. SMAP extends this protection to reads and writes
https://en.wikipedia.org/wiki/Supervisor_Mode_Access_Prevent...
These mitigations aren't overly novel at this point and don't prevent exploits (just complicates them). Here's a recent CVE PoC containing an SMEP and KASLR bypass: https://github.com/xairy/kernel-exploits/blob/master/CVE-201...
Full memory safety takes this much further, and should be far harder to bypass.
For example, the kernel repository for Redox (a written-in-Rust OS project) appears to have 242 usages of the unsafe keyword (including comments bc lazy), out of 18205 lines of Rust source.
You can wrap most unsafe operations to be safe with proper checks, I've done it myself and it's much less than you would expect since a lot of the memory accesses can be made safe trivially.
I would imagine that initially as PoC one can start by implementing a simple module... obviously a small portion of the Rust stdlib and runtime needs to be ported and of course rustc needs to be integrated into the kernel toolchain...
Perhaps someone has done it privately (i.e., without attempting to submit patches back to source)?
I don't think you actually solve any of the really hard kernel problems with your choice of programming language.
The big problems tend to be about hardware support
(all those drivers, all the odd details about different platforms,
all the subtleties in memory management and resource accounting)
In [2] (2013) he expands on that, essentially explaining how well C maps to machine instructions, and how that helps optimise the kernel.
Personally I think Rust maps very well to machine code, and although it doesn't solve design problems, I do think it saves a lot of time debugging the security flaws and bugs that can result from memory bugs.
[1] https://www.infoworld.com/article/3109150/linux/linux-at-25-... [2] https://www.reddit.com/r/programming/comments/1t0gfy/linus_t...
I don't see a strong argument against a memory-safe language, although granted it won't solve architectural and hardware issues. Perhaps the effort to support, say Rust, in the kernel is just not worth the trade-off at this point? Perhaps no one has taken on the mantle for doing so? But I can't see how one can categorically argue against it...
This is not how things work. You don't arrive at changes like this by out-talking Linus. Talk is cheap and Linus is opinionated.
You need to demonstrate that what you want to do is worthwile, i.e. is not only feasible but also provides a payoff that carries the weight of what you're proposing. You also need to be fiercely committed to your idea and to making it happen inside mainline Linux.
In other words, show me the code (and maintain it out-of-tree for some time, tracking upstream changes and gathering support from other developers).
I don’t think it’s far off, at least for vms, tbh.
Yeah that may be a really good upside to VMs, that they enable new OSs to have a more level playing field with the established OSs. Letting the VM layer handle all the messy details of real hardware.
That's one of the main advantages of C - it runs on pretty much everything.
https://fuchsia.googlesource.com/garnet/+/HEAD/public/rust/c...
I think Nim belongs with D here. You can freely disable the GC in Nim.
Full disclosure: I'm a Nim core dev.
Even current operating systems use forms of garbage collection (such as refcounting) to track resources.
And if both languages have GC, then you're in even more trouble.
The multiple GCs in a process issue is usually due to the collector not playing nice with signal/exception handler installation when using safepoints, which is purely an issue of lazy implementations. There's even ways to collect cross-heap cycles when working this multiple GCs (Xamarin on Android does this fairly well).
* Boxing anything you take a reference directly to
* Forbidding sum types and complicating the GC to allow interior pointers
* Forbidding references to value types
* A borrow checker
Guess which one is most flexible, and novel in Rust.
We only don't have it thanks to Compaq killing the project after acquiring DEC Olivetti. Politics as usual.
Rust ideas come from Cyclone and ATS, it is not novel in Rust.
The borrow checker still is pretty much WIP, that the NLL changes will surely improve, but don't not yet solve all ergonomic problems.
Cyclone and ATS do not have Rust's combination of ownership and borrowing.
Which should just use controlled types, pools or standard containers.
Also there are a few open experiments with Ada,
https://github.com/Lucretia/bare_bones
Then there are the commercial ones used in the industry, making use of bare metal profiles like Ravenscar.
> It replaces approximately 160,000 lines of C++ with 85,000 lines of Rust.
https://blog.rust-lang.org/2017/11/14/Fearless-Concurrency-I...
I agree with this. But just saying Firefox has X millions of lines of code doesn't say anything about the possibility for Linux to be ported to Rust.
I never said that. My whole premise is that you can't say anything like this by just saying code count on two very different projects. Maybe you didn't read my comments properly.
HN discussion: https://news.ycombinator.com/item?id=15179188
Cyclone only works because it uses garbage collection for the heap. There is a uniqueness extension, but it is limited compared to what Rust can do. (See Grossman's "Existential Types for Imperative Languages" presentation for details.) The uniqueness extension was not designed to (and is not flexible enough to) supplant the garbage collector in most real-world projects.
This theoretical static checker for C code would not be compatible with virtually any existing C code in the wild, and so it would be effectively a new language.
The use of dynamic allocation must be carefully restricted and programmer may need to provide provide assertions or modify the code to pass verification.
There is two ways tho think static verification:
1. Language level verification. All valid programs are verified to be correct in respect of safety guarantees the language gives.
2. Verification of safety features that can't be proved in general. In most cases it's possible to write program in a way that it can be verified to be correct, but finding a way to write provably correct program may need some work.
There might exist logical bugs, but the language semantics allow for a higher thrust of code quality, assuming the binaries haven't been tampered with.
Every line of C code is unsafe, specially if the binary was compiled with -O3.
Regarding Rust, the only issue is lack of support for binary libraries in Cargo, one needs to call rustc directly.
Not even Frama-C can prevent all use cases, if developers don't care.
There is no way to corrupt memory in Ada unless you explicitly import one of the Unchecked packages and ask the compiler permission to do naughty stuff.
and yet even ADA's standard library sometimes has bugs: http://blog.adacore.com/formal-verification-of-legacy-code
However C gets the usual set of logical errors, common to any safe programming language, memory corruption caused by lack of checks on memory access and implicit type conversions, and 200+ cases of UB when taking advantage of full compiler optimizations.
Reducing the amount of possible errors per line of code is already a plus, even if doesn't remove all of them.
Memory safe languages are not panacea, not even close, and especially not in an operating system.