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.
> 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.
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.