File Download

There are no files associated with this item.

  Links for fulltext
     (May Require Subscription)
Supplementary

Conference Paper: Verifying systems rules using rule-directed symbolic execution

TitleVerifying systems rules using rule-directed symbolic execution
Authors
KeywordsPath Slicing
Error Detection
Verification
Systems Rules
Symbolic execution
Issue Date2013
Citation
ACM SIGPLAN Notices, 2013, v. 48, n. 4, p. 329-341 How to Cite?
AbstractSystems code must obey many rules, such as "opened files must be closed." One approach to verifying rules is static analysis, but this technique cannot infer precise runtime effects of code, often emitting many false positives. An alternative is symbolic execution, a technique that verifies program paths over all inputs up to a bounded size. However, when applied to verify rules, existing symbolic execution systems often blindly explore many redundant program paths while missing relevant ones that may contain bugs. Our key insight is that only a small portion of paths are relevant to rules, and the rest (majority) of paths are irrelevant and do not need to be verified. Based on this insight, we create WOODPECKER, a new symbolic execution system for effectively checking rules on systems programs. It provides a set of builtin checkers for common rules, and an interface for users to easily check new rules. It directs symbolic execution toward the program paths relevant to a checked rule, and soundly prunes redundant paths, exponentially speeding up symbolic execution. It is designed to be heuristic-agnostic, enabling users to leverage existing powerful search heuristics. Evaluation on 136 systems programs totaling 545K lines of code, including some of the most widely used programs, shows that, with a time limit of typically just one hour for each verification run, WOODPECKER effectively verifies 28.7% of the program and rule combinations over bounded input, whereas an existing symbolic execution system KLEE verifies only 8.5%. For the remaining combinations, WOODPECKER verifies 4.6 times as many relevant paths as KLEE. With a longer time limit, WOODPECKER verifies much more paths than KLEE, e.g., 17 times as many with a fourhour limit.WOODPECKER detects 113 rule violations, including 10 serious data loss errors with 2 most serious ones already confirmed by the corresponding developers.
Persistent Identifierhttp://hdl.handle.net/10722/207928
ISSN
2015 SCImago Journal Rankings: 0.490

 

DC FieldValueLanguage
dc.contributor.authorCui, H-
dc.contributor.authorHu, G-
dc.contributor.authorWu, J-
dc.contributor.authorYang, J-
dc.date.accessioned2015-01-26T11:46:43Z-
dc.date.available2015-01-26T11:46:43Z-
dc.date.issued2013-
dc.identifier.citationACM SIGPLAN Notices, 2013, v. 48, n. 4, p. 329-341-
dc.identifier.issn1523-2867-
dc.identifier.urihttp://hdl.handle.net/10722/207928-
dc.description.abstractSystems code must obey many rules, such as "opened files must be closed." One approach to verifying rules is static analysis, but this technique cannot infer precise runtime effects of code, often emitting many false positives. An alternative is symbolic execution, a technique that verifies program paths over all inputs up to a bounded size. However, when applied to verify rules, existing symbolic execution systems often blindly explore many redundant program paths while missing relevant ones that may contain bugs. Our key insight is that only a small portion of paths are relevant to rules, and the rest (majority) of paths are irrelevant and do not need to be verified. Based on this insight, we create WOODPECKER, a new symbolic execution system for effectively checking rules on systems programs. It provides a set of builtin checkers for common rules, and an interface for users to easily check new rules. It directs symbolic execution toward the program paths relevant to a checked rule, and soundly prunes redundant paths, exponentially speeding up symbolic execution. It is designed to be heuristic-agnostic, enabling users to leverage existing powerful search heuristics. Evaluation on 136 systems programs totaling 545K lines of code, including some of the most widely used programs, shows that, with a time limit of typically just one hour for each verification run, WOODPECKER effectively verifies 28.7% of the program and rule combinations over bounded input, whereas an existing symbolic execution system KLEE verifies only 8.5%. For the remaining combinations, WOODPECKER verifies 4.6 times as many relevant paths as KLEE. With a longer time limit, WOODPECKER verifies much more paths than KLEE, e.g., 17 times as many with a fourhour limit.WOODPECKER detects 113 rule violations, including 10 serious data loss errors with 2 most serious ones already confirmed by the corresponding developers.-
dc.languageeng-
dc.relation.ispartofACM SIGPLAN Notices-
dc.subjectPath Slicing-
dc.subjectError Detection-
dc.subjectVerification-
dc.subjectSystems Rules-
dc.subjectSymbolic execution-
dc.titleVerifying systems rules using rule-directed symbolic execution-
dc.typeConference_Paper-
dc.description.naturelink_to_subscribed_fulltext-
dc.identifier.doi10.1145/2499368.2451152-
dc.identifier.scopuseid_2-s2.0-84880123775-
dc.identifier.volume48-
dc.identifier.issue4-
dc.identifier.spage329-
dc.identifier.epage341-

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats