Following LLVM, Rust allows global ASM in a module. This means that crates can have arbitrary code that we cannot analyze.

Likelihood

We know of crates that use this feature

Mitigation

We could fail any crate that uses this feature, but this would block any use of those crates, even if they did not use any of the risky features. Even worse, this would block all consumers of such crates, from even compiling, again even if they do not use any of the dangerous features.

Unlike for inline ASM in a function, where we can insert assert(0) as a mechanism to guarantee soundness, there is no obvious way to only fail code paths that use the injected ASM.

• Raise a warning if global asm appears
• Incorporate that warning into viewer

Path to soundness

• Support ASM in CBMC

Documentation

https://rust-lang.github.io/rfcs/1548-global-asm.html