PoK

Author:Donggang Liu,Peng Ning, An Liu,Cliff Wang,Wenliang Kevin Du

Description:
Many sensor network applications require sensors’ locations to function correctly. Despite the recent advances, location discovery for sensor networks in hostile environments has been mostly overlooked. Most of the existing localization protocols for sensor networks are vulnerable in hostile environments. The security of location discovery can certainly be enhanced by authentication. However, the possible node compromises and the fact that location determination uses certain physical features (e.g., received signal strength) of radio signals make authentication not as effective as in traditional security applications. This paper presents two methods to tolerate malicious attacks against range based location discovery in sensor networks. The first method filters out malicious beacon signals on the basis of the “consistency” among multiple beacon signals, while the second method tolerates malicious beacon signals by adopting an iteratively refined voting scheme. Both methods can survive malicious attacks even if the attacks bypass authentication,provided that the benign beacon signals constitute the majority of the beacon signals. This paper also presents the implementation and experimental evaluation (through both field experiments and simulation) of all the secure and resilient location estimation schemes that can be used on the current generation of sensor platforms (e.g., MICA series of motes), including the techniques proposed in this paper, in a network of MICAz motes. The experimental results demonstrate the effectiveness of the proposed methods, and also give the secure and resilient location estimation scheme most suitalbe for the current generation of sensor networks.

Authors: Cecilia Mascolo, Gian Pietro Picco, Gruia-Catalin Roman

Description:
This paper is concerned with an abstract exploration of code mobility constructs designed for use in settings where the level of granularity associated with the mobile units exhibits significant variability. Units of mobility that are both finer and coarser grained than the unit of execution are examined. To accomplish this, we take the extreme view that every line of code and every variable declaration are potentially mobile, i.e., it may be duplicated or moved from one program context to another on the same host or across the network. We also assume that complex code assemblies may move with equal ease. The result is CODEWEAVE, a model that shows how to develop new forms of code mobility, assign them precise meaning, and facilitate formal verification of programs employing them. The design of CODEWEAVE relies greatly on Mobile UNITY, a notation and proof logic for mobile computing. Mobile UNITY offers a computational milieu for examining a wide range of constructs and semantic alternatives in a clean abstract setting, i.e., unconstrained by compilation and performance considerations traditionally associated with programming language design. Ultimately, the notation offered by CODEWEAVE is given exact semantic definition by means of a direct mapping to the underlying Mobile UNITY model. The abstract and formal treatment of code mobility offered by CODEWEAVE establishes a technical foundation for examining competing proposals and for subsequent integration of some of the mobility constructs both at the language level and within middleware for mobility.

Authors: Amy L. Murphy, Gian Pietro Picco, Gruia-Catalin Roman

Description:
Lime is a middleware supporting the development of applications that exhibit physical mobility of hosts, logical mobility of agents, or both. Lime adopts a coordination perspective inspired by work on the Linda model. The context for computation, represented in Linda by a globally accessible, persistent tuple space, is represented in Lime by transient sharing of the tuple spaces carried by each individual mobile unit. Linda tuple spaces are also extended with a notion of location and with the ability to react to a given state. The hypothesis underlying our work is that the resulting model provides a minimalist set of abstractions that enable rapid and dependable development of mobile applications. In this paper, we illustrate the model underlying Lime, present its current design and implementation, report about its initial evaluation in applications that involve physical mobility, and discuss lessons learned and future enhancements that will drive its evolution.

Authors: Gruia-Catalin Roman, Qingfeng Huang, Ali Hazemi

Description:
The design of ad hoc mobile applications often requires the availability of a consistent view of the application state among the participating hosts. Such views are important because they simplify both the programming and verification tasks. Essential to constructing a consistent view is the ability to know what hosts are within proximity of each other, i.e., form a group in support of the particular application. In this paper we propose an algorithm that allows hosts within communication range to maintain a consistent view of the group membership despite movement and frequent disconnections. The novel features of this algorithm are its reliance on location information and a conservative notion of logical connectivity that creates the illusion of announced disconnection. Movement patterns and delays are factored in the policy that determines which physical connections are susceptible to disconnection.

Authors: Gruia-Catalin Roman, Christine Julien, Qingfeng Huang

Description:
Termination detection, a classical problem in distributed computing, is revisited in the new setting provided by the emerging mobile computing technology. A simple solution tailored for use in ad hoc networks is employed as a vehicle for demonstrating the applicability of formal requirements and design strategies to the new field of mobile computing. The approach is based on well understood techniques in specification refinement, but the methodology is tailored to mobile applications and helps designers address novel concerns such as the mobility of hosts, transient interactions, and specific coordination constructs. The proof logic and programming notation of Mobile UNITY provide the intellectual tools required to carry out this task.