[TYPES/announce] Research Positions in Program Analysis and Systems at University College London

[O'Hearn, Peter]

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