Open Positions for Ph.D. Candidates and for Postdocs/Senior Researchers

• Formal Modeling and Tool-Supported Verification (Ph.D. candidate or Postdoc or Senior Researcher)
  
  Faithful formal models and tool-supported reliable verification are essential for establishing reliable guarantees for program analyses and, more generally, for IT systems. The development of complex analyses and IT systems is known to be error prone. Hence, formal methods should be applied in critical domains where bugs cannot be tolerated.
  Your research shall contribute to advancing formal modeling techniques, semantic-based verification techniques, and verification tools, and it shall contribute to ensuring the reliability of program analyses and program transformations using formal methods. For the latter, multiple application areas are possible that fit different backgrounds and interests.
  For more information on the position, click here.
  
  
• Static Side-Channel Analysis and Mitigation (Ph.D. candidate or Postdoc)
  
  When secret data is used by programs, there is a danger that this results in information leakage via side channels. Execution characteristics (like, e.g., running time or power consumption) might provide attackers with information that enables them, for instance, to learn a cryptographic key directly or in combination with a feasible brute-force attack. Meltdown, Spectre, and Platypus are prominent examples of such side-channel vulnerabilities.
  Your research shall contribute to detecting side-channel vulnerabilities, understanding their severity, mitigating them, and/or avoiding them by construction. Three complementary research directions are possible that fit different backgrounds and interests .
  For more information on the position, click here. This position is associated with the project "Secure Refinement of Cryptographic Algorithms" in the DFG CRC CROSSING.
  
  
• Efficient and Reliable Run-Time Monitoring and Enforcement (Ph.D. candidate)
  
  Run-time monitoring is a dynamic program analysis technique. In comparison to static program analysis, run-time monitoring has multiple advantages, including the possibility to achieve better precision due to the knowledge of actual values such as inputs to a system. If run-time monitoring is combined with enforcement mechanisms then this creates the possibility to alter the behavior of a target program on the fly and, thereby, to avoid policy violations. However, there are also disadvantages. Since run-time monitoring tracks the behavior of a target program while it is running, it is unavoidable that some overhead is induced (delays and memory usage). For applying run-time monitoring and enforcement, it is crucial to keep the overhead induced by this technology within acceptable limits and, hence, effective performance optimizations are desirable.
  Your research shall study the performance overhead of dynamic program analyses and contribute to reducing this overhead.
  For more information on the position, click here.
  
  
• Modularizing Semantic-Based Program Analyses (Ph.D. candidate)
  
  Modular reasoning is key to reducing conceptual complexity of analyzing practically relevant programs. Instead of reasoning about a program as a whole, one verifies properties of individual components and afterwards exploits them to derive properties of the entire program. Research on compositional verification aims at improving the efficiency of verification and at making verification scale to complex programs.
  Your research shall contribute to modularizing static / dynamic / hybrid program analyses, for instance, to enable modular reasoning about security requirements for distributed systems, to extend possibilities for modular reasoning about quantitative security guarantees, to improve the precision of modular verification techniques, or to identify conceptual splits into components that facilitate verification.
  For more information on the position, click here. This position will be associated with the project "Secure Refinement of Cryptographic Algorithms" in the DFG CRC CROSSING, with the project "Secure Refinement of Distributed Workflows" in the ATHENE mission TRUDATA, or with the LOEWE research focus Software-Factory 4.0 depending on the actual thematic focus.
  
  

In addition to positions in 3rd-party-funded research projects, we usually have financial flexibility to create additional positions on other research topics within our interests. In case you already have a research agenda and see a clear connection to our research interests, please feel invited to submit an application describing what research topic you have in mind. The more senior you are, the more elaborate the description of this research project should be. In your proposal, you should clearly indicate connections to our research topics and to publications by us.

For candidates with a Ph.D. and a strong publication record, there also is a possibility to apply for a position based on seed-funding for up to 1 year with a clear intention to apply for a new 3rd-party-funded research project that funds a continuation.