Hello, I am looking at the (perhaps dated?) paper “Towards Proving Security in the Presence of Large Untrusted Components” and am interested in studying the Isabelle/HOL formalization thereof.
However I cannot find it. I checked all repos of the seL4 Foundation, the sel4 page, via Google and so on. The closest I could find is a take-grant specification (no refinement to the abstract model) in the l4v repo here.
Is the formalization described in that paper available somewhere?
Textbook for “Advanced Topics in Software Verification” UNSW course:
http://concrete-semantics.org/
plus Further Reading:
https://www.cse.unsw.edu.au/~cs4161/material.html
I hope it helps…
Thank you for sharing. While these are great resources (was not aware of the second one), they do not answer questions related to the take-grant theories I am after. There are also the PhD theses by Elkaduwe [1] and Boyton [2] for even more reading but no more Isabelle theories other than take-grant/.
Yes, the take-grant/ directory is disconnected from the rest of the seL4 proofs – it’s more a conceptual exploration of the model in those two PhD theses than its actual implementation in seL4. And the paper you mentioned (Towards Proving Security in the Presence of Large Untrusted Components) is indeed a bit dated – a more recent account of the ideas in it would be “Comprehensive formal verification of an OS microkernel” and maybe “Formally verified software in the real world” for a shorter summary (sorry, even more to read 
).
The Isabelle theories for these are everything to do with the capDL language and its connection to the integrity theorem and abstract spec of seL4. The entry points for this are spec/capDL, proof/drefine, proof/dpolicy, proof/capDL-api, and finally sys-init for the connection to the user-level system initialiser.