Boston University
                Computer Science Department


   What: PhD Thesis Defense of Dengping Zhu
  Title: To Memory Safety Through Proofs
Speaker: Dengping Zhu
   Date: Monday April 3rd, 2006
   Time: 2:00pm
  Place: MCS 135, 111 Cummington Street
         for directions, see www.cs.bu.edu/colloquium

Abstract:

The need for memory manipulation through pointers is essential in many
applications and especially in those that involve systems programming.
However, it is also commonly understood that the use (or probably
misuse) of pointers is often a rich source for program errors.
Therefore, approaches that can effectively enforce safe use of pointers
in programming are highly sought after. Traditional approaches to
enforcing memory safety of programs rely heavily on runtime checks of
memory accesses and on garbage collection, both of which may entail
excessive run-time cost and thus are often not appropriate for systems
programming and embedded applications. In this work, we are interested
in a more fundamental approach to ensuring memory safety at
compiler-time.

It is not surprising that one of the greatest obstacles to statically
ensuring memory safety has been the lack of a good way to model the
highly dynamic nature of imperative data structures created with heavy
use of pointers such as linked lists and trees. In this work, we show
that the use of stateful views can enable us to model memory layout of
these sophisticated data structures and thus capture many more
invariants in pointer-rich programs while retaining practical
type-checking. For instance, the interesting invariant can be readily
captured in our language that each node in a doubly-linked binary tree
points to its children that point back to the node itself. This is
convincingly demonstrated in an implementation of splay trees.

With its root in the recently developed framework Applied Type System
(ATS), the type system imposes a level of abstraction on program states
and then relies on a form of linear logic to reason about stateful
views. To support practical type-checking, the programmer may need to
construct proofs that attest to the validity of constraints generated
during type-checking. Additionally, we address the issue of memory
sharing by introducing locks, which can readily resolve the conflict
between linearity and sharing. We consider the design and then the
formalization of the type system to constitute the primary contribution
of this dissertation. With various realistic examples based on a
prototype implementation of the type system we argue that stateful views
can significantly facilitate program verification in the presence of
explicit use of pointers and pointer arithmetic.

_________________________________

PhD Examination Committee:
  Hongwei Xi (Major Advisor)
  Assaf Kfoury
  Franklyn A. Turbak
  Peter Gacs
  Azer Bestavros (Chair)