PEPM '22: "Semi-automatic Ladderisation: ..."
Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Christopher Brown, Adam D. Barwell, Yoann Marquer, Olivier Zendra, Tania Richmond, and Chen Gu
(University of St. Andrews, UK; Imperial College London, UK; Inria, France; DGA, France; Hefei University of Technology, China)
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.
@InProceedings{PEPM22p14,
author = {Christopher Brown and Adam D. Barwell and Yoann Marquer and Olivier Zendra and Tania Richmond and Chen Gu},
title = {Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {14--27},
doi = {10.1145/3498886.3502202},
year = {2022},
}
Publisher's Version
PEPM '22: "Dependent Tagless Final ..."
Dependent Tagless Final
Nicolas Biri
(Luxembourg Institute of Science and Technology, Luxembourg)
Tagless final embedding provides a solution to the expression problem that allows efficient code generation, thanks to multi-staged evaluation. It can, however, be a challenge to compose effectful language fragments in this embedding. This paper proposes a dependent tagless final embedding that uses dependent types to ease the composition of effects. We show that this extension preserves the multi-staging capabilities of tagless final and can help scope effects in domain-specific languages.
@InProceedings{PEPM22p1,
author = {Nicolas Biri},
title = {Dependent Tagless Final},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3498886.3502201},
year = {2022},
}
Publisher's Version
PEPM '22: "Semi-automatic Ladderisation: ..."
Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Christopher Brown, Adam D. Barwell, Yoann Marquer, Olivier Zendra, Tania Richmond, and Chen Gu
(University of St. Andrews, UK; Imperial College London, UK; Inria, France; DGA, France; Hefei University of Technology, China)
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.
@InProceedings{PEPM22p14,
author = {Christopher Brown and Adam D. Barwell and Yoann Marquer and Olivier Zendra and Tania Richmond and Chen Gu},
title = {Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {14--27},
doi = {10.1145/3498886.3502202},
year = {2022},
}
Publisher's Version
PEPM '22: "Semi-automatic Ladderisation: ..."
Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Christopher Brown, Adam D. Barwell, Yoann Marquer, Olivier Zendra, Tania Richmond, and Chen Gu
(University of St. Andrews, UK; Imperial College London, UK; Inria, France; DGA, France; Hefei University of Technology, China)
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.
@InProceedings{PEPM22p14,
author = {Christopher Brown and Adam D. Barwell and Yoann Marquer and Olivier Zendra and Tania Richmond and Chen Gu},
title = {Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {14--27},
doi = {10.1145/3498886.3502202},
year = {2022},
}
Publisher's Version
PEPM '22: "Semi-automatic Ladderisation: ..."
Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Christopher Brown, Adam D. Barwell, Yoann Marquer, Olivier Zendra, Tania Richmond, and Chen Gu
(University of St. Andrews, UK; Imperial College London, UK; Inria, France; DGA, France; Hefei University of Technology, China)
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.
@InProceedings{PEPM22p14,
author = {Christopher Brown and Adam D. Barwell and Yoann Marquer and Olivier Zendra and Tania Richmond and Chen Gu},
title = {Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {14--27},
doi = {10.1145/3498886.3502202},
year = {2022},
}
Publisher's Version
PEPM '22: "Semi-automatic Ladderisation: ..."
Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Christopher Brown, Adam D. Barwell, Yoann Marquer, Olivier Zendra, Tania Richmond, and Chen Gu
(University of St. Andrews, UK; Imperial College London, UK; Inria, France; DGA, France; Hefei University of Technology, China)
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.
@InProceedings{PEPM22p14,
author = {Christopher Brown and Adam D. Barwell and Yoann Marquer and Olivier Zendra and Tania Richmond and Chen Gu},
title = {Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {14--27},
doi = {10.1145/3498886.3502202},
year = {2022},
}
Publisher's Version
PEPM '22: "Semi-automatic Ladderisation: ..."
Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Christopher Brown, Adam D. Barwell, Yoann Marquer, Olivier Zendra, Tania Richmond, and Chen Gu
(University of St. Andrews, UK; Imperial College London, UK; Inria, France; DGA, France; Hefei University of Technology, China)
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.
@InProceedings{PEPM22p14,
author = {Christopher Brown and Adam D. Barwell and Yoann Marquer and Olivier Zendra and Tania Richmond and Chen Gu},
title = {Semi-automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {14--27},
doi = {10.1145/3498886.3502202},
year = {2022},
}
Publisher's Version