Dear Andrew

You can find a lot of infomation about seL4 on the website (https://sel4.systems/), especially the white paper. (Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations)

The seL4 came form NICTA and now it joins Data61, so you also find a lot of paper on the website. (https://ts.data61.csiro.au/projects/seL4/)

For the formal verification, I think the following reference is useful.

[1] http://proofcraft.org/blog/proof-engineer-reading.html
[2] https://frap.csail.mit.edu/main

In 21st, I think it exists three different design principles of kernel style.

1. monolithic kernel, e.g. Linux, FreeBSD

2. microkernel, e.g. seL4, more example : http://www.microkernel.info/

3. unikernel, example: http://unikernel.org/projects/

Thanks

Gapry

2016-08-22 4:16 GMT+08:00 Andrew Mine <secondmine@gmail.com>:

Hi

I have just started looking at seL4 and I was wondering where can I find some documentation explaining the features and difference between seL4 and other kernels. I have gone through the manual and tutorial documents but nothing majorly explains how seL4 is different and its features. Any guidance towards any documentation will be helpful.

Thanks
Andrew

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel