Hi, capability-security folk here. Have you considered adopting capability-security language for describing what's going on here? It seems to me that Mill portals are very much like capability-designed syscalls. In particular, I am reminded of the "no stale stack frame" rule from Monte [0], and its interesting justification:

"Since Monte permits mutable state, one author’s code’s behavior could be affected by another author’s code running further up the frame stack. Stale frames make comprehension of code much harder as a result."

I wish that we were having more conversations and classes like [1] to get knowledge of KeyKOS and other capability-safe kernels out to CPU makers. We have ideas to share!

[0] http://monte.readthedocs.io/en/latest/semantics.html#scope-i...

[1] https://pdos.csail.mit.edu/6.828/2009/lec/l-microkernel.html