Securing GPU Kernels with Lightweight Formal Methods

This paper reports our initial experience of applying lightweight formal method to validate the security of CUDA, the main programming language used for GPGPU programming. By “lightweight formal method”, we mean a pragmatic approach to verifying the security of CUDA programs coded by programmers. We do not aim to achieve full formal verification, but instead emphasize automation, usability, and the ability to continually ensure security as program evolve over time. Our approach first analyzes the program annotated with specification and loop invariants, and generates the corresponding verification conditions, which can be verified to ensure the security that is essential to GPU programs. Our work shows promising potentials by successfully verifying representative CUDA programs, including matrix multiplication optimized by using shared memory. Compared with some existing tools, our method exhibits better performance in CUDA programs security verification of without excessively increasing the programmer’s usage cost.