CAREER: Programming Languages for Secure and Reliable Computing

Princeton University, Princeton NJ

Investigators

Abstract

ABSTRACT CCR-0238328 David Walker Princeton University This research develops advanced program analysis techniques that increase the security and reliability of component software systems. In particular, the researchers design, implement and analyze programming languages that contain both of the following complementary technologies. 1) Effective Type Refinements (ETR) that conservatively extend modern type systems. ETR allow programmers to specify fine-grained invariants about contents of component data structures and the ordering and effect of operations in a computation. ETR guarantee properties of programs when they are written and as they evolve through the software development cycle. 2) Run-time Program Monitors (RPM). RPM execute in parallel with an untrusted application, monitoring, auditing and modifying the untrusted application's actions so that it obeys critical security and resource usage policies. RPM complement ETR by enforcing those properties at run-time that cannot be enforced at compile-time. Together effective type refinements and run-time program monitors provide a cohesive language-based framework for improving the reliability and security of large-scale software systems.