3 papers
cs.AR2024★ 1 cited
RTL Verification for Secure Speculation Using Contract Shadow Logic
Qinhan Tan, Yuheng Yang, Thomas Bourgeat +2
Modern out-of-order processors face speculative execution attacks. Despite various proposed software and hardware mitigations to prevent such attacks, new attacks keep arising from…
cs.AR2023★ 7 cited
Security Verification of Low-Trust Architectures
Qinhan Tan, Yonathan Fisseha, Shibo Chen +4
Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave compo…
cs.DC2014
Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom
Divjyot Sethi, Muralidhar Talupur, Sharad Malik
We consider the problem of verifying deadlock freedom for symmetric cache coherence protocols. In particular, we focus on a specific form of deadlock which is useful for the cache…