We have a range of projects and collaborations in the area of programming language security for systems which depend on the mobility of code, data, or both. Common themes include ensuring the secure use of resources such as time, memory space, or network access; and the verification of security with machine-checked proof. Follow the links below for more details on individual projects.
App Guarden is a UK EPSRC project investigating mechanisms for improving app stores and mobile operating systems to improve security and resilience. The project aims to combine fine-grained policies discovered through machine learning and enforced using machine-checkable digital evidence. Research is carried out using Android devices as an experimental vehicle.
CerCo is a collaborative project with research groups in Bologna and Paris building a verified C compiler that provides cycle-precise execution costs for an embedded microcontroller.
The project result will be a compiler that takes C source code and generates both a binary microcontroller executable and annotations on the source that indicate the runtime cost of each piece of code. Formal verification means that there is a machine-checked mathematical proof of two properties: the executable correctly implements the source program; and the cost annotations exactly describe the runtime behaviour of that executable. These certified annotations provide a reliable infrastructure for programmers to reason about source code while ensuring precise performance of the target executable.
CerCo is funded by the European Commission as FP7 project 243381: a STReP (Specific Targeted Research Project) under the FET Open scheme of the ICT Future and Emerging Technologies (FET) initiative in the 7th Research Framework Programme.
The technique of static analysis is a way to analyse software without running it, to help detect and repair defects in programs before they are even executed. The RESA project created new static analyses for Java to address resource usage violations, using the methods of amortised analysis and lattice-point enumeration.
Mobius was an integrated project bringing together 16 academic and industrial partners from across Europe to develop novel technologies for trustworthy global computing. Starting with the concept of proof-carrying code, the project partners extended this to draw together a range of code validation techniques: each one contributing digital evidence to certificates that guarantee program behaviour.
The Mobius project applied these technologies to Java applets on mobile phones, certifying the safe behaviour of downloadable applications. Standard digital certificates tell users about who is distributing the code: Mobius digital evidence gives reliable information about what is in the code itself.
Mobius was funded by the European Commission as project IST-015905 under the Global Computing proactive initiative of the Future and Emerging Technologies (FET) objective in the Information Society Technologies priority of the 6th Framework programme.
The ReQueST project developed methods to automatically check e-Science applications for errors that would cause them to fail by running out of resources such as memory or allotted processing time. These methods were based on logical and mathematical techniques including separation logic and polytopes. Error checks like these can be done before running the code, which saving time and resources.
Using the technology of proof-carrying code, ReQueST extended the Grid Services framework by attaching certificates to Java applications that give mathematical proofs of their resource consumption. These certificates can be independently checked by remote service providers who can then trust that these programs will run securely.
The Mobile Resource Guarantees (MRG) project developed the infrastructure needed to endow mobile code with independently verifiable certificates describing its resource behaviour (space, time, etc.). These certificates are condensed and formalised mathematical proofs of a resource-related property which are by their very nature self-evident and unforgeable (proof-carrying code). Arbitrarily complex methods may be used by the code producer to construct these certificates, but their verification by the code consumer will always be a simple computation. One may compare this to the verification of alleged solutions to combinatorial problems such as Rubik's cube or the travelling salesman problem.
This was a joint project with the Group for Theoretical Informatics at Ludwig-Maximilians-Universität, München, funded by the European Commission as project IST-2001-33149 under the Global Computing proactive initiative of the Future and Emerging Technologies objective in the Information Society Technologies priority of the Fifth Framework Programme.