Nobuko Yoshida
We introduce a new expressive theory of types for the higher-order
pi-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 [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. 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.