{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T17:59:46Z","timestamp":1773511186121,"version":"3.50.1"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031626449","type":"print"},{"value":"9783031626456","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-62645-6_9","type":"book-chapter","created":{"date-parts":[[2024,6,12]],"date-time":"2024-06-12T05:01:51Z","timestamp":1718168511000},"page":"155-173","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formally Verifying a\u00a0Rollback-Prevention Protocol for\u00a0TEEs"],"prefix":"10.1007","author":[{"given":"Weili","family":"Wang","sequence":"first","affiliation":[]},{"given":"Jianyu","family":"Niu","sequence":"additional","affiliation":[]},{"given":"Michael K.","family":"Reiter","sequence":"additional","affiliation":[]},{"given":"Yinqian","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,6,13]]},"reference":[{"key":"9_CR1","unstructured":"The Coq proof assistant. https:\/\/coq.inria.fr. Accessed 03 May 2022"},{"key":"9_CR2","unstructured":"Errors found in distributed protocols. https:\/\/github.com\/dranov\/protocol-bugs-list. Accessed 03 May 2022"},{"key":"9_CR3","unstructured":"TLA+ proof system (TLAPS). http:\/\/tla.msr-inria.inria.fr\/tlaps\/content\/Home.html. Accessed 03 May 2022"},{"key":"9_CR4","unstructured":"Z3 SMT solver. https:\/\/github.com\/Z3Prover\/z3. Accessed 03 May 2022"},{"key":"9_CR5","unstructured":"AMD secure encrypted virtualization. https:\/\/www.amd.com\/en\/processors\/amd-secure-encrypted-virtualization"},{"key":"9_CR6","unstructured":"Angel, S., et al.: Nimble: rollback protection for confidential cloud services. In: 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2023), pp. 193\u2013208 (2023)"},{"key":"9_CR7","unstructured":"ARM confidential compute architecture. https:\/\/www.arm.com\/architecture\/security-features\/arm-confidential-compute-architecture"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-030-25543-5_15","volume-title":"Computer Aided Verification","author":"I Berkovits","year":"2019","unstructured":"Berkovits, I., Lazi\u0107, M., Losa, G., Padon, O., Shoham, S.: Verification of threshold-based distributed algorithms by decomposition to decidable logics. In: Dillig, I., Tasiran, S. (eds.) CAV 2019, Part II. LNCS, vol. 11562, pp. 245\u2013266. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_15"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-319-48989-6_8","volume-title":"FM 2016: Formal Methods","author":"S Chand","year":"2016","unstructured":"Chand, S., Liu, Y.A., Stoller, S.D.: Formal verification of multi-paxos for distributed consensus. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 119\u2013136. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_8"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/s10703-016-0257-4","volume":"49","author":"A Cimatti","year":"2016","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant checking with IC3 and predicate abstraction. Form. Methods Syst. Des. 49, 190\u2013218 (2016)","journal-title":"Form. Methods Syst. Des."},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Dinis, B., Druschel, P., Rodrigues, R.: RR: a fault model for efficient tee replication. In: The Network and Distributed System Security Symposium. Internet Society (2023)","DOI":"10.14722\/ndss.2023.24001"},{"key":"9_CR12","unstructured":"Hance, T., Heule, M., Martins, R., Parno, B.: Finding invariants of distributed systems: it\u2019s a small (enough) world after all. In: 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2021), pp. 115\u2013131 (2021)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., et al.: IronFleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles, pp. 1\u201317 (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"9_CR14","unstructured":"Intel software guard extensions. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-and-technology\/software-guard-extensions.html"},{"key":"9_CR15","unstructured":"Jangid, M.K., Chen, G., Zhang, Y., Lin, Z.: Towards formal verification of state continuity for enclave programs. In: 30th USENIX Security Symposium (USENIX Security 2021), pp. 573\u2013590 (2021)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-030-78089-0_13","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"L Jehl","year":"2021","unstructured":"Jehl, L.: Formal verification of HotStuff. In: Peters, K., Willemse, T.A.C. (eds.) FORTE 2021. LNCS, vol. 12719, pp. 197\u2013204. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78089-0_13"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: 2013 Formal Methods in Computer-Aided Design, pp. 201\u2013209. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.ic.2016.03.006","volume":"252","author":"I Konnov","year":"2017","unstructured":"Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf. Comput. 252, 95\u2013109 (2017)","journal-title":"Inf. Comput."},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-030-03424-5_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems","author":"I Konnov","year":"2018","unstructured":"Konnov, I., Widder, J.: ByMC: byzantine model checker. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11246, pp. 327\u2013342. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03424-5_22"},{"key":"9_CR20","volume-title":"Specifying Systems","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems, vol. 388. Addison-Wesley, Boston (2002)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-24100-0_22","volume-title":"Distributed Computing","author":"L Lamport","year":"2011","unstructured":"Lamport, L.: Byzantizing Paxos by refinement. In: Peleg, D. (ed.) DISC 2011. LNCS, vol. 6950, pp. 211\u2013224. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24100-0_22"},{"key":"9_CR22","unstructured":"Lamport, L., Merz, S., Doligez, D.: TLAPS proof of basic PAXOS. https:\/\/github.com\/tlaplus\/tlapm\/blob\/main\/examples\/paxos\/Paxos.tla. Accessed 03 May 2022"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"9_CR24","unstructured":"Li, X., et al.: Design and verification of the arm confidential compute architecture. In: 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022), pp. 465\u2013484 (2022)"},{"key":"9_CR25","unstructured":"Matetic, S., et al.: ROTE: rollback protection for trusted execution. In: 26th USENIX Security Symposium (USENIX Security 2017), pp. 1289\u20131306 (2017)"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Niu, J., Peng, W., Zhang, X., Zhang, Y.: Narrator: secure and practical state continuity for trusted execution in the cloud. In: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, pp. 2385\u20132399 (2022)","DOI":"10.1145\/3548606.3560620"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Programm. Lang. 1(OOPSLA), 1\u201331 (2017)","DOI":"10.1145\/3140568"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 614\u2013630 (2016)","DOI":"10.1145\/2908080.2908118"},{"key":"9_CR29","doi-asserted-by":"publisher","unstructured":"Peng, W., Li, X., Niu, J., Zhang, X., Zhang, Y.: Ensuring state continuity for confidential computing: a blockchain-based approach. IEEE Trans. Depend. Secure Comput., 1\u201314 (2024). https:\/\/doi.org\/10.1109\/TDSC.2024.3381973","DOI":"10.1109\/TDSC.2024.3381973"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Reiter, M.K.: Secure agreement protocols: Reliable and atomic group multicast in rampart. In: Proceedings of the 2nd ACM Conference on Computer and Communications Security, CCS 1994, pp. 68\u201380. Association for Computing Machinery, New York (1994). https:\/\/doi.org\/10.1145\/191177.191194","DOI":"10.1145\/191177.191194"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Schultz, W., Dardik, I., Tripakis, S.: Formal verification of a distributed dynamic reconfiguration protocol. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 143\u2013152 (2022)","DOI":"10.1145\/3497775.3503688"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. Proc. ACM Programm. Lang. 2(POPL), 1\u201330 (2017)","DOI":"10.1145\/3158116"},{"key":"9_CR33","unstructured":"Tamarin prover. https:\/\/tamarin-prover.com\/"},{"issue":"OOPSLA2","key":"9_CR34","doi-asserted-by":"publisher","first-page":"1878","DOI":"10.1145\/3622864","volume":"7","author":"O Tamir","year":"2023","unstructured":"Tamir, O., et al.: Counterexample driven quantifier instantiations with applications to distributed protocols. Proc. ACM Programm. Lang. 7(OOPSLA2), 1878\u20131904 (2023)","journal-title":"Proc. ACM Programm. Lang."},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Taube, M., et al.: Modularity for decidability of deductive verification with applications to distributed systems. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 662\u2013677 (2018)","DOI":"10.1145\/3192366.3192414"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Wang, W., Deng, S., Niu, J., Reiter, M.K., Zhang, Y.: ENGRAFT: enclave-guarded raft on byzantine faulty nodes. In: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, pp. 2841\u20132855 (2022)","DOI":"10.1145\/3548606.3560639"},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, New York, NY, USA, pp. 357\u2013368 (2015). https:\/\/doi.org\/10.1145\/2737924.2737958","DOI":"10.1145\/2737924.2737958"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.: Planning for change in a formal verification of the raft consensus protocol. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 154\u2013165 (2016)","DOI":"10.1145\/2854065.2854081"},{"key":"9_CR39","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J.: DuoAI: fast, automated inference of inductive invariants for verifying distributed protocols. In: 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022), pp. 485\u2013501 (2022)"},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-62645-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,12]],"date-time":"2024-06-12T05:02:53Z","timestamp":1718168573000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-62645-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031626449","9783031626456"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-62645-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"13 June 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Groningen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"44","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}