LBT Project Proposals

IT-systems in the public or private sector increasingly aggregate data about citizens that may be of a personal or even sensitive nature. Clearly the citizen may wish to be in control of the usage of data.

The purpose of this project is to take a look at the existing policy language APPEL and determine to which extent it is suitable for describing such policies.

Example issues include access control, i.e. who can access the data, but may involve temporal issues, e.g. for which duration of time should access be granted, and more advanced properties relating to information flow, e.g. who can the data be used. Finally, there might be a need for expressing general erasure policies and rules for conflict resolution.

This project touches upon problems studied in the European Union Integrated Project SENSORIA that focuses on the service-oriented systems of tomorrow.

Digital processing of images is often performed using tools like Photoshop, DPP or GIMP. Each of these tools contains a huge collection of rather independent operations and plug-ins allowing the user to manipulate his/her images in a variety of ways—brightness adjustment, cropping, sharpening, etc. Experienced photographers develop individual workflows utilizing only a small fraction of these operations - the workflow may depend on the kind of image as e.g. portraits and landscape pictures may require different modifications just as different combinations of cameras and lens.

The idea in the project is to view this multitude of operations as services and hence specifying the preferred workflow becomes an instance of service orchestration. But can we then use workflow languages as for example BPEL to guide us in digital processing? Or, alternatively, can adapt one of the SENSORIA calculi to provide a convenient modeling language?

In service-oriented architectures, components distributed over a network communicate with one-another by providing and requesting services. Mobile agents, on the other hand, roam over the network while performing their computations. The idea in this project is to combine the two programming paradigms.

The starting point could be some of the process calculi developed as models of computation - some take the service oriented view (as e.g. COWS) while others focus on mobility (as e.g. mobile ambients). Can we suggest a common calculus? Can we model some interesting scenarios in it? What about service discovery, service orchestration and service choreography in this setting? The project is very open and could involve implementation of a prototype as well as development of static analysis tools for validating safety and security properties.

Various kinds of data flow analyses for imperative programs are expressible in a generic formalisation, namely Monotone Frameworks. This genericity comes with various benefits, for example a uniform algorithm for computing solutions of data flow analyses.

Recently, various analyses of concurrent systems have been proposed which are based on the general idea of Monotone Frameworks. For a system given in a process calculus these analyses produce the system's abstract control flow graph. Originally applied to calculi for biological systems (and therefore sometimes referred to as pathway analyses), such analyses have been developed in the LBT group for various calculi such as CCS, the pi-calculus, PEPA, and broadcast calculi. The definition of these analyses suggests that there is again an underlying framework, just as in Monotone Frameworks.

The task of this theory-oriented Master's project is to explore this connection, and to provide a description of the generic framework, which can serve as a pattern for defining new analyses.

It is quite normal for people to go together and form an organisation of some sort, be it a sports club, a public health care department, or a private business, in order to achieve a common goal. Generally, the behaviour of the organisation will emerge as the result of the capabilities of the individual collaborators as well as the formal and informal cooperative structures formed amongst them.

In Computer Science such systems of collaborating entities are traditionally modelled using Process Algebras—often extended to incorporate stochastic information, which allows quality of service measures to be computed.

The idea of the proposed project is to apply a collaborator-as-computational-process abstraction to a small organisation, in order to facilitate formal reasoning about the performance of the organisation.

Authentication is one of the most important issues in computer networks security. Many authentication protocols have been specified and implemented, and many of these were shown to be flawed, and corrected, afterwards. The Needham-Schroeder protocol, published in 1978, became the basis for many similar protocols. In 1981, Denning-Sacco demonstrated that the protocol was flawed and proposed an alternative protocol. In 1994 Martin Abadi demonstrated that the public key protocol of Denning-Sacco was flawed. In 1995, Lowe demonstrated an attack on the public key protocol of Needham-Schroeder.

In this project, the authentication protocols in latest wireless standards will be examined. Latest versions of IEEE 802.11 (WiFi), IEEE 802.16 (WiMAX), IEEE 802.15.1 (Bluetooth) and IEEE 802.15.4 (ZigBee) standards employ interesting authentication protocols, and the security features of this protocols will be studied in a comparative manner to get useful insights.

The 'Sensoria Reference Markovian Calculus' is a process calculus that allows modellers to make high-level descriptions of computer systems where there is some uncertainty about which of a set of components will be used. Such uncertainty arises naturally in service-oriented computing where it is not known to which service instance a service consumer will choose to bind. This kind of uncertainty also arises when evaluating two or more candidate designs for a component. Either might be usable but which will give better performance when in use?

Using a compact and intuitive process calculus language, SRMC allows documenting this kind of uncertainty formally. The SRMC software investigates this uncertainty by evaluating all of the possibly reachable configurations, generating Markov chain representations for each one. However, not all configurations theoretically possible are indeed feasible. The objective of this thesis is to develop static analyses of SRMC models that allow reducing the size and number of Markov chains generated. This project may be conducted jointly with the University of Edinburgh.

Theoretical approaches, to validate communication in distributed systems, often rely on process calculi. Several calculi have been developed for this purpose (e.g. LySa and Spi), and similarly have several corresponding automatic verification tools been deviced (e.g. LySaTool and Cryptyc). Industrial systems, on the other hand, are almost never described in process calculi, but usually in SOAP messages. Recent projects (e.g. the TulaFale project) have shown that SOAP holds enough information to assist an translation into more formal models.

The purpose of this project is to develop a tool that performs a translation from SOAP into the process calculus LySa, with as little human interaction required as possible. LySa is developed solely with the purpose of modelling cryptographic protocols in distributed systems, and it is supported by a fully automatic validation tool, the LySaTool, and thus the resulting tool would be a complete validation tool for SOAP specified distributed systems.

Microsoft's research project SPEC# is aiming at supporting Design by Contract for the widely used platform .NET. The SPEC# framework extends the .NET core language C# with annotations such as restricted types, invariants, and pre- and postconditions, and employs a theorem prover to guarantee program-wide properties.

Static analysis techniques, on the other hand, allow making guarantees that hold during any possible execution of the program.

A goal in this project is to investigate how static analysis techniques can benefit from and/or contribute to the results of a theorem prover.

Another direction might be to compare the qualitative differences between guarantees given by the theorem prover with those provided by static analysis results.

In order to succinctly describe asynchronous hardware designs a number of high-level notations have been suggested. A good example is Martin's CHP (Communicating Hardware Processes).

They fall in the tradition of standard process algebras for expressing the high-level nature of systems but have been specifically targeted to deal with the hardware level using specific operators for handshake synchronization.

One goal of this project is to investigate how to make use of such notations in describing the design of FPGA circuits of the sort designed at IMM.

A secondary goal of the project is to investigate the potential for analysing such descriptions for properties useful for ensuring the correctness of the design.

Other directions might be possible based on the background of the student.

Recently Aspect-Oriented Programming has emerged as a complementary method to support the traditional Object-Oriented Programming approach, for aiding the programmer to realize a better "separation of concern".

For example, the security features of a given system are usually scattered across various classes. In Aspect-Oriented programming terms, these security features could be considered as a concern, and might be integrated in a security aspect module. This would result in an increased modularization, and ease code maintenance.

This project will explore what aspect-oriented techniques can be used to solve security problems, e.g., in financial systems. The project involves modeling an reasonable interesting scenario, using an aspect-oriented language such as AspectJ (Java based) or AspectML (SML based), and to develop a prototype of such a system. We will then investigate, which security properties can be shown to hold for the aspect-oriented version versus the regular approach.

Service-oriented architectures are complex systems with evolving structures. Services can be composed on demand to fulfill changing requests, and it often is unclear which service will be chosen at any given time (and for which reasons). Being able to guarantee properties of such systems is therefore essential for ensuring successful adaptation by the market.

A goal of this project is to investigate how to integrate state-of-the-art analysis tools, such as the LysaTool, with state-of-the-art development and design tools, such as Eclipse. The challenge is to extract relevant information from the design tool, and to reflect the analysis result back into it.

This project will work on problems studied in the European Union Integrated Project SENSORIA that focuses on the service-oriented systems of tomorrow. The platform used will be the case tool developed in the SENSORIA project.