Program Analysis and the Typed Pi-Calculus:
Foundations and Applications to Security

Description

The central aim of the present project is to investigate the feasibility of using the Pi-calculus as a general foundation of PA technologies. We choose qualitative and quantitative Information Flow Analysis as a concrete domain in which we experiment our thesis. The concrete objectives are:

1. The extension of the typed Pi-calculus to cover all major language constructs, including genericity and synchronisation.
2. The development of theory of quantitative secrecy in the context of typed Pi-calculi.
3. Development of prototypical PA tools based on the developed theories, applied to concrete programs with security concerns.

For a detailed description of the project's objectives read our project proposal .

Members

Chris Hankin Kohei Honda Nobuku Yoshida

Herbert Wiklicky Alessandra Di Pierro Martin Berger

Papers

Assigning Types to Processes (full version). Nobuko Yoshida and Matthew Hennessy. Journal of Information and Computation, 2004. ( .ps.gz )

SafeDpi: A Language for Controlling Mobile Code. (Extended abstract) Matthew Hennessy, Julian Rathke and Nobuko Yoshida Proc. of 7th International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2004) ( .pdf )

Noninterference through Flow Analysis. Kohei Honda and Nobuko Yoshida, Revised in June 2004. To appear in Journal of Functional Programming, 2004. ( .ps )

A Compositional Program Logic for Polymorphic Higher-Order Functions. Kohei Honda and Nobuko Yoshida, PPDP'2004, 6th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming, ACM Press, 2004. ( .ps )

From Process Logic to Program Logic. Kohei Honda. To appear in 9th ACM-SIGPLAN International Conference on Functional Programming (ICFP 04), ACM Press, 2004. ( .ps )

Basic Theory of Reduction Congruence for Two Timed Aysnchronous Pi-Calculi (extended abstract) . Martin Berger. Proc. of CONCUR'2004 LNCS, Springer-Verlag, 2004. ( .ps )

A Distributed Abstract Machine for Boxed Ambient Calculi. A. Phillips, N. Yoshida and S. Eisenbach. Proceedings of the European Symposium on Programming, (ETAPS'04), LNCS, April 2004 (Barcelona, Spain). ©Springer. ( .ps )

Channel Dependent Types for Higher-Order Mobile Processes (Part I). Nobuko Yoshida. Extended Abstract appears in Proc. of POPL'2004, Proc. of 31th ACM Symposium on Principles of Programming Languages, ACM Press, 2004. ( .ps )

Control in the Pi-Calculus (extended abstract). Kohei Honda, Nobuko Yoshida and Martin Berger. Fourth ACM-SIGPLAN Continuation Workshop (CW'04) ACM, January, 2004 ( .ps )

Genericity and the Pi-Calculus (full version). Martin Berger, Kohei Honda and Nobuko Yoshida. Extended abstract appears in Proc. of 6th International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2003). Last update 19 March 2004. ( .ps )

A Uniform Type Structure for Secure Information Flow (full version). Kohei Honda and Nobuko Yoshida, Revised June, 2004. Extended Abstract appears in Proc. of POPL'2002, Proc. of 29th ACM Symposium on Principles of Programming Languages, ACM Press, 2002. ( .ps )

Strong Normalisation in the Pi-Calculus (full version). Nobuko Yoshida, Martin Berger and Kohei Honda, Revised August 2003. Journal of Information and Computation. ( .ps )

Linearity and Bisimulation (extended abstract). Nobuko Yoshida, Kohei Honda and Martin Berger. Proc. of 5th International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2002) ( .ps.gz )

Sequentiality and the Pi-Calculus (full version). Martin Berger, Kohei Honda and Nobuko Yoshida. Extended abstract appeared in Proc. TLCA'01. Last modified on August 12, 2001. ( .ps )

Secure Information Flow as Typed Process Behaviour (extended abstract). Kohei Honda, Vasco Vasconcelos and Nobuko Yoshida. A revised version appeared in Proc. of European Symposium on Programming (ESOP) 2000, LNCS 1782, pp. 180--199, Springer, 2000. ( .ps.gz )

Minimality and Separation Results on Asynchronous Mobile Processes: representability theorem by concurrent combinators (extended abstract) Nobuko Yoshida, Proc. of CONCUR'98, LNCS, Springer-Verlag, Nice, France, 8--11 September, 1998. The first version in October 1997, Revised in March, June 1998. ( .ps.gz )

Reports/Other

Program Logic and Program Analysis Kohei Honda, Nobuko Yoshida and Martin Berger, Draft. August 2004. ( .ps )

SafeDpi: A Language for Controlling Mobile Code. (full version) Matthew Hennessy, Julian Rathke and Nobuko Yoshida Technical Report 02/2003, University of Sussex, Oct 2003. Extended Abstract will appear in Proc. of 7th International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2004) ( .ps )