{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:33:11Z","timestamp":1767929591873,"version":"3.49.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We consider the problem of how to verify\u00a0the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a number of complexities that feature in the semantics and invariants needed to verify the security of many practical probabilistic oblivious algorithms. We propose an approach based on reasoning over perfectly oblivious approximations, using a program logic that combines\u00a0both classical Hoare logic reasoning and probabilistic independence reasoning to support all the needed features. We formalise and prove our new\u00a0logic sound in Isabelle\/HOL and apply our approach\u00a0to formally verify the security\u00a0of several challenging case studies beyond the reach\u00a0of prior methods for proving obliviousness.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_10","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"188-205","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Combining Classical and\u00a0Probabilistic Independence Reasoning to\u00a0Verify the\u00a0Security of\u00a0Oblivious Algorithms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0396-8343","authenticated-orcid":false,"given":"Pengbo","family":"Yan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8271-0289","authenticated-orcid":false,"given":"Toby","family":"Murray","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9735-0538","authenticated-orcid":false,"given":"Olga","family":"Ohrimenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9871-3695","authenticated-orcid":false,"given":"Van-Thuan","family":"Pham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0313-9764","authenticated-orcid":false,"given":"Robert","family":"Sison","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"10_CR1","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: USENIX Security Symposium, vol.\u00a016, pp. 53\u201370 (2016)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Barthe, G., Hsu, J., Liao, K.: A probabilistic separation logic. Proc. ACM Program. Lang. 4(POPL), 1\u201330 (2019). https:\/\/doi.org\/10.1145\/3371123","DOI":"10.1145\/3371123"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Bittau, A., et al.: Prochlo: strong privacy for analytics in the crowd. In: Proceedings of the 26th Symposium on Operating Systems Principles (SOSP 2017), pp. 441\u2013459. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3132747.3132769","DOI":"10.1145\/3132747.3132769"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Cauligi, S., et al.: Fact: a DSL for timing-sensitive computation. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 174\u2013189 (2019)","DOI":"10.1145\/3314221.3314605"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Chan, T.H.H., Chung, K.M., Maggs, B., Shi, E.: Foundations of differentially oblivious algorithms. J. ACM 69(4), 1\u201349 (2022). https:\/\/doi.org\/10.1145\/3555984","DOI":"10.1145\/3555984"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Darais, D., Sweet, I., Liu, C., Hicks, M.: A language for probabilistically oblivious computation. Proc. ACM Program. Lang. 4(POPL), 1\u201331 (2019). https:\/\/doi.org\/10.1145\/3371118","DOI":"10.1145\/3371118"},{"key":"10_CR8","unstructured":"Fletcher, C.W., Ren, L., Kwon, A., van Dijk, M., Stefanov, E., Devadas, S.: RAW path ORAM: a low-latency, low-area hardware ORAM controller with integrity verification. IACR Cryptol. ePrint Arch. 431 (2014). http:\/\/eprint.iacr.org\/2014\/431"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Goldreich, O., Ostrovsky, R.: Software protection and simulation on oblivious rams. J. ACM 43(3), 431\u2013473 (1996). https:\/\/doi.org\/10.1145\/233551.233553","DOI":"10.1145\/233551.233553"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/978-3-642-22012-8_46","volume-title":"Automata, Languages and Programming","author":"MT Goodrich","year":"2011","unstructured":"Goodrich, M.T., Mitzenmacher, M.: Privacy-preserving access of outsourced data via oblivious RAM simulation. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 576\u2013587. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22012-8_46"},{"key":"10_CR11","unstructured":"Gruss, D., Spreitzer, R., Mangard, S.: Cache template attacks: automating attacks on inclusive last-level caches. In: 24th USENIX Security Symposium (USENIX Security 15), pp. 897\u2013912. USENIX Association, Washington, D.C. (2015). https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/gruss"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-46674-6_11","volume-title":"Advances in Computing Science \u2014 ASIAN\u201999","author":"JI Hartog","year":"1999","unstructured":"Hartog, J.I.: Verifying probabilistic programs using a hoare like logic. In: Thiagarajan, P.S., Yap, R. (eds.) ASIAN 1999. LNCS, vol. 1742, pp. 113\u2013125. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-46674-6_11"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Kushilevitz, E., Lu, S., Ostrovsky, R.: On the (in)security of hash-based oblivious ram and a new balancing scheme. In: Proceedings of the Twenty-Third Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2012), pp. 143\u2013156. Society for Industrial and Applied Mathematics (2012)","DOI":"10.1137\/1.9781611973099.13"},{"key":"10_CR14","unstructured":"Lago, U.D., Davoli, D., Kapron, B.M.: On separation logic, computational independence, and pseudorandomness (extended version) (2024). https:\/\/arxiv.org\/abs\/2405.11987"},{"key":"10_CR15","unstructured":"Lee, S., Shih, M.W., Gera, P., Kim, T., Kim, H., Peinado, M.: Inferring fine-grained control flow inside SGX enclaves with branch shadowing. In: 26th USENIX Security Symposium (USENIX Security 17), pp. 557\u2013574. USENIX Association, Vancouver (2017). https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/lee-sangho"},{"key":"10_CR16","unstructured":"Leung, H., Ringer, T., Fletcher, C.W.: Towards formally verified path Oram in COQ (2023). https:\/\/dependenttyp.es\/pdf\/oramproposal.pdf"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Li, J.M., Ahmed, A., Holtzen, S.: Lilac: a modal separation logic for conditional probability. Proc. ACM Program. Lang. 7(PLDI), 148\u2013171 (2023). https:\/\/doi.org\/10.1145\/3591226","DOI":"10.1145\/3591226"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Li, J.M., Aytac, J., Johnson-Freyd, P., Ahmed, A., Holtzen, S.: A nominal approach to probabilistic separation logic. In: Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2024). Association for Computing Machinery, New York (2024). https:\/\/doi.org\/10.1145\/3661814.3662135","DOI":"10.1145\/3661814.3662135"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Liu, C., Wang, X.S., Nayak, K., Huang, Y., Shi, E.: Oblivm: a programming framework for secure computation. In: 2015 IEEE Symposium on Security and Privacy, pp. 359\u2013376 (2015). https:\/\/doi.org\/10.1109\/SP.2015.29","DOI":"10.1109\/SP.2015.29"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Liu, F., Yarom, Y., Ge, Q., Heiser, G., Lee, R.B.: Last-level cache side-channel attacks are practical. In: 2015 IEEE Symposium on Security and Privacy, pp. 605\u2013622 (2015). https:\/\/doi.org\/10.1109\/SP.2015.43","DOI":"10.1109\/SP.2015.43"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Maas, M., et al.: Phantom: practical oblivious computation in a secure processor. In: Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security (CCS 2013), pp. 311\u2013324. Association for Computing Machinery, New York (2013). https:\/\/doi.org\/10.1145\/2508859.2516692","DOI":"10.1145\/2508859.2516692"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11734727_14","volume-title":"Information Security and Cryptology - ICISC 2005","author":"D Molnar","year":"2006","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: Won, D.H., Kim, S. (eds.) ICISC 2005. LNCS, vol. 3935, pp. 156\u2013168. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11734727_14"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Ohrimenko, O., Costa, M., Fournet, C., Gkantsidis, C., Kohlweiss, M., Sharma, D.: Observing and preventing leakage in mapreduce. In: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security (CCS 2015), pp. 1570\u20131581. Association for Computing Machinery, New York (2015). https:\/\/doi.org\/10.1145\/2810103.2813695","DOI":"10.1145\/2810103.2813695"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"556","DOI":"10.1007\/978-3-662-43951-7_47","volume-title":"Automata, Languages, and Programming","author":"O Ohrimenko","year":"2014","unstructured":"Ohrimenko, O., Goodrich, M.T., Tamassia, R., Upfal, E.: The Melbourne shuffle: improving oblivious storage in the cloud. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 556\u2013567. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43951-7_47"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Rand, R., Zdancewic, S.: VPHL: a verified partial-correctness logic for probabilistic programs. Electron. Notes Theor. Comput. Sci. 319, 351\u2013367 (2015). https:\/\/doi.org\/10.1016\/j.entcs.2015.12.021","DOI":"10.1016\/j.entcs.2015.12.021"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-030-53288-8_11","volume-title":"Computer Aided Verification","author":"S Sahai","year":"2020","unstructured":"Sahai, S., Subramanyan, P., Sinha, R.: Verification of quantitative hyperproperties using trace enumeration relations. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 201\u2013224. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_11"},{"key":"10_CR28","unstructured":"Sasy, S., Ohrimenko, O.: Oblivious sampling algorithms for private data analysis. In: Proceedings of the 33rd International Conference on Neural Information Processing Systems. Curran Associates Inc., Red Hook (2019)"},{"key":"10_CR29","doi-asserted-by":"publisher","unstructured":"Schr\u00f6er, P., Batz, K., Kaminski, B.L., Katoen, J.P., Matheja, C.: A deductive verification infrastructure for probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA2), 2052\u20132082 (2023). https:\/\/doi.org\/10.1145\/3622870","DOI":"10.1145\/3622870"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Shi, E.: Path oblivious heap: optimal and practical oblivious priority queue. Cryptology ePrint Archive, Paper 2019\/274 (2019). https:\/\/eprint.iacr.org\/2019\/274","DOI":"10.1109\/SP40000.2020.00037"},{"key":"10_CR31","unstructured":"Son, J., Prechter, G., Poddar, R., Popa, R.A., Sen, K.: ObliCheck: efficient verification of oblivious algorithms with unobservable state. In: 30th USENIX Security Symposium (USENIX Security 21), pp. 2219\u20132236. USENIX Association (2021). https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/son"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Stefanov, E., et al.: Path Oram: an extremely simple oblivious ram protocol. J. ACM 65(4), 1\u201326 (2018). https:\/\/doi.org\/10.1145\/3177872","DOI":"10.1145\/3177872"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Yan, P., Murray, T., Ohrimenko, O., Pham, V.T., Sison, R.: Combining classical and probabilistic independence reasoning to verify the security of oblivious algorithms (extended version). arXiv preprint arXiv:2407.00514 (2024)","DOI":"10.1007\/978-3-031-71162-6_10"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"Ye, Q., Delaware, B.: Oblivious algebraic data types. Proc. ACM Program. Lang. 6(POPL), 1\u201329 (2022). https:\/\/doi.org\/10.1145\/3498713","DOI":"10.1145\/3498713"},{"key":"10_CR35","unstructured":"Zheng, W., Dave, A., Beekman, J.G., Popa, R.A., Gonzalez, J.E., Stoica, I.: Opaque: an oblivious and encrypted distributed analytics platform. In: 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17), pp. 283\u2013298. USENIX Association, Boston (2017). https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/zheng"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T23:01:32Z","timestamp":1732748492000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}