The focus of this proposal is on the detection and survival of wrong code compiler defects, which we argue present a cyber-security threat that has been largely ignored to date. First, incorrectly compiled code can introduce exploitable vulnerabilities that are not visible at the source code level, and thus cannot be detected by source-level static analysers. Second, incorrectly compiled code can undermine the reliability of the application, which can have dramatic repercussions in the context of safety-critical systems. Third, wrong code compiler defects can also be the target of some of the most insidious security attacks. A crafty attacker posing as an open source developer can introduce a compiler-bug-based backdoor into a security-critical application by adding a patch that looks perfectly innocent but which, when compiled with a certain compiler, yields binary code that allows the attacker to compromise the software. In this project, we aim to explore automated techniques that can detect and prevent such problems. In particular, we plan to investigate techniques for automatically finding compiler-induced vulnerabilities in real software, approaches for understanding the extent to which an attacker could maliciously modify an application to create a compiler-induced vulnerability, and methods for preventing against such vulnerabilities at runtime.

High Performance Embedded and Distributed Systems (HiPEDS), ranging from implantable smart sensors to secure cloud service providers, offer exciting benefits to society and great opportunities for wealth creation. Although currently UK is the world leader for many technologies underpinning such systems, there is a major threat which comes from the need not only to develop good solutions for sharply focused problems, but also to embed such solutions into complex systems with many diverse aspects, such as power minimisation, performance optimisation, digital and analogue circuitry, security, dependability, analysis and verification. The narrow focus of conventional UK PhD programmes cannot bridge the skills gap that would address this threat to the UK's leadership of HiPEDS. The proposed Centre for Doctoral Training (CDT) aims to train a new generation of leaders with a systems perspective who can transform research and industry involving HiPEDS. The CDT provides a structured and vibrant training programme to train PhD students to gain expertise in a broad range of system issues, to integrate and innovate across multiple layers of the system development stack, to maximise the impact of their work, and to acquire creativity, communication, and entrepreneurial skills. The taught programme comprises a series of modules that combine technical training with group projects addressing team skills and system integration issues. Additional courses and events are designed to cover students' personal development and career needs. Such a comprehensive programme is based on aligning the research-oriented elements of the training programme, an industrial internship, and rigorous doctoral research. Our focus in this CDT is on applying two cross-layer research themes: design and optimisation, and analysis and verification, to three key application areas: healthcare systems, smart cities, and the information society. Healthcare systems cover implantable and wearable sensors and their operation as an on-body system, interactions with hospital and primary care systems and medical personnel, and medical imaging and robotic surgery systems. Smart cities cover infrastructure monitoring and actuation components, including smart utilities and smart grid at unprecedented scales. Information society covers technologies for extracting, processing and distributing information for societal benefits; they include many-core and reconfigurable systems targeting a wide range of applications, from vision-based domestic appliances to public and private cloud systems for finance, social networking, and various web services. Graduates from this CDT will be aware of the challenges faced by industry and their impact. Through their broad and deep training, they will be able to address the disconnect between research prototypes and production environments, evaluate research results in realistic situations, assess design tradeoffs based on both practical constraints and theoretical models, and provide rapid translation of promising ideas into production environments. They will have the appropriate systems perspective as well as the vision and skills to become leaders in their field, capable of world-class research and its exploitation to become a global commercial success.

Systems modelled by partial differential equations (PDEs) are ubiquitous in science and engineering. They are used to model problems including structures, fluids, materials, electromagnetics, wave propagation and biological systems, and in areas as varied as aerospace, image processing, medical therapeutics and economics. PDEs comprise a forward model for predicting the response of a system, but are also a key component in the solution of inverse problems, for design optimisation, uncertainty quantification and data science applications, where the forward computation is repeated many times with different inputs. The numerical simulation of complex systems modeled by PDEs is a challenging topic. It involves the choice of underlying equations, the selection of suitable numerical solvers, and implementation on specific hardware. Over the decades numerous software libraries have been developed to support this task. But adapting these libraries to the specific model and combining the various components in a low-level high-performance programming language requires a major development effort. This required effort has become significantly more challenging with the advent of heterogeneous mixed CPU/GPU devices on the path to exascale systems. Implementations need to be adapted for each individual device type in order to achieve good performance. As a consequence, developing new simulations at scale has become an ever more costly and time-intensive task. In this project we propose a different simulation paradigm, based on the use of high-productivity languages such as Python to describe the problem, and automatic code generation and just-in-time compilation to translate the high-level formulations into high-performance exascale-ready code. Based on the experience with the component software libraries Firedrake, FEniCS and Bempp, the investigators will build a toolchain for complex exascale simulations of PDEs on unstructured grids, using state of the art finite element and boundary element technologies. The research will include mathematical and algorithmic underpinnings, concrete software development for automatic code generation of low-level CPU/GPU kernels, high-productivity language interfaces, and the application to 21st century exascale challenge problems in the areas of battery storage systems, net-zero flight, and high-frequency wave propagation.

Modern computing systems are becoming increasingly diverse, but the common feature of all emerging computing platforms is the increased potential for performing many computations in parallel, by providing large numbers of processor cores. Computer systems consisting of various different platforms have great potential for performing tasks fast and efficiently. However, programming such systems is a great challenge. The era of performance increase through increased clock speeds has come to an end and we have entered a period where performance increases can only come from increased numbers of heterogeneous computational cores and their effective exploitation by software. Because of the immense effort required to adapt existing parallel software to novel hardware architectures with present technology, there is a very real danger that future advances in hardware performance will have little impact on practical large-scale computing using legacy software. The specific challenge that we want to address in this proposal is how to exploit the parallelism of a given computing platform, e.g. a multicore CPU, a graphics processor (GPU) or a Field-Programmable Gate Array (FPGA), in the best possible way, without having to change the original program. These different platforms have very different properties in terms of the available parallelism, depending on the nature and organisation of the processing cores and the memory. In particular FPGAs have great potential for parallelism but they are radically different in architecture from mainstream processors. This makes them very difficult to program. The key problem here is how to transform a program so that it will best use the potential for parallelism provided by the computing platform, and crucially, how to do this so that the resulting program is guaranteed to have the same behaviour as the original program. Our proposed approach is to use an advanced type system called Multi-Party Session Types to describe the communication between the tasks that make up a computation. To use a rough analogy, the computation could for instance be viewed as a car assembly line, where every unit performs a particular task such as painting, inserting doors, wheels, motor etc. Depending on the organisation and composition of the factory, the order in which these operations is performed will determine the speed with which a car can be assembled. However, when reordering the operations, one must of course ensure that changing the order does not lead to incorrect assembly. To return to the computational problem, by using the Multi-Party Session Types to describe the communication, we have a formal way of reasoning about the transformations. By developing a formal language for the transformations we can prove their correctness. This is the main novelty of the proposal: the formal system for type transformations. The actual transformations can be viewed as "programs" in this formal language. They will be informed by the properties of the computing platform. To provide this link between the transformation and the platform, we will also develop a formal description of parallel computing platforms. By building these formal systems into a compiler we will be able to transform programs to run in the most efficient way on hybrid manycore platforms. The main benefit from the proposed research is that the programmer will not need to have in-depth knowledge of the highly complex architecture of a hybrid manycore platform. This will be of great benefit to in particular scientific computing, because it also means that programs will not need to be rewritten to run with best performance on novel systems. To demonstrate the effectiveness of our approach we aim to develop a proof-of-concept compiler which will transform programs so that they can run on FPGAs, because this type of computing platform is the most different from other platforms and hence the most challenging.