{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:05:35Z","timestamp":1784797535421,"version":"3.55.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325365","type":"print"},{"value":"9783032325372","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Reference counting bugs in Linux kernel drivers can lead to severe resource mismanagement and security vulnerabilities. We introduce\n                    <jats:sc>DrvHorn<\/jats:sc>\n                    , a novel automated tool to detect these bugs by reducing reference counting verification to an assertion checking problem leveraging the Linux driver interface. Through efficient modeling of the Linux kernel and aggressive program slicing,\n                    <jats:sc>DrvHorn<\/jats:sc>\n                    discovered 545 bugs, of which 424 were previously unknown, across all platform drivers in v6.6 Linux kernel, with a lower false positive rate of 29.9% compared to prior studies. To address the root causes of these newly discovered bugs, we submitted patches to the Linux kernel, and 45 of them were merged.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32537-2_9","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:43:38Z","timestamp":1784796218000},"page":"191-203","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5177-8275","authenticated-orcid":false,"given":"Joe","family":"Hattori","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0537-0604","authenticated-orcid":false,"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3238-9279","authenticated-orcid":false,"given":"Ken","family":"Sakayori","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"9_CR1","unstructured":"Devicetree Kernel API. https:\/\/docs.kernel.org\/devicetree\/kernel-api.html"},{"key":"9_CR2","unstructured":"Linux and the Devicetree. https:\/\/docs.kernel.org\/devicetree\/usage-model.html"},{"key":"9_CR3","unstructured":"LLVM\u2019s Analysis and Transform Passes. https:\/\/llvm.org\/docs\/Passes.html"},{"key":"9_CR4","unstructured":"MITRE. CVE-2019-11487. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2019-11487"},{"key":"9_CR5","unstructured":"MITRE. CVE-2023-7192. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2023-7192"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Bai, S., Zhang, Z., Hu, H.: Countdown: refcount-guided fuzzing for exposing temporal memory errors in Linux kernel. In: Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, pp. 1315\u20131329 (2024)","DOI":"10.1145\/3658644.3690320"},{"issue":"4","key":"9_CR7","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/1218063.1217943","volume":"40","author":"T Ball","year":"2006","unstructured":"Ball, T., et al.: Thorough static analysis of device drivers. ACM SIGOPS Oper. Syst. Rev. 40(4), 73\u201385 (2006)","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"issue":"7","key":"9_CR8","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68\u201376 (2011)","journal-title":"Commun. ACM"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-00768-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Emmi","year":"2009","unstructured":"Emmi, M., Jhala, R., Kohler, E., Majumdar, R.: Verifying reference counting implementations. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 352\u2013367. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_30"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-66706-5_8","volume-title":"Static Analysis","author":"A Gurfinkel","year":"2017","unstructured":"Gurfinkel, A., Navas, J.A.: A context-sensitive memory model for verification of C\/C++ programs. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 148\u2013168. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_8"},{"key":"9_CR13","unstructured":"Hattori, J., Kobayashi, N., Sakayori, K.: Automatic detection of reference counting bugs in Linux kernel drivers. arXiv:2605.13246 (2026)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"TA Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235\u2013239. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44829-2_17"},{"issue":"1","key":"9_CR15","doi-asserted-by":"publisher","first-page":"14","DOI":"10.2307\/2268661","volume":"16","author":"A Horn","year":"1951","unstructured":"Horn, A.: On sentences which are true of direct unions of algebras1. J. Symbolic Logic 16(1), 14\u201321 (1951)","journal-title":"J. Symbolic Logic"},{"key":"9_CR16","unstructured":"Kroah-Hartman, G.: Kobjects and krefs. In: Linux Symposium, p.\u00a0295 (2004)"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: International Symposium on Code Generation and Optimization, 2004. CGO 2004, pp. 75\u201386. IEEE (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"9_CR18","unstructured":"Liu, J., Yi, L., Chen, W., Song, C., Qian, Z., Yi, Q.: LinKRID: vetting imbalance reference counting in Linux kernel with symbolic execution. In: 31st USENIX Security Symposium (USENIX Security 22), pp. 125\u2013142 (2022)"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Mao, J., Chen, Y., Xiao, Q., Shi, Y.: RID: finding reference count bugs with inconsistent path pair checking. In: Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 531\u2013544 (2016)","DOI":"10.1145\/2872362.2872389"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-70952-7_14","volume-title":"Formal Methods: Applications and Technology","author":"JT M\u00fchlberg","year":"2007","unstructured":"M\u00fchlberg, J.T., L\u00fcttgen, G.: Blasting Linux code. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds.) FMICS 2006. LNCS, vol. 4346, pp. 211\u2013226. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-70952-7_14"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-540-73210-5_27","volume-title":"Integrated Formal Methods","author":"H Post","year":"2007","unstructured":"Post, H., K\u00fcchlin, W.: Integrated static analysis for Linux device driver verification. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 518\u2013537. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73210-5_27"},{"issue":"2","key":"9_CR22","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1002\/stvr.399","volume":"19","author":"H Post","year":"2009","unstructured":"Post, H., Sinz, C., K\u00fcchlin, W.: Towards automatic software model checking of thousands of Linux modules\u2013A case study with Avinux. Softw. Test. Verification Reliab. 19(2), 155\u2013172 (2009)","journal-title":"Softw. Test. Verification Reliab."},{"key":"9_CR23","unstructured":"Priya, S., Su, Y., Bao, Y., Zhou, X., Vizel, Y., Gurfinkel, A.: Bounded model checking for LLVM. In: 2022 Formal Methods in Computer-Aided Design (FMCAD), pp. 214\u2013224. TU Wien Academic Press (2022)"},{"key":"9_CR24","unstructured":"Tan, X., Zhang, Y., Yang, X., Lu, K., Yang, M.: Detecting kernel refcount bugs with $$\\{$$two-dimensional$$\\}$$ consistency checking. In: 30th USENIX Security Symposium (USENIX Security 21), pp. 2471\u20132488 (2021)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32537-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:43:42Z","timestamp":1784796222000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32537-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325365","9783032325372"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32537-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"All authors declare that they have no competing interests.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}