Channel Dependent Types for Higher-Order Mobile Processes

Nobuko Yoshida

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


Abstract

This paper introduces a new expressive theory of types for the higher-order pi-calculus and demonstrates its applicability via two security analyses for higher-order code mobility. The new theory significantly improves our previous one presented in [Yoshida and Hennessy 2002] by the use of channel dependent/existential types. New dependent types control dynamic change of process accessibility via channel passing, while existential types guarantee safe scope-extrusion in higher-order process passing. This solves an open issue in [Yoshida and Hennessy 2002], leading to significant enlargement of original typability. The resulting typing system is coherently integrated with the linear/affine typing disciplines as well as state, concurrency and distribution, allowing precise analysis of software behaviour with higher-order mobility. As illustration of the usage of the typed calculus, two basic security concerns for mobile computation, secrecy for data confidentiality and role-based access control for authorised resources, are analysed in a uniform type-based framework, leading to the noninterference theorem and authority-error freedom in the presence of higher-order code mobility.


Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems