Specification and Verification of Strong Timing Isolation of Hardware Enclaves.
Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 2024
Nimble: Rollback Protection for Confidential Cloud Services (extended version).
IACR Cryptol. ePrint Arch., 2023
Nimble: Rollback Protection for Confidential Cloud Services.
Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation, 2023
Pensieve: Microarchitectural Modeling for Security Evaluation.
Proceedings of the 50th Annual International Symposium on Computer Architecture, 2023
Effective simulation and debugging for a high-level hardware language using software compilers.
Proceedings of the ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2021
Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019