[TYPES/announce] Postdoc in Munich (LMU) in programming language theory (secure coding) for 36 months

[Martin Hofmann]

We are looking for a

Postdoctoral researcher in programming language theory (secure coding) 
for 36 months

to work within the new DFG-sponsored project GuideForce whose goal is
to develop a framework for the rigorous specification of secure coding
guidelines in such a way that their strict observance can be
automatically checked. We plan to use a combination of methods 
including
Buchi automata, type systems, and aspect-oriented programming. See the 
project summary below for more detail.

The successful applicant
should have a solid background in at least one of the following
topics: program analysis, type systems, automata theory, security,
software engineering. Candidates with a very good and topical Master's
degree are also encouraged to apply; in this case it is possible to
base a PhD thesis on the project work.

Duration: up to 36 months

Start date: as soon as possible but not later than October 2014.

Remuneration: German scale 13 TV-L (38k-54k EUR p.a. according to age,
experience, family status)

Principal investigator: Martin Hofmann

Location: The project will be carried out at the Institute for
Informatics of Ludwig-Maximilians-Universität Munich, Germany.
LMU is an equal opportunities employer.

Applications should be sent by E-Mail to Sigrid Roden
roden at tcs.ifi.lmu.de as a single PDF file containing in particular CV
and the names of two potential referees. There is no
deadline. Applications will be assessed on an on-going basis until the
position is filled.

Questions about the position can be directed to the investigator
mhofmann at tcs.ifi.lmu.de.


Project summary:


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.