Robigalia: seL4 and Rust
robigalia.org
robigalia.org
I didn't plan on posting this for another week :( There's a bunch of stuff that still needs doing, especially with docs and tutorials. The writing on the website is only a first draft. There are also no easy tasks for new contributor onboarding at this point in time, which I think is really important before anouncing a new project.
This largely started as a learning project by me and a few of my friends at uni last semester. A lot of people were interested in it, so we (I) decided to take it somewhere.
Here's the announcement email draft:
https://lists.robigalia.org/pipermail/robigalia-dev/2016-Jan...
https://gandro.github.io/2015/09/27/rust-on-rumprun/
https://polyfractal.com/post/adding-a-disk-to-a-rust-rumprun...
More info about L4 micro-kernel:
https://sel4.systems/Info/FAQ/
Now user-level here means drivers as well. So that would be interesting how it would work with Rust. Will it all default to unsafe code and just end up with pointer twiddling and memory overwrites and all the same errors. I hope not.
Currently it seems that the verification mode had DMA turned off and for SMP they run a kernel instance on each core and then send messages to each other via shared memory. That probably means not load balancing or not scheduling?
It shows a variety of ways to safely wrap unsafe code and then provide strongly-typed safe interfaces to the hardware, no pointer twiddling required. A particularly good example is the section "Some Clever Solution" in the "Page Tables" post.
I was looking at the printing to screen section:
http://os.phil-opp.com/printing-to-screen.html
It is so helpful to have the explanation of what is going and why the code looks the way it is, what are some alternatives and why those wouldn't work.
This goal fills me with nerd lust. Getting ourselves a secure foundation to build on doesn't solve all our problems (not by a long shot), but such a drastic reduction in attack surface would be an incredible achievement.
I remember a L4 talk in which the speaker showed how more than 95% of the code of new OSes where devoted to being POSIX compatible and yet they 1) lacked a lot of features 2) missed many edge cases 3) had to modify their beautiful kernel design to accommodate POSIX use cases.
I think the only way forward is to do like Plan9 did. Just forget about POSIX and implement your own set of primitives (but first study what has been done in the last 40 years!). POSIX compatibility can come later with 80/20 library that maps POSIX calls and behaviour to the new primitives.
And maybe POSIX is not needed at all. If your OS is interesting enough people will add #ifdef'd code for your platform, just like many UNIX-y applications do now for Android, OS X or Windows.
Android, for these purposes, is, of course, Linux with a different libc, so most of the POSIXy stuff is there, even if bionic is pretty awful.
The solution high assurance security adopted was to virtually or physically isolate a UNIX/Linux stack that interacted with security-critical software that ran directly on microkernel and through mediated interfaces. This resulted in commercial work like INTEGRITY-178B and LynxSecure with Nizza, Perseus, and OKL4/OKLinux in OSS space. Look up "Mikro-SINA VPN" (yes with a k) for great case study. Middleware like Camkes was developed for integration. Similarly, kernels like INTEGRITY and PikeOS developed safe/secure runtimes that ran directly on kernel for Ada and Java.
What this project and all others like it need to do is this:
A. Drop all efforts at rebuilding UNIX in language X.
B. Get a user-mode version of Linux running on it with user-space drivers on microkernel for one, easily-acquired board.
C. Redirect safe language efforts on creating a secure runtime on the microkernel.
D. Create middleware tools along lines of Protocol Buffers, ZeroMQ, or LANGSEC stuff. These should allow seemless, efficient integration between untrusted (esp GUI) stuff in Linux VM and trusted stuff in safe lang uage runtime.
E. Begin on a POSIX-like runtime whose components can be stripped on a case-by-case basis. Focus on syscalls used by critical libraries and services first.
F. The current goal of full POSIX. 99% dont make it to E. If they get here, then great. If to E, then we get at least some apps. If to C and D, then we at least have trustworthy runtime.
That's my two cents worth and builds on what's historically happened in these efforts.
... OK, but then you say "full POSIX" later. So how does that differ?
> B. Get a user-mode version of Linux running on it with user-space drivers on microkernel for one, easily-acquired board.
How is this relevant to what happens later? The whole goal is to not rely on the Linux kernel.
> C. Redirect safe language efforts on creating a secure runtime on the microkernel.
There aren't "safe language efforts". There is a safe language that already exists, and the effort has already been expended to make that exist. The project is creating a secure runtime on the microkernel using that safe language.
> D. Create middleware tools along lines of Protocol Buffers, ZeroMQ, or LANGSEC stuff
You mean like serde? This is already done for the Rust ecosystem.
> E. Begin on a POSIX-like runtime whose components can be stripped on a case-by-case basis. Focus on syscalls used by critical libraries and services first.
How is this not what this project is doing?
> F. The current goal of full POSIX. 99% dont make it to E. If they get here, then great. If to E, then we get at least some apps. If to C and D, then we at least have trustworthy runtime.
... in other words, exactly what the project is doing?
This is a different project.
In this case, it would be a RTOS or user-mode Linux, plus a custom runtime or target for Rust apps, and IPC/middleware to connect the two. Way easier to build. POSIX comes later if effort comes along.
Im glad your doing it gradually with intermediates. That will let it benefit spinoff projects or even products hopefully. Plus keep you from getting overloaded.
I also like that RISC-V is in your long-term vision. Keeping that in mind early will help avoid architectural mistakes early on. Id say use the ISA closest to it in meantime so little change is necessary.
Far as overall scheme, I'll email you some reference work if your interested in prior work on safe runtimes, split apps, high-security dev techniques, and so on. Might be able to integrate that into idiomatic Rust. That's your call though.
You did notice how I went from an extremely hard task (full POSIX) to a series of them that gradually deliver more and more useful functionality over time if resources and labor permit? First goal is a runtime. Next is key POSIX features (80/20 rule). Next is full POSIX. If you cant do a runtime, you cant do POSIX.
Re B
Linux kernel is a user-mode API that gets you lefacy apps inmediately. You gradually replace the syscalls with your own and eventually get off it. Meanwhile, critical stuff runs outside Linux VM on a Rust runtime directly on microkernel or other trusted components. WAY better than just Linux kernel.
Re C
No, there are dozens of projects trying to make OS'S or runtimes in safe languages. There's closer to 100 that started as learning projects then petered out when hard reality set in. Dead link after dead link. Hence, I said it in plural as my recommendation and gradual progression applies to most. Including a Rust project.
Re D
Im not a Rust user so that's new to me. Good to know they have it. Thanks for tip.
Re E
You addressed that point in isolation. The context is a series of steps with gradual increase of difficulty and intermediate deliverables. Starting at Step 5 is clearly not my recommendation.
Re F
And Step 6 follows Step 5 if author had skill and resources to achieve it. Starting at Step 6, like 5, dramatically increases odds it will be another entry in archive.org rathet than protecting real systems.
More to point, I can name many systems that tool my route to success even on a budget and some resisting NSA pentesting w/ source. Maybe it's ny broken memory but I can't name even one project that implemented POSIX in a safe language clean slate. Hence, my recommendation.
Whether the C side IR has enough debug metadata or could be annotated automatically would be the make or break.
Real problem with your scheme is that the typing and structure are important to effectively using Rust. Those that you get in LLVM will be nothing like what you would want in Rust and you'll need additional information. In other words, source to source with annotations is a better option.
Rust is a good choice given its adoption. Only if they focus on a runtime instead of POSIX, though.
Rust has effectively no runtime these days. Same amount as C or C++, basically.
http://os.phil-opp.com/entering-longmode.html
Interesting stuff and seems like a good description of the code. Bookmarking it in case I do more in this area.
The reason you'd want to combine seL4 with Rust is to give confidence that (a) the core part of the system (microkernel) works right and that (b) the less core parts of the system (drivers, libc) are least free from nasty memory safety problems. To a first approximation, it's a compromise between a project like the OS in the "Writing an OS in Rust" series, which guarantees memory safety but doesn't guarantee that any part of the system actually does the right thing, and a hypothetical fully formally-verified OS, which is (with current technology) something that would be way too expensive and time-consuming to be practical.
" In short, the implementation is proved to be bug-free (see below). This also implies a number of other properties, such as freedom from buffer overflows, null pointer exceptions, use-after-free, etc.
There is a further proof that the binary code which executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary.
Furthermore, there are proofs that seL4's specification, if used properly, will enforce integrity and confidentiality, core security properties. Combined with the proofs mentioned above, these properties are guaranteed to be enforced not only by a model of the kernel (the specification) but the actual binary that executes on the hardware. Therefore, seL4 is the world's first (and still only) OS that is proved secure in a very strong sense.
Finally, seL4 is the first (and still only) protected-mode OS kernel with a sound and complete timeliness analysis. Among others this means that it has provable upper bounds on interrupt latencies (as well as latencies of any other kernel operations). It is therefore the only kernel with memory protection that can give you hard real-time guarantees."
https://blogs.microsoft.com/cybertrust/2007/08/23/the-ethics...
The system he refers to is here:
http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf
The seL4 team certainly built tools to make the job easier. However, their work takes even more effort than the development of some early designs. Lipner and others indicated it took several quarters to turn a major change on a product. Schell's company usually quoted 2 years per new design based on their highly-assured GEMSOS kernel. The STOP OS, INTEGRITY-178B, and VxWorks MILS similarly moved slowly in new features due to assurance requirements. Now, most of these were evaluated against all kinds of security and functional criteria whereas seL4 just did development assurance: other stuff for seL4 is ongoing research at NICTA while finished for alternatives. So, in some ways it's less work and others it's a lot of work.
So, rule of thumb is that you will have these issues: less features, slower development, slower time-to-market (critical weakness), slower maintenance, less HW support, possibly worse interface/management, and performance hits potentially. Also, worst part is that anything you apply high assurance to that hasn't been dealt with in CompSci requires fresh R&D then the actual work. That with time-to-market and feature gap were huge, deal-breakers in the past.
So, all that might be fine depending on the nature of the problem. It might not even all show up in the project. Yet, you should assume it because it showed up in many projects and products before. Still does. It's just that high assurance systems are precise, labor-intensive, custom developments that also require uncommon to rare expertise. No wonder seL4 is still behind even ancient QNX in what it can pull off and is actually behind the separation kernels in functionality. Assurance target just makes it that much harder. Maybe labor available, too.