Theses and Dissertations Collection

This dissertation is a case study of type safety with respect to the C programming

language. In short, C is not type safe, as its integer data types are not protected against

entering one of several possible error conditions. Once a single integer error occurs,

an entire system is potentially at risk to fail or is vulnerable to hostile takeover. The

consequence of error can be devastating, depending on the critical nature of the system.

At worst, the losses could have major implications on national security.

Contained within, the problem space is explored after dening the concepts behind

type safety. Then, a syntax like typing specication for the language is introduced and a

simplied static typing semantics for its expressions and statements are expressed before

a solution is oered with a prototype tool that statically analyzes an abstraction of the

original C source code for type safety violations. Algorithms for the tool are based on an

enumeration of the likely causes to enter an integer error, a formalization of the static

typing semantics of C, and the requirements for safe C language constructs. Because of

the tool's underling language and by using the aforementioned formalizations, the tool

has the ability to prove that its reasoning about the code it is analyzing is correct.