Semi-automatic ladderisation: improving code security through rewriting and dependent types
Semi-automatic ladderisation: improving code security through rewriting and dependent types
复制标题
DOI：
10.1145/3498886.3502202
复制
发表时间：
2022-01
期刊：
影响因子：
--
通讯作者：
Christopher Brown;Adam D. Barwell;Yoann Marquer;Olivier Zendra;Tania Richmond;Chen Gu
中科院分区：
文献类型：
--
作者：
Christopher Brown;Adam D. Barwell;Yoann Marquer;Olivier Zendra;Tania Richmond;Chen Gu
网络攻击每天都变得越来越普遍。一种类型的网络攻击被称为侧信道攻击，其中攻击者利用来自程序的物理执行的信息泄漏（例如，定时或功率泄漏）来揭露秘密信息，诸如加密密钥或其他敏感数据。已经有各种尝试来解决防止边信道攻击的问题，通常依赖于各种措施来降低若干代码变体或代码路径的可验证性。大多数技术都需要开发人员的高度专业知识，他们经常使用临时的手工代码修补来使其更加安全。在本文中，我们采取了不同的方法：建立在阶梯化的想法，灵感来自蒙哥马利梯子。我们提出了一个半自动的工具支持的技术，针对非专业的开发人员，重构（一类）C程序到功能（甚至算法）等效的同行，提高了安全性能。我们的方法提供了重构，将源代码转换成其梯形等效，驱动底层验证重写系统，依赖类型的基础上。我们的重写系统自动发现重写选定的C表达式，促进其等效的梯形对应物的C子集的生产。我们展示了我们的方法从加密域的一些代表性的例子，显示出更高的安全性。
Cyber attacks become more and more prevalent every day. 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 preventing 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 refactors (a class of) C programs into functionally (and even algorithmically) equivalent counterparts with improved security properties. Our approach 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 selected C expressions, facilitating the production of their equivalent ladderised counterparts for a subset of C. We demonstrate our approach on a number of representative examples from the cryptographic domain, showing increased security.