Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

9 résultats
Image document

Verifying Constant-Time Implementations by Abstract Interpretation

Sandrine Blazy , David Pichardie , Alix Trieu
European Symposium on Research in Computer Security, Sep 2017, Oslo, Norway
Communication dans un congrès hal-01588444v1
Image document

Proving full-system security properties under multiple attacker models on capability machines

Thomas Van Strydonck , Aïna Linn Georges , Armaël Guéneau , Alix Trieu , Amin Timany , et al.
CSF 2022 - 35th IEEE Computer Security Foundations Symposium, Aug 2022, Haifa, Israel
Communication dans un congrès hal-03826851v1
Image document

Verifying constant-time implementations by abstract interpretation

Sandrine Blazy , David Pichardie , Alix Trieu
Journal of Computer Security, 2019, 27 (1), pp.137--163. ⟨10.3233/JCS-181136⟩
Article dans une revue hal-02025047v1
Image document

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code

Aïna Linn Georges , Armaël Guéneau , Thomas Van Strydonck , Amin Timany , Alix Trieu , et al.
Journal of the ACM (JACM), 2023, ⟨10.1145/3623510⟩
Article dans une revue hal-03826854v3
Image document

33èmes journées francophones des langages applicatifs

Chantal Keller , Timothy Bourke , Sandrine Blazy , Frédéric Bour , Guillaume Bury , et al.
Chantal Keller; Timothy Bourke. , pp.1-292, 2022
Ouvrages hal-03689075v1
Image document

Verified Translation Validation of Static Analyses

Gilles Barthe , Sandrine Blazy , Vincent Laporte , David Pichardie , Alix Trieu
Computer Security Foundations Symposium, Aug 2017, Santa-Barbara, United States
Communication dans un congrès hal-01588422v1
Image document

Static conflict detection for a policy language

Alix Trieu , Robert Dockins , Andrew Tolmach
Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), David Baelde; Jade Alglave, Jan 2015, Le Val d'Ajol, France
Communication dans un congrès hal-01099124v1
Image document

Formal verification of a constant-time preserving C compiler

Gilles Barthe , Sandrine Blazy , Benjamin Grégoire , Rémi Hutin , Vincent Laporte , et al.
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩
Article dans une revue hal-02975012v1
Image document

Formal Verification of Control-flow Graph Flattening

Sandrine Blazy , Alix Trieu
Certified Proofs and Programs (CPP 2016), Jan 2016, Saint-Petersburg, United States. pp.12, ⟨10.1145/2854065.2854082⟩
Communication dans un congrès hal-01242063v1