The amount of security critical infrastructure that runs on single core CPUs with a MMU seems to be be very small. The world just doesn’t use a lot of single core CPUs with memory protection nowadays.
Which got me thinking: why has eChronos development ceased? It seems like it would have the lower technical complexity threshold to get to a useful commercial result.
The main difference between RTOSes like eChronos and seL4 is the MMU – without MMU or at least an MPU the kernel cannot protect itself from user-level code and user-level code from each other, so verification can only be conditional on user-level code not behaving maliciously.
That means seL4 can enforce security properties like integrity without knowing what user-level code is in the system, and eChronos cannot.
As Gerwin says, without memory protection you can’t isolate the OS from applications, or applications from each other. Some of this can be achieved with an MPU, as most Arm-M processors have it, and there’s MPU support in eChronos.
While it is true that many (possibly most in pure processor numbers) critical systems run on microcontrollers without memory protection, these systems are highly vulnerable. And with mushrooming functionality and processor consolidation (eg in cars) this model is reaching its use-by date. (Happened in phones about 20 years ago…)
As Gerwin says, without memory protection you can’t isolate the OS from applications, or applications from each other. Some of this can be achieved with an MPU, as most Arm-M processors have it, and there’s MPU support in eChronos.
Most baseband processors have an MPU. These are generally closed loop systems and would be ripe for targeted policies. For example, Australia could place a small per-unit tax on every smartphone vendor over a certain volume if their baseband isn’t running a formally verified OS.
While it is true that many (possibly most in pure processor numbers) critical systems run on microcontrollers without memory protection, these systems are highly vulnerable.
Can’t an IR like WASM do fine grained memory isolation within a single address space?
My apologies if the above comes across as stupid: I don’t do low-level programming or systems development. SeL4 is amazing and I look forward to bullet-proof hypervisors being built on it. Everything seems ready to click into place and whether it would have been better to start with embedded is largely a moot point.
However, I would like to understand the strategy. AFAICT embedded seems like the ideal place to start as the MVP would be cheaper (simpler vertically integrated product line with low churn codebases) and this is where corporations seem to be willing to spend money on security (boot integrity, crypto operations, etc).
What do I not understand?
So I think I answered this on my own: what counts as “embedded” is a gray area, not just whether it has an MMU or not. seL4/LionOS is targeting a subset of the embedded systems field. The team did explore producing software for non-MMU hardware with eChronos but (for whatever reason) they didn’t get funding for that line of research. I’m guessing the DoD and a certain fruit based computing company were fine with the MMU requirement? At any rate, one certainly could do formal verification for chips with just an MPU but the limitations of the memory protections available make that harder.
At least that’s my guess.
It wasn’t really funding back then – back in those days we were all employed at a research institution, and for instance investigating multicore is much more interesting and a much more important problem to solve than doing yet another verification of something smaller, but essentially the same. You are pretty much forced to do novel things in research.
This has changed now with the seL4 foundation and with multiple companies being strongly involved in all of this. We can take more of an engineering and community focus now. I still think it’s more important to make fully verified seL4 configurations easy to use and deploy than branching out into the smaller embedded space, but in some sense, I’m much more willing to let the market decide now: if someone really wanted an MPU kernel for the smaller embedded space (maybe an seL4 variant, maybe an eChronos variant, maybe something completely different), and came up with a convincing amount of money for it, many of us could likely be convinced to work on it. Currently, the convincing amount of funding is for multicore and usable seL4. We’re not actively looking for funding for that smaller embedded space currently, because seL4 work is keeping us fully at capacity, but that could change in the future.
The formal verification part would not necessarily be harder, it’d just be redoing a lot of what is already done in seL4. Building (as opposed to verifying) systems on an MPU kernel might be harder compared to what people are used to in this space now – which is no protection and full access of everything to everything. The basic trust model in that entire space is different: in systems with larger CPUs we expect to potentially run untrusted code. In small embedded systems, we expect to run only code that we control ourselves, so we are protecting mostly from bugs, not from malicious execution on the same CPU. This trust model is increasingly wrong even for small embedded systems, of course, because once you have networking, you have attacks, but it’s still ingrained in the industry.