Limitations of Existing Program Analyses

While these and other ongoing research activities are rapidly advancing the applicability of PA technologies to real software, the existing framework alone may not be able to meet the needs for safety in modern computing. As an illustration, let us return to the initial example: a company wishes to distribute an application for which there are crucial safety properties to be ensured, such as proper execution of authentication and secrecy/confidentiality of information. As already mentioned, in order to ensure such properties in earnest, the analysis should cover a wide variety of behaviours. For example, suppose the software includes an instant messaging service to be done with another peer in Internet: the correctness relies on not only the sequential part of the software but also interaction among distributed components. Moreover, as is increasingly found in practice, distributed components may be written in multiple languages, whose behaviour as a whole should be taken into account for ensuring safety. Such a situation poses fundamental challenges to the well-established PA techniques, as we summarise in the following.

(1)

Advanced Language Features including Concurrency and Distribution. The existing framework of PA is mostly restricted to basic sequential programming, and lacks a systematic methodology to analyse advanced features found in object-oriented programs (such as inheritance and information hiding) and concurrent, distributed programming. This is a basic limitation in the presence of advanced programming practice omnipresent in today's software. The issue is related to, and in fact reflects, the lack of semantic basis of these advanced features, in comparison with those for basic sequential computation.

(2)

Language Independence. In general, existing PAs are strongly oriented towards specific languages and calculi (for example, type-based analyses often use typed $\lambda$-calculi, while traditional analyses use sequential imperative programs). This makes it hard to adapt one technique developed for a specific language/formalism to other languages. It also makes it difficult to conceive PA technologies for emerging multi-language software. This again reflects the fact that each semantic and logical theory is tied to a particular class of language constructs, without a unifying common basis.

These observations suggest that, while the foregoing development of PA technologies has lead to a rich accumulation of theories and techniques, we need a new unifying framework which can treat PAs for diverse classes of programs' behaviours on a uniform basis. Such a framework should be able to accommodate and extend existing methods, allowing the general technology to be reflected onto concrete programming languages and offering a common platform where one can experiment with the integration and generalisation. The development of such a general mathematical basis for PAs and the demonstration of its effectiveness is the central concern underlying this project. To achieve this goal, the project chooses a typed version of the $\pi$-calculus as a fundamental tool, intended to play the role of UNICOL mentioned in the beginning.