I've only briefly skimmed the paper, but on that glance, it looks like what they did was (effectively) drop all the attributes in LLVM that can indicate UB, e.g., the inbounds flags on getelementptr instructions, or the nsw flags on arithmetic operations.
As you note, it doesn't remove the more core UB behaviors in LLVM, in particular LLVM's reliance on pointer provenance.
As you note, it doesn't remove the more core UB behaviors in LLVM, in particular LLVM's reliance on pointer provenance.