Hardware security threats have raised significant privacy and security concerns and caused enormous financial loss in the past two decades. While new attacks and defenses keep being proposed, there is a lack of systematic and formal studies in this field. Formal verification is a promising approach to address this as it can exhaustively find out all the security vulnerabilities or prove security by showing the absence of vulnerabilities for a given attacker model. To conduct formal verification, security vulnerabilities need to first be specified as formal security properties.Then, a DUV (design under verification) that includes the hardware to be verified and extra logic to express the security properties is constructed. Finally, the DUV along with the security properties are sent to a formal tool such as a model checker that can automatically verify whether properties hold in the DUV. My thesis includes research related to all three steps in this flow.

The first section is security verification of low-trust architectures [CCS2023] where secret value is restricted within a small enclave and everything outside of the enclave is untrusted. Instead of writing down the security properties solely based on the understanding of the hardware design, this work derives hardware security properties from the assumptions made security proofs for programs running on a given architecture. It studies how these program-level assumptions can be related to hardware signals in a specific implementation and models them as hardware information flow properties which then can be checked by standard formal tools.

The second section is improving security verification scalability for transient execution vulnerabilities in modern processors [ASPLOS2025]. Such vulnerabilities have already been formalized by previous works as contract properties, but they were notoriously difficult to verify due to the high complexity of the DUV in previous works. This work proposes a novel and efficient way to construct the DUV, which is called contract shadow logic that reduces the complexity of the DUV and thus of the proof-search. The evaluation demonstrates that this technique drastically increases the scalability of verifying contract properties in multiple open-source processors.

The third section is improving the model checking efficiency for security properties. Because security properties such as hardware information flow are usually checked with DUVs with a fixed symmetric pattern, such symmetry can be exploited to enhance the model checking speed. However, the model checker is designed for properties in general and it is not aware of such a pattern in the DUV. Thus, this work is trying to let the model checker know this information and exploit it for faster verification. This section is still ongoing and will be briefly introduced in the Pre-FPO.

[CCS2023] Tan, Q., Fisseha, Y., Chen, S., Biernacki, L., Jeannin, J. B., Malik, S., & Austin, T. (2023, November). Security Verification of Low-Trust Architectures. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 945-959).

[ASPLOS2025] Tan, Q., Yang, Y., Bourgeat, T., Malik, S., & Yan, M. (2024). RTL verification for secure speculation using contract shadow logic. arXiv preprint arXiv:2407.12232.

Adviser: Sharad Malik 

Zoom Mtg: https://princeton.zoom.us/j/2441381005