Adam Humphries (University of North Carolina), Kartik Cating-Subramanian (University of Colorado), Michael K. Reiter (Duke University)

We present the design and implementation of a tool called TASE that uses transactional memory to reduce the latency of symbolic-execution applications with small amounts of symbolic state.
Execution paths are executed natively while operating on concrete values, and only when execution encounters symbolic values (or modeled functions) is native execution suspended and interpretation begun. Execution then returns to its native mode when symbolic values are no longer encountered. The key innovations in the design of TASE are a technique for amortizing the cost of checking whether values are symbolic over few instructions, and the use of hardware-supported transactional memory (TSX) to implement native execution that rolls back with no effect when use of a symbolic value is detected (perhaps belatedly). We show that TASE has the potential to dramatically improve some latency-sensitive applications of symbolic execution, such as methods to verify the behavior of a client in a client-server application.

View More Papers

Evaluating Personal Data Control In Mobile Applications Using Heuristics

Alain Giboin (UCA, INRIA, CNRS, I3S), Karima Boudaoud (UCA, CNRS, I3S), Patrice Pena (Userthink), Yoann Bertrand (UCA, CNRS, I3S), Fabien Gandon (UCA, INRIA, CNRS, I3S)

Read More

Demo #2: Sequential Attacks on Kalman Filter-Based Forward Collision...

Yuzhe Ma, Jon Sharp, Ruizhe Wang, Earlence Fernandes, and Jerry Zhu (University of Wisconsin–Madison)

Read More

On Building the Data-Oblivious Virtual Environment

Tushar Jois (Johns Hopkins University), Hyun Bin Lee, Christopher Fletcher, Carl A. Gunter (University of Illinois at Urbana-Champaign)

Read More