Topic

When secret data is used by programs, there is a danger that this results in information leakage. While access control can prevent attackers from accessing secrets directly, a serious threat remains: An attacker might be able to learn secret information indirectly by observing the behavior of the program. Such vulnerabilities might have been inserted intentionally into a program by malicious developers or might have been introduced accidentally. Research on information-flow security aims at countering both threats.

There are many possibilities for how information might be leaked during the execution of a program, in particular for complex programs. All of these possibilities must be addressed by an information-flow analysis. Since this is tricky, reliable information-flow guarantees can only be obtained based on solid semantic foundations, that is, formal program semantics and formally defined security properties (like, e.g., noninterference). On such a semantic basis, analysis tools can be developed that provide a high degree of automation and reliable end-to-end security guarantees for software-based systems that operate on sensitive data. Formal foundations have many further benefits. For instance, verified security guarantees for systems often differ in very subtle ways. Formally defined security properties provide the precision needed for comparing such security guarantees to each other and, thereby, provide solid grounds to users for choosing a system that satisfies their security needs.

Ultimately, our goal in the research project is to create a flexible verification infrastructure for proving information-flow guarantees for programs using modular reasoning and to derive a taxonomy of the security guarantees that can be verified with our verification infrastructure.

The Position

In this position, you will develop and improve static program analysis techniques for proving information-flow security and develop tools that automate these analyses reliably and efficiently. You will capture varying degrees of security by formally defined security properties, derive a taxonomy of these security properties by comparing them to each other, and prove soundness guarantees for program analyses that you developed. For making information-flow analysis scale, you could develop modular analyses that are reliable and have high precision (e.g., by exploiting techniques like rely-guarantee reasoning or separation logic). Beyond proving soundness on paper, you could employ a theorem prover (like, e.g., Isabelle/HOL) to mechanize such proofs. By using automatic code generation of such theorems provers, you might even automatically generate implementations of analysis tools, in addition to programming them.

This position is associated with the ATHENE Mission QoSeC.

Prior Skills and Experiences

Prior knowledge in at least one of program analyses, formal methods, mathematical logic, or information-flow security, is expected. Competences in tool development, in using theorem provers, or in other aspects of IT-security are not expected, but would be a plus.

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
• 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 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.