Channel Dependent Types for Higher-Order Mobile Processes (Extended Abstract)

Nobuko Yoshida Imperial College London ABSTRACT We introduce a new expressive theory of types for the higher-order p-calculus and demonstrate its applicability via non-trivial security analyses of a simple class-based language with distributed code mobility. The new theory significantly improves our previous one presented in [52] 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 [52], leading to significant enlargement of original typability. Two basic security concerns for mobile computation, secrecy for data confidentiality and access controls for authorised resources are analysed in a uniform type-based static framework, culminating in the noninterference theorem and authority-error freedom in the presence of higher-order code mobility. The generality and expressiveness of the new type discipline are tested with a sound embedding of multi-threaded class-based language with dynamic code/class distribution, enforcing secrecy and accessibility