{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T09:38:33Z","timestamp":1766050713152,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031720437"},{"type":"electronic","value":"9783031720444"}],"license":[{"start":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:00:00Z","timestamp":1725926400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:00:00Z","timestamp":1725926400000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-72044-4_5","type":"book-chapter","created":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:02:41Z","timestamp":1725897761000},"page":"87-106","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Runtime Verification for\u00a0High-Level Security Properties: Case Study on\u00a0the\u00a0TPM Software Stack"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-8540-1273","authenticated-orcid":false,"given":"Yani","family":"Ziani","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1557-2813","authenticated-orcid":false,"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9301-7829","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Loulergue","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5364-8244","authenticated-orcid":false,"given":"Daniel","family":"Gracia P\u00e9rez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,10]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Arthur, W., Challener, D.: A Practical Guide to TPM 2.0: Using the Trusted Platform Module in the New Age of Security, 1st edn. Apress, USA (2015)","DOI":"10.1007\/978-1-4302-6584-9_1"},{"issue":"8","key":"5_CR2","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/3470569","volume":"64","author":"P Baudin","year":"2021","unstructured":"Baudin, P., et al.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64(8), 56\u201368 (2021). https:\/\/doi.org\/10.1145\/3470569","journal-title":"Commun. ACM"},{"key":"5_CR3","unstructured":"Baudin, P., et al.: ACSL: ANSI\/ISO C specification language. http:\/\/frama-c.com\/acsl.html"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Blanchard, A., Kosmatov, N., Loulergue, F.: Logic against ghosts: comparison of two proof approaches for a list module. In: Proceedings of the 34th Annual ACM\/SIGAPP Symposium on Applied Computing, Software Verification and Testing Track (SAC-SVT 2019), pp. 2186\u20132195. ACM (2019). https:\/\/doi.org\/10.1145\/3297280.3297495","DOI":"10.1145\/3297280.3297495"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-52234-0_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Blazy","year":"2017","unstructured":"Blazy, S., B\u00fchler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 112\u2013130. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_7"},{"key":"5_CR6","unstructured":"Burghardt, J., Gerlach, J., Lapawczyk, T.: ACSL by example (2016). http:\/\/www.fokus.fraunhofer.de\/download\/acsl_by_example"},{"issue":"3","key":"5_CR7","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/1127878.1127900","volume":"31","author":"LA Clarke","year":"2006","unstructured":"Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. SIGSOFT Softw. Eng. Notes 31(3), 25\u201337 (2006). https:\/\/doi.org\/10.1145\/1127878.1127900","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-030-90870-6_23","volume-title":"Formal Methods","author":"A Djoudi","year":"2021","unstructured":"Djoudi, A., H\u00e1na, M., Kosmatov, N.: Formal verification of a JavaCard virtual machine with Frama-C. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 427\u2013444. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_23"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"5_CR10","unstructured":"Herrmann, P., Signoles, J.: RTE: runtime error annotation generation (2024). https:\/\/frama-c.com\/download\/frama-c-rte-manual.pdf"},{"issue":"3","key":"5_CR11","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573\u2013609 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0326-7","journal-title":"Formal Asp. Comput."},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-40787-1_29","volume-title":"Runtime Verification","author":"N Kosmatov","year":"2013","unstructured":"Kosmatov, N., Signoles, J.: A lesson on runtime assertion checking with Frama-C. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 386\u2013399. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_29"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-319-92994-1_11","volume-title":"Tests and Proofs","author":"F Loulergue","year":"2018","unstructured":"Loulergue, F., Blanchard, A., Kosmatov, N.: Ghosts for lists: from axiomatic to executable specifications. In: Dubois, C., Wolff, B. (eds.) TAP 2018. LNCS, vol. 10889, pp. 177\u2013184. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_11"},{"key":"5_CR14","unstructured":"Pariente, D., Signoles, J.: Static analysis and runtime assertion checking: contribution to security counter-measures. In: Symposium sur la S\u00e9curit\u00e9 des Technologies de l\u2019Information et des Communications (SSTIC) (2017)"},{"key":"5_CR15","unstructured":"Rao, S.P., Limonta, G., Lindqvist, J.: Usability and security of trusted platform module (TPM) library APIs. In: Chiasson, S., Kapadia, A. (eds.) Eighteenth Symposium on Usable Privacy and Security, SOUPS 2022, Boston, MA, USA, 7\u20139 August 2022, pp. 213\u2013232. USENIX Association (2022). https:\/\/www.usenix.org\/conference\/soups2022\/presentation\/rao"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-030-17462-0_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Robles","year":"2019","unstructured":"Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Le Gall, P.: MetAcsl: specification and verification of high-level properties. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 358\u2013364. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_22"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-030-31157-5_11","volume-title":"Tests and Proofs","author":"V Robles","year":"2019","unstructured":"Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Le Gall, P.: Tame your annotations with MetAcsl: specifying, testing and proving high-level properties. In: Beyer, D., Keller, C. (eds.) TAP 2019. LNCS, vol. 11823, pp. 167\u2013185. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31157-5_11"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Le\u00a0Gall, P.: Methodology for specification and verification of high-level properties with MetAcsl. In: 9th IEEE\/ACM International Conference on Formal Methods in Software Engineering (FormaliSE 2021), pp. 54\u201367. IEEE (2021). https:\/\/doi.org\/10.1109\/FormaliSE52586.2021.00012","DOI":"10.1109\/FormaliSE52586.2021.00012"},{"issue":"2","key":"5_CR19","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1049\/iet-ifs.2016.0005","volume":"12","author":"J Shao","year":"2018","unstructured":"Shao, J., Qin, Y., Feng, D.: Formal analysis of HMAC authorisation in the TPM2.0 specification. IET Inf. Secur. 12(2), 133\u2013140 (2018). https:\/\/doi.org\/10.1049\/iet-ifs.2016.0005","journal-title":"IET Inf. Secur."},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Signoles, J.: The E-ACSL perspective on runtime assertion checking. In: ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX), pp. 8\u201312. ACM, New York (2021). https:\/\/doi.org\/10.1145\/3464974.3468451","DOI":"10.1145\/3464974.3468451"},{"key":"5_CR21","unstructured":"Trusted Computing Group: Trusted Platform Module Library Specification, Family \u201c2.0\u201d, Level 00, Revision 01.59 (2019). https:\/\/trustedcomputinggroup.org\/work-groups\/trusted-platform-module\/. Accessed May 2023"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-319-50011-9_33","volume-title":"Information and Communications Security","author":"W Wang","year":"2016","unstructured":"Wang, W., Qin, Yu., Yang, B., Zhang, Y., Feng, D.: Automated security proof of cryptographic support commands in TPM 2.0. In: Lam, K.-Y., Chi, C.-H., Qing, S. (eds.) ICICS 2016. LNCS, vol. 9977, pp. 431\u2013441. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-50011-9_33"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Zhang, Q., Zhao, S.: A comprehensive formal security analysis and revision of the two-phase key exchange primitive of TPM 2.0. Comput. Netw. 179 (2020). https:\/\/doi.org\/10.1016\/j.comnet.2020.107369","DOI":"10.1016\/j.comnet.2020.107369"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-031-47705-8_6","volume-title":"Integrated Formal Methods","author":"Y Ziani","year":"2023","unstructured":"Ziani, Y., Kosmatov, N., Loulergue, F., P\u00e9rez, D.G., Bernier, T.: Towards formal verification of a TPM software stack. In: Herber, P., Wijs, A. (eds.) iFM 2023. LNCS, vol. 14300, pp. 93\u2013112. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47705-8_6"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-72044-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:05:31Z","timestamp":1725897931000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-72044-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,10]]},"ISBN":["9783031720437","9783031720444"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-72044-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,10]]},"assertion":[{"value":"10 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tests and Proofs","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":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tap2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}