{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:54:23Z","timestamp":1766134463973,"version":"3.48.0"},"reference-count":61,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T00:00:00Z","timestamp":1763424000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T00:00:00Z","timestamp":1763424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/X015114\/1"],"award-info":[{"award-number":["EP\/X015114\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/X015114\/1"],"award-info":[{"award-number":["EP\/X015114\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/X015114\/1"],"award-info":[{"award-number":["EP\/X015114\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/X015114\/1"],"award-info":[{"award-number":["EP\/X015114\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/X015114\/1"],"award-info":[{"award-number":["EP\/X015114\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/X015114\/1"],"award-info":[{"award-number":["EP\/X015114\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Meltdown and Spectre are vulnerabilities known as transient execution vulnerabilities, where an attacker exploits speculative execution (a semantic optimization present in most modern processors) to break confidentiality. We introduce\n                    <jats:italic>relative security<\/jats:italic>\n                    , a general notion of information-flow security that models this type of vulnerability by contrasting the leaks that are possible in a \u201cvanilla\u201d semantics with those possible in a different semantics, often obtained from the vanilla semantics via some optimizations. We describe incremental proof methods, in the style of Goguen and Meseguer\u2019s unwinding, both for proving and for disproving relative security, and deploy these to formally establish the relative (in)security of some standard Spectre examples. Both the abstract results and the case studies have been mechanized in the Isabelle\/HOL theorem prover. This paper is an extension of an earlier conference paper that provides significantly more detail on the Isabelle formalization and the unwinding proof process.\n                  <\/jats:p>","DOI":"10.1007\/s10817-025-09744-7","type":"journal-article","created":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:29:32Z","timestamp":1763458172000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Relative Security: (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities in Isabelle\/HOL"],"prefix":"10.1007","volume":"69","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[]},{"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[]},{"given":"Chelsea","family":"Edmonds","sequence":"additional","affiliation":[]},{"given":"Matt","family":"Griffin","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[]},{"given":"Jamie","family":"Wright","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,18]]},"reference":[{"key":"9744_CR1","unstructured":"Lipp, M., Schwarz, M., Gruss, D., Prescher, T., Haas, W., Fogh, A., Horn, J., Mangard, S., Kocher, P., Genkin, D., Yarom, Y., Hamburg, M.: Meltdown: Reading kernel memory from user space. In: USENIX Sec. (2018)"},{"key":"9744_CR2","doi-asserted-by":"publisher","unstructured":"Kocher, P., Horn, J., Fogh, A., Genkin, D., Gruss, D., Haas, W., Hamburg, M., Lipp, M., Mangard, S., Prescher, T., Schwarz, M., Yarom, Y.: Spectre attacks: Exploiting speculative execution. In: SP, pp. 1\u201319. IEEE, USA (2019). https:\/\/doi.org\/10.1109\/SP.2019.00002","DOI":"10.1109\/SP.2019.00002"},{"key":"9744_CR3","doi-asserted-by":"publisher","unstructured":"Cauligi, S., Disselkoen, C., Moghimi, D., Barthe, G., Stefan, D.: Sok: Practical foundations for software spectre defenses. In: SP, pp. 666\u2013680. IEEE, USA (2022). https:\/\/doi.org\/10.1109\/SP46214.2022.9833707","DOI":"10.1109\/SP46214.2022.9833707"},{"key":"9744_CR4","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: SP, pp. 75\u201387 (1984)","DOI":"10.1109\/SP.1984.10019"},{"key":"9744_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"9744_CR6","unstructured":"Popescu, A., Wright, J.: Relative security. Archive of Formal Proofs (2024). https:\/\/isa-afp.org\/entries\/Relative_Security.html, Formal proof development"},{"key":"9744_CR7","unstructured":"Dongol, B., Griffin, M., Popescu, A., Wright, J.: Secret-directed unwinding. Archive of Formal Proofs (2024). https:\/\/isa-afp.org\/entries\/Secret_Directed_Unwinding.html, Formal proof development"},{"key":"9744_CR8","unstructured":"Wright, J., Popescu, A.: A formalized programming language with speculative execution. Archive of Formal Proofs (2024). https:\/\/isa-afp.org\/entries\/IMP_With_Speculation.html, Formal proof development"},{"key":"9744_CR9","doi-asserted-by":"publisher","unstructured":"Dongol, B., Griffin, M., Popescu, A., Wright, J.: Relative security: Formally modeling and (dis)proving resilience against semantic optimization vulnerabilities. In: 2024 IEEE 37th Computer Security Foundations Symposium (CSF), pp. 403\u2013418. IEEE Computer Society, Los Alamitos, CA, USA (2024). https:\/\/doi.org\/10.1109\/CSF61375.2024.00027","DOI":"10.1109\/CSF61375.2024.00027"},{"key":"9744_CR10","unstructured":"Kocher, P.: Spectre Mitigations in Microsoft\u2019s C\/C++ Compiler. https:\/\/www.paulkocher.com\/doc\/MicrosoftCompilerSpectreMitigation.html (2018)"},{"key":"9744_CR11","doi-asserted-by":"crossref","unstructured":"Cheang, K., Rasmussen, C., Seshia, S.A., Subramanyan, P.: A formal approach to secure speculation. In: CSF, pp. 288\u2013303. IEEE, USA (2019)","DOI":"10.1109\/CSF.2019.00027"},{"issue":"6","key":"9744_CR12","first-page":"1157","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Com. Sec. 18(6), 1157\u20131210 (2010)","journal-title":"Hyperproperties. J. Com. Sec."},{"key":"9744_CR13","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Sel. Areas in Comm. 21(1), 5\u201319 (2003)","DOI":"10.1109\/JSAC.2002.806121"},{"key":"9744_CR14","doi-asserted-by":"crossref","unstructured":"Guarnieri, M., K\u00f6pf, B., Morales, J.F., Reineke, J., S\u00e1nchez, A.: Spectector: Principled detection of speculative information flows. In: SP, pp. 1\u201319. IEEE, USA (2020)","DOI":"10.1109\/SP40000.2020.00011"},{"key":"9744_CR15","doi-asserted-by":"publisher","unstructured":"Popescu, A., Bauereiss, T., Lammich, P.: Bounded-deducibility security (invited paper). In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). LIPIcs, vol. 193, pp. 3\u20131320. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2021.3","DOI":"10.4230\/LIPICS.ITP.2021.3"},{"key":"9744_CR16","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: SP, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"9744_CR17","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: IEEE CSF Workshop, pp. 29\u201343 (2003)","DOI":"10.1109\/CSFW.2003.1212703"},{"key":"9744_CR18","unstructured":"The Isabelle theorem prover. http:\/\/isabelle.in.tum.de\/ (2013)"},{"key":"9744_CR19","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales\u2014a sectioning concept for Isabelle. In: TPHOLs, pp. 149\u2013166 (1999)","DOI":"10.1007\/3-540-48256-3_11"},{"key":"9744_CR20","unstructured":"Ballarin, C.: Tutorial to Locales and Locale Interpretation. In: Contribuciones Cient\u00edficas en Honor de Mirian Andr\u00e9s G\u00f3mez, pp. 123\u2013140. University of Rioja, Spain (2010). Online at https:\/\/dialnet.unirioja.es\/servlet\/articulo?codigo=3216664"},{"issue":"2","key":"9744_CR21","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/S10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: A module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014). https:\/\/doi.org\/10.1007\/S10817-013-9284-7","journal-title":"J. Autom. Reason."},{"key":"9744_CR22","unstructured":"Lochbihler, A.: Coinductive. Archive of Formal Proofs (2010). http:\/\/afp.sourceforge.net\/entries\/Coinductive.shtml, Formal proof development"},{"key":"9744_CR23","unstructured":"Popescu, A., Wright, J.: More operations on lazy lists. Archive of Formal Proofs (2024). https:\/\/isa-afp.org\/entries\/More_LazyLists.html, Formal proof development"},{"issue":"5","key":"9744_CR24","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1017\/S0960129598002527","volume":"8","author":"D Sangiorgi","year":"1998","unstructured":"Sangiorgi, D.: On the bisimulation proof method. Math. Struc. Com. Sci. 8(5), 447\u2013479 (1998)","journal-title":"Math. Struc. Com. Sci."},{"key":"9744_CR25","unstructured":"Mantel, H.: A uniform framework for the formal specification and verification of information flow security. PhD thesis, University of Saarbr\u00fccken (2003)"},{"key":"9744_CR26","doi-asserted-by":"publisher","unstructured":"Mantel, H.: Unwinding possibilistic security properties. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) Computer Security - ESORICS 2000, 6th European Symposium on Research in Computer Security, Toulouse, France, October 4-6, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1895, pp. 238\u2013254. Springer, Berlin, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722599_15","DOI":"10.1007\/10722599_15"},{"key":"9744_CR27","doi-asserted-by":"publisher","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: I. untimed systems. Inf. Comput. 121(2), 214\u2013233 (1995) https:\/\/doi.org\/10.1006\/INCO.1995.1134","DOI":"10.1006\/INCO.1995.1134"},{"key":"9744_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, Switzerland (2014)"},{"key":"9744_CR29","unstructured":"Canella, C., Bulck, J.V., Schwarz, M., Lipp, M., Berg, B., Ortner, P., Piessens, F., Evtyushkin, D., Gruss, D.: A systematic evaluation of transient execution attacks and defenses. In: USENIX Sec., pp. 249\u2013266 (2019)"},{"key":"9744_CR30","doi-asserted-by":"crossref","unstructured":"Guanciale, R., Balliu, M., Dam, M.: Inspectre: Breaking and fixing microarchitectural vulnerabilities by formal analysis. In: CCS, pp. 1853\u20131869 (2020)","DOI":"10.1145\/3372297.3417246"},{"key":"9744_CR31","unstructured":"Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical report, SRI (Dec 1992). http:\/\/www.csl.sri.com\/papers\/csl-92-2\/"},{"key":"9744_CR32","doi-asserted-by":"publisher","unstructured":"Guarnieri, M., K\u00f6pf, B., Reineke, J., Vila, P.: Hardware-software contracts for secure speculation. In: SP, pp. 1868\u20131883 (2021). https:\/\/doi.org\/10.1109\/SP40001.2021.00036","DOI":"10.1109\/SP40001.2021.00036"},{"key":"9744_CR33","doi-asserted-by":"publisher","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Expressive declassification policies and modular static enforcement. In: 2008 IEEE Symposium on Security and Privacy (SP 2008), 18-21 May 2008, Oakland, California, USA, pp. 339\u2013353. IEEE Computer Society, USA (2008). https:\/\/doi.org\/10.1109\/SP.2008.20","DOI":"10.1109\/SP.2008.20"},{"issue":"5","key":"9744_CR34","doi-asserted-by":"publisher","first-page":"517","DOI":"10.3233\/JCS-2009-0352","volume":"17","author":"A Sabelfeld","year":"2009","unstructured":"Sabelfeld, A., Sands, D.: Declassification: Dimensions and principles. J. Comput. Secur. 17(5), 517\u2013548 (2009)","journal-title":"J. Comput. Secur."},{"key":"9744_CR35","doi-asserted-by":"publisher","unstructured":"Askarov, A., Myers, A.C.: A semantic framework for declassification and endorsement. In: Gordon, A.D. (ed.) Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6012, pp. 64\u201384. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_5","DOI":"10.1007\/978-3-642-11957-6_5"},{"key":"9744_CR36","doi-asserted-by":"crossref","unstructured":"Mantel, H., Reinhard, A.: Controlling the what and where of declassification in language-based security. In: Programming Languages and Systems. LNCS, vol. 4421, pp. 141\u2013156 (2007)","DOI":"10.1007\/978-3-540-71316-6_11"},{"key":"9744_CR37","doi-asserted-by":"publisher","unstructured":"Zdancewic, S., Myers, A.C.: Robust declassification. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada, pp. 15\u201323. IEEE Computer Society, USA (2001). https:\/\/doi.org\/10.1109\/CSFW.2001.930133","DOI":"10.1109\/CSFW.2001.930133"},{"issue":"2","key":"9744_CR38","doi-asserted-by":"publisher","first-page":"157","DOI":"10.3233\/JCS-2006-14203","volume":"14","author":"AC Myers","year":"2006","unstructured":"Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification and qualified robustness. J. Comput. Secur. 14(2), 157\u2013196 (2006). https:\/\/doi.org\/10.3233\/JCS-2006-14203","journal-title":"J. Comput. Secur."},{"key":"9744_CR39","doi-asserted-by":"crossref","unstructured":"Griffin, M., Dongol, B.: Isabelle files for \u201cVerifying Secure Speculation in Isabelle\/HOL\u201d. (2021). https:\/\/figshare.com\/s\/c185541c43a7cac258b6","DOI":"10.1007\/978-3-030-90870-6_3"},{"key":"9744_CR40","doi-asserted-by":"crossref","unstructured":"Amorim, A.A., Collins, N., DeHon, A., Demange, D., Hri\u0163cu, C., Pichardie, D., Pierce, B.C., Pollack, R., Tolmach, A.: A verified information-flow architecture. In: POPL, pp. 165\u2013178 (2014)","DOI":"10.1145\/2535838.2535839"},{"key":"9744_CR41","doi-asserted-by":"crossref","unstructured":"Dam, M., Guanciale, R., Khakpour, N., Nemati, H., Schwarz, O.: Formal verification of information flow security for a simple ARM-based separation kernel. In: CCS, pp. 223\u2013234 (2013)","DOI":"10.1145\/2508859.2516702"},{"key":"9744_CR42","doi-asserted-by":"crossref","unstructured":"Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: From general purpose to a proof of information flow enforcement. In: IEEE Symposium on Security and Privacy, pp. 415\u2013429 (2013)","DOI":"10.1109\/SP.2013.35"},{"key":"9744_CR43","doi-asserted-by":"crossref","unstructured":"Barthe, G., Nieto, L.P.: Formally verifying information flow type systems for concurrent and thread systems. In: FMSE, pp. 13\u201322 (2004)","DOI":"10.1145\/1029133.1029136"},{"issue":"1","key":"9744_CR44","doi-asserted-by":"publisher","first-page":"1","DOI":"10.6092\/issn.1972-5787\/3690","volume":"6","author":"A Popescu","year":"2013","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Formal verification of language-based concurrent noninterference. J. Formaliz. Reason. 6(1), 1\u201330 (2013). https:\/\/doi.org\/10.6092\/issn.1972-5787\/3690","journal-title":"J. Formaliz. Reason."},{"key":"9744_CR45","doi-asserted-by":"publisher","unstructured":"Murray, T., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp. 417\u2013431. IEEE, Lisbon (2016). https:\/\/doi.org\/10.1109\/CSF.2016.36 . https:\/\/ieeexplore.ieee.org\/document\/7536391\/ Accessed 2024-03-25","DOI":"10.1109\/CSF.2016.36"},{"key":"9744_CR46","doi-asserted-by":"publisher","unstructured":"Winter, K., Coughlin, N., Smith, G.: Backwards-directed information flow analysis for concurrent programs. In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF), pp. 1\u201316. IEEE, Dubrovnik, Croatia (2021). https:\/\/doi.org\/10.1109\/CSF51468.2021.00017 . https:\/\/ieeexplore.ieee.org\/document\/9505223\/ Accessed 2024-03-25","DOI":"10.1109\/CSF51468.2021.00017"},{"key":"9744_CR47","doi-asserted-by":"crossref","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: SP, pp. 79\u201393 (1994)","DOI":"10.1109\/RISP.1994.296590"},{"key":"9744_CR48","doi-asserted-by":"crossref","unstructured":"Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: CPP, pp. 126\u2013142 (2012)","DOI":"10.1007\/978-3-642-35308-6_12"},{"issue":"2","key":"9744_CR49","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/S10817-020-09566-9","volume":"65","author":"A Popescu","year":"2021","unstructured":"Popescu, A., Lammich, P., Hou, P.: CoCon: A conference management system with formally verified document confidentiality. J. Autom. Reason. 65(2), 321\u2013356 (2021). https:\/\/doi.org\/10.1007\/S10817-020-09566-9","journal-title":"J. Autom. Reason."},{"key":"9744_CR50","doi-asserted-by":"crossref","unstructured":"Volpano, D., Smith, G.: Probabilistic noninterference in a concurrent language. Journal of Computer Security 7(2,3), 231\u2013253 (1999)","DOI":"10.3233\/JCS-1999-72-305"},{"key":"9744_CR51","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: IEEE Computer Security Foundations Workshop, pp. 200\u2013214 (2000)","DOI":"10.1109\/CSFW.2000.856937"},{"issue":"1\u20132","key":"9744_CR52","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0304-3975(02)00010-5","volume":"281","author":"G Boudol","year":"2002","unstructured":"Boudol, G., Castellani, I.: Noninterference for concurrent programs and thread systems. Theor. Comp. Sci. 281(1\u20132), 109\u2013130 (2002)","journal-title":"Theor. Comp. Sci."},{"key":"9744_CR53","doi-asserted-by":"publisher","unstructured":"Shivakumar, B.A., Barthe, G., Gr\u00e9goire, B., Laporte, V., Oliveira, T., Priya, S., Schwabe, P., Tabary-Maujean, L.: Typing high-speed cryptography against spectre v1. In: SP, pp. 1094\u20131111. IEEE, USA (2023). https:\/\/doi.org\/10.1109\/SP46215.2023.10179418","DOI":"10.1109\/SP46215.2023.10179418"},{"key":"9744_CR54","doi-asserted-by":"publisher","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Proving concurrent noninterference. In: Hawblitzel, C., Miller, D. (eds.) Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7679, pp. 109\u2013125. Springer, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35308-6_11","DOI":"10.1007\/978-3-642-35308-6_11"},{"key":"9744_CR55","doi-asserted-by":"publisher","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Formalizing probabilistic noninterference. In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings. Lecture Notes in Computer Science, vol. 8307, pp. 259\u2013275. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_17","DOI":"10.1007\/978-3-319-03545-1_17"},{"key":"9744_CR56","doi-asserted-by":"publisher","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: FM. LNCS, vol. 6664, pp. 200\u2013214 (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17","DOI":"10.1007\/978-3-642-21437-0_17"},{"issue":"3","key":"9744_CR57","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1002\/STVR.1472","volume":"23","author":"B Godlin","year":"2013","unstructured":"Godlin, B., Strichman, O.: Regression verification: proving the equivalence of similar programs. Softw. Test. Verif. Reliab. 23(3), 241\u2013258 (2013). https:\/\/doi.org\/10.1002\/STVR.1472","journal-title":"Softw. Test. Verif. Reliab."},{"key":"9744_CR58","doi-asserted-by":"publisher","unstructured":"Hur, C., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: POPL, pp. 193\u2013206. ACM, USA (2013). https:\/\/doi.org\/10.1145\/2429069.2429093","DOI":"10.1145\/2429069.2429093"},{"issue":"8","key":"9744_CR59","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1016\/j.scico.2007.09.003","volume":"74","author":"C Morgan","year":"2009","unstructured":"Morgan, C.: The shadow knows: Refinement and security in sequential programs. Sci. Comput. Program. 74(8), 629\u2013653 (2009)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"9744_CR60","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/S00165-010-0167-Y","volume":"24","author":"C Morgan","year":"2012","unstructured":"Morgan, C.: Compositional noninterference from first principles. Form. Asp. Comput. 24(1), 3\u201326 (2012). https:\/\/doi.org\/10.1007\/S00165-010-0167-Y","journal-title":"Form. Asp. Comput."},{"key":"9744_CR61","volume-title":"Advanced Compiler Design and Implementation","author":"SS Muchnick","year":"1998","unstructured":"Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (1998)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09744-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09744-7","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09744-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:50:30Z","timestamp":1766134230000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09744-7"}},"subtitle":["Extended Version"],"short-title":[],"issued":{"date-parts":[[2025,11,18]]},"references-count":61,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["9744"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09744-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,11,18]]},"assertion":[{"value":"17 February 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 October 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 November 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"31"}}