{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/102486"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/102486","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"A formal semantics of P4 and applications","abstract":"Programmable packet processors and P4 as a programming language for such devices have gained significant interest, because their flexibility enables rapid development of a diverse set of applications that work at line rate. However, this flexibility, combined with the complexity of devices and networks, increases the chance of introducing subtle bugs that are hard to discover manually. Worse, this is a domain where bugs can have catastrophic consequences, yet formal analysis tools for P4 programs and networks are missing. We argue that formal analysis tools must be based on a formal semantics of the target language, rather than on its informal specification. To this end, we provide an executable formal semantics of the P4 language in the K framework. Based on this semantics, K provides an interpreter and various analysis tools including a symbolic model checker and a deductive program verifier. This thesis overviews our formal K semantics of P4, as well as several P4 language design issues that we found during our formalization process. We also discuss some applications resulting from the tools provided by K for P4 programmers and network administrators as well as language designers and compiler developers, such as detection of unportable code, state space exploration of P4 programs and networks, bug finding using symbolic execution, data plane verification, program verification, and translation validation.","abstract_html":"Programmable packet processors and P4 as a programming language for such devices have gained significant interest, because their flexibility enables rapid development of a diverse set of applications that work at line rate. However, this flexibility, combined with the complexity of devices and networks, increases the chance of introducing subtle bugs that are hard to discover manually. Worse, this is a domain where bugs can have catastrophic consequences, yet formal analysis tools for P4 programs and networks are missing. We argue that formal analysis tools must be based on a formal semantics of the target language, rather than on its informal specification. To this end, we provide an executable formal semantics of the P4 language in the K framework. Based on this semantics, K provides an interpreter and various analysis tools including a symbolic model checker and a deductive program verifier. This thesis overviews our formal K semantics of P4, as well as several P4 language design issues that we found during our formalization process. We also discuss some applications resulting from the tools provided by K for P4 programmers and network administrators as well as language designers and compiler developers, such as detection of unportable code, state space exploration of P4 programs and networks, bug finding using symbolic execution, data plane verification, program verification, and translation validation.","abstract_has_math":false,"creators":["Kheradmand, Ali"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Roşu, Grigore"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018-12-06","date_published":"2018-12-06","updated_at":"2026-07-22T22:24:42Z","subjects":["Formal Semantics, P4, K Framework, Network Verification"],"languages":["en"],"rights":["Copyright 2018 Ali Kheradmand"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/102486","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Roşu, Grigore"]},{"key":"dc:creator","label":"Author","values":["Kheradmand, Ali"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2018-12-06","2019-02-06T19:36:36Z","2018-12"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Formal Semantics, P4, K Framework, Network Verification"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2018 Ali Kheradmand"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/102486"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Programmable packet processors and P4 as a programming language for such devices have gained significant interest, because their flexibility enables rapid development of a diverse set of applications that work at line rate. However, this flexibility, combined with the complexity of devices and networks, increases the chance of introducing subtle bugs that are hard to discover manually. Worse, this is a domain where bugs can have catastrophic consequences, yet formal analysis tools for P4 programs and networks are missing. We argue that formal analysis tools must be based on a formal semantics of the target language, rather than on its informal specification. To this end, we provide an executable formal semantics of the P4 language in the K framework. Based on this semantics, K provides an interpreter and various analysis tools including a symbolic model checker and a deductive program verifier. This thesis overviews our formal K semantics of P4, as well as several P4 language design issues that we found during our formalization process. We also discuss some applications resulting from the tools provided by K for P4 programmers and network administrators as well as language designers and compiler developers, such as detection of unportable code, state space exploration of P4 programs and networks, bug finding using symbolic execution, data plane verification, program verification, and translation validation.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-02-05 without embargo terms","The student, Ali Kheradmand, accepted the attached license on 2018-12-05 at 17:21.","The student, Ali Kheradmand, submitted this Thesis for approval on 2018-12-05 at 17:22.","This Thesis was approved for publication on 2018-12-06 at 12:06.","DSpace SAF Submission Ingestion Package generated from Vireo submission #13226 on 2019-02-05 at 11:15:18","Made available in DSpace on 2019-02-06T19:36:36Z (GMT). No. of bitstreams: 2 KHERADMAND-THESIS-2018.pdf: 608259 bytes, checksum: b887b11602919d71d3ab5267ecaca243 (MD5) LICENSE.txt: 4211 bytes, checksum: a6d1c2cb8a18277ca37978344524aee1 (MD5) Previous issue date: 2018-12-06"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["A formal semantics of P4 and applications"]}]}],"canonical_facts":{"dc:contributor":["Roşu, Grigore"],"dc:creator":["Kheradmand, Ali"],"dc:date":["2018-12-06","2019-02-06T19:36:36Z","2018-12"],"dc:description":["Programmable packet processors and P4 as a programming language for such devices have gained significant interest, because their flexibility enables rapid development of a diverse set of applications that work at line rate. However, this flexibility, combined with the complexity of devices and networks, increases the chance of introducing subtle bugs that are hard to discover manually. Worse, this is a domain where bugs can have catastrophic consequences, yet formal analysis tools for P4 programs and networks are missing. We argue that formal analysis tools must be based on a formal semantics of the target language, rather than on its informal specification. To this end, we provide an executable formal semantics of the P4 language in the K framework. Based on this semantics, K provides an interpreter and various analysis tools including a symbolic model checker and a deductive program verifier. This thesis overviews our formal K semantics of P4, as well as several P4 language design issues that we found during our formalization process. We also discuss some applications resulting from the tools provided by K for P4 programmers and network administrators as well as language designers and compiler developers, such as detection of unportable code, state space exploration of P4 programs and networks, bug finding using symbolic execution, data plane verification, program verification, and translation validation.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-02-05 without embargo terms","The student, Ali Kheradmand, accepted the attached license on 2018-12-05 at 17:21.","The student, Ali Kheradmand, submitted this Thesis for approval on 2018-12-05 at 17:22.","This Thesis was approved for publication on 2018-12-06 at 12:06.","DSpace SAF Submission Ingestion Package generated from Vireo submission #13226 on 2019-02-05 at 11:15:18","Made available in DSpace on 2019-02-06T19:36:36Z (GMT). No. of bitstreams: 2 KHERADMAND-THESIS-2018.pdf: 608259 bytes, checksum: b887b11602919d71d3ab5267ecaca243 (MD5) LICENSE.txt: 4211 bytes, checksum: a6d1c2cb8a18277ca37978344524aee1 (MD5) Previous issue date: 2018-12-06"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/102486"],"dc:language":["en"],"dc:rights":["Copyright 2018 Ali Kheradmand"],"dc:subject":["Formal Semantics, P4, K Framework, Network Verification"],"dc:title":["A formal semantics of P4 and applications"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:42Z"}