[Prev][Next][Index][Thread]
Paper Announcement: Secure Information Flow as Typed Process Behaviour
We are pleased to announce the following paper:
Secure Information Flow as Typed Process Behaviour
by
Kohei Honda Vasco Vasconcelos Nobuko Yoshida
* Long version: - Queen Mary and Westfield College, CS Technical Paper 767
- University of Leicester, MCS Technical Paper, 1/2000
* Short version: a revised version will appear in ESOP 2000, LNCS, Springer
are available from:
http://www.dcs.qmw.ac.uk/~kohei (Queen Mary and Westfield College)
http://www.di.fc.ul.pt/~vv/publications.html (Lisbon University)
http://www.mcs.le.ac.uk/~nyoshida/paper.html (Leicester University)
Your comments are warmly welcome.
Kohei Honda: Queen Mary and Westfield College, kohei@qmw.dcs.ac.uk
Vasco Vasconcelos: University of Lisbon, vv@padme.di.fc.ul.pt
Nobuko Yoshida: University of Leicester, ny11@mcs.le.ac.uk
----------------------------- ABSTRACT ------------------------------
We propose a new type discipline for the $\pi$-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. Other fundamental
technical elements, culminating in the behavioural non-interference
result, are also sketched.
---------------------------------------------------------------------------