Publication:
A Principled approach to kernel memory management

dc.contributor.advisor Elphinstone, Kevin en_US
dc.contributor.advisor Heiser, Gernot en_US
dc.contributor.author Elkaduwe, Karunadipathi Wasala H. M. R. D. D. B. en_US
dc.date.accessioned 2022-03-23T16:54:30Z
dc.date.available 2022-03-23T16:54:30Z
dc.date.issued 2010 en_US
dc.description.abstract 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 system is composed of user-level components, isolated from one another using the kernel-provided mechanisms. The abstract formal model facilitates the enforcement, and reasoning about the enforcement of different policies between these user-level components. However, existing formal models only capture the application-level interface of a small kernel with no clear relationship between the externally visible access control model and the kernel's low-level management of physical memory. 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 physical memory management within the kernel to that of controlling the authority to perform these explicit allocations and controlling the dissemination of authority over already allocated objects. A formal protection model that unifies in-kernel management of physical memory with access control is developed by extending the take-grant model. A formal analysis carried out on the above developed model demonstrates that the model is capable of enforcing spatial partitioning and isolation. The extension preserves the decidability of the original take-grant model 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 significant performance degradation due to exporting all in-kernel memory allocations to user-level. When enforcing spatial partitioning to 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 resource managers through a capability-based, decidable, protection model. The model shows no performance degradation in the scenarios examined and can be used to make strong formal guarantees on memory consumption of components. en_US
dc.identifier.uri http://hdl.handle.net/1959.4/45068
dc.language English
dc.language.iso EN en_US
dc.publisher UNSW, Sydney en_US
dc.rights CC BY-NC-ND 3.0 en_US
dc.rights.uri https://creativecommons.org/licenses/by-nc-nd/3.0/au/ en_US
dc.subject.other Kernel memory management en_US
dc.subject.other Microkernels en_US
dc.subject.other Security en_US
dc.subject.other Formal verification en_US
dc.title A Principled approach to kernel memory management en_US
dc.type Thesis en_US
dcterms.accessRights open access
dcterms.rightsHolder Elkaduwe, Karunadipathi Wasala H. M. R. D. D. B.
dspace.entity.type Publication en_US
unsw.accessRights.uri https://purl.org/coar/access_right/c_abf2
unsw.identifier.doi https://doi.org/10.26190/unsworks/23083
unsw.relation.faculty Engineering
unsw.relation.originalPublicationAffiliation Elkaduwe, Karunadipathi Wasala H. M. R. D. D. B., Computer Science & Engineering, Faculty of Engineering, UNSW en_US
unsw.relation.originalPublicationAffiliation Elphinstone, Kevin, Computer Science & Engineering, Faculty of Engineering, UNSW en_US
unsw.relation.originalPublicationAffiliation Heiser, Gernot, Computer Science & Engineering, Faculty of Engineering, UNSW en_US
unsw.relation.school School of Computer Science and Engineering *
unsw.thesis.degreetype PhD Doctorate en_US
Files
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
whole.pdf
Size:
1.68 MB
Format:
application/pdf
Description:
Resource type