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

Low-risk Privacy-preserving Electric Vehicle Charging with Payments

Andreas Unterweger, Fabian Knirsch, Clemens Brunner and Dominik Engel (Center for Secure Energy Informatics, Salzburg University of Applied Sciences, Puch bei Hallein, Austria)

Read More

Data Analytics and Expert Judgment in Time of Crisis:...

Igor Linkov, PhD Senior Science and Technology Manager, US Army Engineer Research and Development Center; Senior Data Analyst (on detail), FEMA/HHS R1 COVID Task Force; Adjunct Professor, Carnegie Mellon University

Read More

FlowLens: Enabling Efficient Flow Classification for ML-based Network Security...

Diogo Barradas (INESC-ID, Instituto Superior Técnico, Universidade de Lisboa), Nuno Santos (INESC-ID, Instituto Superior Técnico, Universidade de Lisboa), Luis Rodrigues (INESC-ID, Instituto Superior Técnico, Universidade de Lisboa), Salvatore Signorello (LASIGE, Faculdade de Ciências, Universidade de Lisboa), Fernando M. V. Ramos (INESC-ID, Instituto Superior Técnico, Universidade de Lisboa), André Madeira (INESC-ID, Instituto Superior Técnico, Universidade de…

Read More

CV-Inspector: Towards Automating Detection of Adblock Circumvention

Hieu Le (University of California, Irvine), Athina Markopoulou (University of California, Irvine), Zubair Shafiq (University of California, Davis)

Read More