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 areavailable. 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 thatit 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 makingprincipled 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 atthe 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 codebase. 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 toenforce 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. Systemsresearchers 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, andnovel 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 humanunderstanding 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 analysisand 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 PhDstudy. 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/dxrcvjpInformation on the research engineer post, including how to apply (closing date 27th of May 2013) may be found on http://tinyurl.com/cr7atcu