[TYPES/announce] Research positions in Systems Software Verification

[Peter Sewell]

Research positions in Systems Software Verification

Applications are invited for full-time research positions working with
Professors Sewell and Krishnaswami in Systems Software Verification. The
positions are available to start as soon as possible; the funds for the
posts are available until 30 September 2026 in the first instance.

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://urldefense.com/v3/__https://www.cl.cam.ac.uk/*cp526/popl23.pdf__;fg!!IBzWLUs!RA-lKkxEiARH_gGyAtC77Vo427g4920ZapNNfOYjPu3ferRVURW3__mu6RI5bdH7QIzegOrcL5-qMTFwC3Qxy4a1Qo7MnDPTAW3rjI73yQ$ ), 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.

These positions are 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.

They are 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://urldefense.com/v3/__https://www.cl.cam.ac.uk/*pes20/__;fg!!IBzWLUs!RA-lKkxEiARH_gGyAtC77Vo427g4920ZapNNfOYjPu3ferRVURW3__mu6RI5bdH7QIzegOrcL5-qMTFwC3Qxy4a1Qo7MnDPTAW2S2u__5g$ )
offer a lively environment with researchers working on various aspects of
systems semantics and verification.

Essential criteria:

- 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 positions are available at one of three grades: Research Associate (the
normal postdoc grade), Senior Research Associate (for those with more
experience), and Research Assistant (for those without a PhD). Formally,
there are two open adverts:

- Research Associate/Senior Research Associate (£36,024- £44263 or £45,585-
£57,696), NR42871, Closing date 10 September 2024
- Research Assistant/Research Associate (£29,605- £33,966 or £36,024-
£44,263), NR42880, Closing date 6 September 2024

See https://urldefense.com/v3/__https://www.jobs.cam.ac.uk/job/?unit=u00194__;!!IBzWLUs!RA-lKkxEiARH_gGyAtC77Vo427g4920ZapNNfOYjPu3ferRVURW3__mu6RI5bdH7QIzegOrcL5-qMTFwC3Qxy4a1Qo7MnDPTAW2LI3FNug$  for the details and the
further particulars. Please quote those reference numbers on your
application and in any correspondence about these vacancies.

- for the first, you should have a PhD or equivalent experience in Computer
Science, or related subject area
- for the second, appointment at Research Associate level is dependent on
having a PhD. Those who have submitted but not yet received their PhD will
be appointed at Research Assistant level, which will be amended to Research
Associate once the PhD has been awarded.

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 see https://urldefense.com/v3/__https://www.cst.cam.ac.uk__;!!IBzWLUs!RA-lKkxEiARH_gGyAtC77Vo427g4920ZapNNfOYjPu3ferRVURW3__mu6RI5bdH7QIzegOrcL5-qMTFwC3Qxy4a1Qo7MnDPTAW0UQFyAbQ$  to find out more about our Department.

More information on the criteria for the role can be found in the further
particulars.

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20240814/d2c47cd5/attachment-0001.htm>