The SLam calculus is a typed -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 owof-control or the actions of other agents, can in uence or be in uenced by the content of the object). We prove that the type system prevents security violations and give some examples of its power.
Nevin Heintze, Jon G. Riecke