{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:01:22Z","timestamp":1750309282936,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,9,22]],"date-time":"2023-09-22T00:00:00Z","timestamp":1695340800000},"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":[],"published-print":{"date-parts":[[2023,9,22]]},"DOI":"10.1145\/3641584.3641768","type":"proceedings-article","created":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T22:44:43Z","timestamp":1718405083000},"page":"1225-1230","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal verification of eBPF program security based on PTL"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-1406-0280","authenticated-orcid":false,"given":"Yang","family":"Chen","sequence":"first","affiliation":[{"name":"Xi'an University of Posts and Telecommunications, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7293-4510","authenticated-orcid":false,"given":"Xinfeng","family":"Shu","sequence":"additional","affiliation":[{"name":"Xi'an University of Posts and Telecommunications, China"}]}],"member":"320","published-online":{"date-parts":[[2024,6,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNSM.2021.3055676"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNSM.2022.3174138"},{"key":"e_1_3_2_1_3_1","volume-title":"Formal Verification of the Linux Kernel eBPF Verifier Range Analysis[J]","author":"Bhat S","year":"2022","unstructured":"Bhat S, Shacham H. Formal Verification of the Linux Kernel eBPF Verifier Range Analysis[J]. 2022."},{"key":"e_1_3_2_1_4_1","first-page":"37","article-title":"Decoupling policy decisions and execution[C]\/\/Proceedings of the 16th Workshop on Hot Topics","volume":"2017","author":"Amit N","unstructured":"Amit N, Wei M, Tu C C. Hypercallbacks: Decoupling policy decisions and execution[C]\/\/Proceedings of the 16th Workshop on Hot Topics in Operating Systems. 2017: 37-41.","journal-title":"Operating Systems."},{"key":"e_1_3_2_1_5_1","first-page":"1","volume":"2023","author":"Li\u00a0 H","unstructured":"Li\u00a0H,\u00a0Gu\u00a0JY,\u00a0Xia\u00a0YB,\u00a0Zang\u00a0BY,\u00a0Chen\u00a0HB.\u00a0Memory Isolation Mechanism of eBPF Based on PKS Hardware Feature[J]. Journal of Software, 2023: 1-19.","journal-title":"Journal of Software"},{"volume-title":"Simple and precise static analysis of untrusted linux kernel extensions[C]\/\/Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2019: 1069-1084","author":"Gershuni E","key":"e_1_3_2_1_6_1","unstructured":"Gershuni E, Amit N, Gurfinkel A, Simple and precise static analysis of untrusted linux kernel extensions[C]\/\/Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2019: 1069-1084."},{"issue":"10","key":"e_1_3_2_1_7_1","first-page":"29","article-title":"A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic[J]","volume":"44","author":"Chen DUAN","year":"2010","unstructured":"YANG Chen, DUAN Zhenhua. A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic[J]. Journal of Xi'an Jiaotong University, 2010, 44(10):29-34.","journal-title":"Journal of Xi'an Jiaotong University"},{"volume-title":"Sixth International Symposium on Theoretical Aspects of Software Engineering. IEEE","author":"Pang T","key":"e_1_3_2_1_8_1","unstructured":"Pang T, Duan Z, Tian C. Symbolic Model Checking for Propositional Projection Temporal Logic[C]. Sixth International Symposium on Theoretical Aspects of Software Engineering. IEEE, 2012: 9-16."},{"key":"e_1_3_2_1_9_1","volume-title":"Temporal logic and temporal logic programming","author":"Duan","year":"2005","unstructured":"Z. Duan, Temporal logic and temporal logic programming, Science Press, 2005."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.001"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1016\/j.tcs.2016.06.031","article-title":"Model checking of pushdown systems for projection temporal logic[J]","volume":"774","author":"Liang Zhao","year":"2019","unstructured":"Liang Zhao, Xiaobing Wang,Zhenhua Duan. Model checking of pushdown systems for projection temporal logic[J]. Theoretical Computer Science, 2019, 774: 82-94.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1016\/j.tcs.2017.09.026","article-title":"A decision procedure and complete axiomatization for projection temporal logic[J]","volume":"819","author":"Xinfeng Shu","year":"2020","unstructured":"Xinfeng Shu, Zhenhua Duan, Hongwei Du. A decision procedure and complete axiomatization for projection temporal logic[J]. Theor. Comput. Sci., 2020, 819: 50-84.","journal-title":"Theor. Comput. Sci."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2008.22"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","first-page":"544","DOI":"10.1016\/j.tcs.2015.08.039","article-title":"A canonical form based decision procedure and model checking approach for propositional projection temporal logic[J]","volume":"609","author":"Zhenhua Duan","year":"2016","unstructured":"Zhenhua Duan, Cong Tian, Nan Zhang. A canonical form based decision procedure and model checking approach for propositional projection temporal logic[J]. Theoretical Computer Science, 2016, Vol. 609: 544-560.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1016\/j.tcs.2019.12.038","article-title":"Translating Xd-C programs to MSVL programs[J]","volume":"809","author":"Meng Wang","year":"2020","unstructured":"Meng Wang, Cong Tian, Nan Zhang, Zhenhua Duan, Chenguang Yao. Translating Xd-C programs to MSVL programs[J]. Theoretical Computer Science, 2020, 809: 430-465.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_2_1_16_1","volume-title":"Extending MSVL with Semaphore[C]\/\/ International Computing and Combinatorics Conference","author":"Shu X","year":"2016","unstructured":"Shu X, Duan Z. Extending MSVL with Semaphore[C]\/\/ International Computing and Combinatorics Conference. Springer International Publishing, 2016:599-610."},{"key":"e_1_3_2_1_17_1","series-title":"Lecture Notes in Computer Science","volume-title":"Model Checking C Programs with MSVL[C]\/\/ Structured Object-Oriented Formal Language and Method","author":"Yu Y","year":"2013","unstructured":"Yu Y, Duan Z, Tian C, Model Checking C Programs with MSVL[C]\/\/ Structured Object-Oriented Formal Language and Method. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2013. 87-103."},{"issue":"1","key":"e_1_3_2_1_18_1","first-page":"75","article-title":"Automatic theorem proving technique for MSVL[J]","volume":"43","author":"Qian DUAN","year":"2016","unstructured":"MA Qian, DUAN Zhenhua. Automatic theorem proving technique for MSVL[J]. Journal of Xidian University, 2016, 43(1): 75-81.","journal-title":"Journal of Xidian University"}],"event":{"name":"AIPR 2023: 2023 6th International Conference on Artificial Intelligence and Pattern Recognition","acronym":"AIPR 2023","location":"Xiamen China"},"container-title":["2023 6th International Conference on Artificial Intelligence and Pattern Recognition (AIPR)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641584.3641768","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3641584.3641768","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:03:12Z","timestamp":1750291392000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641584.3641768"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,22]]},"references-count":18,"alternative-id":["10.1145\/3641584.3641768","10.1145\/3641584"],"URL":"https:\/\/doi.org\/10.1145\/3641584.3641768","relation":{},"subject":[],"published":{"date-parts":[[2023,9,22]]},"assertion":[{"value":"2024-06-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}