Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866915907754786816 |
|---|---|
| author | Baumann, Jonathan Kim, Yonghyun Farba, Yan Hritcu, Catalin Leatherman-Brooks, Julay |
| author_facet | Baumann, Jonathan Kim, Yonghyun Farba, Yan Hritcu, Catalin Leatherman-Brooks, Julay |
| contents | This paper introduces Triosecuris, a formally verified defense against Spectre BTB, RSB, and PHT that combines CET-style hardware-assisted control-flow integrity with compiler-inserted speculative load hardening (SLH). Triosecuris is based on the novel observation that in the presence of CET-style protection, we can precisely detect BTB misspeculation for indirect calls and RSB misspeculation for returns and set the SLH misspeculation flag. We formalize Triosecuris as a transformation in Rocq and provide a machine-checked proof that it achieves relative security: any transformed program running with speculation leaks no more than what the source program leaks without speculation. This strong security guarantee applies to arbitrary programs, even those not following the cryptographic constant-time programming discipline. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_22978 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking Baumann, Jonathan Kim, Yonghyun Farba, Yan Hritcu, Catalin Leatherman-Brooks, Julay Cryptography and Security Programming Languages This paper introduces Triosecuris, a formally verified defense against Spectre BTB, RSB, and PHT that combines CET-style hardware-assisted control-flow integrity with compiler-inserted speculative load hardening (SLH). Triosecuris is based on the novel observation that in the presence of CET-style protection, we can precisely detect BTB misspeculation for indirect calls and RSB misspeculation for returns and set the SLH misspeculation flag. We formalize Triosecuris as a transformation in Rocq and provide a machine-checked proof that it achieves relative security: any transformed program running with speculation leaks no more than what the source program leaks without speculation. This strong security guarantee applies to arbitrary programs, even those not following the cryptographic constant-time programming discipline. |
| title | Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking |
| topic | Cryptography and Security Programming Languages |
| url | https://arxiv.org/abs/2601.22978 |