Abgeschlossene Forschungsprojekte
GuideForce: Enforcing and analysing programming guidelines for secure web programming with type systems
| Laufzeit: | 2014-2017 |
| Finanzierung: | DFG-Sachbeihilfe |
Modern software typically must be able to interact with the whole world. While until recently such worldwide interaction was quite rare now almost any business software has a web interface allowing anyone to interact with the software be it only by entering a wrong password.
Since almost anyone writes software exposed to the resulting security threats, one can no longer rely on high skill and experience of specialists who were formerly the only having to deal with such risks. To address this issue programming guidelines and best practices have been developed, see e.g. www.owasp.org, that summarise and condense the expert knowledge and make it available to a larger community (secure coding). Whether or not such programming guidelines are applied and whether they have been correctly applied, is however left to the good will of the programmers. In this project we want to develop automatic methods based on type systems that are capable of checking that programming guidelines have been correctly and reasonable applied without compromising the flexibility of writing code. Besides further developing type system methodology this also requires us to devise a formalism in which to rigorously define such policies which typically are given in plain English and by examples. In order that users will actually trust the system and perceive it as a useful tool it will be necessary to achieve a rather high degree of accuracy. For example, if an already sanitized user input is stored in a string buffer and later on read out it is not necessary to re-sanitize it. If the system does not recognize such a situation users will neglect its warnings in the future. Similarly, if we want to ensure appropriate authorisation prior to accessing sensitive data then, if such access happens within a method of a class admitting the invariant that authorization has taken place prior to creation of any of its objects then the system must be able to discover this. All this means that cutting edge techniques such as careful analysis of strings, objects, and control flow, must be harnessed and further developed in this project. In order to guarantee appropriate feedback to the user and to achieve seamless integration we will use type-theoretic formulations of these methods resulting then in a single customizable type system capable of enforcing a large span of guidelines and best practices for secure web programming.
A running example will be the security threat posed by code injection where a malicious user inputs strings containing code fragments that may potentially be executed. Other examples will be provided by industrial contacts such as SAP Research and from topical WWW portals such as OWASP and SANS.
The key scientific innovations of the project are the focus on guidelines rather than risks and the development of a configurable type system.
Publications:
- Martin Hofmann, Wei Chen: Abstract interpretation from Büchi automata. CSL-LICS 2014: 51
- Martin Hofmann, Wei Chen: Büchi Types for Infinite Traces and Liveness. CoRR abs/1401.5107 (2014)
- Lennart Beringer, Robert Grabowski, Martin Hofmann: Verifying pointer and string analyses with region type systems. Computer Languages, Systems & Structures 39(2): 49-65 (2013)
- Robert Grabowski, Martin Hofmann, Keqin Li: Type-Based Enforcement of Secure Programming Guidelines - Code Injection Prevention at SAP. Formal Aspects in Security and Trust 2011: 182-197
PURPLE: Pointers as an abstract data type: complexity-theoretic and programming-language aspects (PURPLE)
| Laufzeit: | 2010-2015 |
| Finanzierung: | DFG-Sachbeihilfe |
In programming languages and logics, graphs and similar data structures are often treated as structured data rather than bit-sequences or words. This means that elements of abstract data structures are often accessed using pointers, which support only a restricted set of operations, such as lookup, update and test for equality. The concrete representation of pointers remains hidden. Traditional computability and complexity theory, on the other hand, rely on concrete representations of data.
In this project we want to explore the expressivity of abstract pointer concepts in the sense of complexity theory. In particular we aim at a separation of programming language versions of LOGSPACE and PTIME. For example, we conjecture that the PTIME-complete problem of Horn-satisfiability cannot be solved with a constant number of abstract pointers, even in the presence of non-determinism or an oracle for reachability.
Additionally, we want to contribute to the formal specification and verification of programs with abstract pointers. For instance, we would like to ascribe rigorous meaning to preconditions like ‘It makes no guarantees as to the iteration order of the set …’ in the specification of the HashSet class in java.util.
Verifikation von effektbasierten Programmtransformationen
| Laufzeit: | 2009-? |
| Finanzierung: | Microsoft Research Cambridge |
| Projektpartner: | Microsoft Research Cambridge |
This informal research collaboration between LMU Munich and Microsoft Research Cambridge (Andrew Kennedy, Nick Benton) aims at developing a rigorous theory of equivalence of programs with procedure variables about which some effect information is known.
For example, the equivalence e;e = e is in general not valid; however, it does hold if the memory regions e reads from are disjoint from the ones it writes to and moreover e does not make allocations.
We develop a semantic theory of such equivalences in the presence of higher-order functions and object-orientation with the aim of rigorously justifying program transfromations based on effect information.
PUMA: Graduiertenkolleg Programm- und Modell-Analyse
| Laufzeit: | 2008-2017 |
| Finanzierung: | Doctorate Program Program- and Model Analysis, funded by DFG |
| Projektpartner: | TU München |
| Offizielle Website: | http://puma.in.tum.de/wiki/Doctorate_Program_PUMA |
The doctorate program (Graduiertenkolleg) PUMA brings together the four fundamental approaches of program and model analysis, namely, type systems, theorem proving, model-checking, and abstract interpretation. Its goal is to develop new analysis techniques through cross-fertilization. The new methods should prototypically be implemented and be evaluated on selected analysis problems of software-intensive systems.
PolyNI: Verification of polymorphic noninterference for mobile code
| Laufzeit: | 2010-2013 |
| Finanzierung: | DFG Sachbeihilfe |
This project focusses on technologies to verify information flow security propertiesthat partly depend on the execution environment. Motivated by mobile application scenarios, we plan to develop specification notations forparametric noninterference policies, and to define type systems and program logics to statically certify these policies for Java and bytecode programs.
MLSolver: A Solver for Modal Fixpoint Logics
| Laufzeit: | 2009-? |
Aim of this project is to develop a satisfiability and validity solver for various modal fixpoint logics like the modal and linear-time mu-calculus, CTL*, PDL, etc. It is based on PGSolver.
PGSolver: A Parity Game Solver
| Laufzeit: | 2008-? |
Aim of this project is to develop an efficient parity game solver.
CFSC: Computational Foundations of Social Choice
| Laufzeit: | 2008-2011 |
| Finanzierung: | ESF collaborative research project |
This collaborative research project will address some of the key issues in computational social choice, an interdisciplinary field of study at the interface of social choice theory and computer science. It aims at deepening our understanding of algorithmic and complexity-theoretic issues in social choice, at developing logic-based languages for modeling and reasoning about choice problems and preference structures, and at applying established techniques from AI, such as preference elicitation and learning, to problems of collective decision making.
PAMAS: Preference Aggregation in Multiagent Systems
| Laufzeit: | 2005-2010 |
| Finanzierung: | Nachwuchsgruppe im Emmy-Noether-Programm (Aktionsplan Informatik) der DFG |
The PAMAS research group is devoted to studying distributed protocols that allow autonomous entities to aggregate their conflicting preferences. Well-known examples of conventional preference aggregation among humans are auctions and voting. Scientific fields that traditionally deal with preference aggregation, such as social choice theory, game theory, mechanism design, and implementation theory reside somewhere on the boundaries of economics, mathematics, and political science. During the last years, preference aggregation has experienced a dramatic increase of attention from computer scientists coming from various fields such as artificial intelligence, theory, or networking. Computer science extends existing research by introducing computational and communication efficiency, decentralized mechanism execution, correctness, privacy, or new applications like scheduling, file-sharing, or knowledge transfer. The lab is hosted by the chair for theoretical computer science at the University of Munich and is funded by the DFG (German Research Foundation) within the Emmy Noether Program.
VeriNonReg: Verifikation nicht-regulärer Eigenschaften
| Laufzeit: | 2005-2009 |
| Finanzierung: | DFG Sachbeihilfe |
The verification of non-regular program properties involves the investigation of program models which are structurally more complex than usually assumed in this context. Non-regularity is here to be understood in the sense of formal language theory, i.e. regarding the more expressive segments of the Chomsky hierarchy such as the context-free or context-sensitive languages. In order to capture these languages, a similarly increasing expressivity is needed on the specification side.
Several different logics capable of expressing context-free and context-sensitive properties have been proposed in the literature (follow the links to see a list of publications/ information):
- Fixed Point Logic with Chop (FLC)
- Higher Order Fixpoint Logic (HFL)
- Propositional Dynamic Logic of non-regular grammars (PDL[CFG], PDL[IG])
- Modal Iteration Calculus (MIC)
Example properties are unlimited counting, absence of buffer underflows (for unlimited buffer sizes) or bisimilarity to a balanced tree, just to name a few. The project aims at comparing these logics regarding expressivity and to develop model checking algorithms for them. As expressivity increases, the meaning of “model checking” is less restricted to “method used in program verification” but must be viewed as a general logic problem in which various important and general problems can be encoded. It is for example possible to solve universality of nondeterministic finite automata, satisfiability of modal logic K and evaluation of quantified boolean formulas as instances of the model checking problem for the first-order fragment of HFL (HFL1).
Taking a model checking algorithm as a template to analyze problem structures bears a high potential for optimizations, in particular, if we take into account that the formulas for these logics are typically fixed regardless of the input size.
Formulas of the above logics tend to be difficult to read. Simplifications of the logical syntax (maybe at the cost of lesser expressivity) are desirable with regard to the development of verification tools that can be used by engineers without a formal background. The goal here is to extract fragments of these logics for which intuitive specification languages can be provided.
Mobius: Mobility, Ubiquity and Security
| Laufzeit: | 2005-2009 |
| Finanzierung: | Integriertes Projekt im Rahmen der FET Global Computing Proactive Initiative der Europäischen Kommission |
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
| Laufzeit: | 2005-2009 |
| Finanzierung: | Funded under Framework VI of the EU, as research project IST-510255 (FET-OPEN programme) |
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
| Laufzeit: | 2007-2008 |
| Finanzierung: | DFG-Sachbeihilfe |
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
| Laufzeit: | 2005-2009 |
| Finanzierung: | DFG Sachbeihilfe |
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
| Laufzeit: | 2003-2008 |
| Finanzierung: | Projekt im IST-Programm des EU 5th Framework Programme |
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
| Laufzeit: | 2002-2006 |
| Finanzierung: | Projekt des Bayerischen Kultusministeriums zur Nachqualifikation von Gymnasiallehrern bis 2005 |
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
| Laufzeit: | 2002-2006 |
| Finanzierung: | Projekt im IST Programm des EU 5th Framework Programme |
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
| Laufzeit: | 2001-2006 |
| Finanzierung: | Nachwuchsgruppe im Emmy-Noether-Programm der DFG |
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
| Laufzeit: | 2000-2002 |
| Finanzierung: | EPSRC Projekt |
This project draws on ideas of Martin Hofmann, see his papers.
Laufende Projekte
Artikelaktionen