3 ms·

Have you tried L4?

by maaku 11y ago

Have you tried L4?

nickpsecurity 11y ago
It was lightening-fast but too primitive & had weaknesses. Something like EROS (capability-secure kernel) or INTEGRITY-178B (separation kernel) were more ideal. Back when I was implementing, I did work with L4 (esp OKL4) based on the Nizza Security Architecture: http://genode-labs.com/publications/nizza-2005.pdf http://genode-labs.com/publications/nizza-2005.pdf Case study for a secure, IPsec VPN with Nizza below: http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=B12EF1739E0D9515BC0B892BC05833BB?doi=10.1.1.65.6309&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=B12... Applied to secure filesystems https://www.usenix.org/legacy/event/atc11/tech/slides/weinhold.pdf https://www.usenix.org/legacy/event/atc11/tech/slides/weinho... You can do a lot with that model whether you use a recent L4 kernel or some other microkernel. If you're into that stuff, I'd say check out the GenodeOS project at genode.org. Unlike most, their OS is using as many robust components from academia as possible while attempting to integrate them into something usable. They have a microkernel, a resource architecture, Nitpicker GUI, and so on. It needs help wherever people can get it.
- maaku 11y ago
  I'm a fan of EROS as well. But primitive is the point, no? Support only what minimal feature set is necessary to implement the rest in higher layers with optimal performance, while adding some sort of security guarantees (even if just about threads & memory).
  - nickpsecurity 11y ago
    Sort of. The point is less primitive and more verifiable. A lot of the security kernels of the past were a decent size. So was Dijkstra's THE OS which pioneered the robust, construction processes. Hamilton's team's flawless code for Apollo certainly wasn't small either: https://upload.wikimedia.org/wikipedia/commons/thumb/2/2e/Margaret_Hamilton.gif/220px-Margaret_Hamilton.gif https://upload.wikimedia.org/wikipedia/commons/thumb/2/2e/Ma... We tend to keep the TCB small as less code = less bugs. We simplify it because simpler code = easier verification. Usually... More important is you know what states or execution effects each component can have in a way that can be abstracted into analyzing those above it. So, the thing can be 4Kloc or 100Kloc, but it should be easily analyzed and composed modules. One problem I noticed, though, is that systems without needed functionality get continuous, ad-hoc versions of that functionality from their developers. C and UNIX were perfect examples with all kinds of extensions there was a mess trying to cover stuff that came by default in prior languages and platforms. So, there was less safety & consistency anyway despite underlying tool being primitive. This led me to shift from "simple & tiny as possible" to the simplest version of tools that make it as easy as possible to do right. Bernstein et al's Ethos & NaCl projects are perfect examples where internally they're a bit complex but interface is simple to use & securely. Just got to find the right balance. A lot of good wisdom on such things is from Karger et al in the link below on high assurance virtualization. See "layered design" especially for verbal and visual explanation: http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf

Have you tried L4?

by maaku 11y ago

Have you tried L4?

It was lightening-fast but too primitive & had weaknesses. Something like EROS (capability-secure kernel) or INTEGRITY-178B (separation kernel) were more ideal. Back when I was implementing, I did work with L4 (esp OKL4) based on the Nizza Security Architecture: http://genode-labs.com/publications/nizza-2005.pdf http://genode-labs.com/publications/nizza-2005.pdf Case study for a secure, IPsec VPN with Nizza below: http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=B12EF1739E0D9515BC0B892BC05833BB?doi=10.1.1.65.6309&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=B12... Applied to secure filesystems https://www.usenix.org/legacy/event/atc11/tech/slides/weinhold.pdf https://www.usenix.org/legacy/event/atc11/tech/slides/weinho... You can do a lot with that model whether you use a recent L4 kernel or some other microkernel. If you're into that stuff, I'd say check out the GenodeOS project at genode.org. Unlike most, their OS is using as many robust components from academia as possible while attempting to integrate them into something usable. They have a microkernel, a resource architecture, Nitpicker GUI, and so on. It needs help wherever people can get it.

maaku 11y ago
I'm a fan of EROS as well. But primitive is the point, no? Support only what minimal feature set is necessary to implement the rest in higher layers with optimal performance, while adding some sort of security guarantees (even if just about threads & memory).
- nickpsecurity 11y ago
  Sort of. The point is less primitive and more verifiable. A lot of the security kernels of the past were a decent size. So was Dijkstra's THE OS which pioneered the robust, construction processes. Hamilton's team's flawless code for Apollo certainly wasn't small either: https://upload.wikimedia.org/wikipedia/commons/thumb/2/2e/Margaret_Hamilton.gif/220px-Margaret_Hamilton.gif https://upload.wikimedia.org/wikipedia/commons/thumb/2/2e/Ma... We tend to keep the TCB small as less code = less bugs. We simplify it because simpler code = easier verification. Usually... More important is you know what states or execution effects each component can have in a way that can be abstracted into analyzing those above it. So, the thing can be 4Kloc or 100Kloc, but it should be easily analyzed and composed modules. One problem I noticed, though, is that systems without needed functionality get continuous, ad-hoc versions of that functionality from their developers. C and UNIX were perfect examples with all kinds of extensions there was a mess trying to cover stuff that came by default in prior languages and platforms. So, there was less safety & consistency anyway despite underlying tool being primitive. This led me to shift from "simple & tiny as possible" to the simplest version of tools that make it as easy as possible to do right. Bernstein et al's Ethos & NaCl projects are perfect examples where internally they're a bit complex but interface is simple to use & securely. Just got to find the right balance. A lot of good wisdom on such things is from Karger et al in the link below on high assurance virtualization. See "layered design" especially for verbal and visual explanation: http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf