GuideForce - Enforcing and analysing programming guidelines for secure web programming with type systems
|Period of project:||2014 - 2017|
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.
- 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)
|Period of project:||2010 - 2015|
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
|Period of project:||2009 -|
|Funding:||Microsoft Research Cambridge|
|Partner of project:||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
|Period of project:||2008 - 2017|
|Funding:||Doctorate Program Program- and Model Analysis, funded by DFG|
|Partner of project:||TU München|
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.