CMSC 838Z Spring 2005

Language-Based Security

Instructor Michael Hicks
CSI 1122 MW 2:00-3:15pm
Office Hours By appointment AVW 4131

Syllabus / Topics / Wiki / Resources

OS-level and hardware protection cannot solve the security problem alone.  We need ways to establish the trustworthiness of software, to augment or even replace these mechanisms.  In this class we consider how programming language techniques can be used to fill the security gap.  Starting with a simple property, memory safety, we look at ways to certify the safety of mobile code, using techniques like software fault isolation, proof-carrying code, and typed assembly language.  We will also consider higher-level security properties, as might be enforced by a reference monitor, like an operating system.  Techniques such as model checking, type checking, stack inspection, and code rewriting will come into play here.  We will consider the role languages can play in certifying availability properties, e.g., by avoiding resource overuse or exhaustion.  We will also see how languages can enforce proper access control, information flow, and protocol usage.