Critical Compilation Strictness for Certified Selective Hardening Against Compiler-Conditioned DNN Backdoors

Deep-learning compiler transformations can change security-sensitive inference decisions without changing trained model parameters. Critical compilation strictness measures the smallest set of enforceable source/reference-semantic sites whose protection excludes a prescribed decision violation for every legal joint compiler configuration on a declared input domain. We characterize this minimum by decision-violating transformed supports and instantiate an exact implicit hitting-set synthesis method with an executable witness oracle. On a five-site ConvNet evaluated using PyTorch 2.6.0+cpu and its Inductor backend, the triggered target-label proportion increases from 0.1078 under eager execution to 0.9996 under compilation; protecting only the feature stem is the unique minimum decision-preserving policy over the 10,000 evaluated triggered inputs. An executable oracle recovers this policy in seven protected-set queries (425.59 s total, including 320.21 s of first-use compilation/setup). A second architecture, VGG16-BN, also has a one-site minimum under Inductor. An independently trained ONNX Runtime 1.21.0 case yields the same unique minimum on a separate 5000-input policy-synthesis domain and records no eligible violations under that fixed policy across its 16 compatible configurations on the 10,000-input evaluation domain. In a controlled Inductor timing experiment, selective strictness reduces warmed batch latency by approximately 29% relative to all-strict execution. The exact guarantees apply to the specified finite input and compiler-configuration families; structural experiments separately exhibit higher-order interactions and differences between exact and heuristic selection.