A Memory Allocation Model For An Embedded Microkernel

High-end embedded systems featuring millions of lines of code, with varying degrees of assurance, are becom- ing commonplace. These devices are typically expected to meet diverse application requirements within tight re- source budgets. Their growing complexity makes it in- creasingly difficult to ensure that they are secure and robust. One approach is to provide strong guarantees of iso- lation between components — thereby ensuring that the effects of any misbehaviour are confined to the misbe- having component. This paper focuses on an aspect of the system's behaviour that is critical to any such guar- antee: management of physical memory resources. In this paper, we present a secure physical memory management model that gives hard guarantees on phys- ical memory consumption. The model dictates the in- kernel mechanisms for allocation, however the alloca- tion policy is implemented outside the kernel. We also argue that exporting allocation to user-level provides the flexibility necessary to implement the diverse re- source management policies needed in embedded sys- tems, while retaining the high-assurance properties of a formally verified kernel.