A lightweight framework for regular expression verification

Xiao Liu; Yufei Jiang; Dinghao Wu

doi:10.1109/HASE.2019.00011

A lightweight framework for regular expression verification

Xiao Liu, Yufei Jiang, Dinghao Wu

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

8 Scopus citations

Abstract

Regular expressions and finite state automata have been widely used in programs for pattern searching and string matching. Unfortunately, despite the popularity, regular expressions are difficult to understand and verify even for experienced programmers. Conventional testing techniques remain a challenge as large regular expressions are constantly used for security purposes such as input validation and network intrusion detection. In this paper, we present a lightweight verification framework for regular expressions. In this framework, instead of a large number of test cases, it takes in requirements in natural language descriptions to automatically synthesize formal specifications. By checking the equivalence between the synthesized specifications and target regular expressions, errors will be detected and counterexamples will be reported. We have built a web application prototype and demonstrated its usability with two case studies.

Original language	English (US)
Title of host publication	Proceedings - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019
Editors	Vu Nguyen, Congfeng Jiang, Dongjin Yu
Publisher	IEEE Computer Society
Pages	1-8
Number of pages	8
ISBN (Electronic)	9781538685402
DOIs	https://doi.org/10.1109/HASE.2019.00011
State	Published - Mar 22 2019
Event	19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019 - Hangzhou, China Duration: Jan 3 2019 → Jan 5 2019

Publication series

Name	Proceedings of IEEE International Symposium on High Assurance Systems Engineering
Volume	2019-January
ISSN (Print)	1530-2059

Conference

Conference	19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019
Country/Territory	China
City	Hangzhou
Period	1/3/19 → 1/5/19

All Science Journal Classification (ASJC) codes

Software
Safety, Risk, Reliability and Quality

Access to Document

10.1109/HASE.2019.00011

Cite this

Liu, X., Jiang, Y., & Wu, D. (2019). A lightweight framework for regular expression verification. In V. Nguyen, C. Jiang, & D. Yu (Eds.), Proceedings - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019 (pp. 1-8). Article 8673038 (Proceedings of IEEE International Symposium on High Assurance Systems Engineering; Vol. 2019-January). IEEE Computer Society. https://doi.org/10.1109/HASE.2019.00011

Liu, Xiao ; Jiang, Yufei ; Wu, Dinghao. / A lightweight framework for regular expression verification. Proceedings - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019. editor / Vu Nguyen ; Congfeng Jiang ; Dongjin Yu. IEEE Computer Society, 2019. pp. 1-8 (Proceedings of IEEE International Symposium on High Assurance Systems Engineering).

@inproceedings{285f96881eb94bf5b3eee72aa579e1ce,

title = "A lightweight framework for regular expression verification",

abstract = "Regular expressions and finite state automata have been widely used in programs for pattern searching and string matching. Unfortunately, despite the popularity, regular expressions are difficult to understand and verify even for experienced programmers. Conventional testing techniques remain a challenge as large regular expressions are constantly used for security purposes such as input validation and network intrusion detection. In this paper, we present a lightweight verification framework for regular expressions. In this framework, instead of a large number of test cases, it takes in requirements in natural language descriptions to automatically synthesize formal specifications. By checking the equivalence between the synthesized specifications and target regular expressions, errors will be detected and counterexamples will be reported. We have built a web application prototype and demonstrated its usability with two case studies.",

author = "Xiao Liu and Yufei Jiang and Dinghao Wu",

note = "Publisher Copyright: {\textcopyright}2019 IEEE.; 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019 ; Conference date: 03-01-2019 Through 05-01-2019",

year = "2019",

month = mar,

day = "22",

doi = "10.1109/HASE.2019.00011",

language = "English (US)",

series = "Proceedings of IEEE International Symposium on High Assurance Systems Engineering",

publisher = "IEEE Computer Society",

pages = "1--8",

editor = "Vu Nguyen and Congfeng Jiang and Dongjin Yu",

booktitle = "Proceedings - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019",

address = "United States",

}

Liu, X, Jiang, Y & Wu, D 2019, A lightweight framework for regular expression verification. in V Nguyen, C Jiang & D Yu (eds), Proceedings - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019., 8673038, Proceedings of IEEE International Symposium on High Assurance Systems Engineering, vol. 2019-January, IEEE Computer Society, pp. 1-8, 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019, Hangzhou, China, 1/3/19. https://doi.org/10.1109/HASE.2019.00011

A lightweight framework for regular expression verification. / Liu, Xiao; Jiang, Yufei; Wu, Dinghao.
Proceedings - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019. ed. / Vu Nguyen; Congfeng Jiang; Dongjin Yu. IEEE Computer Society, 2019. p. 1-8 8673038 (Proceedings of IEEE International Symposium on High Assurance Systems Engineering; Vol. 2019-January).

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

TY - GEN

T1 - A lightweight framework for regular expression verification

AU - Liu, Xiao

AU - Jiang, Yufei

AU - Wu, Dinghao

PY - 2019/3/22

Y1 - 2019/3/22

N2 - Regular expressions and finite state automata have been widely used in programs for pattern searching and string matching. Unfortunately, despite the popularity, regular expressions are difficult to understand and verify even for experienced programmers. Conventional testing techniques remain a challenge as large regular expressions are constantly used for security purposes such as input validation and network intrusion detection. In this paper, we present a lightweight verification framework for regular expressions. In this framework, instead of a large number of test cases, it takes in requirements in natural language descriptions to automatically synthesize formal specifications. By checking the equivalence between the synthesized specifications and target regular expressions, errors will be detected and counterexamples will be reported. We have built a web application prototype and demonstrated its usability with two case studies.

AB - Regular expressions and finite state automata have been widely used in programs for pattern searching and string matching. Unfortunately, despite the popularity, regular expressions are difficult to understand and verify even for experienced programmers. Conventional testing techniques remain a challenge as large regular expressions are constantly used for security purposes such as input validation and network intrusion detection. In this paper, we present a lightweight verification framework for regular expressions. In this framework, instead of a large number of test cases, it takes in requirements in natural language descriptions to automatically synthesize formal specifications. By checking the equivalence between the synthesized specifications and target regular expressions, errors will be detected and counterexamples will be reported. We have built a web application prototype and demonstrated its usability with two case studies.

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

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

U2 - 10.1109/HASE.2019.00011

DO - 10.1109/HASE.2019.00011

M3 - Conference contribution

AN - SCOPUS:85064004332

T3 - Proceedings of IEEE International Symposium on High Assurance Systems Engineering

SP - 1

EP - 8

BT - Proceedings - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019

A2 - Nguyen, Vu

A2 - Jiang, Congfeng

A2 - Yu, Dongjin

PB - IEEE Computer Society

T2 - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019

Y2 - 3 January 2019 through 5 January 2019

ER -

Liu X, Jiang Y, Wu D. A lightweight framework for regular expression verification. In Nguyen V, Jiang C, Yu D, editors, Proceedings - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019. IEEE Computer Society. 2019. p. 1-8. 8673038. (Proceedings of IEEE International Symposium on High Assurance Systems Engineering). doi: 10.1109/HASE.2019.00011

A lightweight framework for regular expression verification

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this