6 ms·
seL4 isn't really written in C, AFAIK it's written in Haskell then translated in C. Because C is one of the few language to have a formally verified compiler Co
by renox 7y ago
seL4 isn't really written in C, AFAIK it's written in Haskell then translated in C.
Because C is one of the few language to have a formally verified compiler CompCert.
Now does seL4 support properly modern CPUs: multiple cores, with different power settings?
This I don't know.
And what about Spectre?
- pjmlp 7y agoWith the caveat that CompCert is mostly C99 and requires MISRA like C. What about Spectre? It is an hardware exploit, thus there is only so much one can don in software to prevent it. However that shouldn't be an argument for not improving the security of the IT stack, people still die when wearing security belts and helmets, but they surely do surving in higher rates than when they weren't a requirement. Exploits due to logical programming errors, false premises, hardware bugs, will always be around, however reducing the attack surface is already a big improvement.
- renox 7y ago>What about Spectre? It is an hardware exploit, thus there is only so much one can don in software to prevent it. And there has been mitigations done in software in the Linux kernel (and the web browsers but that's userspace), so my question: has seL4 being updated with mitigations for Spectre? Plus for a microkernel, this can be a big performance issue..
- pjmlp 7y agoMitigations never solve 100% the problems, as proven by 40 years of C related security mitigations, including hardware memory tagging. As for seL4, I only have superficial knowledge of the project.