Theory, in Practice

Security via Type Qualifiers Jeff Foster
Modern programming languages have little support for writing secure software, making it all too easy to write programs with exploitable vulnerabilities. In these lectures, we explore a general technique based on type qualifiers that allows programmers to write down, in their souce code, their intentions with respect to security. We will describe how to mechanically verify that annotated code adheres to the policy. We will discuss the theoretical foundations and practical implementation issues. As a particular example, we show how to use type qualifiers to find format-string vulnerabilities in widely-deployed C programs and to find other security vulnerabilites in the Linux kernel. we will also look at alias analysis, another important program analysis problem, and show how a must-alias analysis system corresponds to a system for statically checking access control.

Network Security Architectures Carl Gunter
This series of lectures will discuss the requirements, protocols, and components of network security software on the Internet. Topics will include secure tunnels, security for web services, privacy constraints, design features that create or address DoS threats, and the use of programmable security tokens in network protocols. The primary emphasis will be the relationship between models and design, including topics like the quantification of DoS threats, models for code security in programmable tokens, strategies for composition and interoperation, and practical strategies for formal analysis of network protocol designs and software.

Current Techniques in Language-Based Security Steve Zdancewic
In these lectures, we will analyze the security infrastructure in current, main-stream programming systems and platforms such as the Java Virtual Machine and Common Language Runtime. We will explain how byte code verification collaborates with the class loader and security manager to provide a secure run-time environment. We will also use theoretical tools to determine what properties current security systems based on stack inspection have and provide concrete proposals for improving the infrastructure for next-generation programming languages and systems.


This page is the property of the University of Oregon