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