The University of Sheffield is a remarkable place to work. Our people are at the heart of everything we do. Their diverse backgrounds, abilities and beliefs make Sheffield a world-class university.

We offer a fantastic range of benefits including a highly competitive annual leave entitlement (with the ability to purchase more), a generous pensions scheme, flexible working opportunities, a commitment to your development and wellbeing, a wide range of retail discounts, and much more. Find out more about our benefits (opens in a new window) and join us to become part of something special.

Overview

A research associate position is available within an exciting project aiming to conduct research into the safety and security of advanced hardware architectures. The project is called “Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT)” and is funded by the EPSRC. The project benefits from working with a number of academic, industrial and governmental partners: ARM, Galois, Defence Science and Technology (DST) and the Universities of Amsterdam, Augsburg, Melbourne and Oldenburg.

The post will be based in Sheffield working at Sheffield’s School of Computer Science within the Faculty of Engineering. The post-holder will join researchers at Kent and Surrey working on the “Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT)” project, led at Sheffield by Prof. John Derrick and Dr. Andrei Popescu and sponsored by the Engineering and Physical Sciences Research Council (EPSRC). The project aims to conduct research into the safety and security of advanced hardware architectures.

The continuing evolution of computing hardware has led to enormously complex architectures with execution models that integrate advanced memory technologies and hardware models. This evolution affects all devices, ranging from large-scale data centres to mobile phones. However, these advanced architectures break assumptions that programmers have relied on, causing new safety bugs and security vulnerabilities. We target multi-processor systems and concurrent architectures. Concurrent behaviour is notoriously difficult – incorrect synchronisation can lead to many dangerous safety and security vulnerabilities (see the Common Weaknesses database), ranging from “out-of-bounds writes” and “use-after-free” errors to “improper synchronisation and race conditions”. Further, architecture-based attacks (e.g., Spectre) show the urgency of addressing these important problems today. Even when low-level programs are well synchronised, the design of the underlying concurrent algorithms can themselves be vulnerable. In particular, well understood safety conditions such as linearizability do not guarantee security, and current approaches to addressing this issue lead to overly synchronised implementations (degrading performance). This introduces a tension between the goals of the hardware designers (who aim to maximise performance), and end users (who require trustworthy software). In the middle are developers, who are tasked with producing software that balances this tension. COVERT will provide mechanisms for provably correct reusable abstractions that maximise flexibility in program design, allowing fine tuning of both safety and security guarantees based on the architecture.

Our vision is to provide:

• reusable models, tools and techniques that enable the verification of safety and security properties over a range of advanced architectures, and
• a verified set of concurrency abstractions that guarantee both safety and security.

This effort involves two key strands of work. In the first, we bring together different facets of modern systems and provide a rigorous foundation covering a range of architectural features such as out-of-order execution and speculative execution, and memory features such as weak memory and NVM. Additionally, we extend existing reasoning techniques to our newly established foundation by developing threat models that cast the intricate behaviours allowed by advanced architectures through the lens of a malicious attacker. Our second strand involves the practical realisation of these techniques via verified litmus tests, verified concurrency libraries and associated verification tools. We will build novel techniques and tools that strengthen traditional correctness criteria (linearizability, opacity, etc.) to provide architecture-aware correctness of both safety and security. To ensure a high degree of reliability, our theory and case studies will be mechanised within the Isabelle proof assistant. Our chosen case studies include those from the MITRE database, the Folly concurrency library, as well as examples provided by our industrial partners.

We are seeking a highly motivated researcher willing to cooperate with the project investigators in pursuing groundbreaking verification work and to publish it in top conferences and journals.

Main duties and responsibilities

• Perform research in the project's areas of interest: formal modelling and verification of safety and security properties for advanced hardware architectures.
• Create and adapt any necessary software to do the above.
• Engage the industry partners (e.g., at ARM) to aid the deployment of verification solutions.
• Publish in high quality outlets (high profile and reputable conferences and journals), prepare detailed research reports where appropriate (e.g. as formal project deliverables), and communicate our results to non-academic or non-verification specialist audiences as required, e.g. to project-wide workshops.
• Plan work to meet project deliverables and be appropriately prepared for supervision and project meetings. 
• Carry out administrative roles as required, e.g. to coordinate meetings across various sites.
• Participate in the general collaborative working of the Verification Group, e.g., to present to the group, participate in its seminar meetings, engage in its training events, and to demonstrate research to visitors etc.
• As a member of staff you will be encouraged to make ethical decisions in your role, embedding the University sustainability strategy into your working activities wherever possible.
•  Contribute to the development of further research proposals.
• Carry out other duties, commensurate with the grade and remit of the post

Person Specification

Our diverse community of staff and students recognises the unique abilities, backgrounds, and beliefs of all. We foster a culture where everyone feels they belong and are respected. Even if your past experience doesn't match perfectly with this role's criteria, your contribution is valuable, and we encourage you to apply. Please ensure that you reference the application criteria in the application statement when you apply.

Further Information

Next steps in the recruitment process

It is anticipated that the selection process will take place during week commencing 1 Sept. 2025. This will consist of an online interview. We plan to let candidates know of the decision (whether an employment offer is being made) as soon as possible, and no later than the week commencing 15 Sept. 2025.

Our vision and strategic plan

We are the University of Sheffield. This is our vision: sheffield.ac.uk/vision (opens in new window).

What we offer

• A minimum of 41 days annual leave including bank holiday and closure days (pro rata) with the ability to purchase more.
• Flexible working opportunities, including hybrid working for some roles.
• Generous pension scheme.
• A wide range of discounts and rewards on shopping, eating out and travel.
• A variety of staff networks, providing opportunities for social interaction, peer support and personal development (for example, Race Equality, LGBT+, Women’s and Parent’s networks).
• Recognition Awards to reward staff who go above and beyond in their role.
• A commitment to your development access to learning and mentoring schemes; integrated with our Academic Career Pathways
• A range of generous family-friendly policies
  • paid time off for parenting and caring emergencies
  • support for those going through the menopause
  • paid time off and support for fertility treatment
  • and more

More details can be found on our benefits page: sheffield.ac.uk/jobs/benefits (opens in a new window).

We are a Disability Confident Employer. If you have a disability and meet the essential criteria for this job you will be invited to take part in the next stage of the selection process.

Closing Date : 31/08/2025 

We are a research university with a global reputation for excellence. Our ideas and expertise change the world for the better, making a real difference to society. We know that when people come together with different views, approaches and insights it can lead to richer, more creative and innovative teaching and research and the highest levels of student experience. Our University Vision (www.sheffield.ac.uk/vision) outlines our commitment to building a diverse community of staff and students that recognises and values the abilities, backgrounds, beliefs and ways of living for everyone.