“security is no excuse for poor performance”, says seL4 FTW

[Zenaan Harkness]

For those unwilling to compromise, the stack begins …

http://ts.data61.csiro.au/projects/seL4/

Easy introductions:

 seL4 is free: What does this mean for you? (2015)
 https://www.youtube.com/watch?v=lRndE7rSXiI

 From L3 to seL4: What have we learned in 20 years
 of L4 microkernels? (2014)
 https://www.youtube.com/watch?v=RdoaFc5-1Rk

(from here:
https://docs.sel4.systems/GettingStarted.html
)


https://research.csiro.au/tsblog/sel4-raspberry-pi-3/
  The seL4 kernel is a burgeoning project that’s been creating a buzz
  in the security world for its uncompromising capability-based
  security model that comes with end-to-end proofs of conformance to
  its formal specification. It’s a microkernel, and it’s the fastest
  of its ilk. It says, “Security is no excuse for poor performance!”,
  and then backs it up. It’s open source. It’s free. It’s an
  increasingly relevant disruption in the Operating Systems monolith.

https://research.csiro.au/tsblog/introducing-device-untyped-memory-sel4/
  These invariants allow us to prove that any kernel memory access is
  not to a device register, no matter what the initialisation
  component does, and no matter whether it is trusted or not. This
  means, verification helped us to not only improve one specific
  case, but also makes sure this entire kind of problem will not
  re-occur, and to reduce the trust that is necessary in the rest of
  the system.

More¦
https://research.csiro.au/tsblog/


Plenty to learn, plenty to improve (from the raspberry pi 3 link
above):
  There is no silver-tongued way to say, that seL4 has a fairly
  involved build-dependency set-up procedure. We know it’s tedious,
  and we’re working on it.
  Here’s the simple description: you’ll need a compiler toolchain
  that can target your platform, and the “Repo” script, which is
  really just a script released by Google, that is a git
  submodule-management replacement. We use some Python scripts to
  generate some headers and our custom bitfield functions, so you’ll
  need some python modules. Slap on an XML parser which we use to
  generate our syscall invocation stubs, and ncurses for our “make
  menuconfig”, and you’re good to go.

O—M—G, sounds too difficult for folks round ’ere ... ;D


Hero level bonus for the significance junkie who just can't get
enough and is not in need of a trigger warning, cry-in, or
sky-scream:
  Plug in SNABB as an isolated ubermaxx performance user space
  network snack and build that GPL chaff-filled I2P module the
  world awaits with baited breath…


Dang, you know you love it :)