Abstract
The Trusted Platform Module (TPM) is a cryptoprocessor designed to provide hardware-based secure storage and protect integrity of modern computers. Communications with the TPM go through the TPM Software Stack (TSS), a popular implementation of which is the open-source library tpm2-tss. It is thus crucial to ensure that no leak of sensitive data may occur in the TSS during communications between the host platform and the TPM. Recent work on deductive verification of functional and safety properties for this library faced several challenges. The purpose of this case study paper is to focus on high-level security properties, and to propose an alternative validation approach for such properties on the library by using runtime verification. We describe the proposed approach, apply it to specify and verify at runtime some key security properties using the Frama-C verification platform and report on our first evaluation results.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Available (with all necessary annotations) on https://doi.org/10.5281/zenodo.12773113.
- 2.
- 3.
- 4.
Like CVE-2023-22745 and CVE-2020-24455, documented on www.cve.org.
- 5.
For simplicity, when an element is removed, we do not shift the following array elements to the left. This feature can be easily added and particularly useful for long-running programs, where pieces of sensitive data are frequently added and removed.
References
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)
Baudin, P., et al.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64(8), 56–68 (2021). https://doi.org/10.1145/3470569
Baudin, P., et al.: ACSL: ANSI/ISO C specification language. http://frama-c.com/acsl.html
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–2195. ACM (2019). https://doi.org/10.1145/3297280.3297495
Blazy, S., Bühler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 112–130. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52234-0_7
Burghardt, J., Gerlach, J., Lapawczyk, T.: ACSL by example (2016). http://www.fokus.fraunhofer.de/download/acsl_by_example
Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. SIGSOFT Softw. Eng. Notes 31(3), 25–37 (2006). https://doi.org/10.1145/1127878.1127900
Djoudi, A., Hána, M., Kosmatov, N.: Formal verification of a JavaCard virtual machine with Frama-C. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 427–444. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-90870-6_23
Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8
Herrmann, P., Signoles, J.: RTE: runtime error annotation generation (2024). https://frama-c.com/download/frama-c-rte-manual.pdf
Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573–609 (2015). https://doi.org/10.1007/s00165-014-0326-7
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–399. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40787-1_29
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–184. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92994-1_11
Pariente, D., Signoles, J.: Static analysis and runtime assertion checking: contribution to security counter-measures. In: Symposium sur la Sécurité des Technologies de l’Information et des Communications (SSTIC) (2017)
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–9 August 2022, pp. 213–232. USENIX Association (2022). https://www.usenix.org/conference/soups2022/presentation/rao
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–364. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_22
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–185. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31157-5_11
Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Le Gall, 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–67. IEEE (2021). https://doi.org/10.1109/FormaliSE52586.2021.00012
Shao, J., Qin, Y., Feng, D.: Formal analysis of HMAC authorisation in the TPM2.0 specification. IET Inf. Secur. 12(2), 133–140 (2018). https://doi.org/10.1049/iet-ifs.2016.0005
Signoles, J.: The E-ACSL perspective on runtime assertion checking. In: ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX), pp. 8–12. ACM, New York (2021). https://doi.org/10.1145/3464974.3468451
Trusted Computing Group: Trusted Platform Module Library Specification, Family “2.0”, Level 00, Revision 01.59 (2019). https://trustedcomputinggroup.org/work-groups/trusted-platform-module/. Accessed May 2023
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–441. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-50011-9_33
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
Ziani, Y., Kosmatov, N., Loulergue, F., Pérez, 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–112. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-47705-8_6
Acknowledgment
Part of this work was supported by ANR (grants ANR-22-CE39-0014, ANR-22-CE25-0018) and French Ministry of Defense (PhD grant of Yani Ziani). We thank the anonymous referees for many helpful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Ziani, Y., Kosmatov, N., Loulergue, F., Gracia Pérez, D. (2025). Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack. In: Huisman, M., Howar, F. (eds) Tests and Proofs. TAP 2024. Lecture Notes in Computer Science, vol 15153. Springer, Cham. https://doi.org/10.1007/978-3-031-72044-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-031-72044-4_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-72043-7
Online ISBN: 978-3-031-72044-4
eBook Packages: Computer ScienceComputer Science (R0)