[Prev][Next][Index][Thread]
Paper on a type system for security
We would like to announce the availability of a draft paper on
adding security information to types in the typed lambda calculus:
Title: The SLam Calculus: Programming with Secrecy and Integrity
Abstract: The SLam calculus is a typed lambda-calculus that
maintains *security information* as well as type information. The
type system propagates security information for each object in
four forms: the object's creators and readers, and the object's
*indirect* creators and readers (i.e., those agents who, through
flow-of-control or the actions of other agents, can influence or
be influenced by the content of the object). We prove that the
type system prevents security violations and give some examples of
its power.
The paper is available from the Web page
http://cm.bell-labs.com/who/riecke/bib.html
or more directly from
ftp://ftp.research.bell-labs.com/dist/riecke/slam-extended-abstract.ps.gz
Comments are most welcome.
-Nevin Heintze
Jon G. Riecke