Research Associate £32,816 - £40,322 or Senior Research Associate £41,526 - £52,559
Fixed-term: The funds for this post are available for 2 years in the first instance.
Are you interested in developing and applying semantics and verification techniques to improve the foundations and security of mainstream computer systems? We are looking for postdoctoral researchers to do exactly that, in two related projects:
(1) CHERI verification. CHERI (https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/) extends conventional Instruction-Set Architectures (ISAs) with architectural capabilities, for fine-grained memory protection and scalable software compartmentalization. CHERI allows memory-unsafe programming languages, eg C and C++, to be adapted to protect against many currently widely exploited security vulnerabilities. CHERI is a hardware/software/semantics co-design project, combining 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 ARMv8-A processor, to be available from late 2021. Morello is part of the UKRI £187M Digital Security by Design Challenge (DSbD), supported by the UK Industrial Strategy Challenge Fund and over £50M from 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/techreports/UCAM-CL-TR-940.pdf).
We are now collaborating with Arm and researchers at Edinburgh to do the same for the full Morello CHERI ARMv8 ISA, building on our Sail ARMv8-A ISA semantics (https://www.cl.cam.ac.uk/~pes20/sail/), and to study the semantics and security of higher-level languages and system software above CHERI, building on our Cerberus C semantics (https://www.cl.cam.ac.uk/~pes20/cerberus/). This verification could improve the security of all Arm mobile device software.
(2) Arm system software verification. We have an ongoing project, in collaboration with Google and with researchers at multiple institutions, to establish correctness and security properties of key system software above the ARMv8-A ISA semantics (https://www.cl.cam.ac.uk/~pes20/sail/), 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/).
We are looking for postdocs to contribute to all aspects of both projects. You should have a strong background in semantics and verification and the motivation and flexibility to develop practical ways to use them at scale for real systems. The ability to assist in the development of robust and widely usable tools based on the above is also desirable.
Experience in the following areas would be highly desirable:
- interactive theorem proving, in Coq, HOL4 and/or Isabelle
- program logics
- low-level system software
- programming language semantics and type systems
- programme analysis
- hardware verification
- functional programming, especially OCaml
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.
Further details may be obtained from Prof. Peter Sewell, Peter.Sewell@cl.cam.ac.uk
Click the 'Apply' button below to register an account with our recruitment system (if you have not already) and apply online.
You will need to upload a full curriculum vitae (CV) and a covering letter outlining your interests, potential contributions, and relevant past experience; you should also include the contact details for at least 2 referees.
Please quote reference NR21859 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.Apply online