Slashdot Mirror

← Back to Domains

Domain: tudos.org

Stories and comments across the archive that link to tudos.org.

Comments · 4

  1. Re:Um, maybe I'm missing why this is such a big de by Lemming+Mark · · Score: 1 · on World's First Formally-Proven OS Kernel

    Disclaimer: my background is on working on Xen but I have a research interest in L4, amongst other things. Should also note that I've not yet RTFA'd but I will do as it sounds awesome.

    Well, for one thing you can use L4 as a hypervisor. L4 doesn't provide much in the way of high-level functionality - but neither does hardware. It can act as a hypervisor for running Linux VMs on. Bang, you've just formally proven a hypervisor so you can - hopefully - make precise guarantees about security between VMs, etc. In reality the picture is unlikely to be quite so rosy, since you still need to provide virtual devices to your VMs and there are potential security holes in paravirtualised device drivers. Still, it's a step in the right direction - the direction being that we can be *really* certain about how isolated VMs are, despite sharing the same hardware. And that isolation is, after all, part of the core purpose of virtualisation.

    Going a bit more futuristic / researchy, there's been various work on running special high-assurance applications directly on L4 *alongside* Linux. So, for instance, modified versions of your crypto apps can be protected from Linux kernel exploits by running them outside Linux on L4 and using a very narrow communications channel to minimise the available vectors for an attacker. Or, conversely, you could distributed untrusted "applet" code to people that can be run directly on L4 - then they can run it outside Linux so they don't have to trust it as much.

    Some of these concepts are demonstrated on a (separate) L4-based demo OS here, which is pretty cool: http://demo.tudos.org/

  2. It's paravirtualization by Lemming+Mark · · Score: 2, Interesting · on World's First Formally-Proven OS Kernel

    Disclaimer: my background is on working on Xen but I have a research interest in L4, amongst other things. Should also note that I've not yet RTFA'd but I will do as it sounds awesome.

    Paravirtualization is where you modify a kernel so that it can run on something other than "bare hardware". Often in this situation you call the kernel that *does* run on bare hardware the "hypervisor" to distinguish it from the Linux (or whatever) kernel running on top. In this case Linux is running on top of their L4 kernel as a userspace program - instead of accessing parts of the hardware to get its job done it uses L4 system calls. This is basically the same as what Xen does, with L4 taking the role of the hypervisor. Researchers working on L4 have been playing with Linux-on-L4 for many years - longer than Xen has been about, AFAIK.

    One nice trick you get, in this case, is that you have the ability to run Linux programs on your nice, formally-proven microkernel. But alongside that you can still run programs *directly* on the L4 kernel, independently of Linux (or with some controlled interaction with it). So, say you have some untrusted code you want to sandbox - you can run it directly on L4, which (now) has proven security properties. Or perhaps you have a crypto app which you want to isolate from Linux in case a root exploit leaves it vulnerable - you can run it directly on L4, outside Linux. You could potentially do similar things for programs that need realtime guarantees - let normal applications get scheduled by Linux's scheduler and realtime apps run directly on L4.

    Basically, having L4 there is giving you an ability to start other "virtual machines" running paravirtualised OSes or high assurance applications. It's always been part of the goal that because L4 is simpler than Linux you get to have high assurance that it'll do what it's supposed to. Now a derivative has been formally proven the guarantees could potentially be even better.

    The TUD:OS demo CD website has some interesting information about a real-world system that mixes the ability to run (multiple) Linux virtual machines, plus isolated secure applications, all under a security-oriented GUI. It's a pretty cool demo and you can run it as a LiveCD: http://demo.tudos.org/

  3. Why not go all the way and have separate OSes? by Anonymous Coward · · Score: 0 · on 'Extreme Security' Web Browsing

    You can with TUDOS, both OS instances controlled by a common microkernel that doesn't allow communication between instances

  4. Re:Performance by Anonymous Coward · · Score: 0 · on Fully Open Source NTFS Support Under Linux
    Dear god, not another micro versus macro debate. No amount of word twisting will change that fact that even when comparing theoretically perfect implementations of Macro and Micro kernels the Macro kernel will ALWAYS be faster performing.
    Yes, but with a modern microkernel, the difference can be small enough to ignore. L4Linux (a Linux server running on the L4 microkernel), for example, is only about 4% slower than Linux, where as MkLinux (a Linux server running on the Mach microkernel) was typically much slower (around 50%, IIRC). Mac OS X also tends to be quite slow, owing to its Mach heritage (even though the BSD server is run in kernel mode, so the system is effectively monolithic).

    If a superior architecture (superior in terms of security and robustness) produces a 50% performance hit, it can reasonably be argued that the trade-off has to be considered on a case-by-case basis, and may not generally be worthwhile (though some of us would still opt for the more secure/robust system). When that number falls to 4%, however, the argument for the inferior design ceases to be at all reasonable.

    A macro kernel does not have the overhead required to allow all of your independent pieces of functionally to communicate with one another. A macro kernel is equally easy for a developer to manage because logical division of code does not require seperation after compilation and runtime.
    It's mostly a matter of what you're used to. However, a microkernel is arguably easier to manage because each of the servers is isolated in its own address space, so a bug in one server can't cause another to mysteriously fail. Having done a fair amount of kernel mode debugging, I've found that bugs where one module corrupts data owned by another module are much harder to track down than bugs where a module corrupts its own data. Simply put, a monolithic kernel with loadable kernel modules has a much larger range of variations in the layout of the kernel address space than a microkernel (and with a microkernel, the server address space layouts also tend to be less variable).

    Security is another issue. A macro kernel reserves access to hardware and critical functions to trusted kernel code developed and tested by trusted sources. A microkernel requires interfaces that offload control to any malicious code that strolls along and takes advantage of it.
    This comment is patently absurd. Isolation of trusted modules in their own address spaces, with minimal rights granted to each server, is clearly more secure than throwing them all into the kernel address space. For example, if an audio server process is compromised, the attacker can make a lot of noise, but can't attack trusted modules in other servers, or in kernel mode. If a kernel-mode audio driver is compromised, the entire trusted base (kernel, drivers, etc) is handed over to the attacker.