Type-directed Program Transformation for Constant-Time Enforcement - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2023

Type-directed Program Transformation for Constant-Time Enforcement

Abstract

Constant-time is a programming discipline which protects security sensitive code against a wide class of timing attacks. This discipline can be formalised as a non-interference property and enforced by an information flow type system which prevents branching and memory accesses over secret data. We propose a relaxed information flow type system which tracks indirect flows but only rejects programs leaking secrets through direct flows. The main result of this paper is that any program that is accepted using this relaxed type system can be transformed automatically into a semantically equivalent constant-time program. Our algorithms are implemented in the jasmin compiler and validated against synthetic programs.
Fichier principal
Vignette du fichier
ppdp2023-6.pdf (687.97 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-04268830 , version 1 (02-11-2023)

Licence

Attribution

Identifiers

Cite

Frédéric Besson, Thomas Jensen, Gautier Raimondi. Type-directed Program Transformation for Constant-Time Enforcement. PPDP 2023 - International Symposium on Principles and Practice of Declarative Programming, Oct 2023, Lisboa, Portugal. pp.1-13, ⟨10.1145/3610612.3610618⟩. ⟨hal-04268830⟩
30 View
27 Download

Altmetric

Share

Gmail Facebook X LinkedIn More