Harnessing Logic to Improve the Reliability and Security of Software

Limin Jia
University of Pennsylvania
Philadelphia


Software bugs cost US economy an estimated 60 billion dollars per year, 
according to a 2002 NIST study. In this talk, I will present two 
projects, both of which use formal logics and type systems to improve 
software reliability and security. The first one aims to verify existing

software; the second focuses on developing new language features to 
allow programmers to produce better code.

In the first part of the talk, I will present a framework for verifying 
the memory-safety properties of existing C-like pointer programs. This 
framework makes novel use of a substructural logic as the specification 
language for memory-safety properties that allows static and dynamic 
verification methods to interact smoothly.

In the second part of my talk, I will present AURA, a domain-specific 
language for programming reference monitors implementing logic-based 
access control. Using AURA's type system, access-control policies can be

part of the definition of safe interfaces for accessing protected 
resources. Thanks to this, reference monitor written in AURA enjoy high 
security and reliability guarantees.