Unterstützt von der Deutschen Forschungsgemeinschaft und dem Bundesministerium für Bildung und Forschung, arbeiten wir an den folgenden Forschungsprojekten:
|
IFC for Mobile Components
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. |
 |
|
InvasIC
Unter dem Begriff Invasives Rechnen soll ein völlig neues Paradigma für den Entwurf und die Programmierung zukünftiger paralleler Rechensysteme erforscht werden. Die Grundidee besteht darin, parallelen Programmen die Fähigkeit zu verleihen, in einer als Invasion bezeichneten Phase ressourcengewahr Berechnungen auf eine Menge aktuell verfügbarer Ressourcen zu verteilen, und nach paralleler Abarbeitung diese in einer als Rückzug bezeichneten Phase wieder frei zu geben. Um diese neue Art der selbstadaptiven und ressourcengewahren Programmierung auf zukünftigen MPSoCs (engl. Multi-Processor-Systems-on-a-Chip) effizient zu ermöglichen, bedarf es neuer Programmierkonzepte, Sprachen und Compilern wie auch Laufzeit- bzw. Betriebssystemen sowie revolutionärer Architekturerfindungen, die sich auf die Rekonfigurierbarkeit von sowohl Prozessor-, Verbindungs- als auch Speicherressourcen beziehen. |
 |
|
JOANA Framework Open-Source
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: Visit these projects sites for further information about publications and technical details.[mehr] |
 |
|
libFirm
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. [mehr] |
 |
|
PRAKTOMAT
Praktomat ist eine WWW-gestützte Praktikumsverwaltung zur besseren Qualitätskontrolle im Programmierpraktikum. Praktomat bietet:
[mehr] |
 |
|
Quis-Custodiet
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. |
 |
|
CoreC++
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. |
 |
|
KABA
Kaba analyses Java bytecode and creates a refactoring proposal, based on the use of members. |
 |