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.sew...@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.
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
