Software is integral to the fabric of our lives, controlling transport, the economy and infrastructure, and providing the main tools of work and leisure. The cost of software failures is therefore high, to productivity, stability, safety, and privacy. As an indication of the economic impact, it is estimated that software errors cost the US economy tens of billions of dollars last decade. Software errors can also impact human safety as software is used to control transport, infrastructure, and medical equipment. The research agenda of program verification aims to mitigate these risks by putting software engineering on a rigorous foundation through techniques to guarantee program correctness. As software becomes more complex and pervasive, program verification is ever more important. This work aims to advance the state-of-the-art in verification at the point of program development through advancements in programming language theory and practice. Programming languages are the core tool in which software is constructed; they are the means of communicating our intentions to computer hardware. There are various design trade-offs when creating a programming language, which has led to the variety of programming languages in use today. Some languages support verification by including a "type system" which categorises data and operations, ensuring that operations are only applied to data of the correct type. This provides some guarantees about the correctness of the program by ruling out various kinds of error before the program is ever executed. A subfield of programming language research aims to make type systems more expressive so that they can describe and enforce more properties of programs and thus raise the level of verification possible within the language. The current proposal aims to do just this, focussing on the notion of data as a "resource" subject to constraints which should be enforced by a language's type system. This project develops a particular technique for building such type systems in a way that can capture various kinds of property in one system. The manipulation of data is central to the task of programming. Current programming languages essentially view data as an infinitely-replicable resource that can be stored, manipulated, and communicated without restriction. However, this perspective is naive. Some data is private and thus should not be arbitrarily copied, stored, or communicated. Some data is large and thus should not be replicated too frequently. Some data acts as a way of interfacing with other parts of a system, e.g., files or communication channels, which are then subject to restrictions on how they can be used, such as agreed protocols of interaction. Most programming languages are agnostic to these constraints however, treating data as totally unconstrained. This can lead to various software errors, including privacy breaches, performance problems, and crashes due to incorrect interactions between parts of a system. The goal of this research is to embed the constraints associated with data into the type system of a language so that these additional constraints can be automatically enforced. The key technology for doing this is a novel notion of types called "graded modal types" which can capture and track different kinds of information about the structure of programs and the flow of data through them. This work will develop the theory and practice of graded modal types, producing a prototype language that demonstrates their use for verifying program properties. Three case studies will be carried out to demonstrate their power: (1) ensuring privacy and confidentiality, (2) capturing and reasoning about performance e.g., how fast a program will execute relative to the size of its inputs and how much memory it will consume (3) enforcing fine-grained protocols of interaction. This work is a step towards a new generation of trustworthy software.

This project aims to improve the program development process, using a process of "Type-driven Development". We believe that in order to enable the highest levels of productivity, programming should be a conversation between the programmer and the machine. In type-driven development, we begin by giving a type as a plan for a program. Then the machine, rather than being seen as an adversary which rejects incomplete or incorrect programs, is the programmer's assistant. A limited form of this idea exists in modern integrated development environments: when typing "x." into a text buffer, the environment will show with methods "x" implements. This project will take this idea several steps further. Not only can we give feedback on partial programs, we can also use types and their structure to generate significant parts of a program and direct the implementation of more complex components such as communication and security protocols. During development, programs spend most of their time in an incomplete state, and the act of programming is as much about the steps required to achieve a complete program as it is about the end result. Accordingly, language implementations and tools must support the editing process as well as check and compile the end result. In this project, we will develop the necessary tooling to support interactive type-driven development, based on sound theoretical foundations. Furthermore, we will make the tooling itself programmable: the foundations will essentially give a language of programming "tactics", which will be composable intro sophisticated methods for automatic program construction, directed by the type. We will liaise with industry throughout to ensure that the techniques we develop are well-suited to commercially relevant problems.

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, thus support the development of concurrent programs. Concurrent behaviour is notoriously difficult -- incorrect synchronisation can lead to many dangerous safety and security vulnerabilities, 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 provides 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 (a) reusable models, tools and techniques that enable the verification of safety and security properties over a range of advanced architectures, and (b) 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 above 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. In terms of academic dissemination, we expect a minimum of 2 journal publications per year per institution, plus several associated conference publications and keynote / invited talks per year. We have a direct link to standardisation work, and we have costed in continued visits to standards meetings (eg attendance of Subgroup 1, concurrency, at Workgroup 21, C++, at the ISO - Batty is a voting member of the UK delegation) in order that our work can have a direct impact on the relevant programming model standards. By involvement of our wider project partners and our existing collaboration networks we expect not only enhanced opportunities for dissemination, but also enhanced opportunities for development of our PDRAs through interaction with these wider communities.

The fellowship will examine the science, technology and application of Multi-Party Computation technology in various application domains. MPC is a long standing theoretical construct, which is only now becoming practically realisable. It has the potential to revolutionize the way we enable trust in our computing infrastructure (by distributing trust amongst different parties). It will enable greater privacy aware applications, (by enabling parties to compute on data without holding it `in the clear'), and it will ensure greater security (by providing robust and secure protocols for tasks currently performed in an insecure and ad-hoc manner). It can also enable new business models and applications by allowing parties who currently do not share data resources, to share the said resources without compromising on either privacy or security. The research programme covers a pipeline of work covering the lower TRL levels. We will conduct basic scientific research in the underlying mathematics and protocols, we will conduct research in the systems engineering needed to bring such protocols to an efficient reality, including work on programming tools and models, and finally we will examine potential applications via demonstrators and our industrial advisory board (all of whome have been selected due to their long term interaction with our group and their expertise in specific application domains of MPC).

Scientific models play a vital role in science and policy making. Many models are now expressed as complex computer programs which are often the result of decades of research and development, possibly involving multiple researchers or teams. This has lead to significant investment in maintaining these models and evolving them to use modern programming approaches or to work efficiently on new hardware platforms (such as cloud computing resources). However, the complexity of these models makes maintenance and evolution difficult. In particular, changing a complex model's code whilst ensuring it produces the same results is difficult; maintenance/evolution of complex models is often error prone. The complexity of a piece of software can be classified as either intrinsic or accidental. Intrinsic complexity is an essential reflection of the complexity inherent in the problem and solution at hand. Alternatively, accidental complexity arises from the particular programming language, design or tools used to implement the solution. Many of the research contributions of programming language design and software engineering have been aimed at reducing the accidental complexity of software. However, many of these approaches have not been targetted at scientific computing. There is now a need to develop these contributions so that they meet the needs of scientists. Addressing these needs will provide huge benefits to science and policy through increased productivity and trust in models. Our collaborations with leading research groups in science have highlighted the huge existing investments in established models. We are therefore aiming to support the evolution, rather than replacement, of existing code and working practices. Our goal is to apply cutting edge programming language and software engineering research to help develop "sustainable" software, which maintains its value over generations of researcher. Our focus is on models developed in the Fortran language, as this remains a dominant programming language in scientific computing, owing in part to its longevity. We will provide practical tools which scientists can use to reduce the accidental complexity of models through evolving a code base, as well as tools for automatically verifying that any maintenance/evolution activities preserve the models behaviour. We will develop new mechanisms for program comprehension and transformation in order to bring effective techniques from programming language design and software engineering across the chasm to scientific computing. Ultimately, reducing the effort to maintain and evolve code will free-up scientists to focus on the core aspects of the science, and will lead to models that are more easily communicated, disseminated, and reused between researchers, supporting core ideals of science.