The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Verifying constant-time implementations in a verified compilation toolchain
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
Vérification d'implémentations constant-time dans une chaîne de compilation vérifiée Les attaques par canaux cachés sont une forme d'attaque particulièrement dangereuse. Dans cette thèse, nous nous intéressons au canal caché temporel. Un programme est dit ''constant-time'' lorsqu'il n'est pas vulnérable aux attaques par canal caché temporel. Nous présentons dans ce manuscrit deux méthodes reposant sur l'analyse statique afin de s'assurer qu'un programme est constant-time. Ces méthodes se placent dans le cadre de vérification formelle afin d'obtenir le plus haut niveau d'assurance possible en s'appuyant sur une chaîne de compilation vérifiée composée du compilateur CompCert et de l'analyseur statique Verasco. Nous proposons aussi une méthode de preuve afin de s'assurer qu'un compilateur préserve la propriété de constant-time lors de la compilation d'un programme.
How it got here
How it got here
agent via openalex
Added
2026-10-26 16:33 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@phdthesis{trieu2018verifying,
title = {Verifying constant-time implementations in a verified compilation toolchain},
author = {Alix Trieu},
year = {2018},
doi = {10.70675/c041309azf0faz4ae5za91fz3eb6c96c0d82},
}