[TYPES/announce] Postdoc and research engineer positions in Semantics and Verification for Secure Systems Software

[Peter Sewell]

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