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.