Formally Verifying a Rollback-Prevention Protocol for TEEs

Formal verification of distributed protocols is challenging and usually requires great human effort. Ivy, a state-of-the-art formal verification tool for modeling and verifying distributed protocols, automates this tedious process by leveraging a decidable fragment of firstorder logic. Observing the successful adoption of Ivy for verifying consensus protocols, we examine its practicality in verifying rollback-prevention protocols for Trusted Execution Environments (TEEs). TEEs suffer from rollback attacks, which can revert confidential applications' states to stale ones to compromise security. Recently, designing distributed protocols to prevent rollback attacks has attracted significant attention. However, the lack of formal verification of these protocols leaves them potentially vulnerable to security breaches. In this paper, we leverage Ivy to formally verify a rollback-prevention protocol, namely the TIKS protocol in ENGRAFT (Wang et al., CCS 2022). We select TIKS because it is similar to other rollback-prevention protocols and is self-contained. We detail the verification process of using Ivy to prove a rollback-prevention protocol, present lessons learned from this exploration, and release the proof code to facilitate future research (https://github.com/wwl020/TIKS-Proofin-Ivy). To the best of our knowledge, this is the first endeavor to explain the formal verification of a rollback-prevention protocol in detail.