Design Environments for Global ApplicationS (DEGAS)

The Design Environments for Global ApplicationS project (DEGAS) project was funded under the IST Programme - FET pro-active initiative VI.2.2 "Global computing, cooperation of autonomous and mobile entities in dynamic environments". Initiated in 2001, the project completed in April 2005. The DEGAS project brought together academic partners at the University of Edinburgh, Technical University of Denmark, University of Pisa, and the University of Trento, and industrial partners in Motorola Electronics SPA and OMNYS Wireless Technology.

The DEGAS project has been selected as an IST success story to be featured in the IST Results publication.

Overview

The safety and reliability of networked software applications becomes a highly significant matter as such systems play an ever-increasing role in society and public life. Software systems win the trust of users by being secure against attack and by remaining available and responsive under increasing workload. Security and quality-of-service valuations such as these give rise to subtle and complex questions about these complex systems. Determining the answers to these questions necessitates careful modelling and analysis of these systems in well-founded formal modelling languages. Such reasoning is both too detailed and too arduous to be undertaken by hand and so modelling and design tools play a crucial role in designing and evaluating the computing applications of today and tomorrow.

Security in Global Applications

Global computing devices roam free within widespaning and unchartered computer networks. While this can offer many new services to the application running on the devices, it also poses new threats because the applications may be attacked by any malicious party also populating the networks. To counter these attacks, the application must deploy safeguards but ensuring that these safeguards are sufficiently strong is a difficult task for an application developer. To aid the developer, the DEGAS project has developed automated analysis techniques that can give developers guarantees about the security of their applications.

In the DEGAS project we have advanced classical static analysis techniques to cater for analysis of the security problems that arise within network communication of global applications. The analysis techniques are characterised by being fully automated, which means that they can be used by non-experts with only a limited amount of additional training. Furthermore, the techniques are computationally efficient, thereby, making them viable for analysis of industrial scale problems already with the computing power of today. Within the DEGAS project we have successfully illustrated that these techniques are viable for tracing numerous kinds of security problems facing modern global applications.

Performance of Global Applications

Global applications are characterised by geographical distribution and the need for remote evaluation of programs on distant servers across the network. Despite impressive advances in computing power, such systems are difficult to engineer and tune to the levels of responsiveness and performance which are demanded by their users. Maintaining quality of service while supporting a growing population of users requires careful planning and analysis of performance models of systems.

Performance models may be analysed by simulation, numerical solution or analytical solution. Simulation models have the advantage of being insensitive to state space size. Unfortunately such models are time-consuming to analyse and bring the intellectual burden of evaluating the trustworthiness of results by the calculation of confidence intervals. In contrast analytic solution (in which an expression for the performance measure of interest is derived in terms of the input parameters of the model) can be extremely efficient to use. However, constructing such solutions is very much the domain of the expert and typically each system requires a bespoke solution.

The approach used by the DEGAS project, numerical solution of a Markov chain, is a compromise between these two extremes. Some assumptions about the system are needed, particularly with respect to the timing of events. But the resulting models can be automatically solved by efficient procedures of numerical linear algebra which are built into the DEGAS Choreographer design platform. Thus a user of Choreographer can access the results which they need without resorting to error-prone simulation or needing the services of a performance analysis expert. Through collaboration with our industrial partners in the project we have demonstrated that these methods can be applied in practice to real-world performance problems.

Awards

Dr Jane Hillston, site leader of the Edinburgh site of the DEGAS project, became the first recipient of the Roger Needham Award for her work on Performance Evaluation Process Algebra and compositional approaches to performance modelling. The award was given by the British Computer Society and sponsored by Microsoft Research Cambridge.

Dr Hillston gave a public lecture on her work on Performance Evaluation Process Algebra and the DEGAS project at the Royal Society in London in December 2004. A paper summarising the talk entitled Tuning systems: from composition to performance is to appear in the Computer Journal. The Needham Lecture is to be reprised at the Informatics Jamboree.

Dr Jane Hillston, site leader of the Edinburgh site of the DEGAS project, delivering her Needham Award lecture at the Royal Society in London. (Click images to enlarge.)

Beneficiaries

The impact of the DEGAS project on software development will be to bring state-of-the-art modelling technology within the reach of practising software designers and developers. This will accelerate the production and delivery of software products with strong security properties and guaranteed quality of service. This will inevitably lead to improvements in the rate of delivery and deployment of the high-end technological services which are now a cornerstone of many of the organisations which are depended upon by society, with attendant benefits for wealth creation and improvements in the quality of human life.

One of the achievements of the DEGAS project has been to heighten awareness of the need for education in security and performance analysis for mobile code applications and to make clear the relevance of formal analysis tools developed in academia. The DEGAS project bridges the gap between the process calculi used by academics and the modelling languages used by industrial practitioners by exchanging models between the UML modelling tools used in industry and the process calculi workbenches used in academia. These suites of tools are linked by software connectors known as extractors and reflectors. (Formal content is extracted from a UML model by an extractor and the results of the analysis process are reflected back to the UML model by the associated reflector.) The DEGAS analysis tools have been successfully applied by industrial developers to attack their most difficult security and performance problems.

Future

The success of the IST-FET GC1 DEGAS project will be continued in the IST-FET-funded GC2 SENSORIA project. This project will develop and extend the Choreographer design platform to address the challenges of security, resource usage, scalability and distribution transparency which have been identified as priority areas for the GC2 initiative. The model of UML extraction, analysis and reflection will also be further developed by the industrial partners in the project, taking the techniques used into their own software tools used for product design and development in-house.

Screenshots

Below are screenshots of the DEGAS Choreographer design platform at work. (Click images to enlarge.)

	The DEGAS Choreographer platform is a sophisticated integrated development environment for security and performance modelling of mobile and global applications. Choreographer incorporates a user-friendly feedback mechanism which reports problems in an easy-to-understand way. Significant engineering effort has gone into developing a tool which is intuitive and easy to use.
	With the Choreographer platform process calculus models are extracted from UML models, analysed by static and dynamic model analyser. The results are returned to the UML modeller as an annotated copy of their input model. Security problems in protocols are pinpointed and performance problems such as hot-spots and bottlenecks are also identified.
	Security models are checked by an innovative use of static analysis, an efficient procedure which combines the best features of other formal approaches to the problem. First, the method applies to all possible attacks which a standard network attacker can apply and so it is as general as theorem proving. Second, the method generates informative counter-examples showing where the problems occur and so it is as useful as model checking. Additionally, static analysis is computationally inexpensive so inexpensive hardware can be used to prove security properties of complex real-world communication protocols, and to discover previously-unknown flaws in them.