- Deadline Thursday 20 March 2025
- Duration 36 Months
- Start Date October 2025
- Funding Home fee, Stipend
- Supervisors Jan de Muijnck-Hughes, Bob Atkey
- Groups StrathCyber, MSP
This JARSS PhD studentship will develop new methods for asserting the resilience of existing communicating systems by developing new static analysis methods derived from advanced programming language research as pioneered by the supervising team, and the wider MSP and StrathCyber research groups.
Please go here to apply:
Contact
Informal enquiries about the studentship are to be directed to Jan de Muijnck-Hughes (Jan.de-Muijnck-Hughes@strath.ac.uk)
Project Details
The fragility of modern software has been highlighted by the Whitehouse and the Office of the National Cyber Director (ONCD) in a recent report. The ONCD, and the UK’s National Cyber Security Center (NCSC), advocate secure-by-design approaches to make software more resilient. These reports are the result of not just an awareness of the problem of fragile software, but also the result of the last decade’s advances in programming language research that have shown that resilient software can be developed using correct-by-construction and secure-by-design approaches. However, ascertaining the resilience of existing systems is just as important as building new ones. How we integrate and apply secure-by-design techniques when working with existing systems is an important problem.
This studentship will be concerned with asserting the resilience of software that communicates via networks. Widely used safe programming languages (such as Rust, Java, Python, Go) do not support reasoning about communication behaviour directly in their design. Current secure-by-design approaches to enforcing communication behaviour in programs requires generation of new code from external communication specifications (behavioural types) or the provision of advanced software libraries for creating new software programs. If we are to secure existing communication systems using these ‘behavioural types’, then developers must rewrite existing code bases. Such re-engineering will have a negative effect on developer productivity, morale, and program safety.
Aims & Objectives
Rather than require existing systems to be rewritten, we can look to retrofit existing programming languages with new abilities to reason about program communication at design time using the same behavioural typing ideas. Retrofitting presents a cost-effective way to assert the resilience of existing communicating programs by minimising code modifications and improves developer productivity and morale through engagement with existing tools and coding environments.This studentship will develop novel static analysis methods that automatically extracts communication specifications from communicating systems to compare against existing specifications.
The aims of the studentship are to:
- to develop a formal model for a known programming language that captures program communication;
- to verify the correctness of the developed formal model;
- to develop efficient extraction techniques of program communication from existing programs;
- to develop a new static analysis tool that statically guarantees that programs follow known communication protocols
- to establish the correctness of existing programs using the static analysis tool;
Collaborators
As part of this studentship you will be situated across the StrathCyber and Mathematically Structured Programming (MSP) research groups, with the primary supervisor being from StrathCyber and the other from MSP This studentship also brings opportunities to engage with the wider SICSA (Scottish Information and Computer Science Alliance) and SPLI (Scottish Programming Languages Institute) communities, as well as engaging with the wider UK CyberSecurity and Programming Languages communities.
Funding details
The funding provided for these fully funded PhDs will include three years of both tuition fees and monthly stipend payments.
Fully funded studentships are available at the UK home rate.
Home Students
To be eligible for a fully funded UK home studentship you must:
- Be a UK national or UK/EU dual national or non-UK national with settled status / pre-settled status / indefinite leave to remain / indefinite leave to enter / discretionary leave / EU migrant worker in the UK or non-UK national with a claim for asylum or the family member of such a person, and
- Have ordinary residence in the UK, Channel Islands, Isle of Man or British Overseas Territory, at the Point of Application, and
- Have three years residency in the UK, Channel Islands, Isle of Man, British Overseas Territory or EEA before the relevant date of application unless residency outside of the UK/ EEA has been of a temporary nature only and of a period less than six years