# Secure Access Controller Artifacts \[MILS Architecture\]

**URL:** <https://sel4.discourse.group/t/secure-access-controller-artifacts-mils-architecture/798>\
**Category:** Verification\
**Created:** [November 26, 2023, 1:31pm UTC](https://sel4.discourse.group/t/secure-access-controller-artifacts-mils-architecture/798 "2023-11-26T13:31:40Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![dara](https://avatars.discourse-cdn.com/v4/letter/d/f14d63/32.png) [@dara](https://sel4.discourse.group/u/dara)\
**Post date:** [November 26, 2023, 1:31pm UTC](https://sel4.discourse.group/t/secure-access-controller-artifacts-mils-architecture/798/1 "2023-11-26T13:31:40Z")

</div>

Hello, I am looking at the (perhaps dated?) paper “[_Towards Proving Security in the Presence of Large Untrusted Components_](https://www.usenix.org/conference/ssv10/towards-proving-security-presence-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](https://github.com/seL4/l4v/tree/master/spec/take-grant).

Is the formalization described in that paper available somewhere?

---

<div class="post-metadata">

**Author:** ![nataliya.korovkina](https://yyz2.discourse-cdn.com/free1/user_avatar/sel4.discourse.group/nataliya.korovkina/32/276_2.png) [@nataliya.korovkina](https://sel4.discourse.group/u/nataliya.korovkina)\
**Post date:** [November 26, 2023, 8:52pm UTC](https://sel4.discourse.group/t/secure-access-controller-artifacts-mils-architecture/798/2 "2023-11-26T20:52:31Z")

</div>

Textbook for “Advanced Topics in Software Verification” UNSW course:

[http://concrete-semantics.org/](http://concrete-semantics.org/)

plus Further Reading:

[https://www.cse.unsw.edu.au/~cs4161/material.html](https://www.cse.unsw.edu.au/~cs4161/material.html)

I hope it helps…

---

<div class="post-metadata">

**Author:** ![dara](https://avatars.discourse-cdn.com/v4/letter/d/f14d63/32.png) [@dara](https://sel4.discourse.group/u/dara)\
**Post date:** [November 27, 2023, 9:29am UTC](https://sel4.discourse.group/t/secure-access-controller-artifacts-mils-architecture/798/3 "2023-11-27T09:29:57Z")

</div>

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](https://trustworthy.systems/publications/papers/Elkaduwe%3Aphd.pdf)] and Boyton [[2](https://trustworthy.systems/publications/nicta_full_text/9141.pdf)] for even more reading but no more Isabelle theories other than `take-grant/`.

---

<div class="post-metadata">

**Author:** ![gerwin.klein](https://yyz2.discourse-cdn.com/free1/user_avatar/sel4.discourse.group/gerwin.klein/32/46_2.png) [@gerwin.klein](https://sel4.discourse.group/u/gerwin.klein)\
**Post date:** [November 30, 2023, 11:40pm UTC](https://sel4.discourse.group/t/secure-access-controller-artifacts-mils-architecture/798/4 "2023-11-30T23:40:38Z")

</div>

> [@dara](#):
>
> There are also the PhD theses by Elkaduwe [[1](https://trustworthy.systems/publications/papers/Elkaduwe%3Aphd.pdf)] and Boyton [[2](https://trustworthy.systems/publications/nicta_full_text/9141.pdf)] 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_](https://www.usenix.org/conference/ssv10/towards-proving-security-presence-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](https://trustworthy.systems/publications/nicta_full_text/7371.pdf)” and maybe “[Formally verified software in the real world](https://trustworthy.systems/publications/full_text/Klein_AKMHF_18.pdf)” 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](https://github.com/seL4/l4v/tree/master/spec/capDL), [proof/drefine](https://github.com/seL4/l4v/tree/master/proof/drefine), [proof/dpolicy](https://github.com/seL4/l4v/tree/master/proof/dpolicy), [proof/capDL-api](https://github.com/seL4/l4v/tree/master/proof/capDL-api), and finally [sys-init](https://github.com/seL4/l4v/tree/master/sys-init) for the connection to the user-level system initialiser.