Advanced Type Systems in Computing
The project aims to improve our understanding of the role of
type systems in programming languages.
Type systems provide a very elegant separation of concerns.
Static analyses are typically much easier to reason about
when captured by a logical framework such as a type system.
Implementations of the analyses are separate algorithmic issues
that have their own soundness and completeness proof obligations.
This project is concerned with developing new
type systems and techniques for formal proofs of semantic soundness,
algorithmic issues, and computational lower bounds for these systems.
Relevant papers can be found
here.
Currently, there are two research efforts under way.
Each is addressing different aspects of safe remote execution of code.
However, their approaches are the same in that they are each based
on language design and sound type systems.
A primary goal is to develop suitable security
properties and identify those aspects of language design that
can be shown to preserve these properties.
Secure Flow Type Systems
This effort is concerned with secure information flow in code,
either overt or covert in nature.
Traditional languages abound with features that make covert flows,
such as timing channels, easy to implement.
See SIPL for more information.
Type Systems for Secure Remote Evaluation
This effort aims to identify the rudiments of a provably-secure programming
language.
It requires formulation of appropriate security and safety properties
so that one can prove with respect to a formal semantics that every
well-typed program cannot violate these properties.
For example, it would be nice to prove that every well-typed Java Applet
when executed by Netscape does not cause Netscape to crash.
Clearly, there isn't such a proof for versions 2.X and 3.0 of
Netscape's Navigator, as evidenced by enabling Java in them and
clicking here to run a
tiny (killerApp)let.
1997 Foundations for Secure Mobile Code Workshop
See the workshop home page
for more information and position statements.
Project Personnel
Dennis Volpano
volpano@cs.nps.navy.mil