id:"swepub:oai:DiVA.org:uu-484748"
Search: id:"swepub:oai:DiVA.org:uu-484748" > Applying Symbolic E...
- 1 of 1
- Previous record
- Next record
- To hitlist
Applying Symbolic Execution to Test Implementations of a Network Protocol Against its Specification
-
- Asadian, Hooman (author)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
- Fiterau-Brostean, Paul (author)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
- Jonsson, Bengt, 1957- (author)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
- show more...
- show less...
- (creator_code:org_t)
- Institute of Electrical and Electronics Engineers (IEEE), 2022
- 2022
- English.
- In: 2022 IEEE 15TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST 2022). - : Institute of Electrical and Electronics Engineers (IEEE). - 9781665466790 - 9781665466806 ; , s. 70-81
- Conference paper (peer-reviewed)
Abstract
Subject headings
Close
- Implementations of network protocols must conform to their specifications in order to avoid security vulnerabilities and interoperability issues. We describe our experiences using symbolic execution to thoroughly test several implementations of a network security protocol against its specification. We employ a methodology in which we first extract requirements from the protocol's RFC and turn them into formulas. These formulas are then utilized by symbolically executing the protocol implementation to explore code paths that can be traversed on packet sequences that violate a requirement. When this exploration exposes a bug, corresponding input values are produced and turned into test cases that can validate the bug in the original implementation. Since we let symbolic execution be guided by requirements, it can naturally produce a wide variety of requirement-violating input sequences, which is difficult to achieve with existing techniques for protocol testing. We applied this methodology to test four different implementations of MILS against the protocol's RFC. We were able to quickly expose a known CVE in an older version of OpenSSL, and to discover numerous previously unknown vulnerabilities and nonconformance issues in DTI.S implementations, which have by now been confirmed and fixed by their implementors.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Software Engineering (hsv//eng)
Keyword
- symbolic execution
- network security testing
Publication and Content Type
- ref (subject category)
- kon (subject category)
Find in a library
- 2022 IEEE 15TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VA... (Search for host publication in LIBRIS)
To the university's database
- 1 of 1
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Asadian, Hooman
- Fiterau-Brostean ...
- Jonsson, Bengt, ...
- Sagonas, Konstan ...
- About the subject
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- and Software Enginee ...
- Articles in the publication
- 2022 IEEE 15TH I ...
- By the university
- Uppsala University
Search outside SwePub
- Extend your search to:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - National Library Systems
- LIBRIS.kb.se
