{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:22Z","timestamp":1750308562928,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,1,20]],"date-time":"2016-01-20T00:00:00Z","timestamp":1453248000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2016,1,20]]},"abstract":"<jats:p>Kernel probes allow code to be inserted into a running operating system kernel to gather information for debugging or profiling. Inserting code into the kernel raises a number of safety issues. Current solutions follow one of the two paths: a VM-based approach, where safety properties are checked dynamically by an interpreter, or a static-analysis approach, where probe code is guaranteed to be safe statically. While more attractive, existing static solutions depend on ad-hoc and error-prone analysis. We propose to explore enforcing safety properties using a type system, thus building our analysis on top of the well-studied ground of type theory.<\/jats:p>","DOI":"10.1145\/2883591.2883602","type":"journal-article","created":{"date-parts":[[2016,1,26]],"date-time":"2016-01-26T13:25:01Z","timestamp":1453814701000},"page":"51-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Tapir"],"prefix":"10.1145","volume":"49","author":[{"given":"Ilya","family":"Yanok","sequence":"first","affiliation":[{"name":"University of Lugano"}]},{"given":"Nathaniel","family":"Nystrom","sequence":"additional","affiliation":[{"name":"University of Lugano"}]}],"member":"320","published-online":{"date-parts":[[2016,1,20]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"The coq proof assistant reference manual: Version 6.1","author":"Barras Bruno","year":"1997","unstructured":"Bruno Barras , Samuel Boutin , Cristina Cornes , Judicael Courant , Jean-Christophe Filliatre , Eduardo Gimenez , Hugo Herbelin , Gerard Huet , Cesar Munoz , Chetan Murthy , The coq proof assistant reference manual: Version 6.1 . 1997 . Bruno Barras, Samuel Boutin, Cristina Cornes, Judicael Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The coq proof assistant reference manual: Version 6.1. 1997."},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1145\/202453.202472"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1007\/11964681_5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1145\/1254810.1254830"},{"key":"e_1_2_1_5_1","first-page":"15","volume-title":"Proceedings of the Annual Conference on USENIX Annual Technical Conference, ATEC '04","author":"Cantrill Bryan M.","year":"2004","unstructured":"Bryan M. Cantrill , Michael W. Shapiro , and Adam H. Leventhal . Dynamic instrumentation of production systems . In Proceedings of the Annual Conference on USENIX Annual Technical Conference, ATEC '04 , pages 15 -- 28 , Berkeley, CA, USA , 2004 . USENIX Association. Bryan M. Cantrill, Michael W. Shapiro, and Adam H. Leventhal. Dynamic instrumentation of production systems. In Proceedings of the Annual Conference on USENIX Annual Technical Conference, ATEC '04, pages 15--28, Berkeley, CA, USA, 2004. USENIX Association."},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/1275497.1275503"},{"key":"e_1_2_1_7_1","volume-title":"A formulation of the simple theory of types. The journal of symbolic logic, 5(02):56--68","author":"Church Alonzo","year":"1940","unstructured":"Alonzo Church . A formulation of the simple theory of types. The journal of symbolic logic, 5(02):56--68 , 1940 . Alonzo Church. A formulation of the simple theory of types. The journal of symbolic logic, 5(02):56--68, 1940."},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_1_9_1","first-page":"83","volume-title":"USENIX Security Symposium","author":"Criswell John","year":"2009","unstructured":"John Criswell , Nicolas Geoffray , and Vikram S Adve . Memory safety for low-level software\/hardware interactions . In USENIX Security Symposium , pages 83 -- 100 , 2009 . John Criswell, Nicolas Geoffray, and Vikram S Adve. Memory safety for low-level software\/hardware interactions. In USENIX Security Symposium, pages 83--100, 2009."},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1145\/1323293.1294295"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1145\/286942.286944"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1145\/1328897.1328457"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1145\/1111320.1111071"},{"key":"e_1_2_1_14_1","volume-title":"The inlined reference monitor approach to security policy enforcement","author":"Erlingsson Ulfar","year":"2003","unstructured":"Ulfar Erlingsson . The inlined reference monitor approach to security policy enforcement . 2003 . Ulfar Erlingsson. The inlined reference monitor approach to security policy enforcement. 2003."},{"key":"e_1_2_1_15_1","volume-title":"An overview of the Singularity Project1","author":"Hunt Galen","year":"2005","unstructured":"Galen Hunt , James Larus , Martin Abadi , Mark Aiken , Paul Barham , Manuel Fahndrich , Chris Hawblitzel , Orion Hodson , Steven Levi , Nick Murphy , An overview of the Singularity Project1 . 2005 . Galen Hunt, James Larus, Martin Abadi, Mark Aiken, Paul Barham, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Steven Levi, Nick Murphy, et al. An overview of the Singularity Project1. 2005."},{"key":"e_1_2_1_16_1","first-page":"47","volume-title":"Engineering theories of software construction","author":"Jones Simon P.","year":"2001","unstructured":"Simon P. Jones . Tackling the awkward squad: monadic input\/output, concurrency, exceptions, and foreign-language calls in Haskell . In Tony Hoare, Manfred Broy, and Ralf Steinbruggen, editors, Engineering theories of software construction , pages 47 -- 96 . IOS Press , 2001 . Simon P. Jones. Tackling the awkward squad: monadic input\/output, concurrency, exceptions, and foreign-language calls in Haskell. In Tony Hoare, Manfred Broy, and Ralf Steinbruggen, editors, Engineering theories of software construction, pages 47--96. IOS Press, 2001."},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.5555\/646158.680006"},{"key":"e_1_2_1_18_1","volume-title":"Linux Symposium","volume":"6","author":"Mavinakayanahalli Ananth","year":"2006","unstructured":"Ananth Mavinakayanahalli , Prasanna Panchamukhi , Jim Keniston , Anil Keshavamurthy , and Masami Hiramatsu . Probing the guts of kprobes . In Linux Symposium , volume 6 , 2006 . Ananth Mavinakayanahalli, Prasanna Panchamukhi, Jim Keniston, Anil Keshavamurthy, and Masami Hiramatsu. Probing the guts of kprobes. In Linux Symposium, volume 6, 2006."},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.5555\/646190.683552"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/565816.503286"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1145\/1411204.1411213"},{"key":"e_1_2_1_23_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C","year":"2002","unstructured":"Benjamin C Pierce . Types and programming languages . MIT press , 2002 . Benjamin C Pierce. Types and programming languages. MIT press, 2002."},{"key":"e_1_2_1_24_1","first-page":"49","volume-title":"2005 Ottawa Linux Symposium","author":"Prasad Vara","year":"2005","unstructured":"Vara Prasad , William Cohen , FC Eigler , Martin Hunt , Jim Keniston , and Brad Chen . Locating system problems using dynamic instrumentation . In 2005 Ottawa Linux Symposium , pages 49 -- 64 , 2005 . Vara Prasad, William Cohen, FC Eigler, Martin Hunt, Jim Keniston, and Brad Chen. Locating system problems using dynamic instrumentation. In 2005 Ottawa Linux Symposium, pages 49--64, 2005."},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.2307\/2271658"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1145\/173668.168635"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1145\/2034574.2034818"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1145\/2594291.2594341"}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2883591.2883602","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2883591.2883602","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:04:11Z","timestamp":1750273451000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2883591.2883602"}},"subtitle":["A Language for Verified OS Kernel Probes"],"short-title":[],"issued":{"date-parts":[[2016,1,20]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,1,20]]}},"alternative-id":["10.1145\/2883591.2883602"],"URL":"https:\/\/doi.org\/10.1145\/2883591.2883602","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2016,1,20]]},"assertion":[{"value":"2016-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}