We present the type and effect system for a security-oriented language called lambda-box. Lambda-box is an enriched version of lambda-calculus that allows to represent security-relevant events and local security policies (i.e. policy framing). We show illustrate to associate to the programs an history expression. History expressions approximate the run-time behavior of programs written in lambda-box. It is possible to prove that if an history expression complies with the active security policies then the associated programs will never produce security errors at run-time. We conclude showing how to adjust an existing typing algorithm in order to produce an automatic tool able to extract types and history expressions from the syntax of lambda-box.
From 05/03/2008-12.56 to 05/03/2008-12.56 , Istituto di Informatica e Telematica
Responsible: Gabriele Costa