[TYPES/announce] Funded PhD positions at Edinburgh verifying embedded ARM security

[Ian Stark]

We have two ARM-funded PhD positions at Edinburgh which would suit students 
interested in types and verification.  Details below.

Regards,

Ian Stark


              Two Funded PhD Positions at University of Edinburgh
     Formal Verification of Security Properties for ARM Microcontrollers

We invite applications for two fully-funded PhD studentships to study the 
formal specification and verification of security features for systems built 
using ARM microcontrollers.

Deadline:	 31st July 2017 or until posts filled
Starting date:   Flexible (usual entry Sept 2017/Jan 2018)
Studentship:     Full tuition fees for UK/EU students, 3.5 years
                  Stipend of approximately £14,000 per year
                  Additional £3,500 per year and ARM internship
Requirements:    Good degree, BSC in Computer Science or similar (2.1 minimum)
                  Aptitude for subject area (logic, semantics, theorem proving)

For non UK/EU students, additional fees apply.  Scholarships to cover the 
additional fees are not generally available.

The positions are held in the Centre for Doctoral Training in Pervasive 
Parallelism at the University of Edinburgh and as part of the Security and 
Privacy group in Informatics.

See below for descriptions of the projects.  Details of the research are 
flexible depending on the candidate's interests and background, and ARM's 
progress and priorities at the time of starting.

For more information about the studentships, the CDT and the Security and 
Privacy group go to:

   http://pervasiveparallelism.inf.ed.ac.uk/industry-studentships

   http://web.inf.ed.ac.uk/security-privacy

If you are interested then please contact the project supervisors to discuss 
informally before application:

  * Ian Stark (Ian.Stark at ed.ac.uk)
  * Brian Campbell (Brian.Campbell at ed.ac.uk)
  * David Aspinall (David.Aspinall at ed.ac.uk)



Formal Specification and Proofs for TrustZone in ARMv8-M
--------------------------------------------------------

The increasing complexity and connectivity in microcontroller devices has 
prompted the development of protection mechanisms to improve reliability and 
security. ARM's TrustZone for ARMv8-M provides a separate "secure world" 
execution mode to enable features such as secure firmware updates, safe 
integration of code from multiple suppliers and controlled access to 
privileged peripherals. It is designed in a different way to TrustZone on 
other ARM architectures, with greater hardware support for resource-light 
microcontrollers.

This project will study the low-level instruction set design of TrustZone for 
ARMv8-M, creating formal specifications to describe the security properties 
that hold at the instruction level and proofs that these provide the intended 
protection against low-level attacks. The specifications will also aim to 
provide a basis for higher-level proofs about the security properties of 
software that runs in the secure world.


Formal Verification of Security Properties of the mbed OS uVisor
----------------------------------------------------------------

The mbed OS uVisor is a core security component for ARM's mbed IoT platform. 
It creates isolated security domains on Cortex M3, M4 and M7 microcontrollers 
with a Memory Protection Unit (MPU). The MPU provides a small number of memory 
regions of limited size. On top of these the uVisor provides a more flexible 
compartmentalisation using separate security domains ("Secure Boxes"), 
configured with suitable Access Control Lists.

This project will apply machine-assisted theorem-proving to help define and 
then verify correctness and security properties of the uVisor implementation. 
This will build on previous work that has constructed instruction set models 
and decompilation techniques, and extend it with formal modelling of exception 
handling and memory protection. Example verification goals include correctness 
aspects, such as ensuring that MPU regions get correctly reallocated on demand 
(ensuring progress/availability), or higher-level properties such as 
control-flow integrity (ensuring certain attacks are not possible in client 
code).


About the University of Edinburgh
---------------------------------

The University of Edinburgh School of Informatics brings together world-class 
research groups in computer science, artificial intelligence and cognitive 
science.  It is the largest Informatics or Computer Science department in 
Europe.  It houses a number of specialised centres and subgroups, including 
the ARM Centre of Excellence working on a number of collaborations.  The 
Security and Privacy group is forms the core of the University's Academic 
Centre of Excellence in Cyber Security Research, which one recognition in 
2017.

We welcome applications from members of groups traditionally under-represented 
in the field.  In 2013 (renewed 2016), the School of Informatics received an 
Athena Swan Silver Award, in recognition of its commitment to advancing the 
careers of women in science, technology, engineering, maths and medicine 
(STEMM) employment in higher education and research.

For more information about Edinburgh and studying here, see these pages:

  * Explore Edinburgh: http://www.ed.ac.uk/about/city

  * Overview for prospective postgraduates: 
http://www.ed.ac.uk/schools-departments/informatics/postgraduate


-- 
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.