Verification and Validation of Side-channel Freedom

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.To know more about the topic, please take a look at our following publications: arXiv-2018, ACM-TECS-2019, TCAD/EMSOFT-2018, MEMOCODE-2017, TACAS-2017, ICSTW-2017, ASPDAC-2016.

Acknowledgement: We are grateful to SUTD and Singapore Ministry of Education (MOE) for generously supporting this project.

Open Positions for Postdocs:
We are looking for two (2) Post-Doctoral candidates to work on techniques for analysing, validating and shielding micro-architectural timing channels. The positions are funded by a recent highly competitive three-years grant from the Singapore Ministry of Education (MOE) on automating the analysis and validation of Micro-architectural timing-channel Freedom. Applicants should possess a Ph.D. degree in Computer Science or equivalent. A successful candidate should have a strong research experience in some of the following fields: program analysis, symbolic execution, computer architecture, formal verification, model checking, testing, security. A Post-Doctoral position is time-limited for a year and extendable to two years upon satisfactory evaluation by the investigators.

Application for Postdoc Positions:
Applications should include a two-page research statement describing his/her research interests and experience and how they relate to the project, a detailed CV and the contact information of two referees. Prospective candidates are expected to join from February 2019 or soon after. We will look for applications until the positions are filled. However, prospective applicants are highly encouraged to submit their applications by 31st October, 2018. For submitting the application, combine all the required documents in a single PDF document and send to Sudipta Chattopadhyay (email: sudipta_chattopadhyay@sutd.edu.sg) and Ahmed Rezine (email: ahmed.rezine@liu.se) — the investigators of the project. All research activities will be carried out in SUTD, Singapore.

Open Positions for Student Researchers:
If you are a student (undergraduate or masters) in SUTD or in Singapore, there exists multiple opportunities to participate in the scientific activities within the project (e.g. via UROP). If you are interested to contribute in the project, then simply drop the project investigator Sudipta an email (email: sudipta_chattopadhyay@sutd.edu.sg) to set up a meeting.

People

Chundong Wang
Post Doc (PhD, NUS, Singapore)
Ahmed Rezine
Associate Professor (Linköping University, Sweden)