{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T18:50:50Z","timestamp":1770749450024,"version":"3.50.0"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908996","type":"print"},{"value":"9783031909009","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"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>\n          <jats:p>Hypervisors allow sharing of computing resources between applications\u2014possibly of various levels of criticality\u2014that makes them increasingly relevant for modern embedded systems. In this context, memory isolation properties (including low-level cache isolation) are essential to guarantee. This paper presents a case study on formal verification of the cache coloring mechanism implemented in the Bao hypervisor. It proposes an original technique for coloring memory pages and assigning to each virtual machine only pages of certain colors, aimed to provide strong isolation guarantees. The implementation presents several challenges for formal verification, such as bit-level operations, complex arithmetic operations, multiple levels of nested loops, and linked lists. We identify two subtle bugs in the existing implementation breaking the expected guarantees, and propose bug fixes. We provide formal specification for the key functions of the mechanism and verify their (fixed) version in the  verification platform with a few lemmas proved in the  proof assistant. We present our specification choices, verification approach and obtained results. Finally, we outline possible optimizations of the current implementation.<\/jats:p>","DOI":"10.1007\/978-3-031-90900-9_11","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:44:37Z","timestamp":1745988277000},"page":"214-235","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Prove your Colorings: Formal Verification of Cache Coloring of Bao Hypervisor"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-5172-7823","authenticated-orcid":false,"given":"Axel","family":"Ferr\u00e9ol","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9089-288X","authenticated-orcid":false,"given":"Laurent","family":"Corbin","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1557-2813","authenticated-orcid":false,"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"11_CR1","unstructured":"Bao project, https:\/\/github.com\/bao-project\/bao-hypervisor"},{"key":"11_CR2","unstructured":"Jailhouse hypervisor, https:\/\/github.com\/siemens\/jailhouse"},{"key":"11_CR3","unstructured":"KVM hypervisor, https:\/\/linux-kvm.org\/page\/Main_Page"},{"key":"11_CR4","unstructured":"VmWare hypervisor, https:\/\/www.vmware.com"},{"key":"11_CR5","unstructured":"Xen Dom0-less hypervisor, https:\/\/xenproject.org\/2019\/12\/16\/true-static-partitioning-with-xen-dom0-less\/"},{"key":"11_CR6","unstructured":"Xen project, https:\/\/xenproject.org"},{"key":"11_CR7","unstructured":"XtratuM hypervisor, https:\/\/www.fentiss.com\/xtratum\/"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Armborst, L., Bos, P., van\u00a0den Haak, L.B., Huisman, M., Rubbens, R., Sakar, \u00d6., Tasche, P.: The VerCors verifier: A progress report. In: Proc. of the 36th International Conference on Computer Aided Verification (CAV 2024). LNCS, vol. 14682, pp. 3\u201318. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_1","DOI":"10.1007\/978-3-031-65630-9_1"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: Proc. of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022). LNCS, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Baudin, P., Bobot, F., B\u00a8uhler, D., Correnson, L., Kirchner, F., Kosmatov, N., Maroneze, A., Perrelle, V., Prevosto, V., Signoles, J., Williams, N.: 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","DOI":"10.1145\/3470569"},{"key":"11_CR11","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, http:\/\/frama-c.com\/acsl.html"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Beckert, B., Sanders, P., Ulbrich, M., Wiesler, J., Witt, S.: Formally verifying an efficient sorter. In: Proc. of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024). LNCS, vol. 14570, pp. 268\u2013287. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_15","DOI":"10.1007\/978-3-031-57246-3_15"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P. (eds.): Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S.: Z3 and SMT in industrial R &D. In: Proc. of the 22nd International Symposium on Formal Methods (FM 2018). LNCS, vol. 10951, pp. 675\u2013678. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_44","DOI":"10.1007\/978-3-319-95582-7_44"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Blanchard, A., Kosmatov, N., Loulergue, F.: Ghosts for lists: A critical module of Contiki verified in Frama-C. In: Proc. of the 10th NASA Formal Methods Symposium (NFM 2018). LNCS, vol. 10811, pp. 37\u201353. Springer (2018)","DOI":"10.1007\/978-3-319-77935-5_3"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Blanchard, A., Kosmatov, N., Loulergue, F.: Logic against ghosts: Comparison of two proof approaches for a list module. In: Proc. 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":"11_CR17","unstructured":"Bolignano, P.: Formal models and verification of memory management in a hypervisor. Ph.D. thesis, Universit\u00e9 de Rennes ; Prove & Run (May 2017), https:\/\/theses.hal.science\/tel-01637937"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Cassez, F., Fuller, J., Quiles, H.M.A.: Deductive verification of smart contracts with Dafny. In: Proc. of the 27th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2022). LNCS, vol. 13487, pp. 50\u201366. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-15008-1_5","DOI":"10.1007\/978-3-031-15008-1_5"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Cluzel, G., Georgiou, K., Moy, Y., Zeller, C.: Layered formal verification of a TCP stack. In: Proc. of the IEEE Secure Development Conference (SecDev 2021). pp. 86\u201393. IEEE (2021). https:\/\/doi.org\/10.1109\/SecDev51306.2021.00028","DOI":"10.1109\/SecDev51306.2021.00028"},{"key":"11_CR20","unstructured":"Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-Ergo 2.2. In: SMT Workshop: International Workshop on Satisfiability Modulo Theories (2018), https:\/\/hal.inria.fr\/hal-01960203"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Correnson, L., Blanchard, A., Djoudi, A., Kosmatov, N.: Automate where automation fails: Proof strategies for Frama-C\/WP. In: Proc. of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2024). LNCS, vol. 14570, pp. 331\u2013339. Springer (Apr 2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_18","DOI":"10.1007\/978-3-031-57246-3_18"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"de Boer, M., de Gouw, S., Klamroth, J., Jung, C., Ulbrich, M., Weigl, A.: Formal specification and verification of JDK\u2019s identity hash map implementation. Formal Aspects Comput. 35(3), 18:1\u201318:26 (2023). https:\/\/doi.org\/10.1145\/3594729","DOI":"10.1145\/3594729"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Djoudi, A., H\u00e1na, M., Kosmatov, N.: Formal Verification of a JavaCard Virtual Machine with Frama-C. In: Proc. of the 24th International Symposium on Formal Methods (FM 2021). LNCS, vol. 13047, pp. 427\u2013444. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_23","DOI":"10.1007\/978-3-030-90870-6_23"},{"key":"11_CR24","unstructured":"Djoudi, A., H\u00e1na, M., Kosmatov, N., K\u0159\u00ed\u017eeneck\u00fd, M., Ohayon, F., Mouy, P., Fontaine, A., F\u00e9liot, D.: A bottom-up formal verification approach for common criteria certification: Application to JavaCard virtual machine. In: Proc. of the 11th European Congress on Embedded Real-Time Systems (ERTS 2022) (Jun 2022)"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Dordowsky, F.: An experimental study using ACSL and Frama-C to formulate and verify low-level requirements from a DO-178C compliant avionics project. Electronic Proceedings in Theoretical Computer Science 187, 28\u201341 (2015). https:\/\/doi.org\/10.4204\/EPTCS.187.3","DOI":"10.4204\/EPTCS.187.3"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Dross, C., Moy, Y.: Auto-active proof of red-black trees in SPARK. In: Proc. of the 9th International Symposium on NASA Formal Methods (NFM 2017). LNCS, vol. 10227, pp. 68\u201383 (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_5","DOI":"10.1007\/978-3-319-57288-8_5"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Ferr\u00e9ol, A., Corbin, L., Kosmatov, N.: Prove your colorings: Formal verification of cache coloring of Bao hypervisor. Companion artifact for the paper submitted to FASE 2025 (2025). https:\/\/doi.org\/10.5281\/zenodo.14616331","DOI":"10.5281\/zenodo.14616331"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3 - where programs meet provers. In: Proc. of the 22nd European Symposium on Programming (ESOP 2013). LNCS, vol.\u00a07792, pp. 125\u2013128. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: From pen-and-paper proofs to industrial tools. In: Computing and Software Science \u2013 State of the Art and Perspectives, LNCS, vol. 10000, pp. 345\u2013373. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Proc. of the Third International Symposium on NASA Formal Methods (NFM 2011). LNCS, vol.\u00a06617, pp. 41\u201355. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"11_CR31","doi-asserted-by":"publisher","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","DOI":"10.1007\/s00165-014-0326-7"},{"key":"11_CR32","doi-asserted-by":"publisher","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: Proc. of the 22nd ACM Symposium on Operating Systems Principles (SOSP 2009). pp. 207\u2013220. ACM (2009). https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Kosmatov, N., Prevosto, V., Signoles, J. (eds.): Guide to Software Verification with Frama-C. Core Components, Usages, and Applications. Computer Science Foundations and Applied Logic Book Series, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-55608-1","DOI":"10.1007\/978-3-031-55608-1"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Leinenbach, D., Santen, T.: Verifying the microsoft Hyper-V hypervisor with VCC. In: Proc. of the Second World Congres on Formal Methods (FM 2009). LNCS, vol.\u00a05850, pp. 806\u2013809. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_51","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"11_CR35","unstructured":"Leino, K.R.M.: Program Proofs. The MIT Press (2023)"},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Loulergue, F., Blanchard, A., Kosmatov, N.: Ghosts for lists: from axiomatic to executable specifications. In: Proc. of the 12th International Conference on Tests and Proofs (TAP 2018). LNCS, vol. 10889, pp. 177\u2013184. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_11","DOI":"10.1007\/978-3-319-92994-1_11"},{"key":"11_CR37","doi-asserted-by":"publisher","unstructured":"Martins, J., Tavares, A., Solieri, M., Bertogna, M., Pinto, S.: Bao: A lightweight static partitioning hypervisor for modern multi-core embedded systems. In: Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2020). Open Access Series in Informatics (OASIcs), vol.\u00a077, pp. 3:1\u20133:14. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/OASIcs.NG-RES.2020.3","DOI":"10.4230\/OASIcs.NG-RES.2020.3"},{"key":"11_CR38","doi-asserted-by":"publisher","unstructured":"Oortwijn, W., Huisman, M.: Formal verification of an industrial safety-critical traffic tunnel control system. In: Proc. of the 15th International Conference on Integrated Formal Methods (IFM 2019). LNCS, vol. 11918, pp. 418\u2013436. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_23","DOI":"10.1007\/978-3-030-34968-4_23"},{"key":"11_CR39","doi-asserted-by":"publisher","unstructured":"Philippaerts, P., M\u00a8uhlberg, J., Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with VeriFast: Industrial case studies. Sci. Comput. Program. 82, 77\u201397 (2014). https:\/\/doi.org\/10.1016\/J.SCICO.2013.01.006","DOI":"10.1016\/J.SCICO.2013.01.006"},{"key":"11_CR40","unstructured":"The Coq Development Team: The Coq proof assistant. http:\/\/coq.inria.fr,"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90900-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:44:49Z","timestamp":1745988289000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90900-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908996","9783031909009"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90900-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}