  Software-based fault isolation (SFI) is a technique to isolate a potentially
faulty or malicious software module from the rest of a system using
instruction-level rewriting. SFI implementations on CISC architectures,
including Google Native Client, use instruction padding to enforce an address
layout invariant and restrict control flow. However this padding decreases code
density and imposes runtime overhead. We analyze this overhead, and show that
it can be reduced by allowing some execution of overlapping instructions, as
long as those overlapping instructions are still safe according to the original
per-instruction policy. We implemented this change for both 32-bit and 64-bit
x86 versions of Native Client, and analyzed why the performance benefit is
higher on 32-bit. The optimization leads to a consistent decrease in the number
of instructions executed and savings averaging 8.6% in execution time (over
compatible benchmarks from SPECint2006) for x86-32. We describe how to modify
the validation algorithm to check the more permissive policy, and extend a
machine-checked Coq proof to confirm that the system's security is preserved.
