4 ms·

An obligatory mention when we talk about secure operating systems is the seL4 microkernel (https://github.com/seL4/seL4 https://github.com/seL4/seL4) where they

An obligatory mention when we talk about secure operating systems is the seL4 microkernel (https://github.com/seL4/seL4 https://github.com/seL4/seL4) where they have formally verified every line of code using the proof assistant Isabelle/HOL.

doener 8y ago
Yes, I read about it in the German Wikipedia (https://de.wikipedia.org/wiki/L4_(Mikrokernel) https://de.wikipedia.org/wiki/L4_(Mikrokernel)), but the link provided there as a source does not work anymore: http://ertos.nicta.com.au/research/l4.verified http://ertos.nicta.com.au/research/l4.verified The other link provided is a press release in German: http://pressetext.de/news/090817022/sicherheits-beweis-fuer-betriebssystem-kernel/ http://pressetext.de/news/090817022/sicherheits-beweis-fuer-...
- doener 8y ago
  PS: As always I recommend https://www.deepl.com/translator https://www.deepl.com/translator for translation.
  - ColanR 8y ago
    Thanks for mentioning that site. Did not know about it, glad I do now.
martin1975 8y ago
Always made me curious why Google didn't decide to use seL4 as a base for Fuchsia and instead went with Zircon...
- casual_slacker 8y ago
  There might be license issues between AGPLv3 of GenodeOS and the Apache 2.0 or GPLv2 that Android components use.
  - renox 8y ago
    ? I know that this is a GenodeOS topic, but the GP wondered about seL4 which has some parts in GPLv2 and other BSD (2-clause). IMHO the reason that few use seL4 is that it isn't ready: AFAIK seL4 isn't able to use efficiently multiple core with power savings, which is mandatory for usage in phones (and phones can use complex CPU with big and little cores).
- petecox 8y ago
  synergy - Android's bootloader (fastboot mode, etc) uses LK, of which Zircon is a fork.
jcelerier 8y ago
> where they have formally verified every line of code using the proof assistant Isabelle/HOL. and it's interesting to note that even then, they still had a few bugs here and there due to incomplete / wrong formalisation
- Koshkin 8y ago
  Also, I imagine, automatic theorem provers, too, can have bugs.
  - nickpsecurity 8y ago
    Yes. That's the reason the formal methodists started building verified or checkable tools with the checkers being tiny. Doing an solver might involve making it produce a log of each step it made with a simpler system checking them. The checking is also easy to parallelize with linear scaling. My current recommendation is checkable solvers done in a parallel language like Chapel with tiny, verified checkers. Run it logless first to see if it even passes at all. Once passes, run it in logging mode to get evidence to feed to checker. Use multiple, sequential processes to check that as concurrency in checker reduces confidence.

doener 8y ago

Yes, I read about it in the German Wikipedia (https://de.wikipedia.org/wiki/L4_(Mikrokernel) https://de.wikipedia.org/wiki/L4_(Mikrokernel)), but the link provided there as a source does not work anymore: http://ertos.nicta.com.au/research/l4.verified http://ertos.nicta.com.au/research/l4.verified The other link provided is a press release in German: http://pressetext.de/news/090817022/sicherheits-beweis-fuer-betriebssystem-kernel/ http://pressetext.de/news/090817022/sicherheits-beweis-fuer-...

doener 8y ago
PS: As always I recommend https://www.deepl.com/translator https://www.deepl.com/translator for translation.
- ColanR 8y ago
  Thanks for mentioning that site. Did not know about it, glad I do now.

martin1975 8y ago

Always made me curious why Google didn't decide to use seL4 as a base for Fuchsia and instead went with Zircon...

casual_slacker 8y ago
There might be license issues between AGPLv3 of GenodeOS and the Apache 2.0 or GPLv2 that Android components use.
- renox 8y ago
  ? I know that this is a GenodeOS topic, but the GP wondered about seL4 which has some parts in GPLv2 and other BSD (2-clause). IMHO the reason that few use seL4 is that it isn't ready: AFAIK seL4 isn't able to use efficiently multiple core with power savings, which is mandatory for usage in phones (and phones can use complex CPU with big and little cores).
petecox 8y ago
synergy - Android's bootloader (fastboot mode, etc) uses LK, of which Zircon is a fork.

jcelerier 8y ago

> where they have formally verified every line of code using the proof assistant Isabelle/HOL. and it's interesting to note that even then, they still had a few bugs here and there due to incomplete / wrong formalisation

Koshkin 8y ago
Also, I imagine, automatic theorem provers, too, can have bugs.
- nickpsecurity 8y ago
  Yes. That's the reason the formal methodists started building verified or checkable tools with the checkers being tiny. Doing an solver might involve making it produce a log of each step it made with a simpler system checking them. The checking is also easy to parallelize with linear scaling. My current recommendation is checkable solvers done in a parallel language like Chapel with tiny, verified checkers. Run it logless first to see if it even passes at all. Once passes, run it in logging mode to get evidence to feed to checker. Use multiple, sequential processes to check that as concurrency in checker reduces confidence.