Several Research Positions Available
January 2007
All Ph.D. Positions have been filled.

Postdoc Position in Applied Formal Methods

MOBIUS: Integrated Development Environments supporting Logic-based Verification of Sequential and Concurrent Java programs with Proof-Carrying Code

School of Computer Science and Informatics, University College Dublin,
Belfield, Dublin 4, Ireland.

Research Summary

Through their global, uniform provision of services, and their distributed nature, global computers have the potential to profoundly enhance our daily life. However, they will not realize their full potential, unless the necessary levels of trust and security can be guaranteed.

We aim to develop the technology for establishing trust and security for the next generation of global computers, using the Proof Carrying Code (PCC) paradigm. The essential features of the MOBIUS security architecture will be:

  • innovative trust management, dispensing with centralized trust entities, and allowing individual components to gain trust by providing verifiable certificates of their innocuousness; and
  • static enforcement mechanisms, sufficiently flexible to cover the wide range of security concerns arising in global computing, and sufficiently resource-aware and configurable to be applicable to the wide range of devices in global computers; and
  • support for system component downloading, for compatibility with the view of a global computer as an evolving network of autonomous, heterogeneous and extensible devices.

The PCC paradigm is known for decentralized trust management, but has generally been restricted to simple safety properties, and to monolithic, non-distributed applications. We shall pioneer the first PCC framework applicable to global computers, and the first to allow enforcement of functional properties as well as advanced security properties. We shall extend the two technologies that enable PCC--- type systems and program logics---to allow enforcement of more advanced security properties, and combine them in hybrid certificates to be checked through type checking together with proof checking.

To maximize the impact of our work, we will focus on Java-enabled global computers. This will also allow us to implement our security architecture and evaluate it on case studies from a range of application domains.

UCD's Specific Responsibilities

UCD is participating in several specific research activities in this project. Our responsibilities include:

  • analysing and formalising generic framework-specific security properties,
  • analysing, formalising, and verifying application-specific security (e.g., SSL),
  • developing, implementing, and utilising new formal methods for automatically and interactively verifying concurrent Java systems (much of this work will focus on the new concurrency API in Java 1.5),
  • co-developing a programing verification environment,
  • managing the software engineering effort at several institutions,
  • analysing, developing, and utilising scenarios for proof-carrying code, particularly with respect to the compositional proprieties of PCC-centric code development,
  • developing a proof certificate compiler for automatically verified Java bytecode,
  • developing an on-device proof checker for minimal devices (e.g, mobiles),
  • and being involved in many case studies using the project technology.

UCD leads the entire effort to develop a program verification environment incorporating all the theories and tools developed by MOBIUS partners. This work will require significant software engineering effort, coordinating multiple research and development sites, and will utilise many cutting-edge FLOSS tools for project management, distributed collaboration, version control, bug tracking, testing, and more. Essentially, we are responsible for not only building the world's greatest IDE that incorporates automatic and interactive verification, but also incorporating many best-of-breed software engineering practices into such a formal framework and tool. We expect to work with several modern Integrated Development Environments, including Eclipse.

Positions Available

We are seeking candidates who want to be part of the formation of a world-class Systems Research Group. The group is funded by a 2.5 Million Euro award by Science Foundation Ireland to Professor Paddy Nixon in Secure and Predictable Pervasive Computing.

About the School

The Irish Government (SFI/Forfas) Baseline Study that ranked Irish research groups identified the School of Computer Science and Informatics at University College Dublin as the best Computer Science department in the country, having "a very strong impact internationally in their research." This research excellence is further reflected in the large number of prestigious Science Foundation Ireland (SFI) funded projects won by members of the School.

Contact Information

Please contact Dr. Joe Kiniry for further details of the above posts.


This work is funded under an EU FP6 Global Computing II Grant: MOBIUS.