Mobius - Mobility, Ubiquity and Security

Mobius is a European Integrated Project developing novel technologies for trustworthy global computing, using proof-carrying code to give users independent guarantees of the safety and security of Java applications for their mobile phones and PDAs.
Global computing means that applications today may run anywhere, with data and code moving freely between servers, PCs and other devices: this kind of mobility over the ubiquitous internet magnifies the challenge of making sure that such software runs safely and reliably. In this context, the Mobius project focuses on securing applications downloaded to the Java MIDP platform: globally deployed across a host of phones, this is the common runtime environment for a myriad mobile applications.
Techniques of static analysis make it possible to check program behaviour by analysing source code before it ever executes. But mobile code means that this assurance must somehow travel with the application to reach the user. Conventional digital signatures use cryptography to identify who supplied a program; the breakthrough of proof-carrying code is to give mathematical proofs that guarantee the security of the code itself. We can strengthen digital signatures with digital evidence.
Key features of the Mobius security architecture are:

• Innovative trust management, with digital evidence of program behaviour that can be independently checked by users or any third party.
• Static enforcement, checking code before it starts; adaptable to manage a range of user security concerns, and configurable to match the real-world mix of mobile platforms.
  
• Modularity, allowing developers to build up trusted applications from trusted components.
  

EmBounded - Resource Bounds for Embedded Systems

The aims of the EmBounded Project are to identify, to quantify and to certify resource-bounded code in Hume, a domain-specific high-level programming language for real-time embedded systems.
Using formal models of resource consumption as a basis, the project will develop static analyses for time and space consumption and assess these against realistic applications for embedded systems. The work is novel in combining analyses of both source and machine code into a single framework.

InfoZert - Verification and Certification of Information Flows

The goal of this project is the development of technology enabling the specification of information flow policies in a state-oriented manner as well as the verification of policy conformance of system implementations.
It also aims to allow for generating certificates for policy-compliant system components with little personal effort on the code producer side, which can then producer-independently and automatically be checked by any code consumer prior to code execution.

Pro.Platz - Programmiersprachliche Aspekte sublinearer Platzkomplexitätsklassen

In diesem Projekt sollen Komplexitätsklassen, die durch geringen Speicherplatzbedarf gekennzeichnet sind, maschinenunabhängig und ressourcenfrei durch Verwendung von logischen und programmiersprachlichen Konzepten charakterisiert werden.
 Neben theoretischen Einsichten über die Natur dieser Klassen ist dies bei der Entwicklung automatischer Analysen zur Abschätzung von Laufzeit und Platzverbrauch von Programmen nützlich. Eine andere Anwendung ist die Entwicklung spezifischer Optimierungen, die sich aus der komplexitätstheoretischen Analyse ergeben.
 Für polynomielle Rechenzeit (P) und höhere Klassen sind solche Charakterisierungen seit längerer Zeit bekannt; für kleinere Klassen, die durch logarithmischen Speicherplatzbedarf definiert sind, existieren dagegen keine oder nur rudimentäre Ansätze.
 Im Zusammenhang mit den erwähnten Anwendungen sind gerade diese aber von besonderem Interesse bei stark ressourcenbeschränkten Szenarien, wie Peer-to-peer Computing, eingebetteten Systemen, mobilem Code. Obwohl im Projekt die theoretische Grundlagenarbeit im Vordergrund steht, werden solche Anwendungen exemplarisch untersucht.

APPSEM II - Applied Semantics II

APPSEM is a thematic network funded by the IST programme of the European Union.
 Its objective is to promote research into application-oriented semantics of programming languages.
 APPSEM does this by organising and sponsoring workshops, summer schools, and individual visits.
 APPSEM does not fund researchers or PhD students.
 The APPSEM research programme is structured into nine themes.
 More details can be found in the  Technical Annex and the Annual Report.

SIGNAL

Die Neueinführung des Pflichtfaches Informatik an den bayerischen Gymnasien erfordert die Nachqualifizierung von ca. 400 Lehrkräften bis zum Jahr 2007. Auf Initiative des Bayerischen Staatsministeriums für Unterricht und Kultus wurde im September 2001 mit Pilotkursen begonnen, Lehrerinnen und Lehrer auf das Staatsexamen Informatik vorzubereiten.
 Im September 2002 startete das bayernweite Projekt SIGNAL (Sofortprogramm Informatik am Gymnasium - Nachqualifikation von Lehrkräften), welches bis zum Sommer 2006 Lehrkräfte in Form von jeweils zweijährigen Kursen in Informatik nachqualifiziert.
 Die Zielsetzung dieser Nachqualifizierungskurse ist in erster Linie ein fundiertes Fachwissen in Informatik mit dem Abschluss 1. Staatsexamen. Weiterhin wird auf didaktische Aspekte des ab Schuljahr 04/05 am Gymnasium neuen Faches Informatik eingegangen.

MRG - Mobile Resource Guarantees

The Mobile Resource Guarantees (MRG) project has developed the infrastructure needed to endow mobile code with independently verifiable certificates describing its resource behaviour (space, time, etc.).
An article on MRG, explaining the results in general terms, has appeared in the IST Results website, and in EVCA Barometer.

Komplexität monotoner Schaltkreise und aussagenlogischer Beweissysteme

Es sollen Probleme aus der Komplexitätstheorie monotoner Schaltkreise und ihre Anwendung auf Probleme aus der Theorie der Komplexität aussagenlogischer Beweissysteme untersucht werden. Insbesondere sollen untere Schranken an die Tiefe und Größe boolescher Schaltkreise verbessert und auf weitere Klassen monotoner Schaltkreise (boolesche Schaltkreise mit unbeschränktem Eingangsgrad, monotone reelle Schaltkreise) verallgemeinert werden. Als Anwendung folgen neue und verbesserte untere Schranken für aussagenlogische Beweissysteme, etwa Varianten des Cutting-Planes Systems, mittels der Methode der effektiven monotonen Interpolation. Weiterhin soll untersucht werden, inwieweit diese Interpolationsmethode auf verschiedene, in der Literatur vorgeschlagene und neue, Erweiterungen von Cutting-Planes-Beweissystemen verallgemeinert werden kann.
 Außerdem soll die relative Komplexität von eingeschränkten Formen des Resolutionskalküls untersucht werden. Dabei sollen insbesondere solche Einschränkungen betrachtet werden, die in Anwendungen, etwa in automatischen Theorembeweisern oder in Erfüllbarkeitsalgorithmen, verwendet werden, beispielsweise negative/positive Resolution, reguläre und Davis-Putnam-Resolution oder lineare Resolution.

Type Systems for Resource-Bounded Computation

This project draws on ideas of Martin Hofmann, see his papers on the subject area.

 Laufende Projekte