Position on Information-Flow Security (Ph.D. or PostDoc/Senior Researcher)
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.
For a Ph.D. position, you should have a M.Sc. in Computer Science, Mathematics, or Electrical Engineering or be about to graduate within a few months.
For a postdoc position, you should hold a Ph.D. or have completed all requirements for your Ph.D. upon start of employment.
For a senior-researcher position, you should already have at least 1 year of research experience after your Ph.D. and have good organizational skills.
For both, postdoc positions and senior-researcher positions, you must have demonstrated your ability to perform research at an internationally competitive level by multiple reviewed publications.
Please submit your application to recruiting@mais.informatik.tu-darmstadt.de, attaching your application package as pdf-file(s).
Your application package should include
your detailed CV,
a letter explaining your motivation for the position and outlining relevant prior work and experiences,
for each of your degrees, complete transcripts (including certificates of degrees, lists of courses, and individual grades), and
all theses or final projects that you have completed for your degrees.
If you are applying for a postdoc or senior-researcher position, you should include in addition
complete list of publications,
up to three selected publications, and
if possible, up to three references whom we may contact for letters of recommendation.
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.