Tue 18 Jan 2022 08:15 - 08:45 at PEPM - Contributed Talks 3 Chair(s): Youyou Cong

Cyber attacks become more and more prevalent every day. An arms race is thus engaged between cyber attacks and cyber defences. One type of cyber attack is known as a side channel attack, where attackers exploit information leakage from the physical execution of a program, e.g. timing or power leakage, to uncover secret information, such as encryption keys or other sensitive data. There have been various attempts at addressing the problem of side-channel attacks, often relying on various measures to decrease the discernibility of several code variants or code paths. Most techniques require a high-degree of expertise by the developer, who often employs ad hoc, hand-crafted code-patching in an attempt to make it more secure. In this paper, we take a different approach: building on the idea of ladderisation, inspired by Montgomery Ladders. We present a semi-automatic tool-supported technique, aimed at the non-specialised developer, which rewrites (a class of) C programs into functionally (and even algorithmically) equivalent counterparts with improved security properties. Our rewriting mechanism provides refactorings that transform the source code into its ladderised equivalent, driven by an underlying verified rewrite system, based on dependent types. Our rewrite system automatically finds rewritings of C programs producing their equivalent ladderised counterparts for a subset of C. We demonstrate our ladder rewriting technique on a number of representative examples from the cryptographic domain, showing increased security thanks to the process.

Tue 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

08:15 - 09:15
Contributed Talks 3PEPM at PEPM
Chair(s): Youyou Cong Tokyo Institute of Technology
08:15
30m
Talk
Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent TypesRemote
PEPM
Christopher Brown University of St. Andrews, UK, Adam D. Barwell Imperial College London, UK, Yoann Marquer INRIA, Rennes, France, Olivier Zendra INRIA, Rennes, France, Tania Richmond INRIA, Rennes, France then DGA - Maîtrise de l’Information, Chen Gu Hefei University of Technology, China
Link to publication
08:45
30m
Talk
Dependent tagless finalRemote
PEPM
Nicolas Biri Luxembourg Institute of Science and Technology
Link to publication