| |
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.
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.
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.
|
|
