Open Positions

Postdoc and Ph.D. Positions in Security & Concurrency with Formal Methods

The Chair MAIS is offering multiple positions. We are looking for researchers who are interested in addressing foundational problems that will be of practical relevance or in addressing practical problems based on formal methods. The research focus shall be on software security, concurrency, or their combination.

Modular Reasoning about Information-Flow Security (Postdocs and/or PhD candidates)

possible topics include
- theoretical foundations for sound security analyses and for security by design
- modular security analyses across components (horizontal modularity)
- modular security analyses across system layers (vertical modularity)
- security guarantees for entities (e.g. libraries) usable in modular reasoning
- increasing the precision of modular reasoning by rely-guarantee reasoning
- development/improvement of security analyses tools (e.g. for mobile apps)
In your research you could build on our existing information-flow analysis tools
(including Cassandra and SPASCA).

Sound Program Analysis under Relaxed Consistency Guarantees (Postdoc or PhD candidate)

possible topics include
- formalizing semantics of languages under weak memory models
- relating axiomatic and operational formulations of semantics with relaxed consistency
- experimental evaluation of weak memory models (litmus tests)
- analysis of effects of relaxed consistency on the soundness of program analyses
- optimization of program analyses for specific weak memory models
- targeted insertion of synchronization/fences to ensure soundness of program analyses
- development of sound analyses tools
In your research you could build on our existing generic framework for defining operational
semantics under relaxed consistency guarantees in Isabelle/HOL.

Sound Re-Engineering of Code for more Parallelism (Postdoc)

possible topics include
- dependency analysis of existing code (C, C++, or machine code)
- sound modularization of existing code based on dependence information
- sound parallelization of existing code
- development of tool support
- case studies in the areas high-performance computing and/or Industrie 4.0
In your research you could benefit from our collaborating partners in the Software-Factory 4.0 project.

Definition of Security Requirements and Security Policy Languages (Postdoc or PhD candidate)

possible topics include
- development/extension of security policy languages
- application of security policy languages in usage control
- application of security policy languages in information-flow control
- decomposition of global security policies into local policies
- persistent guarantees under dynamically changing security policies
- development of tools for policy engineering
- case studies in usage control and information flow control
In your research you could benefit from our tools for usage control and information-flow
control (CliSeAu, Cassandra, SPASCA, and the Side-Channel Finder)

How to Apply

Information on how to apply is described in the PDF version of the position announcement, available below.

PDF version of the position anouncement

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang