1. 21
  1.  

  2. 7

    Big fan of work like this. Good article. I’ll note a good and bad point.

    The good point is forcing user-space processes to donate their own resources to kernel calls. I’ve been promoting that wherever possible ever since I saw INTEGRITY-178B do it. Although unsure if they did, one might also want to apply that to partitioned subsystems for networking, filesystems, and graphics. Then, malicious code usually only DDOS’s or leaks within its partition thanks to fewer shared resources.

    The bad point is the security vs performance claim. We default on security and performance being inverse for a reason. In many situations, you get better performance through resource sharing, increased coupling, and/or removing checks. Each of these can create security vulnerabilities. Additionally, layered systems operating on potentially-malicious inputs might have several levels of somewhat-redundant checks covering for how data safe early on might become malicious in the middle. Finally, monitoring cost something, too.

    1. 7

      The bad point is the security vs performance claim. We default on security and performance being inverse for a reason. In many situations, you get better performance through resource sharing, increased coupling, and/or removing checks. Each of these can create security vulnerabilities. Additionally, layered systems operating on potentially-malicious inputs might have several levels of somewhat-redundant checks covering for how data safe early on might become malicious in the middle. Finally, monitoring cost something, too.

      Their point is that you won’t see adoption without competitive performance. The first generation of microkernels dropped user space drivers because their IPC was too slow [1], so the L4 family [2] pay special attention to IPC overhead. seL4 still brings some critical operations into kernel space (timing drivers and scheduling) despite the verification overhead.

      FWIW, the same holds true regarding usability and security: if you don’t nail usability, then users will circumvent the security protocols.

    2. 5

      Our recent work on [side channel] protection indicates that we can solve this problem in seL4, by temporally or spatially partitioning all shared hardware resources, we partition even the kernel. This assumes that the hardware manufacturers get their act together and provide mechanisms for resetting all time-shared resources (and I’m working on the RISC-V Foundation to ensure that RISC-V does).

      This is why we need Free and Open Source systems, so that we can solve problems collectively. Closed shops get away with it because they hide their terrible code in opaque binary blobs. Those sins are usually the result of short sighted management and FOSS has a way of forcing companies to do better. From Dave Airlie’s rejection of the initial AMDGPU driver (which had an HAL):

      There have been countless requests from various companies and contributors to merge unsavoury things over the years and we’ve denied them. They’ve all had the same reasons behind why they couldn’t do what we want and why we were wrong, but lots of people have shown up who do get what we are at and have joined the community and contributed drivers that conform to the standards.

      Here’s the thing, we want AMD to join the graphics community not hang out inside the company in silos. We need to enable FreeSync on Linux, go ask the community how would be best to do it, don’t shove it inside the driver hidden in a special ioctl. Got some new HDMI features that are secret, talk to other ppl in the same position and work out a plan for moving forward.