Verification (Fixed Term) -
Fixed-term: The funds for this post are available until 30 September 2026 in the first instance.
Applications are invited for a full-time Research Associate/Senior Research Associate working with Professors Sewell and Krishnaswami in Systems Software Verification. The position is available to start as soon as possible.
Systems software is critical to our modern infrastructure, but it is pervasively subject to security flaws and attacks; it is trusted but not trustworthy. Advances in program verification over the last decades have brought formal verification of such software within reach, but there remains a wide gulf between existing verification technologies and the world of conventional systems software development.
CN (https: // www. cl.cam.ac.uk/~cp526/popl23.pdf), by Pulte et al., is an ongoing project aiming to improve the user experience and reduce the cost of verification, using a separation-logic refinement type system for C systems software, the realistic Cerberus semantics of C, and integration of testing and SMT- and Rocq-based verification. The CN specification language has carefully restricted expressiveness, to enable predictable proof automation (in the decidable fragment of SMT) and runtime testing of specifications.
This high-level position is to help develop CN, aiming to make it possible to routinely specify, test, and verify production systems software, with high fidelity to the underlying C and hardware semantics, and with substantially reduced effort.
It is part of the VERSE project, a DARPA-funded collaboration between Galois, U. Cambridge (Pulte, Krishnaswami, Sewell, and others), U. Penn (Pierce, Head, Weirich), UMD (Lampropoulos), EPFL (Pit-Claudel), UIUC (Ringer), U.Mass (Brun), and other industry partners. CN is being applied to examples from VERSE and to the open-source pKVM hypervisor, being developed by Google to protect Android. This provides a rich environment of developers and users, including HCI work to guide the development of a truly usable system.
Cambridge and the REMS research group (https: // www. cl.cam.ac.uk/~pes20/) offer a lively environment with researchers working on various aspects of systems semantics and verification.
Essential criteria :
A PhD or equivalent experience in Computer Science, or related subject area
Expertise in one or more of the following: SMT-based verification, proof- assistant verification and the Rocq (Coq) theorem prover, separation logic, static analysis, OCaml (the implementation language of CN), relaxed concurrency, C, systems code
The ability to work well both independently and within the CN and VERSE teams
The ability to contribute to the design of the system as a whole, and to the writing and presentation of research papers.
Considerable research experience with an excellent specialist knowledge in the discipline and of research methods/techniques .
The Department of Computer Science and Technology is an academic department that encompasses computer science along with many aspects of engineering, technology and mathematics. We have a world-wide reputation for academic research with consistent top research ratings. The Department has an open and collaborative culture, supporting revolutionary fundamental computer science research, strong cross-cutting collaborations internally and externally, and ideas which transform computing outside the University. Please follow the link at: https: // www. cst.cam.ac.uk to find out more about our Department.
Click the 'Apply' button below to register an account with our recruitment system (if you have not already) and apply online.
More information on the criteria for the role can be found in the further particulars.
Please quote reference NR42871 on your application and in any correspondence about this vacancy.
The University actively supports equality, diversity and inclusion and encourages applications from all sections of society.
The University has a responsibility to ensure that all employees are eligible to live and work in the UK. Please note that we provide the support of applying for the relevant visa (if required) and will reimburse the cost of the first visa.
Further informationDepartment of Computer Science and Technology, West Cambridge
Salary£36,024-£57,696
ReferenceNR42871
CategoryResearch
Published13 August 2024
Closing date10 September 2024