nomicon
seL4
Our great sponsors
nomicon | seL4 | |
---|---|---|
87 | 60 | |
1,682 | 4,516 | |
3.3% | 1.2% | |
5.5 | 9.0 | |
12 days ago | 5 days ago | |
CSS | C | |
Apache License 2.0 | GNU General Public License v3.0 or later |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
nomicon
-
[Media] I'm comparing writing a double-linked list in C++ vs with Rust. The Rust implementation looks substantially more complex. Is this a bad example? (URL in the caption)
it’s even written by the same person that wrote the Nomicon (the guide to the dark arts of unsafe)
-
Rust books to read
If you want to dive deeper you can always have other options but now there are concrete cases, if you want to do low level thing https://doc.rust-lang.org/nomicon/ while if you want multi thread/concurrency stuff https://marabos.nl/atomics/ . There are many many books so you will have to point yourself to what you want
-
Unsafe Rust
Nice video! Glad I could help out. This stuff is hard, and I'm still learning a lot about it myself even years later. The Rustonomicon is a great read if you haven't already.
-
Stepping up the YAML engineer game
Have you got a moment to read through the good book , after reading through this perhaps try the Rustonomicon.
- Questions about ownership rule
-
How to write deserializer for custom binary protocol?
However, this is a wide topic out of scope for a Reddit comment, so maybe just read the Rustonomicon. It explains everything about data handling in Rust.
-
Performance critical ML: How viable is Rust as an alternative to C++
The ownership model & borrow checker makes rust a bit of an awkward language in which to write complex data structures like trees and graphs. It can be done - since you can always use raw pointers & unsafe code when you absolutely need to to treat rust like C. But the language fights you, and the community can get a bit moralistic about this sort of thing. The rust nomicon is a fantastic resource for learning the limits of the borrow checker, and where and how to use unsafe code correctly. You will need unsafe less than you think you will, but sometimes you will have no choice.
-
Sudo and Su Being Rewritten in Rust for Memory Safety
That's a really good point that I feel like isn't talked about enough. Unsafe rust is a lot harder to write correctly than bog standard C, because you have to uphold the invariants to avoid undefined behavior (1). It's why there's a whole ebook about it (2).
That doesn't mean it's impossible to write correct unsafe code, it's just not as obvious as "trust me bro I know better than borrowck." You can't actually elide the invariants Rust upholds, you just have to take over from the compiler when it can't prove them.
(1) https://doc.rust-lang.org/reference/behavior-considered-unde...
-
C++ to Rust Books?
If you are interested in the theoretical stuff that doesn't have much overlap with C++, give the Nomicon a try, or even Learn Rust the Dangerous Way.
-
How can I use rust libraries in zig/C
There's also cbindgen for automating the generation of C headers once you've got your code in the right shape and you'll also want to read the Rustonomicon.
seL4
-
From L3 to seL4 what have we learnt in 20 years of L4 microkernels? [video]
> People like to snob Unix but the fact is: the world runs on Unix.
The world you are aware of runs on it.
> Can we really do that much better or is it just hubris?
Yes. Have a look at seL4[1] and Barrelfish too[2], even though that's no longer active. seL4 in particular is powering a lot of highly secure computing systems. There is a surprisingly large sphere outside of Unix/POSIX.
-
On the Costs of Syscalls
There are also RTOS-capable microkernels such as seL4[0], with few but extremely fast syscalls[1]. Note times are in cycles, not usec.
-
Can the language of proof assistants be used for general purpose programming?
https://sel4.systems
Working on a number of platforms, verified on some. Multicore support is an ongoing effort afaict.
On OS built on this kernel is still subject to some assumptions (like, hardware working correctly, bootloader doing its job, etc). But mostly those assumptions are less of a problem / easier to prove than the properties of a complex software system.
As I understand it, guarantees that seL4 does provide, go well beyond anything else currently out there.
-
Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs
You can use it to (mostly) validate small snippets are the same. See Alive2 for the application of Z3/formalization of programs as SMT for that [1]. As far as I'm aware there are some problems scaling up to arbitrarily sized programs due to a lack of formalization in higher level languages in addition to computational constraints. With a lot of time and effort it can be done though [2].
-
What are the current hot topics in type theory and static analysis?
Formal methods. This is not in most general-purpose programming languages and probably never will be (maybe we'll see formal methods to verify unsafe code in Rust...) because it's a ton of boilerplate (you have to help the compiler type-check your code) and also extremely complicated. However, formal methods is very important for proving code secure, such as sel4 (microkernel formally verified to not have bugs or be exploitable) which has just received the ACM Software Systems Award 3 days ago.
- Rust Now Available for Real-Time Operating System and Hypervisor PikeOS
-
A plan for cybersecurity and grid safety
Efforts: seL4, Project Everest, the Prossimo project of the ISRG, Let's Encrypt, and Prusti for the Rust language
- Better not fire anyone now
-
Linux Kernel Ksmbd Use-After-Free Remote Code Execution Vulnerability
Yet another exploit that just wouldn't be possible on a well-designed system, such as Genode[0] with seL4[1].
Monolithic UNIX clones are an anachronism we should get rid of.
-
Pegasus spyware was used to hack reporters’ phones. I’m suing its creators; When you’re infected by Pegasus, spies effectively hold a clone of your phone – we’re fighting back.
There is also a long-term idea with Qubes OS of supporting seL4 as a secure kernel (although there are issues to fix first, some of which also make it clear just why seL4 sees few mention as far as desktops go right now - these are the practical issues I was mentioning).
What are some alternatives?
book - The Rust Programming Language
mdBook - Create book from markdown files. Like Gitbook but implemented in Rust
rust-ffmpeg - Safe FFmpeg wrapper.
Theseus - Theseus is a modern OS written from scratch in Rust that explores 𝐢𝐧𝐭𝐫𝐚𝐥𝐢𝐧𝐠𝐮𝐚𝐥 𝐝𝐞𝐬𝐢𝐠𝐧: closing the semantic gap between compiler and hardware by maximally leveraging the power of language safety and affine types. Theseus aims to shift OS responsibilities like resource management into the compiler.
Exercism - website - The codebase for Exercism's website.
l4v - seL4 specification and proofs
fprime - F´ - A flight software and embedded systems framework
miri - An interpreter for Rust's mid-level intermediate representation
patterns - A catalogue of Rust design patterns, anti-patterns and idioms
CompCert - The CompCert formally-verified C compiler
CppCoreGuidelines - The C++ Core Guidelines are a set of tried-and-true guidelines, rules, and best practices about coding in C++
unsafe-code-guidelines - Forum for discussion about what unsafe code can and can't do