8 ms·

Tangentially, I'd have loved to see a modern, (se)L4 based desktop (general purpose) operating system, capabilities-based, with services written in a safe langu

by senko 2y ago

Tangentially, I'd have loved to see a modern, (se)L4 based desktop (general purpose) operating system, capabilities-based, with services written in a safe language, with no legacy (POSIX) baggage. Failing that, I hope to be able to hack on something along those lines when I retire :) (before someone mentiones Fuchsia - Zircon is cool'n'all, but we're talking about L4 here)

throwawaymaths 2y ago
Safe what? Rust isn't memory safe if you are using unsafe anywhere. There are other "safety" issues with rust as well. Sel4 is in c but it's provably safe (if you're on arm).
- junon 2y ago
  This comment demonstrates a lack of understanding of what the unsafe keyword is for in Rust. Unsafe specifically states that no code within it may introduce UB after the unsafe block exits (post-condition). It also doesn't allow certain operations no matter how hard you try (e.g. the borrow checker still applies, but you can use raw pointers in ways you couldn't outside of an unsafe block, assuming you don't introduce UB). As someone designing a kernel in Rust, you literally cannot avoid unsafe code, regardless of the language, to implement a kernel. It's worth mentioning that "unsafe" and "vulnerable" are two different things. SeL4 is safe because of its extensively verified codebase written in a language suited for verification. Last I checked they port it to C after the fact, but it could just as well be ported to Rust. It'd still be "unsafe" but significantly less "vulnerable". For example, modifying cr3 or TTBRn_EL1 is incredibly unsafe. But it happens all the time when context switching. In the kernel I use `unsafe` pretty commonly to denote functions with preconditions not representable by the type system. This enforcement wouldn't even be possible in C or any other language I know of personally that'd be efficient to write an OS in. The only gripe I have with Rust's unsafe is that I can't mark methods with preconditions as unsafe while still requiring `unsafe` clauses within the function body. I've thought about opening an RFC for `unsafe(pub)` for this reason. But doing so has made iteration and overall safety of the codebase much easier to reason about because it forces me to think about every call site in which I might introduce a problem if not done carefully.
  - pizlonator 2y ago
    The point still stands: rust isn’t memory safe if you use unsafe. It’s true that to write a kernel safely, you need more than memory safety, but that’s kind if a different point. Folks don’t just use the unsafe construct in Rust to do kernely things.
    - junon 2y ago
      > rust isn’t memory safe if you use unsafe. Did you read my comment at all? How do you define "memory safe"?
      - pizlonator 2y ago
        Yeah I read it. I define memory safe as: Any program accepted by the compiler follows the typing rules of the language. That holds for Rust if you don’t use unsafe at all. It also holds in other memory safe languages (like JavaScript). Some memory safe languages gaurantee this without any caveats (JavaScript) while others guarantee it with caveats (Rust if you don’t use unsafe, Java if you don’t use certain APIs, etc).
  - throwawaymaths 2y ago
    > SeL4 is safe because of its extensively verified codebase written in a language suited for verification I think this is incorrect. It is written in C, compiled to arm assembly, and the assembly is analyzed and checked by Isabelle/HOL.
    - junon 2y ago
      You may be right, I was under the impression that the Haskell version was the verified version.
      - CarpaDorada 2y ago
        Section 3 in the whitepaper <https://sel4.systems/About/seL4-whitepaper.pdf https://sel4.systems/About/seL4-whitepaper.pdf> describes how it is done: (1) they restrict themselves to a possible-to-reason subset of C (that they have a parser in Isabelle for), and implement a kernel and prove the implementation is formally correct, and (2) to avoid compiler/kernel bugs of host & trojan horses, they verify the compiled/linked output as well. Their Figure 3.2 shows how this is done: each transformation into the "Graph Language" nodes is proven formally correct. They need two proofs because the binary is automatically proven correct, i.e. what they prove is that their formalized binary is equivalent to the original binary using a HOL4 disassembler, without knowing what sort of binary they have at their hands. On the C side, they preserve semantics while proving the program correct (manually, i.e. they wrote the proofs themselves), and then they prove the two are equivalent, again automatically, using SMT solvers and throwing small chunks of data at it. As they explain, proving the two "Graph Language" representations to be equivalent semantically is, in general, undecidable like the halting problem. However, they get away with it because the C compiler is not too wild in its output.
- senko 2y ago
  I didn't neccessarily mean Rust, but was curios to see how that would look. Here's a Rust demo implementation of the seL4 root task (the first process that gets started on boot) using their Rust SDK and it doesn't look like it's using unsafe anywhere: https://github.com/seL4/rust-root-task-demo/blob/main/crates/example/src/main.rs https://github.com/seL4/rust-root-task-demo/blob/main/crates... (I don't speak Rust so I might have missed it). Go might be another interesting choice. (let's not turn this thread into Rust vs Go vs whatever agaaaaaain ... we've got enough of those please).
mech422 2y ago
This(1)(2) might hold you over for a bit: "Genode's microkernel architecture, capability-based security, sandboxed device drivers, and virtual machines in a novel operating system for commodity PC hardware and the PinePhone. Sculpt is used as day-to-day OS by the Genode developers. " It looks pretty neat - could be fun to play with! 1) https://genode.org/ https://genode.org/ 2) https://genode.org/download/sculpt https://genode.org/download/sculpt They
- mikewarot 2y ago
  Genode Sculpt releases, in April and October, are where they roll out user interface and other visible upgrades that form a complete system. I'm hoping to make it my daily driver in the near future.
  - mech422 2y ago
    Oh! How is it for a dev. box ?? Can you get gcc/clang/rust/python ? Does it have a decent browser and code editor? It sounds like fun to play with - I've been wanting to try something new...
    - snvzz 2y ago
      They have native 3d acceleration, native modern web browser and virtualization support to e.g. run Linux and any non-ported software on that. Genode is no joke.
      - mech422 2y ago
        Thanks man - definitely gonna have a go at then :-)
- codethief 2y ago
  > Genode is based on a recursive system structure. Each program runs in a dedicated sandbox and gets granted only those access rights and resources that are needed for its specific purpose. Programs can create and manage sub-sandboxes out of their own resources, thereby forming hierarchies where policies can be applied at each level. Damn, I've been hoping someone would create something like this for quite some time!
mlinksva 2y ago
Same. I still check ~yearly https://news.ycombinator.com/item?id=25554912 https://news.ycombinator.com/item?id=25554912 to see if Robigalia is progressing (sadly it seems the website has casino spam on it now, cmrx64 in case you look for mentions) or someone else has taken up the mantle. I haven't looked much further but some indication https://d3s.mff.cuni.cz/files/teaching/nswi161/martin-decky-microkernels-capabilities.pdf https://d3s.mff.cuni.cz/files/teaching/nswi161/martin-decky-... Huawei is doing interesting work.
- cmrx64 2y ago
  I don’t look for mentions, but how could i miss this thread ;) The new authoritative link is <https://rbg.systems https://rbg.systems>; a DNS registration oversight has that spam parked on the old site :( I still dream about taking that project back up. Maybe there’s some way to find funding for it… otherwise i am currently looking for a job (if anyone reading wants to hire me :) Check out https://www.dbos.dev/ https://www.dbos.dev/ for a different take on “persistent OS”, i think it’s neat!
  - snapplebobapple 2y ago
    Out of curiosity what would it cost to hire you to work on rdg project full time?
    - cmrx64 2y ago
      90k USD per yr should do it. I don’t have the skills/inclination/bullshit tolerance to deal with any kind of SBIR or VC, tho i did briefly explore the SBIR route with the encouragement of a brave collaborator (we visited DARPA together)
nineteen999 2y ago
> with no legacy (POSIX) baggage. Cool, who's going to write all the new software for your platform?
- pjmlp 2y ago
  It worked pretty well for Apple, Google and Microsoft.
pjmlp 2y ago
Currently Android is the best we have gotten thus far in that sense. - Managed userspace - OS services can be written in Java/Kotlin if desired, and some actually are. - NDK has a limited set of use cases, mainly for writing native method implementations, 3D rendering and real time audio, and POSIX isn't officially supported beyond to what ISO C and ISO C++ require for their standard libraries implementation. Naturally OEMs and people that root their devices, push stuff directly with ADB to their phones in developer mode have a different view, but I am writing from the point of view of how the OS behaves in normal devices, by people that don't even know there is such thing as the magic incantation to enable developer mode. Is this the best we can have, I surely hope not. I also would like to see something similar, but industry always takes one step forward, two back, in this kind of stuff. By the way, look into TamaGo, Go based toolchain for bare metal programming firmware. https://www.phoronix.com/news/TamaGo-Bare-Metal-Go-ARM https://www.phoronix.com/news/TamaGo-Bare-Metal-Go-ARM
- ActorNightly 2y ago
  I wouldn't call Android even close to micro. Its just a different linux kernel. You would be best off getting like an SoC with wifi and display and usb ports. There are quite a few floating around these days that you can get a 3d printed case for.
andreww591 2y ago
It's not completely "legacy-free", nor is it purely capability-oriented, but I'm writing a QNX-like OS (https://gitlab.com/uxrt/uxrt-toplevel https://gitlab.com/uxrt/uxrt-toplevel) based on a kernel forked from seL4 with a preference for servers written in safer languages. Even though it is going to be fairly Unix-like it will diverge from conventional Unix in a number of ways and either discard or demote quite a few legacy Unix features. For example, there will be no support for reversion to the traditional Unix security model in the core OS, with the base VFS implementing a security model based on a mix of per-process ACLs and capability transfers, and on top of that there will be a role-based access control model (there will be a fakeroot-type compatibility layer that simulates traditional Unix security within an environment constrained by the native security model). I don't think there's a good way to make a purely capability-oriented general-purpose OS since as soon as you have a way to look up files by human-readable names instead of capabilities your OS is no longer purely capability-oriented. IMO most of the issues with typical Unix-like OSes are more due to specific outdated architectural features rather than the Unix API or shell environment. A lot of what could be done with a completely new OS could instead be done by designing a Unix-like OS for extensibility by reducing the core API down to a small set of file calls that act as an IPC transport layer and name service and then building everything on top of that, building object-oriented wrapper libraries on top of the filesystem, and reimplementing the traditional Unix APIs outside the core filesystem ones on top of the newer APIs. Existing applications could be ported to such a system incrementally rather than having to do everything all at once or relegate them to some kind of limited "penalty box" compatibility layer (and any binary compatibility layer for Linux or other conventional Unices would integrate better into such a system than into something completely new).

by senko 2y ago

throwawaymaths 2y ago

Safe what? Rust isn't memory safe if you are using unsafe anywhere. There are other "safety" issues with rust as well. Sel4 is in c but it's provably safe (if you're on arm).

junon 2y ago
This comment demonstrates a lack of understanding of what the unsafe keyword is for in Rust. Unsafe specifically states that no code within it may introduce UB after the unsafe block exits (post-condition). It also doesn't allow certain operations no matter how hard you try (e.g. the borrow checker still applies, but you can use raw pointers in ways you couldn't outside of an unsafe block, assuming you don't introduce UB). As someone designing a kernel in Rust, you literally cannot avoid unsafe code, regardless of the language, to implement a kernel. It's worth mentioning that "unsafe" and "vulnerable" are two different things. SeL4 is safe because of its extensively verified codebase written in a language suited for verification. Last I checked they port it to C after the fact, but it could just as well be ported to Rust. It'd still be "unsafe" but significantly less "vulnerable". For example, modifying cr3 or TTBRn_EL1 is incredibly unsafe. But it happens all the time when context switching. In the kernel I use `unsafe` pretty commonly to denote functions with preconditions not representable by the type system. This enforcement wouldn't even be possible in C or any other language I know of personally that'd be efficient to write an OS in. The only gripe I have with Rust's unsafe is that I can't mark methods with preconditions as unsafe while still requiring `unsafe` clauses within the function body. I've thought about opening an RFC for `unsafe(pub)` for this reason. But doing so has made iteration and overall safety of the codebase much easier to reason about because it forces me to think about every call site in which I might introduce a problem if not done carefully.
- pizlonator 2y ago
  The point still stands: rust isn’t memory safe if you use unsafe. It’s true that to write a kernel safely, you need more than memory safety, but that’s kind if a different point. Folks don’t just use the unsafe construct in Rust to do kernely things.
  - junon 2y ago
    > rust isn’t memory safe if you use unsafe. Did you read my comment at all? How do you define "memory safe"?
    - pizlonator 2y ago
      Yeah I read it. I define memory safe as: Any program accepted by the compiler follows the typing rules of the language. That holds for Rust if you don’t use unsafe at all. It also holds in other memory safe languages (like JavaScript). Some memory safe languages gaurantee this without any caveats (JavaScript) while others guarantee it with caveats (Rust if you don’t use unsafe, Java if you don’t use certain APIs, etc).
- throwawaymaths 2y ago
  > SeL4 is safe because of its extensively verified codebase written in a language suited for verification I think this is incorrect. It is written in C, compiled to arm assembly, and the assembly is analyzed and checked by Isabelle/HOL.
  - junon 2y ago
    You may be right, I was under the impression that the Haskell version was the verified version.
    - CarpaDorada 2y ago
      Section 3 in the whitepaper <https://sel4.systems/About/seL4-whitepaper.pdf https://sel4.systems/About/seL4-whitepaper.pdf> describes how it is done: (1) they restrict themselves to a possible-to-reason subset of C (that they have a parser in Isabelle for), and implement a kernel and prove the implementation is formally correct, and (2) to avoid compiler/kernel bugs of host & trojan horses, they verify the compiled/linked output as well. Their Figure 3.2 shows how this is done: each transformation into the "Graph Language" nodes is proven formally correct. They need two proofs because the binary is automatically proven correct, i.e. what they prove is that their formalized binary is equivalent to the original binary using a HOL4 disassembler, without knowing what sort of binary they have at their hands. On the C side, they preserve semantics while proving the program correct (manually, i.e. they wrote the proofs themselves), and then they prove the two are equivalent, again automatically, using SMT solvers and throwing small chunks of data at it. As they explain, proving the two "Graph Language" representations to be equivalent semantically is, in general, undecidable like the halting problem. However, they get away with it because the C compiler is not too wild in its output.
senko 2y ago
I didn't neccessarily mean Rust, but was curios to see how that would look. Here's a Rust demo implementation of the seL4 root task (the first process that gets started on boot) using their Rust SDK and it doesn't look like it's using unsafe anywhere: https://github.com/seL4/rust-root-task-demo/blob/main/crates/example/src/main.rs https://github.com/seL4/rust-root-task-demo/blob/main/crates... (I don't speak Rust so I might have missed it). Go might be another interesting choice. (let's not turn this thread into Rust vs Go vs whatever agaaaaaain ... we've got enough of those please).

mech422 2y ago

This(1)(2) might hold you over for a bit: "Genode's microkernel architecture, capability-based security, sandboxed device drivers, and virtual machines in a novel operating system for commodity PC hardware and the PinePhone. Sculpt is used as day-to-day OS by the Genode developers. " It looks pretty neat - could be fun to play with! 1) https://genode.org/ https://genode.org/ 2) https://genode.org/download/sculpt https://genode.org/download/sculpt They

mikewarot 2y ago
Genode Sculpt releases, in April and October, are where they roll out user interface and other visible upgrades that form a complete system. I'm hoping to make it my daily driver in the near future.
- mech422 2y ago
  Oh! How is it for a dev. box ?? Can you get gcc/clang/rust/python ? Does it have a decent browser and code editor? It sounds like fun to play with - I've been wanting to try something new...
  - snvzz 2y ago
    They have native 3d acceleration, native modern web browser and virtualization support to e.g. run Linux and any non-ported software on that. Genode is no joke.
    - mech422 2y ago
      Thanks man - definitely gonna have a go at then :-)
codethief 2y ago
> Genode is based on a recursive system structure. Each program runs in a dedicated sandbox and gets granted only those access rights and resources that are needed for its specific purpose. Programs can create and manage sub-sandboxes out of their own resources, thereby forming hierarchies where policies can be applied at each level. Damn, I've been hoping someone would create something like this for quite some time!

mlinksva 2y ago

Same. I still check ~yearly https://news.ycombinator.com/item?id=25554912 https://news.ycombinator.com/item?id=25554912 to see if Robigalia is progressing (sadly it seems the website has casino spam on it now, cmrx64 in case you look for mentions) or someone else has taken up the mantle. I haven't looked much further but some indication https://d3s.mff.cuni.cz/files/teaching/nswi161/martin-decky-microkernels-capabilities.pdf https://d3s.mff.cuni.cz/files/teaching/nswi161/martin-decky-... Huawei is doing interesting work.

cmrx64 2y ago
I don’t look for mentions, but how could i miss this thread ;) The new authoritative link is <https://rbg.systems https://rbg.systems>; a DNS registration oversight has that spam parked on the old site :( I still dream about taking that project back up. Maybe there’s some way to find funding for it… otherwise i am currently looking for a job (if anyone reading wants to hire me :) Check out https://www.dbos.dev/ https://www.dbos.dev/ for a different take on “persistent OS”, i think it’s neat!
- snapplebobapple 2y ago
  Out of curiosity what would it cost to hire you to work on rdg project full time?
  - cmrx64 2y ago
    90k USD per yr should do it. I don’t have the skills/inclination/bullshit tolerance to deal with any kind of SBIR or VC, tho i did briefly explore the SBIR route with the encouragement of a brave collaborator (we visited DARPA together)

nineteen999 2y ago

> with no legacy (POSIX) baggage. Cool, who's going to write all the new software for your platform?

pjmlp 2y ago
It worked pretty well for Apple, Google and Microsoft.

pjmlp 2y ago

Currently Android is the best we have gotten thus far in that sense. - Managed userspace - OS services can be written in Java/Kotlin if desired, and some actually are. - NDK has a limited set of use cases, mainly for writing native method implementations, 3D rendering and real time audio, and POSIX isn't officially supported beyond to what ISO C and ISO C++ require for their standard libraries implementation. Naturally OEMs and people that root their devices, push stuff directly with ADB to their phones in developer mode have a different view, but I am writing from the point of view of how the OS behaves in normal devices, by people that don't even know there is such thing as the magic incantation to enable developer mode. Is this the best we can have, I surely hope not. I also would like to see something similar, but industry always takes one step forward, two back, in this kind of stuff. By the way, look into TamaGo, Go based toolchain for bare metal programming firmware. https://www.phoronix.com/news/TamaGo-Bare-Metal-Go-ARM https://www.phoronix.com/news/TamaGo-Bare-Metal-Go-ARM

ActorNightly 2y ago
I wouldn't call Android even close to micro. Its just a different linux kernel. You would be best off getting like an SoC with wifi and display and usb ports. There are quite a few floating around these days that you can get a 3d printed case for.

andreww591 2y ago

It's not completely "legacy-free", nor is it purely capability-oriented, but I'm writing a QNX-like OS (https://gitlab.com/uxrt/uxrt-toplevel https://gitlab.com/uxrt/uxrt-toplevel) based on a kernel forked from seL4 with a preference for servers written in safer languages. Even though it is going to be fairly Unix-like it will diverge from conventional Unix in a number of ways and either discard or demote quite a few legacy Unix features. For example, there will be no support for reversion to the traditional Unix security model in the core OS, with the base VFS implementing a security model based on a mix of per-process ACLs and capability transfers, and on top of that there will be a role-based access control model (there will be a fakeroot-type compatibility layer that simulates traditional Unix security within an environment constrained by the native security model). I don't think there's a good way to make a purely capability-oriented general-purpose OS since as soon as you have a way to look up files by human-readable names instead of capabilities your OS is no longer purely capability-oriented. IMO most of the issues with typical Unix-like OSes are more due to specific outdated architectural features rather than the Unix API or shell environment. A lot of what could be done with a completely new OS could instead be done by designing a Unix-like OS for extensibility by reducing the core API down to a small set of file calls that act as an IPC transport layer and name service and then building everything on top of that, building object-oriented wrapper libraries on top of the filesystem, and reimplementing the traditional Unix APIs outside the core filesystem ones on top of the newer APIs. Existing applications could be ported to such a system incrementally rather than having to do everything all at once or relegate them to some kind of limited "penalty box" compatibility layer (and any binary compatibility layer for Linux or other conventional Unices would integrate better into such a system than into something completely new).