caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* [Caml-list] Morello: Edinburgh research posts on capability-based security technologies
@ 2021-03-28 17:51 Ian Stark
  0 siblings, 0 replies; only message in thread
From: Ian Stark @ 2021-03-28 17:51 UTC (permalink / raw)
  To: lfcs-interest, isabelle-users, types-announce, spls, sicsa-cyber,
	sicsa-theory, csf-attendees, coq-club, hol-info, caml-list

Morello: Digital Security by Design Technology Platform Prototype

Laboratory for Foundations of Computer Science
School of Informatics
The University of Edinburgh

  *** Applications close 2 April 2021 at 1600 UTC ***

We are recruiting two postdoctoral researchers to join the Innovate UK project 
"Digital Security by Design: Technology Platform Prototype".  This is a 
research collaboration between Arm and the Universities of Cambridge and 
Edinburgh to develop the Morello platform, applying a novel capability-based 
architecture to a mainstream high-performance processor and software stack.

Further information below: for full details and how to apply please follow the 
link above.

If you would like to discuss informally then please contact, the project lead for Edinburgh.

The University of Edinburgh only take formal references after appointment: if 
you have individual letters of support then please submit these as part of 
your initial application.

Follow these links for more about the wider project.

   Morello Platform:

   CHERI Architecture:

   Sail Language:

   Detailed developer information from Arm

   Video presentation of CHERI security architecture and Morello platform

The only essential requirement for these positions is that a PhD or equivalent
research experience in computer science, informatics, mathematics, or a
related discipline.  This includes being close to PhD completion and 

We are particularly interested to hear from candidates with any of the
following.  There is no requirement to demonstrate all of these together: this
project crosses domains and the precise tasks followed will depend on each
researcher's individual skills, experience, and interests.

- Experience with machine-assisted reasoning tools and automated provers: such
   as Coq, Isabelle, HOL4; or SAT/SMT solvers

- Experience with functional programming in OCaml

- Knowledge of instruction-set architectures; specifically Arm A64, but RISC-V
   also relevant

- Knowledge of programming-language semantics and type systems

- Knowledge of program logics, program analysis, and specification

Ian Stark                       Laboratory for Foundations of Computer Science School of Informatics, University of Edinburgh
The University of Edinburgh is a charitable body, registered in Scotland, with
registration number SC005336.

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2021-03-28 17:51 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-03-28 17:51 [Caml-list] Morello: Edinburgh research posts on capability-based security technologies Ian Stark

caml-list - the Caml user's mailing list

This inbox may be cloned and mirrored by anyone:

	git clone --mirror
	git clone --mirror

	# If you have public-inbox 1.1+ installed, you may
	# initialize and index your mirror using the following commands:
	public-inbox-init -V1 caml-list caml-list/ \
	public-inbox-index caml-list

Example config snippet for mirrors.
Newsgroup available over NNTP:

AGPL code for this site: git clone