I agree that the toolchain is large, unwieldy and insufficiently proven itself.
However, given that it competes with other software compiled with random (usually GCC) compiler versions (what, do you think all seL4 drivers that eventually set up DMA will be verified?), the compiler issue is not a problem unique to Muen.
Xen has the same problem (and by extension Qubes), and even seL4 has it for all purposes that exceed running the kernel and sigma0.
The big innovation here is probably the easy general availability of a practical Separation Kernel system. And the other (not quite as big, but still significant) innovation is having a Separation Kernel that you can fix yourself, if anything looks off to you: Many of the commercial offers in that space are held together by lots of duct tape, it's just hidden by means of binary-only releases, certification procedures and sales reps.
"However, given that it competes with other software compiled with random (usually GCC) compiler versions (what, do you think all seL4 drivers that eventually set up DMA will be verified?), the compiler issue is not a problem unique to Muen."
There's how good it is relative to what it competes with and how well it meets its goals. I'm talking about potential issues with the latter. And drivers have nothing to do with what I said about the kernel. There's other methods/tech for handling them.
"the compiler issue is not a problem unique to Muen"
I have a certified compiler for C. Most separation and microkernels use that. Some use a C++ subset which can be easily converted to C. I don't have one for Ada or SPARK. So, of open kernels, the problem is indeed unique to Muen. AdaCore has commercial tech to handle it in a labor-intensive way but I'd also consider making an equivalent C system side-by-side. Then, can use SPARK proofs, C verification methods (eg Frama-C, Astree), and certified translation to object code.
Meanwhile, that the very-complex compiler can destroy the security argument is worth remembering and possibly testing/inspecting for. I'm working on the concept for an easily-built, robust Ada compiler. Once I'm done, I'll pitch it to the AdaCore people to see if they'll do it or assist an external project in doing it.
"Xen has the same problem (and by extension Qubes)"
Yes, it's why I call it low assurance. I told QubesOS team, "secure" appliance vendors, etc about alternatives with low TCB and strong security. A glimpse at the market will show how many people bought that. ;)
"even seL4 has it for all purposes that exceed running the kernel and sigma0"
They admit it. They also have many parallel projects ongoing at NICTA to fix that. They solved the compilation part recently in an unexpected way. Others they're currently working on are here:
The seL4 team and Gernot Heiser were more clear on assumptions and limitations of their tech than most I read. There were certainly no attempts to mislead. Refreshing compared to the marketing crap I had to deal with from likes of Green Hills.
"The big innovation here is probably the easy general availability of a practical Separation Kernel system. And the other (not quite as big, but still significant) innovation is having a Separation Kernel that you can fix yourself, if anything looks off to you: "
I agree. I said the same in another comment here to 'hga.' It's why I promote and bring attention to Muen elsewhere so more people review, try and contribute to it. Medium assurance is certainly better than low and might get replaced with high given time.
Comments
I agree that the toolchain is large, unwieldy and insufficiently proven itself.
However, given that it competes with other software compiled with random (usually GCC) compiler versions (what, do you think all seL4 drivers that eventually set up DMA will be verified?), the compiler issue is not a problem unique to Muen.
Xen has the same problem (and by extension Qubes), and even seL4 has it for all purposes that exceed running the kernel and sigma0.
The big innovation here is probably the easy general availability of a practical Separation Kernel system. And the other (not quite as big, but still significant) innovation is having a Separation Kernel that you can fix yourself, if anything looks off to you: Many of the commercial offers in that space are held together by lots of duct tape, it's just hidden by means of binary-only releases, certification procedures and sales reps.
"However, given that it competes with other software compiled with random (usually GCC) compiler versions (what, do you think all seL4 drivers that eventually set up DMA will be verified?), the compiler issue is not a problem unique to Muen."
There's how good it is relative to what it competes with and how well it meets its goals. I'm talking about potential issues with the latter. And drivers have nothing to do with what I said about the kernel. There's other methods/tech for handling them.
"the compiler issue is not a problem unique to Muen"
I have a certified compiler for C. Most separation and microkernels use that. Some use a C++ subset which can be easily converted to C. I don't have one for Ada or SPARK. So, of open kernels, the problem is indeed unique to Muen. AdaCore has commercial tech to handle it in a labor-intensive way but I'd also consider making an equivalent C system side-by-side. Then, can use SPARK proofs, C verification methods (eg Frama-C, Astree), and certified translation to object code.
Meanwhile, that the very-complex compiler can destroy the security argument is worth remembering and possibly testing/inspecting for. I'm working on the concept for an easily-built, robust Ada compiler. Once I'm done, I'll pitch it to the AdaCore people to see if they'll do it or assist an external project in doing it.
"Xen has the same problem (and by extension Qubes)"
Yes, it's why I call it low assurance. I told QubesOS team, "secure" appliance vendors, etc about alternatives with low TCB and strong security. A glimpse at the market will show how many people bought that. ;)
"even seL4 has it for all purposes that exceed running the kernel and sigma0"
They admit it. They also have many parallel projects ongoing at NICTA to fix that. They solved the compilation part recently in an unexpected way. Others they're currently working on are here:
https://ssrg.nicta.com.au/projects/TS/
The seL4 team and Gernot Heiser were more clear on assumptions and limitations of their tech than most I read. There were certainly no attempts to mislead. Refreshing compared to the marketing crap I had to deal with from likes of Green Hills.
"The big innovation here is probably the easy general availability of a practical Separation Kernel system. And the other (not quite as big, but still significant) innovation is having a Separation Kernel that you can fix yourself, if anything looks off to you: "
I agree. I said the same in another comment here to 'hga.' It's why I promote and bring attention to Muen elsewhere so more people review, try and contribute to it. Medium assurance is certainly better than low and might get replaced with high given time.