Undefined Behavior bugs (UB) are a wide range of programming errors that are increasingly exploited by attackers. OS kernels are particularly plagued by UB because unprivileged userspace programs can often exploit them and cause critical security and reliability issues inside the OS. The previous works on detecting UB in kernels had to sacrifice precision for scalability, and in turn, suffered from extremely high false positive rates and failed to gain adoption in practice. We propose a novel static UB detector for Linux kernel, called KUBO, which simultaneously achieves high precision and whole-kernel scalability. KUBO is focused on detecting critical UB that can be triggered by userspace input. The high precision comes from KUBO’s verification of the satisfiability of the UB-triggering paths and conditions. The whole-kernel scalability is enabled by a novel interprocedural analysis, which incrementally walks backward along callchains in an on-demand fashion. We evaluate KUBO on several versions of whole Linux kernels (including drivers). KUBO found 23 critical UBs in the latest Linux kernel, which were previously unknown. KUBO’s false positive rate is merely 27.5%, which is significantly lower than that of the state-of-the-art kernel UB detectors (91%). Our evaluation also shows the bug reports generated by KUBO are easy to triage.