Project description

Compute Unified Device Architecture (CUDA) is a parallel computing platform and Application Programming Interface (API) model created by NVIDIA, which extends C/C++ and Fortran, in order to create a computational model that aims to harness the computational power of Graphical Processing Units (GPUs). Recent NVIDIA GPUs offer highly tuned implementations for typical routines required by Deep Neural Networks (DNNs), e.g., forward and backward convolution, pooling, normalisation, and activation layers, which lead to a prospect of a wide-scale deployment of such networks for perception modules and end-to-end controllers for self-driving cars. However, this wide-scale deployment also raises additional research questions of how the GPU software can be verified, validated and certified to meet standard requirements of safety-critical applications, especially when those applications are connected to the internet and thus subject to adversarial perturbations. As a result, the main goals of this PhD research are: (1) analyse and develop a deeper understanding of CUDA DNNs to capture main properties of interest to establish a secure and safety operation of CUDA DNNs; (2) model the CUDA DNN library by taking into account aspects of security and safety; and then (3) verify realistic applications of self-driving cars that rely on such library, using explicit-state and symbolic model checking techniques to prevent possible cyber threats/attacks.