No, but to be safe enough it has to be more safe than the Rust compiler, because the latter doesn't get run on untrusted code (with the result automatically executed)[1]. If bounds checks exist in the compiler IR, they're subject to optimization, which is very helpful for performance but also risky, as incorrect optimizations can easily cause memory unsafety. Optimizer bugs in modern backends are rarely encountered in practice, but from a security perspective, that's like saying your C++ program never crashes in practice: it helps, but it doesn't prove the absence of bugs that can only be triggered by pathological inputs; such bugs in fact tend to be quite common.
I've never tried to find an optimizer bug in LLVM, but I have found more than one in V8, so I have some idea what I'm talking about.
[1] More specifically, this doesn't happen in situations where correctness of the generated code is relied on to provide safety guarantees. There are several websites that will compile and run Rust code for you, but none of them try to ban unsafe code, or filesystem/syscall access for that matter, at the language level; rather, their security model relies entirely on the OS sandbox the process runs in. Google's PNaCl uses (or used to use?) LLVM on untrusted code, but AFAIK the output of LLVM, the machine instructions, are still run through the NaCl validator, so getting LLVM to miscompile something wouldn't accomplish much. (NaCl also runs both LLVM itself and the untrusted code in an OS sandbox.)
It seems safe to say that a JIT-trace -> Rust -> machine code compilation pipeline will probably never be fast enough to satisfy the requirements of a high-performance JIT compiler.
Going the long way is just a 'proof of concept' sort of thing. You could design a high-performance JIT around equivalent safety mechanisms, and even prove the tricky parts.
JavaScript's memory model is incompatible with that of Rust anyhow. You would want something like typed assembly language (Google this--it's a fertile research area). Very researchy though, with uncertain payoff.
But note that a lot of security problems are not in the jitcode but rather in C++ implementations of JS objects and in the compiler itself.
BOOM! Typed, assembly language is exactly what I was going to recommend! TALC assembly, Chlipala's Bedrock, and Microsoft's CoqASM are Google keywords to use for anyone following along.
CakeML or Verisoft's C0 could be useful for assembly generation but not as sure there. Tough constraints in JIT. Edited to add Myreen's JIT that I just remembered.
Not that Im aware of. They might privately license it if asked. I mainly bring it up as something worth cloning by FOSS team given there's plenty details in paper. Meanwhile, look up Magnus Myreen's publications and software as they're on a row with verified everything.
Typed assembly language would be an excellent addition to the Rust ecosystem -- there are still segments of software which should (or must) be implemented in assembly, so anything that can help make assembly easier to verify would be helpful to the ecosystem.
