Memory safety bugs, such as out-of-bound accesses (OOB) in GPU programs, can compromise the security and reliability of GPU-accelerated software. We report the existence of input-dependent OOBs in the wild that manifest only under specific inputs. All existing tools to detect OOBs in GPU programs rely on runtime techniques that require an OOB to manifest for detection. Thus, input-dependent OOBs elude them. We also discover intra-allocation OOBs that arise in the presence of logical partitioning of a memory allocation into multiple data structures. Existing techniques are oblivious to the possibility of such OOBs. We make a key observation that the presence (or absence) of semantic relations among program variables, which determines the size of allocations (CPU code) and those calculating offsets into memory allocations (GPU code), helps identify the absence (or presence) of OOBs. We build SCuBA, a first-of-its-kind compile-time technique that analyzes CPU and GPU code to capture such semantic relations (if present). It uses a SAT solver to check if an OOB access is possible under any input, given the captured relations expressed as constraints. It further analyzes GPU code to track logical partitioning of memory allocations for detecting intra-allocation OOB. Compared to NVIDIA's Compute Sanitizer that misses 45 elusive memory bugs across 20 programs, SCuBA misses none with no false alarms.

翻译：GPU程序中的内存安全错误（如越界访问）可能危及GPU加速软件的安全性与可靠性。本文揭示了实际应用中存在仅在某些特定输入下才会显现的输入依赖性越界访问。现有检测GPU程序越界访问的工具均依赖运行时技术，需要错误显现才能被检测，因此这类输入依赖性错误得以隐匿。我们还发现了在内存分配被逻辑划分为多个数据结构时出现的分配内越界访问，现有技术完全忽视了此类错误的可能性。我们提出关键观察：程序变量间语义关系（决定CPU代码中内存分配大小与GPU代码中内存偏移量计算）的存在（或缺失）有助于判定越界访问的缺失（或存在）。基于此，我们构建了SCuBA——首个在编译时分析CPU与GPU代码以捕获此类语义关系（若存在）的技术。该方法将捕获的关系表达为约束条件，利用SAT求解器检验在任何输入下是否可能发生越界访问。SCuBA进一步分析GPU代码以追踪内存分配的逻辑划分，从而检测分配内越界访问。相较于NVIDIA Compute Sanitizer在20个程序中遗漏45个隐匿内存错误的表现，SCuBA实现了零遗漏且无虚假告警。