coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Morello: Edinburgh research post on capability-based security technologies

From: Ian Stark <Ian.Stark AT ed.ac.uk>
To: coq-club AT inria.fr
Subject: [Coq-Club] Morello: Edinburgh research post on capability-based security technologies
Date: Fri, 11 Mar 2022 19:25:54 +0000 (GMT Standard Time)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Ian.Stark AT ed.ac.uk; spf=Pass smtp.mailfrom=Ian.Stark AT ed.ac.uk; spf=Pass smtp.helo=postmaster AT loire.is.ed.ac.uk
Ironport-data: A9a23:3o4QAawa845gy8TtY9x6t+flwCrEfRIJ4+MujC+fZmUNrF6WrkUDy GAeXW3VPKmKNmuhKttwYdzl8xkBuZOGytdiHAc6rVhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefQAOOU5NfsYkidfyc9IMsaoU8lyrZRbrJA24DjWVvW4 Iqq+aUzBXf8s9JKGjJMg068gEg31BjCkGtwUosWOJinFHeH/5UkJMp3yZOZdxMUcaEIdgKOf Nsv+Znilo/vE7jBPfv++lrzWhVirrc/pmFigFIOM0SpqkAqSiDfTs/XOdJEAXq7hQllkPh9l /VxqI67TTwMP/HGwusMXBtUAixhaPguFL/veRBTsOSXyEzcfj3t2LNjAAc/NssF+Y6bA0kXr 61ecmlQKEndwbvuqF64YrEEasALDcDtergDs2tj5TzVS/8tB43AK0nPzYUFg2xg3JgSdRrYT 8YFRzwofQnRWEQMPGoQJYI/28W12VCqJlW0r3rO+fRrujGJpOBr65DmN8OQcdiXT+1Oj0OAr yTH+X74C1cULrSiJSGt9nWtnOKJnDi9VY5UHbb+6/0CbECvKnI7BEI2aUapqv2Cr0/iUYhQO kMW9jsjsv1nnKC0deXVUxq9qX+CmxcTXdtMDuE3gD1hLIKJum514UBYH1Z8hMwaWNweGGF7i g/Z9z/9LXk06ePOEBpx45/JxQ5eLxT5OkctT0fopyMo79jlqpwpgRKnoj1LPY7l5jEZMQr7x CyOpS4y74j/YOYP0KSh8BbGmHShqt7ARUgo5W07v15JDCsnO+ZJhKTxtzA3CMqsyq7FEjFtW 1BYwKCjABgmV83lqcB0aLxl8EuVz/iEKibAplVkAoMs8T+gk1b6I9wOsWohfB8xbJtdEdMMX KM1kV0KjHO0FCXxBZKbn6rqUZRCIVXISo64DayINrKinLAoLVbXpEmCmnJ8L0i2zBZwyPhlU XtqWcSlC3sGQblhzSS7Xfwcza5jwC0i2mTJRvjGI+ePj9KjiIquYe5dajOmN7hnhIvd+VW92 4sBa6OilksOOMWjMni/2dNCdjgicClrbbio8JY/XrDYfWJb9JQJUKK5LUUJINA+wMy4V47go hmAZ6Ov4AGm1COddlnSNCwLhXGGdc8XkE/X9BcEZT6As0XPq672hEvGX5doL7Qh6sJ5yvt4E 6sMd8maUqZCRnLO8HIAbsCl/oBlcR2qgyOIPjakOWBhIcYwFlKRotK0LBHy8CQuDzassZdsq bOX0A6GE4EIQB5vDZqLZf/2lwGxsHERlfhcRUzNJtUPKkzg/JI6eSH9yPY8ZdwPcE2Ryjyf3 geQIBEZueiU+9FrqImY2/jcot7wQeVkH0dcE23K1pqMNHHXrji53ItNcOeUZjSBBmn6z6OvO LdOxPbmPfxbwVtHvtYuE7tvyq5itdLjq6UDkVZgG3TRYhKqEfVtLj+P1o9StfQVlLNevAK3X GOJ+8VbYO3XZpu1QQBJfAd1PP6e0fw0myXJ6apnKkvN5BhooOiNX3JUMkTekydaNrZ0bd0om L9zpM4M5gWjoRM2KdLa3DtM/mGBIyBSSakhrZ1GUobnhhBylQNGZp3GB2n3+9eCZ5NFOQ83I WbM1qbFgr1dwGvEcmYyTCCTg7IN1MpW4B0ankUfI1mpm8begqFl1hNm8QMoElZfwCJB3r8hI WNsLUB0ePuDpm86mMhZUmmwMAhdHxnFqFfpwl4EmWCxo5NEjYARwLnR+Nph/Xz1N0pYeTlB8 feZ0yDoXXDjd4fs3UPenGZ7/uf7Q4UZGhLqwaia8watRvHWogYJRoejaSwBoF36AqvdQWXZ8 PJy8r8YhbLTbEYtTm5SN2Ve/bkcDhmPYnFBKR2kEGXlAkmEEAyPNfOyx4xdty+DyzEmMaN1N iC2Gv9yag==
Ironport-hdrordr: A9a23:Gdqst6oWbKDUvbBQ+eTrZMMaV5oheYIsimQD101hICG9E/bo9P xG88536faZslossRIb+exoWpPgfZq0z/cciuMs1NyZMjUO1lHGEKhSqafuwzrqBzbx96pm36 9mdKRyYeeAb2RHsQ==
Ironport-phdr: A9a23:SXELZx85PM9PG/9uWSC2ngc9DxPPW53KNwIYoqAql6hJOvz6uci4Z gqGv68m1QaYFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoV J8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9qp2+yo5pHffRtEiDWgbb9vK Bi9sBncuNQRjYZ+MKg61wHHomFPe+RYxGNoIUyckhPh7cqu/5Bt7jpdtes5+8FPTav1caI4T adFDDs9KGA6+NfrtRjYQgSR4HYXT3gbnQBJAwjB6xH6Q4vxvy7nvedzxCWWIcv7Rq0yVD+/7 alkVQXohT8JOTA57m/Zl89+g61Hrx+6uxxz35TZbJ2JOPZiYK/Qe84RS2pbXsZWUixMGoCyY JEJD+EcIOhYs5Pyp0ENrRCjAgSiB/ngyjlSinHrwa01yf4hEQLd0QM+At0Cqm7bo8nvOKcPU uC41a/FxijMYP1Kwzny8pTIcgw/rvGWW7J9adbdxEouGg3LgFudrYzoMi6X2+kOrmSW7uVtW +2vhmAntw18oDeiy9kth4fJmI4YyVLJ+CR2zYg1K9O2Rk52bcKiHZBNuS+aMI52TdkjQ2Fuo Cs6yLoGtoWgfCQQ0pso2wTTa+GEc4SQ/B3sSfydLi1ki35/ZbK/hA6+/lSgyuLiTMm00U9Go TZdktnRrHwN0AbT6sefRvRn5Eeh3CyD2BzU6uFBOUw0kK3bK4Q/zb40kpoTtl3PHjfsmEXxj q+ZaFkr+vSy5+TgeLXmqYeQOJNuhQH7KKghgNCwDf4lMggNR2Sa+eO81KD//U3kWrlFleM5n rHEv5DBPssUu7S1AxNL3Yk/6xayCSqt3tcAnXQfMV5JZhaKg5L3N13TIP30F+qzjlW2nDt22 /zKJrPsDojXInTejrvscqxx51NBxAc819xS45ZZB7ccK/zpQEDxrsbXDhohPgy03ennDNJ92 5saWWKIA6+ZKr3dvUWJ5uI0OeWDepIatCznJPc5/fLukHw5lUccfamvw5QXdGi1Eul4L0ide 3bgnMoNHGcQsgYjTeHmkkCOXSJLa3a3Ra085zU7CIy8DYfEQ4CgmL+P0z29HpFMe25GFkqDE W3rd4ifRfgDdTieLdV9nTAeSLihSJct1Re1uwDi0bpoMvLU+jEEtZLkzNV5+vXflQsu+jxsE 8Sdz2aNQnlokWMPXj86xbxwoUhgyliYyqV4mPxZFdlL5/xTSAs6NJjcz/Z7C9/oQA7BcM2JG x6aRYCtBih0RdYsyfcPZVx8EpOslEPtxS2vVp4ckfSwGJUu8eqI/nH3Yf1hwmzF/KQtyVAtB NZMYz71zpVj/hTeUtaa236SkLynIPx0NE/l8W6CyTDLp0RESEtqVq6DW3kDZ0zQpNC/50XYT rboB650ehBZx5ukLa1HIsbskU0AXO3qbfXXZSSKh26qBj6FyvWFZ8z3eDZVxz3TXXANiBtb5 nOaLU47DyalrXjZCWlPHFSpWF/l6+pWpX/9R0Ry0gLZJ1Z52e+N8wUOzeeZV+tV3r8Av3I5r C5oGV+mw9/MI96HphBsOqRHJ94xpl5Mk3/a3+BkFrqnKa0qxlsXcgAt+ljryw0yEIJL184js HItygN2b6OeylJIMT2Cj9j2PfXMJ2/+8QrKCeae00zC0NuQ5qYE6egp41TlsgazE0M+8nJhm 9BL2nqY75/OAUIcS5X0Gkow8hF7ofndbExfr8v13HsqCrW9qDzq1t5vDeBj1xXhN9ZTPaWYF RPjRtUADpvmI+grll61KxMcabkIpehuZp7gLqXAgfb4WYQo1CirhmlG/o1nh0eF9i4mD/XNw 45A2faTmA2OSzb7il6l9MHxg4FNIz8ITQ/dgWDpApBcYqpqcMMFE2CrdoeWz9M4vILkQX1w+ VLlDlhAxczjKn/wJxTtmBZd00gauyntuCK+iQdomisqhqeTmiXFhfnhPklPKitAQ29sik3pK I6/goUBXUSmWAMukQOs+Ufww6UzSL1XF2DIWg8IeiH3KzsnSa6srv+YZMUJ7po0sCJRWeD6Y FaAS7e7rQFImy/kGmJfwng8eVTI8t3Ylho8s36UNnVboXafcMo22BSX6NHHRPFX1yYLX2Eh0 2iRXAHheYD3u4zM357Y+vizTWegSoFefUyJhcubuS236HcrSRyzkvavm8H2RA0z0Cv1zd5vB m3DqBfxZJWu1rzvaLg2OBMxWRmltYwjQtIb8MN4npwb1HkEi4/A+HMGlT22KtBHwefka3FLQ zcXwtnT6Qyj2Ut5L3vPyZiqMxfVisZnedS+ZXsbnywn6MUfQoad6vp/gSJvoXK1oUTYar5gn X1OrJlmoG5fmOwPtAc3m2+8C7ZUJlVRJy/EmhjO5tv4saYdNy6/NLO30kR5h9WoCrqP9xpdV HjOcZAnBSZs7897PQGpsjW7+sT+ddLXd95WqgyMnkKKkb1OMJxo3KlClW99NGn6p3Fg1+Mrk Ukkw8ShpIbeTgcltKOhXkwBbGyzPZpOvGizy/8G1seOg9L2RMQnQGxWGsK3C6jwSnoTrai1b lzfVmdl9zHCRvyGTVL6ig8urmqTQcnxZjfNfSRflIskHUHHbAlWhAReNNkjtqYwDRvihMnoc UMjoysU+ka9sBxHjORhKxj4VG7b4gaucDY9DpaFflJa6QRL5kGdNsL7jKo7ByZD4piotxCAM ESfYAVSACcIQQqJCxbqNf+z5pHM/vOZCey3M/bVKezU+KoEDqrOnMzpi9Mu9i3pVI3HJnR4C vwnxkdPFWt0HcjUgXRHSiAakT7Mc9/OpBq4/X4/pcS+/fL3HQP3sNLVWv0IaIgpok7w2P/QU ozYzDx0IjtZyJ4WkHrBybxFmUUXlzkrbT6mV7IJqS/KSqvU3K5RFR8SLS1pZ64qp+ox2BdAP cnDh5b7zLl927QUAlEDbkDogMKBaMBMKmr7KVCNVyPpfPyWYCbGxc36e/b2UbpLkOBdrAG9o x6fFE75M3KCjH/kW1amOqdRj2vIWX4W8JH4eRFrB2/5SdvgYRDuK957gwo9xrgsj2/LP2oRY nBsNllApbqK4WZEk+1yTiZfu2F9I7DOyEP7p6HIb4wbuvxxDmFomvJGtT4knqBN4ngMTbQwk S/W5LaGQnmileiVx3xmS1xDpnBCj8SWvhc7UU023pRMH3/Pug8Ovzz44/EiqtcjA9appqMCk rDy
Ironport-sdr: pbrMiNzTUkdEGxVav0YOpe3dLm7yYqYo6VFjJhefN+8PzILinxeR7gPoVdWzcZTNFRecckFDyq hxvrLkTYGt8q5IZtDhS07DKd/hB3dc6J0BeBx176heoJwOvJKAHHdXAuys81PJUeHleVclwxWJ Gd+Zp9NFRn/ahFfhOgV3HkHZ1UXt4Wi0JnsitWI0DcHHCe8/gp3YPJSBaXD+HsfjYXzivJJLDr JkF0mq/X44EukJW9/quMcF/FQ+3k4KS6hg6wF1+lwCOeGrWx+solZMpuHRGsjgoKLYRSFNtTif YljkuM/lLLjmhpPLI1nQUovg

Morello: Digital Security by Design Technology Platform Prototype

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

https://www.jobs.ac.uk/job/CNK977/research-associate
Applications close 11 April 2022 at 1600 UTC

We are recruiting a postdoctoral researcher 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. https://blogs.ed.ac.uk/morello

Further information below: for full details and how to apply please visit
https://www.jobs.ac.uk/job/CNK977/research-associate

If you would like to discuss informally then please contact
Ian.Stark AT ed.ac.uk, the project lead for Edinburgh.

The University of Edinburgh only takes formal references after appointment: if
you have individual letters of support then please submit these as part of
your initial application. This position is not restricted to UK or EU citizens
and the university will assist with any visas and work permits necessary.

Follow these links for more about the wider project.

Morello at Edinburgh: https://blogs.ed.ac.uk/morello

CHERI Architecture: https://www.cheri-cpu.org

Morello at Arm: https://www.arm.com/architecture/cpu/morello

Morello Software Stack: https://www.morello-project.org

Sail Language: https://www.cl.cam.ac.uk/~pes20/sail/

Video presentation of CHERI security architecture and Morello platform
https://youtu.be/dxDDZ5aNTNs

Digital Security by Design: https://dsbd.tech

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

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.

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

- Experience with compiler optimization correctness or secure compilation.

- Experience in formal modelling of security properties.

- Knowledge of programming-language semantics and type systems.

- Knowledge of program logics, program analysis, and specification.

--
Ian Stark Laboratory for Foundations of Computer Science
http://homepages.ed.ac.uk/stark School of Informatics, University of Edinburgh
------------------------------------------------------------------------------
The University of Edinburgh is a charitable body, registered in Scotland, with
registration number SC005336.

[Coq-Club] Morello: Edinburgh research post on capability-based security technologies, Ian Stark, 03/11/2022