Specification and Verification of Strong Timing Isolation of Hardware Enclaves
CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA.
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
ACM|Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security
2025
|
| Online Access: | https://hdl.handle.net/1721.1/158084 |
| _version_ | 1824458050822471680 |
|---|---|
| author | Lau, Stella Bourgeat, Thomas Pit-Claudel, Cl?ment Chlipala, Adam |
| author2 | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
| author_facet | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Lau, Stella Bourgeat, Thomas Pit-Claudel, Cl?ment Chlipala, Adam |
| author_sort | Lau, Stella |
| collection | MIT |
| description | CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA. |
| first_indexed | 2025-02-19T04:19:44Z |
| format | Article |
| id | mit-1721.1/158084 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2025-02-19T04:19:44Z |
| publishDate | 2025 |
| publisher | ACM|Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security |
| record_format | dspace |
| spelling | mit-1721.1/1580842025-01-28T14:06:52Z Specification and Verification of Strong Timing Isolation of Hardware Enclaves Lau, Stella Bourgeat, Thomas Pit-Claudel, Cl?ment Chlipala, Adam Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA. The process isolation enforceable by commodity hardware and operating systems is too weak to protect secrets from malicious code running on the same machine: attacks exploit timing side channels derived from contention on shared microarchitectural resources to extract secrets. With appropriate hardware support, however, we can construct isolated enclaves and safeguard independent processes from interference through timing side channels, a step towards confidentiality and integrity guarantees. In this paper, we describe our work on formally specifying and verifying that a synthesizable hardware architecture implements strong timing isolation for enclaves. We reason about the cycle-accurate semantics of circuits with respect to a trustworthy formulation of strong isolation based on "air-gapped machines" and develop a modular proof strategy that sidesteps the need to prove functional correctness of processors. We apply our method on a synthesizable, multicore, pipelined RISC-V design formalized in Coq. 2025-01-28T14:06:49Z 2025-01-28T14:06:49Z 2024-12-02 2025-01-01T08:49:07Z Article http://purl.org/eprint/type/ConferencePaper 979-8-4007-0636-3 https://hdl.handle.net/1721.1/158084 Lau, Stella, Bourgeat, Thomas, Pit-Claudel, Cl?ment and Chlipala, Adam. 2024. "Specification and Verification of Strong Timing Isolation of Hardware Enclaves." PUBLISHER_CC en https://doi.org/10.1145/3658644.3690203 Creative Commons Attribution https://creativecommons.org/licenses/by/4.0/ The author(s) application/pdf ACM|Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security Association for Computing Machinery |
| spellingShingle | Lau, Stella Bourgeat, Thomas Pit-Claudel, Cl?ment Chlipala, Adam Specification and Verification of Strong Timing Isolation of Hardware Enclaves |
| title | Specification and Verification of Strong Timing Isolation of Hardware Enclaves |
| title_full | Specification and Verification of Strong Timing Isolation of Hardware Enclaves |
| title_fullStr | Specification and Verification of Strong Timing Isolation of Hardware Enclaves |
| title_full_unstemmed | Specification and Verification of Strong Timing Isolation of Hardware Enclaves |
| title_short | Specification and Verification of Strong Timing Isolation of Hardware Enclaves |
| title_sort | specification and verification of strong timing isolation of hardware enclaves |
| url | https://hdl.handle.net/1721.1/158084 |
| work_keys_str_mv | AT laustella specificationandverificationofstrongtimingisolationofhardwareenclaves AT bourgeatthomas specificationandverificationofstrongtimingisolationofhardwareenclaves AT pitclaudelclment specificationandverificationofstrongtimingisolationofhardwareenclaves AT chlipalaadam specificationandverificationofstrongtimingisolationofhardwareenclaves |