Micro-architectural timing channels are one of the best-known side channels exploited by attackers. The presence of such timing channels allows attackers to retrieve sensitive information by exploiting dynamic software properties (e.g. time, cache misses and memory access statistics). In the last two decades, the security research community has discovered numerous evidences of practical timing attacks, with more recent and critical attacks reflected in CacheBleed , Spectre and Meltdown. In this project, we will design a set of technologies and tools to validate and verify arbitrary programs against realistic timing-channel attacks. Our goal is not to design a set of techniques to exploit timing channels of a system. Instead, for arbitrary software programs, we will develop efficient algorithms to validate and verify them against realistic, timing-channel attack models. Driven by the results of our verification and validation, we will further synthesize countermeasures to shield program executions from timing-channel attacks. In such a fashion, for arbitrary programs, we will enable strong theoretical guarantees on the level of protection against threats involving timing channels.
Quantifying the Information Leakage in Cache Attacks via Symbolic Execution
Sudipta Chattopadhyay, Moritz Beck, Ahmed Rezine, and Andreas Zeller
ACM Transactions on Embedded Computing Systems (TECS), 2019
Directed Automated Memory Performance Testing
Sudipta Chattopadhyay
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2017
An Exploration of Effective Fuzzing for Side-channel Cache Leakage
Tiyash Basu, Kartik Aggarwal, Chundong Wang, and Sudipta Chattopadhyay
Software Testing, Verification and Reliability (STVR), 2019
ORIGAMI: Folding Data Structures to Reduce Timing Side-Channel Leakage
Eric Rothestein-Morris, Jun Sun, and Sudipta Chattopadhyay
20th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), 2022
KLEESpectre: Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution
Guanhua Wang, Sudipta Chattopadhyay, Arnab Kumar Biswas, Tulika Mitra, and Abhik Roychoudhury
ACM Transactions on Software Engineering and Methodology (TOSEM), 2020
Symbolic Verification of Cache Side-channel Freedom
Sudipta Chattopadhyay and Abhik Roychoudhury
IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems (TCAD), 2018
Acknowledgement: We are grateful to SUTD and Singapore Ministry of Education (MOE) for generously supporting this project.