[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
A post-doctoral researcher position focusing on symbolic verification
techniques for cyber-security is available at Carnegie Mellon University at the
Silicon Valley Campus (Mountain View, CA). The research project titled
"Integrated Symbolic execution for Space-Time Analysis of Code (ISSTAC)"
involves symbolic execution of Java Bytecode for automatically identifying (1)
denial of service attacks (by determining worst case complexity of a program in
terms of both time and space usage) and (2) side channel attacks (by
determining if observations about the execution time or memory usage of a
program can leak secret information). This is a multi-year collaborative effort
with researchers from Vanderbilt University, University of California at Santa
Barbara and Queen Mary University, London. There are many research directions
within the scope of this project, including constraint solving and model
counting techniques, heuristics for scalable symbolic program analysis,
automated worst-case behavior analysis, quantitative information flow using
symbolic execution, attack and defense synthesis, distributed computations,
combinations of symbolic execution and fuzzing, etc.
Candidates for the post-doctoral position should have a doctoral degree in
computer science (or related field) and should have familiarity with symbolic
execution techniques and SMT-solvers. Security knowledge is a plus. Candidates
interested in this position should e-mail a CV, brief statement of research
interests and a reference (with e-mail address) to Corina Pasareanu
(corina.pasare...@west.cmu.edu).
The position is available now and will be open until filled. You can find more
information about the ISSTAC project here
http://www.cmu.edu/silicon-valley/research/isstac/.
