{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,14]],"date-time":"2026-10-14T22:46:26Z","timestamp":1792017986546,"version":"4.4.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    A hyperproperty relates executions of a program and is used to formalize security objectives such as confidentiality, non-interference, privacy, and anonymity. Formally, a hyperproperty is a collection of allowable sets of executions. A program violates a hyperproperty if the set of its executions is not in the collection specified by the hyperproperty. The logic\n                    <jats:sc>HyperCTL*<\/jats:sc>\n                    has been proposed in the literature to formally specify and verify hyperproperties. The problem of checking whether a finite-state program satisfies a\n                    <jats:sc>HyperCTL*<\/jats:sc>\n                    formula is known to be decidable. However, the problem turns out to be undecidable for procedural (recursive) programs. Surprisingly, we show that decidability can be restored if we consider restricted classes of hyperproperties, namely those that relate only those executions of a program which have the same call-stack access pattern. We call such hyperproperties,\n                    <jats:italic>stack-aware hyperproperties.<\/jats:italic>\n                    Our decision procedure can be used as a proof method for establishing security objectives such as noninference for recursive programs, and also for refuting security objectives such as observational determinism. Further, if the call stack size is observable to the attacker, the decision procedure provides exact verification.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_16","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"308-325","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Stack-Aware Hyperproperties"],"prefix":"10.1007","author":[{"given":"Ali","family":"Bajwa","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Minjian","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rohit","family":"Chadha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the 36th Annual ACM Symposium on Theory of Computing. pp. 202\u2013211. ACM (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Bajwa, A., Zhang, M., Chadha, R., Viswanathan, M.: Stack-aware hyperproperties. https:\/\/arxiv.org\/abs\/2301.11521 (2023)","DOI":"10.1007\/978-3-031-30823-9_16"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Concurrency Theory, 8th International Conference. pp. 135\u2013150. Springer (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bozzelli, L.: Alternating automata and a temporal fixpoint calculus for visibly pushdown languages. In: Concurrency Theory, 18th International Conference. pp. 476\u2013491. Springer (2007)","DOI":"10.1007\/978-3-540-74407-8_32"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Principles of Security and Trust - Third International Conference. pp. 265\u2013284. Springer (2014)","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium. pp. 51\u201365. IEEE Computer Society (2008)","DOI":"10.1109\/CSF.2008.7"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: Computer Aided Verification - 31st International Conference. pp. 121\u2013139. Springer (2019)","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M.: EAHyper: Satisfiability, implication, and equivalence checking of hyperproperties. In: Computer Aided Verification - 29th International Conference. pp. 564\u2013570. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_29"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: RVHyper: A runtime verification tool for temporal hyperproperties. In: Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference. pp. 194\u2013200. Springer (2018)","DOI":"10.1007\/978-3-319-89963-3_11"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL*. In: Computer Aided Verification - 27th International Conference. pp. 30\u201348. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy. pp. 11\u201320. IEEE Computer Society (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"16_CR12","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Ohrem, C.: Deciding asynchronous hyperproperties for recursive programs. CoRR abs\/2201.12859 (2022)"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"McLean, J.: Proving noninterference and functional correctness using traces. Journal of Computer Security 1(1), 37\u201358 (1992)","DOI":"10.3233\/JCS-1992-1103"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: IEEE Computer Society Symposium on Research in Security and Privacy. pp. 79\u201393. IEEE Computer Society (1994)","DOI":"10.1109\/RISP.1994.296590"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Molnar, D., Piotrowski, M., Schultz, D., Wagner, D.: The program counter security model: Automatic detection and removal of control-flow side channel attacks. In: Proceedings of the 8th international conference on Information Security and Cryptology. p. 156\u2013168. Springer-Verlag (2005)","DOI":"10.1007\/11734727_14"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Pommellet, A., Touili, T.: Model-checking HyperLTL for pushdown systems. In: Model Checking Software - 25th International Symposium. pp. 133\u2013152. Springer (2018)","DOI":"10.1007\/978-3-319-94111-0_8"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for b\u00fcchi automata with appplications to temporal logic. Theoretical Computer Science 49, 217\u2013237 (1987)","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Walukiewicz, I.: Pushdown processes: Games and model checking. In: Computer Aided Verification, 8th International Conference. pp. 62\u201374. Springer (1996)","DOI":"10.1007\/3-540-61474-5_58"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings of the 16th IEEE Computer Security Foundations Workshop. p.\u00a029. IEEE Computer Society (2003)","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:04:22Z","timestamp":1781024662000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}