Topic

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.

Modular verification can reduce the conceptual complexity of formal verification and program analyses substantially. However, benefiting from modular reasoning is often not straightforward. To ensure soundness, one needs to verify compositionality results that allow one to lift local guarantees, derived for individual program components, to global guarantees for the entire program. To obtain satisfactory precision, one often needs to track and exploit facts about the environment but without having to track too many such facts (as this increases conceptual complexity). In some domains (e.g., for verifying relational properties or quantitative security guarantees), sound compositional reasoning is still at its infancy. Finally, there might be multiple ways in how to decompose a program into components, and this might highly influence the benefits and costs of modular reasoning, hence, finding good splits into components is crucial.

The Position

In this position, you will 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. More concretely, your research

• could focus on developing techniques for decomposing security requirements for distributed systems (e.g., workflow-based systems) into local requirements for system components while guaranteeing that the local verification will contribute to the overall verification (i.e., enabling divide and conquer rather than risking divide and hope);
• could focus on new possibilities for modularizing quantitative program analyses (e.g., for side-channel security) while ensuring soundness in an information-theoretic sense;
• could focus on developing modular verification or program analysis techniques (e.g., for information-flow security or other relational properties) that feature better precision than existing ones (e.g., by performing rely-guarantee reasoning or by fine-grained distinction of how components are composed) and prove that soundness is ensured nevertheless; or
• could focus on developing innovative methods that conceptually split complex programs into simpler components to simplify formal verification.

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.

Prior Skills and Experiences

Prior knowledge of formal methods or mathematical logic is required. Beyond this, the four possible research directions on modular semantic-based program analyses differ in which skills are required.

• Research on decomposing security requirements:  Prior knowledge in at least one of program semantics, IT security or using theorem provers is required.
• Research on modular quantitative analyses:  Prior knowledge in at least one of information theory, program analyses, or using theorem provers is required.
• Research on improving precision:  Prior knowledge in at least one of program analyses, compositional reasoning, or using theorem provers is required.
• Research on helpful decomposition:  Prior knowledge in at least one of program analyses, compositional reasoning, or using theorem provers is required.

For all four directions you should be highly motivated to tackle challenging research problems, to produce innovative insights and tools, to strive for international visibility as a researcher, and be open minded. You need good language skills in English (writing and talking). Prior knowledge of the German language is not expected, but you should be willing to obtain basic skills within a year.

• research problems that are interesting, challenging, and relevant
• funded positions (salary depends on experience and percentage of employment) or scholarships
• excellent technical equipment and workplace
• competent mentoring and highly motivated colleagues
• a top Computer Science department in Germany (frequently the top CS department) with excellent B.Sc./M.Sc. students

TU Darmstadt is one of Germany's top technical universities with an outstanding reputation in research and education in Computer Science. TU Darmstadt is an equal opportunities employer and encourages applications from women. In case of equal qualifications, applicants with a degree of disability of at least 50% will be given preference.

The chair MAIS is led by Prof. Dr. Heiko Mantel. The overall goal of MAIS is to increase the trustworthiness and reliability of software-based systems. The working language at the chair is English.