SLEDE: A Domain-Specific Verification Framework for Sensor Network Security Protocol Implementations

dc.contributor.author Hanna, Youssef
dc.contributor.author Rajan, Hridesh
dc.contributor.author Rajan, Hridesh
dc.contributor.department Computer Science
dc.date 2018-02-14T00:54:08.000
dc.date.accessioned 2020-06-30T01:56:40Z
dc.date.available 2020-06-30T01:56:40Z
dc.date.issued 2007-06-11
dc.description.abstract <p>Sensor networks are often deployed in hostile situations. A number of protocols are being developed to secure these networks. Current means to verify these protocols include simulation, manual inspection, and running them on sensor network testbeds. These techniques leave room for subtle errors in protocol implementations that can be exploited by adversaries. The contribution of this work is the design, implementation and early evaluation of a domain-specific verification framework for nesC implementations of sensor network security protocols. We call our verification framework Slede. Technical underpinnings of Slede include support for automatic extraction of PROMELA models from nesC source code, an annotation language to guide the verification process, and an automatic intrusion model generator. Preliminary evaluation shows that Slede was able to discover flaws in a canonical cryptographic protocol by Needham and Schroeder and two security protocols specific to sensor networks. We also demonstrate that a protocol aware intrusion model automatically generated by Slede incurs a small extra cost compared to models handwritten by model checking experts. By automating a significant portion of the verification process, Slede promises to make it easier to apply finite-state model checking to verify nesC protocol implementations.</p>
dc.identifier archive/lib.dr.iastate.edu/cs_techreports/318/
dc.identifier.articleid 1317
dc.identifier.contextkey 5540029
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath cs_techreports/318
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/20147
dc.source.bitstream archive/lib.dr.iastate.edu/cs_techreports/318/main.pdf|||Fri Jan 14 23:32:41 UTC 2022
dc.subject.disciplines Programming Languages and Compilers
dc.subject.disciplines Software Engineering
dc.subject.disciplines Theory and Algorithms
dc.subject.keywords sensor networks
dc.subject.keywords security protocols
dc.subject.keywords model checking
dc.subject.keywords slede
dc.subject.keywords intrusion model generation
dc.subject.keywords SLEDE
dc.title SLEDE: A Domain-Specific Verification Framework for Sensor Network Security Protocol Implementations
dc.type article
dc.type.genre article
dspace.entity.type Publication
relation.isAuthorOfPublication 4e3f4631-9a99-4a4d-ab81-491621e94031
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456
File
Original bundle
Now showing 1 - 1 of 1
Name:
main.pdf
Size:
941.55 KB
Format:
Adobe Portable Document Format
Description:
Collections