Dynamic Symbolic Execution (DSE) has seen a rise of its popularity as it allows to check applications for specific behaviours like error patterns automatically. One of its biggest challenges is the state space explosion problem: DSE tries to evaluate all possible execution paths of an application, and for every path, it needs to represent the allocated memory and its accesses. Even though different approaches have been proposed to mitigate the state space explosion problem itself, DSE still needs to represent a multitude of states in parallel to analyse them. If too many states are present, they cannot fit into memory and DSE needs to terminate them prematurely. With a more efficient representation of allocated memory, DSE can handle more states in parallel improving its performance. In this work, we introduce an enhanced, fine-grain and performant memory representation of states. Our implementation on top of the symbolic execution engine KLEE shows a significant reduction of the memory consumption of states by up to \reducedmem{} allowing to represent more states in memory more efficiently and in addition its execution time is reduced by \reducedexectime{} - a speedup of \speedup{}.
Debreach: Mitigating Compression Side Channels via Static Analysis and Transformation Research Papers
Compression is an emerging source of exploitable side-channel leakage that threatens data security, particularly in web applications where compression is indispensable for performance reasons. Current approaches to mitigating compression side channels have drawbacks in that they either degrade compression ratio drastically or require too much effort from developers to be widely adopted. To bridge the gap, we develop Debreach, a static analysis and program transformation based approach to mitigating compression side channels. Debreach consists of two steps. First, it uses taint analysis to soundly identify flows of sensitive data in the program and uses code instrumentation to annotate data before feeding them to the compressor. Second, it enhances the compressor to exploit the freedom to not compress of standard compression protocols, thus removing the dependency between sensitive data and the size of the compressor’s output. Since Debreach automatically instruments applications and does not change the compression protocols, it has the advantage of being non-disruptive and compatible with existing systems. We have evaluated Debreach on a set of web server applications written in PHP. Our experiments show that, while ensuring leakage-freedom, Debreach can achieve significantly higher compression performance than state-of-the-art approaches.
