4 ms·

What the sel4 people have achieved is to separate a very small part of the OS and verify it (supposedly - there are some arguments over this). But is the entir

What the sel4 people have achieved is to separate a very small part of the OS and verify it (supposedly - there are some arguments over this). But is the entire system secure if you use sel4? Not necessarily. I fact it may be less secure than vanilla Linux because (1) you need to implement more yourself (2) the distributed approach makes your system more susceptible to certain classes of vulnerabilities (e.g. higher risk for race conditions) and (3) the sel4 security proofs apply to a very specific environment and usage and you could unknowingly break any one of them.

snvzz 7y ago
seL4 does very little, but it provides the fundamental pieces that a secure system can be built on; The capability model maps very well to this problem space. Trying to build a secure system on a kernel that is not secure is a hopeless effort. An example such kernel is Linux, with over a million LoC running in supervisor mode. There's no use trying to make that secure. It only takes a single bug in Linux's code to compromise the whole.
- panpanna 7y ago
  Linux is not running millions lines of code, this is a very dishonest statement! The Linux core is very small. The millions lines are mainly drivers and support for different architecture. You can compile a minimal Linux kernel (there is even a kernel configuration for that) and put certain drivers in user-space. Still not as small as sel4 but quite close to it's commercial siblings.
  - snvzz 7y ago
    Even after configuring and building a linux kernel for your hardware, it's going to be over one megabyte object code. What's dishonest is pretending it can be compared with a microkernel's, nevermind seL4, size.
  - indolering 7y ago
    > Linux is not running millions lines of code ... the millions lines are mainly drivers and support for different architecture. But it's pretty easy to reach into the kernel and access buggy drivers and plenty of other non-essential kernel code (file systems, networking, SMB, etc). > You can compile a minimal Linux kernel (there is even a kernel configuration for that) and put certain drivers in user-space. Still not as small as sel4 but quite close to it's commercial siblings. But it still means that any exploit in driver code == total system compromise.
aidenn0 7y ago
I haven't worked with L4, but have worked with other microkernels. There are parallels between secure kernels and real-time kernels. If you randomly build a system on top of a real-time kernel, you don't have a real-time system. If you randomly build a system on top of a secure kernel, you don't have a secure system. However, if you want to build a real-time system, and understand what that requires, you will use a real-time kernel (assuming you have use for a kernel). If you use a verified kernel (or any component for that matter) and accidentally break the requirements for the security proofs, then you weren't going to be successful building a secure system anyways, because you aren't doing enough systems security analysis. If you are going to do the security analysis, the pre-existing analysis of your kernel is something you can re-use, and your analysis will include evidence that you have met the requirements for reusing that analysis. Similarly in real-time systems if you use a real-time kernel but don't do some sort of time-based analysis (e.g. rate monotonoic analysis), you won't end up with a real-time system. However, those sorts of analyses are not possible with a kernel that lacks proper real-time features.

snvzz 7y ago

seL4 does very little, but it provides the fundamental pieces that a secure system can be built on; The capability model maps very well to this problem space. Trying to build a secure system on a kernel that is not secure is a hopeless effort. An example such kernel is Linux, with over a million LoC running in supervisor mode. There's no use trying to make that secure. It only takes a single bug in Linux's code to compromise the whole.

panpanna 7y ago
Linux is not running millions lines of code, this is a very dishonest statement! The Linux core is very small. The millions lines are mainly drivers and support for different architecture. You can compile a minimal Linux kernel (there is even a kernel configuration for that) and put certain drivers in user-space. Still not as small as sel4 but quite close to it's commercial siblings.
- snvzz 7y ago
  Even after configuring and building a linux kernel for your hardware, it's going to be over one megabyte object code. What's dishonest is pretending it can be compared with a microkernel's, nevermind seL4, size.
- indolering 7y ago
  > Linux is not running millions lines of code ... the millions lines are mainly drivers and support for different architecture. But it's pretty easy to reach into the kernel and access buggy drivers and plenty of other non-essential kernel code (file systems, networking, SMB, etc). > You can compile a minimal Linux kernel (there is even a kernel configuration for that) and put certain drivers in user-space. Still not as small as sel4 but quite close to it's commercial siblings. But it still means that any exploit in driver code == total system compromise.

aidenn0 7y ago

I haven't worked with L4, but have worked with other microkernels. There are parallels between secure kernels and real-time kernels. If you randomly build a system on top of a real-time kernel, you don't have a real-time system. If you randomly build a system on top of a secure kernel, you don't have a secure system. However, if you want to build a real-time system, and understand what that requires, you will use a real-time kernel (assuming you have use for a kernel). If you use a verified kernel (or any component for that matter) and accidentally break the requirements for the security proofs, then you weren't going to be successful building a secure system anyways, because you aren't doing enough systems security analysis. If you are going to do the security analysis, the pre-existing analysis of your kernel is something you can re-use, and your analysis will include evidence that you have met the requirements for reusing that analysis. Similarly in real-time systems if you use a real-time kernel but don't do some sort of time-based analysis (e.g. rate monotonoic analysis), you won't end up with a real-time system. However, those sorts of analyses are not possible with a kernel that lacks proper real-time features.