{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T14:30:06Z","timestamp":1770820206741,"version":"3.50.1"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"name":"SERICS","award":["PE00000014"],"award-info":[{"award-number":["PE00000014"]}]},{"name":"MUR National Recovery and Resilience Plan funded by the European Union - NextGenerationEU","award":["PRIN2022PNRR"],"award-info":[{"award-number":["PRIN2022PNRR"]}]},{"name":"\u201cRAP-ARA\u201d","award":["P2022HXNSC"],"award-info":[{"award-number":["P2022HXNSC"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Priv. Secur."],"published-print":{"date-parts":[[2026,2,28]]},"abstract":"<jats:p>\n                    In modern computing systems, preventing sensitive information leakage is a crucial issue. Indeed, to deploy secure computing systems, data protection is an aspect that cannot be ignored. Many security requirements are adopted in this respect, such as\n                    <jats:italic toggle=\"yes\">opacity<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">non-interference<\/jats:italic>\n                    . The first assures that the truth value of a predicate is masked during computation, while the second prevents confidential information is leaked through uncontrolled system components. Unfortunately, despite their simple intended meaning, confidentiality notions are quite difficult requirements to enforce. In fact, they are actually\n                    <jats:italic toggle=\"yes\">hyperproperties<\/jats:italic>\n                    , and thus require enforcing mechanisms that reason on multiple executions at a time.\n                  <\/jats:p>\n                  <jats:p>\n                    To develop effective verification and validation mechanisms for confidentiality notions, it is crucial to precisely characterize the requirements of system executions they dictate. In this article, we investigate the relation between\n                    <jats:italic toggle=\"yes\">abstract non-interference<\/jats:italic>\n                    (a weakening of non-interference observing properties of data instead of concrete values) and opacity through the lens of\n                    <jats:italic toggle=\"yes\">abstract interpretation<\/jats:italic>\n                    . By adopting such a holistic, abstract approach, we show how to formally characterize the\n                    <jats:italic toggle=\"yes\">structure<\/jats:italic>\n                    of confidentiality notions and to compare them in terms of the constraints on system executions they impose and verification complexity. In addition, we show how\n                    <jats:italic toggle=\"yes\">code obfuscation<\/jats:italic>\n                    can be restated as a confidentiality problem by defining a corresponding confidentiality notion that can possibly be enforced.\n                  <\/jats:p>\n                  <jats:p>\n                    Finally, by exploiting the recently proposed static analysis approach for verifying non-interference, based on\n                    <jats:italic toggle=\"yes\">hypersemantics<\/jats:italic>\n                    , we show how to verify abstract non-interference, therefore opacity and other security requirements. Based on\n                    <jats:italic toggle=\"yes\">abstract interpretation<\/jats:italic>\n                    , this yields an effective mechanism to enforce a broad range of confidentiality notions.\n                  <\/jats:p>","DOI":"10.1145\/3786347","type":"journal-article","created":{"date-parts":[[2025,12,26]],"date-time":"2025-12-26T11:43:16Z","timestamp":1766749396000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Abstract Interpretation-based Verification for Confidentiality: Information Hiding and Code Protection by Abstract Interpretation"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1213-536X","authenticated-orcid":false,"given":"Isabella","family":"Mastroeni","sequence":"first","affiliation":[{"name":"Dept. of Computer Science, University of Verona","place":["Verona, Italy"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9475-4836","authenticated-orcid":false,"given":"Michele","family":"Pasqua","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science, University of Verona","place":["Verona, Italy"]}]}],"member":"320","published-online":{"date-parts":[[2026,2,11]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"874","volume-title":"Proc. of POPL","author":"Assaf M.","year":"2017","unstructured":"M. Assaf, D. A. Naumann, J. Signoles, E. Totel, and F. Tronel. 2017. Hypercollecting semantics and its application to static analysis of information flow. In Proc. of POPL. 874\u2013887."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17499-5"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2023.111153"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.4018\/ijitwe.2015010101"},{"key":"e_1_3_2_6_2","first-page":"1","volume-title":"Symposium on Logic in Computer Science, LICS","author":"Bruni R.","year":"2021","unstructured":"R. Bruni, R. Giacobazzi, R. Gori, and F. Ranzato. 2021. A logic for locally complete abstract interpretations. In Symposium on Logic in Computer Science, LICS. IEEE, New York City, US, 1\u201313."},{"issue":"6","key":"e_1_3_2_7_2","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1007\/s10207-008-0058-x","article-title":"Opacity generalised to transition systems","volume":"7","author":"Bryans J. W.","year":"2008","unstructured":"J. W. Bryans, M. Koutny, L. Mazar\u00e9, and P. Y. A. Ryan. 2008. Opacity generalised to transition systems. Int. J. Inf. Sec. 7, 6 (2008), 421\u2013435.","journal-title":"Int. J. Inf. Sec."},{"issue":"6","key":"e_1_3_2_8_2","doi-asserted-by":"crossref","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","article-title":"Hyperproperties","volume":"18","author":"Clarkson M. R.","year":"2010","unstructured":"M. R. Clarkson and F. B. Schneider. 2010. Hyperproperties. Journal of Computer Security 18, 6 (2010), 1157\u20131210.","journal-title":"Journal of Computer Security"},{"issue":"5","key":"e_1_3_2_9_2","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1145\/1067625.806556","article-title":"Information transmission in computational systems","volume":"11","author":"Cohen E.","year":"1977","unstructured":"E. Cohen. 1977. Information transmission in computational systems. SIGOPS Oper. Syst. Rev. 11, 5 (1977), 133\u2013139.","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"e_1_3_2_10_2","volume-title":"Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection","author":"Collberg C.","year":"2009","unstructured":"C. Collberg and J. Nagra. 2009. Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection. Addison-Wesley Professional."},{"key":"e_1_3_2_11_2","volume-title":"A Taxonomy of Obfuscating Transformations","author":"Collberg C.","year":"1997","unstructured":"C. Collberg, C. Thomborson, and D. Low. 1997. A Taxonomy of Obfuscating Transformations. Technical Report 148. Department of Computer Sciences, The University of Auckland. Retrieved from http:\/\/www.cs.auckland.ac.nz\/collberg\/Research\/Publications\/CollbergThomborsonLow97a\/index.html"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689761"},{"key":"e_1_3_2_13_2","first-page":"238","volume-title":"Proc. of POPL","author":"Cousot P.","year":"1977","unstructured":"P. Cousot and R. Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of POPL. 238\u2013252."},{"key":"e_1_3_2_14_2","first-page":"269","volume-title":"Proc. of Conf. Record of the 6th ACM Symp. on Principles of Programming Languages (POPL\u201979)","author":"Cousot P.","year":"1979","unstructured":"P. Cousot and R. Cousot. 1979. Systematic design of program analysis frameworks. In Proc. of Conf. Record of the 6th ACM Symp. on Principles of Programming Languages (POPL\u201979). ACM Press, New York, 269\u2013282."},{"key":"e_1_3_2_15_2","first-page":"1325","volume-title":"Proc. of ICALP","author":"Preda M. Dalla","year":"2005","unstructured":"M. Dalla Preda and Roberto Giacobazzi. 2005. Semantic-based code obfuscation by abstract interpretation. In Proc. of ICALP. 1325\u20131336."},{"issue":"1","key":"e_1_3_2_16_2","doi-asserted-by":"crossref","first-page":"31","DOI":"10.3233\/JCS-14672","article-title":"Characterizing a property-driven obfuscation strategy","volume":"26","author":"Preda M. Dalla","year":"2018","unstructured":"M. Dalla Preda and I. Mastroeni. 2018. Characterizing a property-driven obfuscation strategy. J. Comput. Secur. 26, 1 (2018), 31\u201369.","journal-title":"J. Comput. Secur."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.15"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-014-0196-4"},{"key":"e_1_3_2_19_2","first-page":"7","volume-title":"Proc. of The 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM\u201908)","author":"Giacobazzi R.","year":"2008","unstructured":"R. Giacobazzi. 2008. Hiding information in completeness holes\u2014new perspectives in code obfuscation and watermarking. In Proc. of The 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM\u201908). IEEE Press, 7\u201320."},{"key":"e_1_3_2_20_2","first-page":"63","volume-title":"Proc. of the ACM SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM\u201912)","author":"Giacobazzi R.","year":"2012","unstructured":"R. Giacobazzi, N. D. Jones, and I. Mastroeni. 2012. Obfuscation by partial evaluation of distorted interpreters. In Proc. of the ACM SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM\u201912), O. Kiselyov and S. Thompson (Eds.). ACM Press, 63\u201372."},{"issue":"5","key":"e_1_3_2_21_2","doi-asserted-by":"crossref","first-page":"751","DOI":"10.3233\/JCS-2009-0382","article-title":"Adjoining classified and unclassified information by abstract interpretation","volume":"18","author":"Giacobazzi R.","year":"2010","unstructured":"R. Giacobazzi and I. Mastroeni. 2010. Adjoining classified and unclassified information by abstract interpretation. Journal of Computer Security 18, 5 (2010), 751\u2013797.","journal-title":"Journal of Computer Security"},{"issue":"2","key":"e_1_3_2_22_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3175660","article-title":"Abstract non-interference: A unifying framework for weakening information-flow","volume":"21","author":"Giacobazzi R.","year":"2018","unstructured":"R. Giacobazzi and I. Mastroeni. 2018. Abstract non-interference: A unifying framework for weakening information-flow. ACM Trans. Priv. Secur. 21, 2 (2018), 1\u201331.","journal-title":"ACM Trans. Priv. Secur."},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0374-2"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1297689.1297694"},{"key":"e_1_3_2_27_2","first-page":"171","volume-title":"Proc. of SAS","author":"Hunt S.","year":"2005","unstructured":"S. Hunt and I. Mastroeni. 2005. The PER model of abstract non-interference. In Proc. of SAS. 171\u2013185."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3720515"},{"key":"e_1_3_2_29_2","first-page":"55","volume-title":"Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE) (FormaliSE\u201924)","author":"Klein Julian","year":"2024","unstructured":"Julian Klein, Paul Kogel, and Sabine Glesner. 2024. Verifying opacity of discrete-timed automata. In Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE) (FormaliSE\u201924). Association for Computing Machinery, New York, NY, USA, 55\u201365. DOI:10.1145\/3644033.3644376"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2024.3516202"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1017\/S096012951100020X"},{"key":"e_1_3_2_32_2","first-page":"452","volume-title":"12th International Conference on Formal Engineering Methods, ICFEM 201 (Lecture Notes in Computer Science)","author":"Mastroeni I.","year":"2010","unstructured":"I. Mastroeni and D. Nikolic. 2010. An abstract unified framework for (abstract) program slicing. In 12th International Conference on Formal Engineering Methods, ICFEM 201 (Lecture Notes in Computer Science). Spinger-Verlag, 452\u2013467."},{"key":"e_1_3_2_33_2","first-page":"232","volume-title":"Proc. of SAS","author":"Mastroeni I.","year":"2017","unstructured":"I. Mastroeni and M. Pasqua. 2017. Hyperhierarchy of semantics - A formal framework for hyperproperties verification. In Proc. of SAS. 232\u2013252."},{"key":"e_1_3_2_34_2","first-page":"1","volume-title":"Proc. of SAS","author":"Mastroeni I.","year":"2018","unstructured":"I. Mastroeni and M. Pasqua. 2018. Verifying bounded subset-closed hyperproperties. In Proc. of SAS. 1\u201320."},{"key":"e_1_3_2_35_2","doi-asserted-by":"crossref","first-page":"2215","DOI":"10.1145\/3297280.3297498","volume-title":"Proceedings of the 34th ACM\/SIGAPP Symposium on Applied Computing, SAC 2019","author":"Mastroeni I.","year":"2019","unstructured":"I. Mastroeni and M. Pasqua. 2019. Statically analyzing information flows: An abstract interpretation-based hyperanalysis for non-interference. In Proceedings of the 34th ACM\/SIGAPP Symposium on Applied Computing, SAC 2019. 2215\u20132223. DOI:10.1145\/3297280.3297498"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477314.3507119"},{"key":"e_1_3_2_37_2","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/978-3-031-44245-2_19","volume-title":"Static Analysis","author":"Mastroeni I.","year":"2023","unstructured":"I. Mastroeni and M. Pasqua. 2023. Domain precision in galois connection-less abstract interpretation. In Static Analysis, Manuel V. Hermenegildo and Jos\u00e9 F. Morales (Eds.). Springer Nature Switzerland, Cham, 434\u2013459."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3029052"},{"key":"e_1_3_2_39_2","first-page":"18","volume-title":"Proc. of ESOP","author":"Ranzato F.","year":"2004","unstructured":"F. Ranzato and F. Tapparo. 2004. Strong preservation as completeness in abstract interpretation. In Proc. of ESOP. 18\u201332."},{"key":"e_1_3_2_40_2","unstructured":"P.Y.A. Ryan and T. Peacock. 2006. Opacity - Further Insights on an Information Flow Property. (2006). Technical Report CS-TR-958 University of Newcastle upon Tyne."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.3390\/math11183880"},{"key":"e_1_3_2_42_2","first-page":"539","volume-title":"Proc. of CSF","author":"Schoepe D.","year":"2015","unstructured":"D. Schoepe and A. Sabelfeld. 2015. Understanding and enforcing opacity. In Proc. of CSF. 539\u2013553."},{"key":"e_1_3_2_43_2","first-page":"5","volume-title":"Proceedings of the 14th IEEE Workshop on Computer Security Foundations (CSFW\u201901)","author":"Zdancewic S.","year":"2001","unstructured":"S. Zdancewic and A. C. Myers. 2001. Robust declassification. In Proceedings of the 14th IEEE Workshop on Computer Security Foundations (CSFW\u201901). IEEE Computer Society, USA, 5."}],"container-title":["ACM Transactions on Privacy and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3786347","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T13:58:23Z","timestamp":1770818303000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3786347"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,11]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,2,28]]}},"alternative-id":["10.1145\/3786347"],"URL":"https:\/\/doi.org\/10.1145\/3786347","relation":{},"ISSN":["2471-2566","2471-2574"],"issn-type":[{"value":"2471-2566","type":"print"},{"value":"2471-2574","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,11]]},"assertion":[{"value":"2025-04-22","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-12-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}