Type safety in the Linux kernel
Abstract/Contents
- Abstract
- Type casts are ubiquitous in Linux and other systems software. Casts reinterpret a pointer to a heap object of one type as a pointer to another type, and are the main way by which programmers can violate type safety, the notion that objects are used as a consistent type throughout their lifetime. A program which is not type safe can exhibit corruption and crashes. Moreover, the C language provides no guarantees about type safety, so responsibility for ensuring type safety falls entirely to programmers. This thesis describes an approach to proving that type casts preserve type safety, specifically in the Linux kernel. This approach uses automated static analysis to infer the abstractions underlying each type cast: type casts are performed for a reason, often to implement polymorphism or another advanced programming language feature, and by identifying this reason the cast can be proved safe. We prove this safety for 75.2% of downcasts to structure types in Linux, out of a population of 28767. Analyzing type casts in Linux requires deep reasoning about the heap at a scale well beyond the previous state of the art. This thesis describes the analysis techniques we developed for this problem, which are broadly applicable to doing sound and precise analysis of the heap at a large scale.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2010 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Hackett, Brian William |
|---|---|
| Associated with | Stanford University, Computer Science Department. |
| Primary advisor | Aiken, Alexander |
| Thesis advisor | Aiken, Alexander |
| Thesis advisor | Engler, Dawson R |
| Thesis advisor | Lam, Monica S |
| Advisor | Engler, Dawson R |
| Advisor | Lam, Monica S |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | Brian William Hackett. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Thesis (Ph. D.)--Stanford University, 2010. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2010 by Brian William Hackett
- License
- This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).
Also listed in
Loading usage metrics...