[HTML][HTML] seL4 in Australia: from research to real-world trustworthy systems
Communications of the ACM, 2020•dl.acm.org
APRIL 2020| VOL. 63| NO. 4| COMMUNICATIONS OF THE ACM 73 hot topics east asia &
oceania region not even manage physical memory; the kernel has no heap, and userlevel
managers must provide the kernel with memory to store metadata, such as page tables and
thread control blocks. Kernel memory thus becomes subject to memory-management
policies defined at the user level. An implication is that userlevel memory partitioning
extends into the kernel, making it easier to reason about isolation in an seL4-based system.
oceania region not even manage physical memory; the kernel has no heap, and userlevel
managers must provide the kernel with memory to store metadata, such as page tables and
thread control blocks. Kernel memory thus becomes subject to memory-management
policies defined at the user level. An implication is that userlevel memory partitioning
extends into the kernel, making it easier to reason about isolation in an seL4-based system.
APRIL 2020| VOL. 63| NO. 4| COMMUNICATIONS OF THE ACM 73 hot topics east asia & oceania region not even manage physical memory; the kernel has no heap, and userlevel managers must provide the kernel with memory to store metadata, such as page tables and thread control blocks. Kernel memory thus becomes subject to memory-management policies defined at the user level. An implication is that userlevel memory partitioning extends into the kernel, making it easier to reason about isolation in an seL4-based system.
ACM Digital Library