[isabelle] Funded PhD positions at Edinburgh verifying embedded ARM security




             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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.