SAT based verification of network data planes

Shuyuan Zhang; Sharad Malik

doi:10.1007/978-3-319-02444-8_43

SAT based verification of network data planes

Shuyuan Zhang, Sharad Malik

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

15 Scopus citations

Abstract

Formal verification has seen relatively less application in verifying computer networking infrastructure. This is in part due to the lack of clean layers of abstraction that enable design modeling and specification of correctness criteria. However, the recent move towards Software Defined Networking (SDN) provides a clean separation between a centralized control plane and a distributed data plane. This provides an opportunity to formally verify critical data plane properties. In this paper, we present a Boolean Satisfiability (SAT) based framework for data plane modeling and checking of key correctness criteria. This provides greater efficiency and/or greater coverage of properties when compared to other existing approaches.

Original language	English (US)
Title of host publication	Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings
Pages	496-505
Number of pages	10
DOIs	https://doi.org/10.1007/978-3-319-02444-8_43
State	Published - 2013
Event	11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013 - Hanoi, Viet Nam Duration: Oct 15 2013 → Oct 18 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8172 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013
Country/Territory	Viet Nam
City	Hanoi
Period	10/15/13 → 10/18/13

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-02444-8_43

Cite this

Zhang, S., & Malik, S. (2013). SAT based verification of network data planes. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings (pp. 496-505). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8172 LNAI). https://doi.org/10.1007/978-3-319-02444-8_43

@inproceedings{f47c36dad28249e7ae753b6027f60a56,

title = "SAT based verification of network data planes",

abstract = "Formal verification has seen relatively less application in verifying computer networking infrastructure. This is in part due to the lack of clean layers of abstraction that enable design modeling and specification of correctness criteria. However, the recent move towards Software Defined Networking (SDN) provides a clean separation between a centralized control plane and a distributed data plane. This provides an opportunity to formally verify critical data plane properties. In this paper, we present a Boolean Satisfiability (SAT) based framework for data plane modeling and checking of key correctness criteria. This provides greater efficiency and/or greater coverage of properties when compared to other existing approaches.",

author = "Shuyuan Zhang and Sharad Malik",

year = "2013",

doi = "10.1007/978-3-319-02444-8_43",

language = "English (US)",

isbn = "9783319024431",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "496--505",

booktitle = "Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings",

note = "11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013 ; Conference date: 15-10-2013 Through 18-10-2013",

}

Zhang, S & Malik, S 2013, SAT based verification of network data planes. in Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8172 LNAI, pp. 496-505, 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, Hanoi, Viet Nam, 10/15/13. https://doi.org/10.1007/978-3-319-02444-8_43

SAT based verification of network data planes. / Zhang, Shuyuan; Malik, Sharad.
Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings. 2013. p. 496-505 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8172 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - SAT based verification of network data planes

AU - Zhang, Shuyuan

AU - Malik, Sharad

PY - 2013

Y1 - 2013

N2 - Formal verification has seen relatively less application in verifying computer networking infrastructure. This is in part due to the lack of clean layers of abstraction that enable design modeling and specification of correctness criteria. However, the recent move towards Software Defined Networking (SDN) provides a clean separation between a centralized control plane and a distributed data plane. This provides an opportunity to formally verify critical data plane properties. In this paper, we present a Boolean Satisfiability (SAT) based framework for data plane modeling and checking of key correctness criteria. This provides greater efficiency and/or greater coverage of properties when compared to other existing approaches.

AB - Formal verification has seen relatively less application in verifying computer networking infrastructure. This is in part due to the lack of clean layers of abstraction that enable design modeling and specification of correctness criteria. However, the recent move towards Software Defined Networking (SDN) provides a clean separation between a centralized control plane and a distributed data plane. This provides an opportunity to formally verify critical data plane properties. In this paper, we present a Boolean Satisfiability (SAT) based framework for data plane modeling and checking of key correctness criteria. This provides greater efficiency and/or greater coverage of properties when compared to other existing approaches.

UR - http://www.scopus.com/inward/record.url?scp=84887492269&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84887492269&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-02444-8_43

DO - 10.1007/978-3-319-02444-8_43

M3 - Conference contribution

AN - SCOPUS:84887492269

SN - 9783319024431

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 496

EP - 505

BT - Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings

T2 - 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013

Y2 - 15 October 2013 through 18 October 2013

ER -

SAT based verification of network data planes

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this