Verifying Properties of Systems Software

University Of California-Berkeley, Berkeley CA

Investigators

Abstract

ABSTRACT Proposal Number 0234689 TITLE Verifying Properties of Systems Software PI Alex Aiken This research focuses on enforcing critical properties in software such as device drivers, high-performance servers, network protocols, and embedded systems. The plan is to design, build and experiment with an analysis tool for C and C++ programs that will achieve two goals: (1) It will check the full range of critical properties of systems software, from low-level checks, such as preventing buffer overruns and null pointer dereferences, to high-level, program-specific checks, such as verifying the steps of a protocol are executed in the correct order. (2) The tool will be used for investigating the trade-offs between static (at compile-time) and dynamic (at run-time) enforcement of properties. The impacts of this work should include: first, a better understanding of when it is sufficient to use the weaker but less expensive (in programmer effort) checking at runtime instead of static checking at compile-time; a coherent model of how to integrate very low-level and high-level program checking in a single system; and a prototype tool that others without specialized knowledge of program analysis can use to improve the quality of complex systems written in C and C++.