Sciweavers

Share
ESOP
2000
Springer

Secure Information Flow as Typed Process Behaviour

9 years 28 days ago
Secure Information Flow as Typed Process Behaviour
Abstract. We propose a new type discipline for the -calculus in which secure information flow is guaranteed by static type checking. Secrecy levels are assigned to channels and are controlled by subtyping. A behavioural notion of types capturing causality of actions plays an essential role for ensuring safe information flow in diverse interactive behaviours, making the calculus powerful enough to embed known calculi for type-based security. The paper introduces the core part of the calculus, presents its basic syntactic properties, and illustrates its use as a tool for programming language analysis by a sound embedding of a secure multi-threaded imperative calculus of Volpano and Smith. The embedding leads to a practically meaningful extension of their original type discipline.
Kohei Honda, Vasco Thudichum Vasconcelos, Nobuko Y
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where ESOP
Authors Kohei Honda, Vasco Thudichum Vasconcelos, Nobuko Yoshida
Comments (0)
books