[TYPES/announce] semantics/verification postdoc positions at Cambridge

[Peter Sewell]

We're advertising several positions, as below - if you know suitable
candidates, please pass this on. Thanks - Peter


Research Associates/Senior Research Associates in Rigorous Engineering for
Mainstream Systems (Fixed Term), University of Cambridge

Research Associate £32,816 - £40,322 or Senior Research Associate £41,526 -
£52,559

Fixed-term: The funds for these posts are available for 2 years in the
first instance, with a possibility of extension.

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 multiple 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, 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, HOL4, and/or Isabelle
- program logics
- low-level system software
- programming language semantics and type systems
- program analysis
- hardware verification
- 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.

There might also be the possibility of internship or PhD positions; for
these contact Prof. Sewell.

For more details of our recent work, see (https://www.cl.cam.ac.uk/~pes20/),
and especially REMS (https://www.cl.cam.ac.uk/~pes20/rems/index.html).

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 at cl.cam.ac.uk

Click the 'Apply' button at (http://www.jobs.cam.ac.uk/job/24501/) to 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20191218/350f65e0/attachment-0001.html>