Find results with:

Add another field

Search by date

to

Searching collections:

Dartmouth Dissertations

Add or remove collections

Home Dartmouth Dissertations Page 1

Reference URL

To link to the entire object, paste this link in email, IM or document

To embed the entire object, paste this HTML in website

To link to this page, paste this link in email, IM or document

To embed this page, paste this HTML in website

Type-safe operating system abstractions.

you wish to report:

Your comment:

Your Name:

Submit

Cancel

...

Back to top

Powered by CONTENTdm®

Call No.	Ph.D. 2004
Author	Wittie, Lea.
Title	Type-safe operating system abstractions.
Date	2004
Abstract	Operating systems and low-level applications are usually written in languages like C and assembly, which provide access to low-level abstractions. These languages have unsafe type systems that allow many bugs to slip by programmers. For example, in 1988, the Internet Worm exploited several insecure points in Unix including the finger command. A call to finger with an unexpected argument caused a buffer overflow, leading to the shutdown of most Internet traffic. A finger application written in a type-safe language would have prevented its exploit and limited the points the Internet Worm could attack. Such vulnerabilities are unacceptable in security-critical applications such as the secure coprocessors of the Marianas network [11, 21], secStore key storage from Plan 9 [6], and self-securing storage [25]. This research focuses on safe language techniques for building OS components that cannot cause memory or IO errors. For example, an Ethernet device driver communicates with its device through IO operations. The device depends on FIFO queues to send and receive packets. A mistake in an IO operation can overflow or underflow the FIFO queues, cause memory errors, or cause configuration inconsistencies on the device. Data structures such as FIFO queues can be written safely in safe languages such as Java and ML but these languages do not allow the access to the low-level resources that an OS programmer needs. Therefore, safe OS components require a language that combines the safety of Java with the low-level control of C. My research formalizes the concurrency, locks, and system state needed by the safety-critical areas of a device driver. These formal concepts are built on top of an abstract syntax and rules that guarantees basic memory safety using linear and singleton types to implement safe memory load and store operations. I proved that the improved abstract machine retains the property of soundness, which means that all well-typed programs will be able to execute until they reach an approved end-state. Together, the concurrency, locks, and state provide safety for IO operations and data structures. Using the OSKit from the University of Utah as a starting point, I developed a small operating system. I ported the 3c509 Ethernet device driver from C to Clay, a C-like type-safe language that uses a type system powerful enough to enforce invariants about low-level devices and data structures. The resulting driver works safely in a multi-threaded environment. It is guaranteed to obtain locks before using shared data. It cannot cause a FIFO queue to overflow or underflow and it will only call IO operations when invariants are satisfied. This type-safe driver demonstrates an actual working application of the theoretical components of my research. The abstract machine is powerful enough to encode a given OS specification and enforce a provably matching implementation. These results lead towards fundamentally secure computing environments.
Description	vii, 151 leaves 28 cm.
Format	application/pdf
Advisor	Chris Hawblitzel.
Subject	Operating systems (Computers) -- Security measures. ; Device drivers (Computer programs).
College	Dartmouth College -- Department of Computer Science.
Issuing Body	Dartmouth Dissertations are made available through the Dartmouth Digital Library.
Degree	Thesis (Ph.D.)--Dartmouth College.
Copyright	All rights reserved. No part of this book may be reproduced in any form by any electronic or mechanical means without permission in writing from the author.
DOI	http://dx.doi.org/10.1349/ddlp.1690

Title	Page 1
Full Text	Type-Safe Operating System Abstractions A Thesis Submitted to the Faculty in partial ful llment of the requirements for the degree of Doctor of Philosophy in Computer Science by Lea Wittie DARTMOUTH COLLEGE Hanover, New Hampshire June 30, 2004 Examining Committee { (chair) Dr. Chris Hawblitzel { Dr. Doug McIlroy { Dr. Stefan Monnier { Dr. Sean Smith { Carol Folt Dean of Graduate Studies

	All
	Pages Enter page numbers or page ranges separated by commas. For example: 1,3,5-12

Find results with:

Searching collections:

Home Dartmouth Dissertations Page 1

Type-safe operating system abstractions.

Page 1

Object Description

Description

Type-safe operating system abstractions.

Type-safe operating system abstractions.