Research Positions in Program Analysis and Systems at University College London

Researcher Positions in Secure Computer Systems through Program Analysis 

The University College London (UCL) Department of Computer Science invites applications for three researcher positions at the intersection of secure computer systems and practical program analysis. Two postdoc positions and one research engineer position are
available. Those chosen to fill these positions will be part of the core team of investigators embarking on a new project to improve the security of real-world systems software (e.g., the Linux operating system, open-source web browsers such as Chrome and Firefox, and the Apache web server) through the development and application of novel automated program analysis techniques. This project is unique in that
it will attack systems security problems by bringing together researchers from the programming languages and computer systems areas--thus allying the strengths of the PL community in formal verification and program analysis with those of the systems community in making
principled and practical advances in the security properties of complex, real-world software.

Broadly speaking, systems approaches to enforcing security properties (such as confidentiality) introduce mechanisms that while powerful, are subtle to use correctly, and that may incur performance overheads (e.g., as with privilege separation with processes, which isolates memory at
the cost of context switches and TLB misses). Formal verification, by contrast, can statically prove that code upholds a property, but does not always yield precise results for every line of code in a vast code
base. By combining these approaches, we hope to use the benefits of each to mitigate the drawbacks of the other. If an analysis tool verifies that a piece of code upholds a property, it may not be necessary to deploy performance-reducing mechanisms such as separate processes to
enforce that property. But on parts of a program where such a tool cannot reach a sound and precise conclusion, such mechanisms provide the useful alternative of enforcing the property.

The work will involve the invention of new program analysis techniques that are sound and yet scalable, and precise enough to prove properties of real-world systems code of the size and complexity of Apache, Chrome, etc.: a significant open problem.

UCL CS is home to world-leading research groups in both programming languages and systems. PL researchers on the project will include Peter O'Hearn, Byron Cook, and Juan Navarro Perez, whose past contributions have included Separation Logic and the program analysis tools Space Invader, Abductor, SLAM, and Terminator. Systems
researchers on the project will include Brad Karp and Mark Handley, whose past contributions in systems security have included automated Internet worm signature generation systems, novel OS primitives to protect sensitive data in complex, legacy networked applications, and
novel secure network protocols and exploit-resistant protocol implementations, as embodied in such systems as Autograph, Polygraph, Wedge, and Tcpcrypt.

We anticipate that one postdoc will concentrate on data-related properties (e.g., memory and numerical safety), while the other will concentrate on temporal properties (e.g., protocol safety, termination). We are also more broadly interested in automatically discovering or abducing the privilege requirements of program components, and other information relevant to enhancing human
understanding of the security properties of real-world code. The successful candidates for these postdoc positions will come from either the programming languages or computer systems areas, with candidates whose research experience combines these areas seen as a particularly good fit. We are looking for postdocs with the aptitude and drive to become world-class researchers. Candidates should be comfortable both with the formalism and techniques of program analysis
and with building tools that run on real-world code.

Candidates for the research engineer position must hold (or be on track to hold upon starting work) a strong first degree in Computer Science, with significant system-building experience and systems security project experience looked on favorably. In addition to building tools in collaboration with the other researchers on the project, the successful candidate will have the opportunity to conduct research and contribute to the writing of research papers. It is possible, though not necessary, to combine this position with PhD
study. Candidates with advanced degrees who are interested in building sophisticated program analysis tools are also encouraged to apply.

All posts are funded for up to three years, subject to satisfactory performance. The project is funded by a major new grant in excess of GBP 850,000, as part of a national UK initiative on Automatic Program Analysis and Verification for Cybersecurity.

Information on the two postdoc positions, including how to apply (closing date 21st of May 2013) may be found on
 http://tinyurl.com/dxrcvjp

Information on the research engineer post, including how to apply (closing date 27th of May 2013) may be found on
 http://tinyurl.com/cr7atcu