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.st...@ed.ac.uk)
* Brian Campbell (brian.campb...@ed.ac.uk)
* David Aspinall (david.aspin...@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.
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
