A principled approach to kernel memory management
Dhammika Elkaduwe · 2010
350 words maximum: (PLEASE TYPE) Small kernels are a promising approach to secure and reliable system construction. These systems reduce the size of the kernel to a point where it is feasible to formally verify the implementation correctness of the kernel with respect to an abstract formal model of the kernel's behaviour. The abstract formal model facilitates the enforcement, and reasoning about the enforcement, of different policies between user-level components that constitute the system, and the formal verification connects the reasoning with the deployed kernel. In this work, a model for managing the in-kernel memory of a formally verified, small kernel is designed and evaluated for its formal and empirical characteristics. The design eliminates all implicit memory allocations within the kernel by promoting all dynamically allocated kernel memory into first-class, explicitly allocated kernel objects. This reduces the problem of kernel memory management to that of controlling the authority to perform these explicit allocations and controlling the dissemination of authority over already allocated objects. A formal security model capturing the behaviour of the kernel is developed by extending the take-grant model and formal analysis is carried out to demonstrate that the model is capable of enforcing spatial partitioning and isolation. The extension preserves the decidability of take-grant while providing the ability to reason about kernel memory consumption of components which is not feasible in the original model. Performance of the model is evaluated using a prototype implementation based on an L4 microkernel. The analysis shows no performance degradation due to exporting all in-kernel memory allocations to user-level. When enforcing spatial partitioning over a para-virtualised Linux kernel the model shows performance improvements compared to a L4 based system enforcing a similar policy by run-time monitoring and shows similar performance to a L4 system that attempts no control over memory consumption, and a Xen-based system. This work demonstrates the feasibility of exporting all in-kernel memory allocations to user-level through a capability-based, decidable, security model. The model shows no performance degradation and can be used to make strong formal guarantees on memory consumption of a component. Declaration relating to disposition of project thesis/dissertation I hereby grant to the University of New South Wales or its agents the right to archive and to make available my thesis or dissertation in whole or in part in the University libraries in all forms of media, now or here after known, subject to the provisions of the Copyright Act 1968. I retain all property rights, such as patent rights. I also retain the right to use in future works (such as articles or books) all or part of this thesis or dissertation. I also authorise University Microfilms to use the 350 word abstract of my thesis in Dissertation Abstracts International (this is applicable to doctoral theses only). Signature Witness Date The University recognises that there may be exceptional circumstances requiring restrictions on copying or conditions on use. Requests for restriction for a period of up to 2 years must be made in writing. Requests for a longer period of restriction may be considered in exceptional circumstances and require the approval of the Dean of Graduate Research. FOR OFFICE USE ONLY Date of completion of requirements for Award: THIS SHEET IS TO BE GLUED TO THE INSIDE FRONT COVER OF THE THESIS ORIGINALITY STATEMENT ‘I hereby declare that this submission is my own work and to the best of my knowledge it contains no materials previously published or written by another person, or substantial proportions of material which have been accepted for the award of any other degree or diploma at UNSW or any other educational institution, except where due acknowledgement is made in the thesis. Any contribution made to the research by others, with whom I have worked at UNSW or elsewhere, is explicitly acknowledged in the thesis. I also declare that the intellectual content of this thesis is the product of my own work, except to the extent that assistance from others in the project's design and conception or in style, presentation and linguistic expression is acknowledged.’ Signed Date