Stephen McCamant

Kartik Ramkrishnan, Antonia Zhai, Stephen McCamant et al.

The last level cache is vulnerable to timing based side channel attacks because it is shared by the attacker and the victim processes even if they are located on different cores. These timing attacks evict the victim cache lines using small conflict groups(SCG), and monitor the cache to observe when the victim uses these cache lines again. A conflict group is a collection of cache lines which will evict the target cache line. Randomization is often used by defenses to prevent creation of SCGs. We introduce new attacks to demonstrate that the current randomization schemes require an extremely high refresh rate to be secure, on average a 15\% performance overhead, and upto 50\% in the worst case. Next, we propose a new randomization strategy using an indirection table, which mitigates this issue. Addresses of cache lines are encrypted and used to lookup the indirection table entry. Each indirection table entry stores a mapping to a randomly chosen cache set. The cache line is placed into this randomly chosen set. The encryption key changes upto 50x faster than CEASER's default rate, by using evictions to trigger the re-randomization. Instead of moving cache lines, this mechanism re-randomizes one iTable entry at a time, whenever the cache lines corresponding to the iTable entry are naturally evicted. Thus, the miss rate is not much worse than the baseline. We quantitatively show that our scheme does almost as well as a fully associative cache to defend against these attacks. We also demonstrate new attacks that target the iTable by oversubscribing its entries, and quantitatively show that our scheme is resilient against new attacks for trillions of years. We estimate low area ( < 7\%) and power overhead compared to a baseline inclusive last-level cache. Lastly, we evaluate a low performance overhead (<4%) using the SPECrate 2017 and PARSEC 3.0 benchmarks.

Navid Emamdoost, Stephen McCamant

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.

Seonmo Kim, Stephen McCamant

Approximate model counting for bit-vector SMT formulas (generalizing \#SAT) has many applications such as probabilistic inference and quantitative information-flow security, but it is computationally difficult. Adding random parity constraints (XOR streamlining) and then checking satisfiability is an effective approximation technique, but it requires a prior hypothesis about the model count to produce useful results. We propose an approach inspired by statistical estimation to continually refine a probabilistic estimate of the model count for a formula, so that each XOR-streamlined query yields as much information as possible. We implement this approach, with an approximate probability model, as a wrapper around an off-the-shelf SMT solver or SAT solver. Experimental results show that the implementation is faster than the most similar previous approaches which used simpler refinement strategies. The technique also lets us model count formulas over floating-point constraints, which we demonstrate with an application to a vulnerability in differential privacy mechanisms.

Vaibhav Sharma, Kesha Hietala, Stephen McCamant

Independently developed codebases typically contain many segments of code that perform same or closely related operations (semantic clones). Finding functionally equivalent segments enables applications like replacing a segment by a more efficient or more secure alternative. Such related segments often have different interfaces, so some glue code (an adapter) is needed to replace one with the other. We present an algorithm that searches for replaceable code segments at the function level by attempting to synthesize an adapter between them from some family of adapters; it terminates if it finds no possible adapter. We implement our technique using (1) concrete adapter enumeration based on Intel's Pin framework (2) binary symbolic execution, and explore the relation between size of adapter search space and total search time. We present examples of applying adapter synthesis for improving security and efficiency of binary functions, deobfuscating binary functions, and switching between binary implementations of RC4. We present two large-scale evaluations, (1) we run adapter synthesis on more than 13,000 function pairs from the Linux C library, (2) using more than 61,000 fragments of binary code extracted from a ARM image built for the iPod Nano 2g device and known functions from the VLC media player, we evaluate our adapter synthesis implementation on more than a million synthesis tasks . Our results confirm that several instances of adaptably equivalent binary functions exist in real-world code, and suggest that adapter synthesis can be applied for reverse engineering and for constructing cleaner, less buggy, more efficient programs.