NDLI: SLEDE: lightweight verification of sensor network security protocol implementations ( ESEC-FSE companion '07 )

Please wait, while we are loading the content...

Foreword to state-of-the-art presentations

Welcome to the WISE track

Exploring motivational differences between software developers and project managers

Foreword to the doctoral symposium

SYANCO 2007: international workshop on synthesis and analysis of component connectors

On marrying ontological and metamodeling technical spaces

Practicum in software project management: an endeavor to effective and pragmatic software project management education

Product integration improvement based on analysis of build statistics

Visualising exemplary program values

Specification and verification of component-based systems 2007

Quantitative verification: models, techniques and tools

A survey of web engineering practice in small Jordanian web development firms

A case study in assessing and improving capacity using an anatomy of good practice

An analysis of developers' tasks using low-level, automatically collected data

IWPSE 2007: 9th international workshop on principles of software evolution

Free/open source software development: recent research results and emerging opportunities

Building a research university ecosystem: the case of software engineering education at Sofia University

Efficient token based clone detection with flexible tokenization

Composition and tradeoff of non-functional attributes in software systems: research directions

2nd international workshop on service oriented software engineering: (IW-SOSWE 2007)

A segment-based approach for reconcilable model transformation

Model-driven test-case construction

SOQUA 2007 4th international workshop on software quality assurance

A behavioural model for product families

SLEDE: lightweight verification of sensor network security protocol implementations

EFTS 2007: the $2^{nd}$ international workshop on engineering fault tolerant systems

A specification-based approach to testing software product lines

Analysis of a deployed software

Engineering software services for pervasive environments: ESSPE '07 workshop summary

A profile-driven statistical analysis framework for the design optimization of soft real-time applications

Component airbag: a novel approach to develop dependable component-based applications

Domain specific approaches to software test automation

A study of interleaving coverage criteria

A model-driven approach to generating user interfaces

An iterative, multi-level, and scalable approach to comparing execution traces

State coverage: a structural test adequacy criterion for behavior checking

Quantifying the effectiveness of testing via efficient residual path profiling

Differential testing: a new approach to change detection

Directed test generation using symbolic grammars

Towards incremental adaptive covering arrays

Predictive testing: amplifying the effectiveness of software testing

Using groupings of static analysis alerts to identify files likely to contain field failures

On impact-oriented automatic resolution of pervasive context inconsistency

SLEDE: lightweight verification of sensor network security protocol implementations ( ESEC-FSE companion '07 )

Content Provider	ACM Digital Library
Author	Hanna, Youssef
Abstract	Finding flaws in security protocol implementations is hard. Finding flaws in the implementations of sensor network security protocols is even harder because they are designed to protect against more system failures compared to traditional protocols. Formal verification techniques such as model checking, theorem proving, etc, have been very successful in the past in detecting faults in security protocol specifications; however, they generally require a model. Developing these models is a non-trivial task for an average developer. This task is further complicated by the impedance mismatch between the implementation language and the modeling language. For example, while the dominant implementation language for sensor network applications (nesC) uses an event-based paradigm, the modeling language (Promela) uses message-driven paradigm. The key goal of this research is to ease the task of verifying sensor network security protocol implementations for the sensor network community by defining an approach for automatically extracting a model from the nesC implementations of a security protocol. We contribute the design and implementation of a verification framework that we call Slede which emulates our approach to extract a PROMELA model from nesC security protocol implementations. By significantly decreasing the cost of verification, we believe our approach will improve the overall quality of the nesC security protocol implementations.
Starting Page	591
Ending Page	594
Page Count	4
File Format	PDF
ISBN	9781595938121
DOI	10.1145/1295014.1295050
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2007-09-03
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Security protocols Model checking Sensor networks Slede
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in