{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T14:22:50Z","timestamp":1761402170378,"version":"3.37.3"},"reference-count":43,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS-1740911"],"award-info":[{"award-number":["CNS-1740911"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Rede Nacional de Ensino e Pesquisa (RNP)\/Coordena\u00e7\u00e3o de Tecnologia da Informa\u00e7\u00e3o e Comunica\u00e7\u00e3o","award":["P4Sec"],"award-info":[{"award-number":["P4Sec"]}]},{"DOI":"10.13039\/501100003593","name":"Conselho Nacional de Desenvolvimento Cient\u00edfico e Tecnol\u00f3gico","doi-asserted-by":"publisher","award":["140317\/2017-1"],"award-info":[{"award-number":["140317\/2017-1"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002322","name":"Coordena\u00e7\u00e3o de Aperfei\u00e7oamento de Pessoal de N\u00edvel Superior (CAPES)\/Brazil","doi-asserted-by":"publisher","award":["001"],"award-info":[{"award-number":["001"]}],"id":[{"id":"10.13039\/501100002322","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE\/ACM Trans. Networking"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1109\/tnet.2021.3068339","type":"journal-article","created":{"date-parts":[[2021,4,1]],"date-time":"2021-04-01T19:37:34Z","timestamp":1617305854000},"page":"1540-1552","source":"Crossref","is-referenced-by-count":5,"title":["Dynamic Property Enforcement in Programmable Data Planes"],"prefix":"10.1109","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6586-2846","authenticated-orcid":false,"given":"Miguel","family":"Neves","sequence":"first","affiliation":[]},{"given":"Bradley","family":"Huffaker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4527-9749","authenticated-orcid":false,"given":"Kirill","family":"Levchenko","sequence":"additional","affiliation":[]},{"given":"Marinho","family":"Barcellos","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2018.00045"},{"key":"ref38","first-page":"467","article-title":"Stroboscope: Declarative network monitoring on a budget","author":"tilmans","year":"2018","journal-title":"Proc 15th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref33","article-title":"P4K: A formal semantics of P4 and applications","author":"kheradmand","year":"2018","journal-title":"arXiv 1804 01468"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"ref31","first-page":"241","article-title":"APKeep: Realtime verification for real networks","author":"zhang","year":"2020","journal-title":"Proc 17th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref30","first-page":"15","article-title":"Veriflow: Verifying network-wide invariants in real time","author":"khurshid","year":"2013","journal-title":"Proc 10th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098829"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3341216.3342206"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185497"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405888"},{"key":"ref10","first-page":"1","article-title":"Dynamic property enforcement in programmable data planes","author":"neves","year":"2019","journal-title":"Proc IFIP Netw Conf (IFIP Netw )"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/3373360.3380838"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098833"},{"key":"ref13","first-page":"209","article-title":"Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"Proc USENIX OSDI"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"ref15","first-page":"953","article-title":"Plankton: Scalable network configuration verification through model checking","author":"prabhu","year":"2020","journal-title":"Proc 17th Symp Netw Syst Design Implement (NSDI)"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2815675.2815692"},{"journal-title":"Simple Router","year":"2018","key":"ref17"},{"key":"ref18","article-title":"Concury: A fast and light-weighted software load balancer","author":"shi","year":"2019","journal-title":"arXiv 1908 01889"},{"key":"ref19","first-page":"19","article-title":"Offloading real-time DDoS attack detection to programmable data planes","author":"lapolli","year":"2019","journal-title":"Proc IFIP\/IEEE Symp Integr Netw Service Manage (IM)"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/3373360.3380831"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230548"},{"key":"ref27","first-page":"969","article-title":"Config2Spec: Mining network specifications from network configurations","author":"birkner","year":"2020","journal-title":"Proc 17th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref3","first-page":"35","article-title":"Netchain: Scale-free sub-RTT coordination","author":"jin","year":"2018","journal-title":"Proc 15th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"ref29","first-page":"201","article-title":"Tiramisu: Fast multilayer network verification","author":"abhashkumar","year":"2020","journal-title":"Proc 17th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281421"},{"article-title":"Automatically verifying reachability and well-formedness in P4 networks","year":"2016","author":"lopes","key":"ref8"},{"key":"ref7","first-page":"499","article-title":"Checking beliefs in dynamic networks","author":"lopes","year":"2015","journal-title":"Proc 12th Symp Netw Syst Design Implement (NSDI)"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132764"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053381"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"ref20","first-page":"1","article-title":"SPINE: Surveillance protection in the network elements","author":"datta","year":"2019","journal-title":"Proc USENIX Workshop Free Open Commun Internet (FOCI)"},{"journal-title":"The Joy of Micro-C","year":"2014","key":"ref22"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3286062.3286068"},{"article-title":"Computer security technology planning study","year":"1972","author":"anderson","key":"ref42"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3050220.3050234"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3373360.3380843"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/ANCS.2019.8901881"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3422604.3425941"},{"key":"ref43","first-page":"543","article-title":"Enforcing network-wide policies in the presence of dynamic middlebox actions using flowtags","author":"fayazbakhsh","year":"2014","journal-title":"Proc 11th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref25","first-page":"329","article-title":"Composing dataplane programs with $\\mu$\nP4","author":"soni","year":"2020","journal-title":"Proc Annu Conf ACM Special Interest Group Data Commun Appl Technol Archit Protocols Comput Commun"}],"container-title":["IEEE\/ACM Transactions on Networking"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielam\/90\/9515194\/9393490-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/90\/9515194\/09393490.pdf?arnumber=9393490","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T19:57:33Z","timestamp":1649188653000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9393490\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":43,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tnet.2021.3068339","relation":{},"ISSN":["1063-6692","1558-2566"],"issn-type":[{"type":"print","value":"1063-6692"},{"type":"electronic","value":"1558-2566"}],"subject":[],"published":{"date-parts":[[2021,8]]}}}