Current Projects

Future software sytems will be dynamically configured from mobile components, and will heavily use parallellism. Security checks thus have to deal precisely with mobile software components and their plug-in, as well as with parallel constructs and multi-threaded programs. Current information Flow algorithms for mobile components and multi-threaded software can be greatly improved if they leverage modern program analysis. In this project, we use information Flow control based on program dependence graphs for the construction of new and precise security analysis methods for mobile components and their dynamic integration, as well as for their concurrent interaction. New theoretical insights into the analysis of parallel programs and invariance detection (as developed at the Software Construction and Verification Group headed by Prof. Dr. Markus Müller-Olm) will improve analysis precision in particular for information Flow in parallel programs. New techniques for context approximation and context inference allow to construct modular dependence graphs and handle missing application contexts for isolated components. A scaling implementation for full Java is being developed and exercised on realistic case studies.
[more]

In the proposed TCRC, we intend to investigate a completely novel paradigm for designing and programming future parallel computing systems called invasive computing. The main idea and novelty of invasive computing is to introduce resource-aware programming support in the sense that a given program gets the ability to explore and dynamically spread its computations to neighbour processors similar to a phase of invasion, then to execute portions of code of high parallelism degree in parallel based on the available (invasible) region on a given multi-processor architecture. Afterwards, once the program terminates or if the degree of parallelism should be lower again, the program may enter a retreat phase, deallocate resources and resume execution again, for example, sequentially on a single processor. In order to support this idea of self-adaptive and resource-aware programming, not only new programming concepts, languages, compilers and operating systems are necessary but also revolutionary architectural changes in the design of MPSoCs (Multi-Processor Systems-on-a-Chip) must be provided so to efficiently support invasion, infection and retreat operations involving concepts for dynamic processor, interconnect and memory reconfiguration.
[more]

This is the homepage for the open source version of the JOANA framework. Joana is a program analysis framework for information flow control for Java programs. It has been developed as part of the projects:

• VALSOFT/Joana
• IFC for Mobile Components

libFirm is a C library implementing the Firm low-level intermediate representation. Firm is used to represent a computer program in order to analyse and transform it. Its main application is compiler construction where we use it to represent, optimize and transform C and Java programs to native machine code.

The most important features of Firm are that it is: low-level which means that the representation of the program is closer to machine code than to the language; completely graph based which means that there are no instruction lists or triple code, only data dependence and control flow graphs; completely SSA based which means that the code of the program is always in SSA form.

Research on libFirm led to advances in SSA construction, modeling of SSA based transformations, general graph transformation, code selection and register allocation.

Praktomat ist eine WWW-gestützte Praktikumsverwaltung zur besseren Qualitätskontrolle im Programmierpraktikum. Praktomat bietet:

• Automatisches Testen eingereichter Aufgaben
• Automatisches Überprüfung von Programmierrichtlinien
• Verwaltung von Testaten und Bewertungen eingereichter Aufgaben
• Rechnergestütztes Programmlesen

Software security analyses are nowadays of ever growing importance. But: Quis Custodiet Ipsos Custodes? (Who will guard the guards?). More and more such analyses are being published, many of them without any proof of correctness, others are happy with using pen-and-paper. This project is a cooperation of two groups (Universität Karlsruhe and TU München) to construct machine checked correctness proofs for several new precise techniques in the area of Language Based Security focusing on their semantical aspects resp. falsify published techniques.
[more]

One of the main sources of complexity in C++ is a complex form of multiple inheritance, in which a combination of shared ("virtual") and repeated ("nonvirtual") inheritance is permitted. Because of this complexity, the behavior of operations on C++ class hierarchies has traditionally been defined informally, and in terms of implementation-level constructs such as v-tables. We provide a formal treatment of the semantics of C++, focusing on the way it uses multiple inheritance. The formalisation was realised and machine checked in the theorem prover Isabelle/HOL, and we were able to prove the type safety of this formalisation. The type safety property that we prove is the fact that the execution of a well-typed, terminating program will deliver a result of the expected type, or end with an exception.
[more]

Kaba analyses Java bytecode and creates a refactoring proposal, based on the use of members.
[more]