The Coq mailing list

[Peter Sewell <Peter.Sewell AT cl.cam.ac.uk>]

Postdoc and research engineer positions in Semantics and Verification for Secure Systems Software

Advert: http://www.jobs.cam.ac.uk/job/28012/
Closing date: 13 January 2021

Are you interested in developing and applying semantics and verification techniques to radically improve the foundations and security of mainstream computer systems? We are looking for postdoctoral researchers and research assistants to do exactly that, in a wide range of topics.

In recent years, working with Arm, IBM, RISC-V International, the CHERI team, the C and C++ standards committees, and others, we have shown how one can develop and use authoritative semantics for full-scale architecture and language definitions, including instruction-set architectures of ARMv8-A, RISC-V, and CHERI in our Sail metalanguage (https://www.cl.cam.ac.uk/~pes20/sail/), our Cerberus C semantics (https://www.cl.cam.ac.uk/~pes20/cerberus/), and relaxed-memory concurrency models at the architecture and C/C++ language levels. These use a combination of semantic definitions made executable as test oracles, test generation, symbolic execution, and mechanised proof; they have resolved many questions about what these fundamental abstractions are or should be; and they can enable both lightweight formal engineering and full verification of key parts of real systems.

We now aim to build above this in two related projects, for CHERI and Arm system software.

(1) CHERI verification. CHERI (https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-941.pdf, https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/) extends conventional hardware Instruction-Set Architectures (ISAs) with new architectural features, using capabilities, to enable fine-grained memory protection and highly scalable software compartmentalization. The CHERI project is led by Robert Watson, Simon Moore, and Peter Sewell at the University of Cambridge and Peter Neumann at SRI International. CHERI allows historically memory-unsafe programming languages such as C and C++ to be adapted to protect against many currently widely exploited security vulnerabilities, and enables the fine-grained decomposition of operating-system (OS) and application code, to limit the effects of security vulnerabilities. CHERI is a hardware/software/semantics co-design project, bringing together computer architecture, systems software, security, and semantics.

In October 2019, Arm announced Morello (https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-morello.html), an experimental CHERI-extended, multicore, superscalar ARMv8-A processor, System-on-Chip (SoC), and prototype board. Morello is a part of the UKRI £187M Digital Security by Design Challenge (DSbD), supported by the UK Industrial Strategy Challenge Fund, including a commitment of over £50M by Arm. Morello will support industrial-scale evaluation of CHERI, with a view to mass-market adoption - which would transform the security landscape.

We have previously developed rigorous engineering methods (https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-formal.html) to precisely define the CHERI ISA, for CHERI-MIPS and CHERI-RISC-V variants, and to prove (in Isabelle) that they satisfy key intended security properties (https://www.cl.cam.ac.uk/users/pes20/cheri-formal.pdf). We are now collaborating with Arm and researchers at the University of Edinburgh to do the same for the full Morello CHERI ARMv8 ISA, building on our Sail ARMv8-A ISA semantics, and to study the semantics and security of higher-level languages and system software above CHERI, building also on our Cerberus C semantics (https://www.cl.cam.ac.uk/~pes20/cerberus/). Morello and this verification aim to improve the security of all Arm mobile device software.

(2) Arm system software verification. This ongoing project, in collaboration with Google and with researchers at MPI-SWS, Radboud, SNU, and Aarhus, aims to establish correctness and security properties of key hypervisor system software above the ARMv8-A ISA semantics mentioned above, integrated with the ARMv8-A concurrency architecture (including both the previous "user-mode" models and the system concurrency semantics, being developed in collaboration with Arm) (https://www.cl.cam.ac.uk/~pes20/armv8-mca/). The Cambridge work is led by Peter Sewell, Neel Krishnaswami, and Robert Watson. Here too, there is the prospect of the resulting system being very widely deployed.

We are looking for postdocs and research assistants to contribute to all aspects of both projects. You should have a strong background in semantics and verification, the motivation and flexibility to develop practical ways to use them at scale for real systems, and experience in one or more of:

- interactive theorem proving, in Coq and/or Isabelle (we use both)
- program logics (especially separation logics and Iris)
- relaxed-memory concurrency
- low-level system software
- programming language semantics and type systems
- program analysis
- model checking
- computer security
- functional programming

We are also seeking candidates with a research engineering focus, to assist in the development of robust and widely usable tools based on the above. For this, you should have experience in functional programming, especially OCaml.

For more details of our recent work, see (https://www.cl.cam.ac.uk/~pes20/), and especially the REMS (https://www.cl.cam.ac.uk/~pes20/rems/index.html) and CHERI (https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/) projects, which are both lively and effective collaborations.

The positions are available to start as soon as possible. For candidates with substantial relevant expertise, we may be able to appoint at the Senior Research Associate level.

Research Assistant (without PhD): £26,715-£30,942, Research Associate (with PhD): £32,816-£40,322, or Senior Research Associate: £41,526-£52,559. Appointment to Senior Research Associate will be considered for exceptional candidates.

Fixed-term: The funds for these posts are available for 2 years in the first instance.

Further details may be obtained from Prof. Peter Sewell, email Peter.Sewell AT cl.cam.ac.uk

You will need to upload a full curriculum vitae (CV) and a covering letter outlining your interests, potential contributions to the project, and relevant past experience; both in pdf format. You should also include the contact details for 2 referees who will be able to promptly provide letters if requested. If you upload any additional documents which haven't been requested we will not be able to consider these as part of your application.

Due to the current circumstances, there may be a possibility for remote working in the first instance. Please contact the HR Manager to discuss the finer details.

Please quote reference NR25056 on your application and in any correspondence about this vacancy.

Apply online: http://hrsystems.admin.cam.ac.uk/recruit-ui/apply/NR25056

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.