We propose a radically new family of geometric graphs, i.e., Hypocomb (HC), Reduced Hypocomb (RHC), and Local Hypocomb (LHC). HC and RHC are extracted from a complete graph; LHC is extracted from a Unit Disk Graph (UDG). We analytically study their properties including connectivity, planarity, and degree bound. All these graphs are connected (provided that the original graph is connected) planar. Hypocomb has unbounded degree while Reduced Hypocomb and Local Hypocomb have maximum degree 6 and 8, respectively. To our knowledge, Local Hypocomb is the first strictly localized, degree-bounded planar graph computed using merely 1-hop neighbor position information. We present a construction algorithm for these graphs and analyze its time complexity. Hypocomb family graphs are promising for wireless ad hoc networking. We report our numerical results on their average degree and their impact on FACE routing. We discuss their potential applications and pinpoint some interesting open problems for future research.

In the field of annotation-based source code level program verification for Java-like languages, separation-logic based verifiers offer a promising alternative to classic JML based verifiers such as ESC/Java2, the Mobius tool or Spec#. Researchers have demonstrated the advantages of separation logic based verification by showing that it is feasible to verify very challenging (though very small) sample code, such as design patterns, or highly concurrent code. However, there is little experience in using this new breed of verifiers on real code. In this paper we report on our experience of verifying several thousands of lines of Java Card code using VeriFast, one of the state-of-the-art separation logic based verifiers. We quantify annotation overhead, verification performance, and impact on code quality (number of bugs found). Finally, our experiments suggest a number of potential improvements to the VeriFast tool.

This paper presents the enforcement of control flow policies for Java bytecode dedicated to open and constrained devices. On-device enforcement of security policies mostly relies on run-time monitoring or inline checking code, which is not appropriate for strongly constrained devices such as mobile phones and smart-cards. We present a proof-carrying code approach with on-device lightweight verification of control flow policies statically at loading-time. Our approach is suitable for evolving, open and constrained Java-based systems as it is compositional, to avoid re-verification of already verified bytecode upon loading of new bytecode, and it is regressive, to cleanly support bytecode unloading.

Wireless sensor networks are of energy-constrained nature, which calls for energy efficient protocols as a primary design goal. Thus, minimizing energy consumption is a main challenge.We are concerned in howcollected data by sensors, can be processed to increase the relevance of certain mass of data and reduce the overall data traffic. Since sensor nodes are often densely deployed, the data collected by nearby nodes are either redundant or correlated. One of the great challenges for the aforementioned problem is to exploit temporal and spatial correlation among the source nodes. Our work is composed of two main tasks: 1- A predictive modeling task that aims to capture the temporal correlation among collected data. 2- A data similarity detection task that measures the data similarity based on the spatial correlation.

Security and trust policy models.- security protocol design and analysis.- formal models of trust and reputation.- logics for security and trust.- distributed trust management systems.- trust-based reasoning.- digital assets protection.- data protection.- privacy and ID issues.- information flow analysis.- language-based security.- security and trust aspects of ubiquitous computing.- validation/analysis tools.- web service security/trust/privacy.- grid security.- security risk assessment.- case studies.

Knowledge discovery and data analysis in resource constrained wireless sensor networks faces different challenges. One of the main challenges is to identify misbehaviors or anomalies with high accuracy while minimizing energy consumption in the network. In this paper, we extend a previous work of us and we present an algorithm for temporal anomalies detection in wireless sensor networks. Our experiments results show that our algorithm can efficiently and accurately detect anomalies in sensor measurements. It also produces low false alarm rate for slow variation time series measurements without harvesting the source of energy.

We propose a radically new family of geometric graphs, i.e., Hypocomb, Reduced Hypocomb and Local Hypocomb. The first two are extracted from a complete graph; the last is extracted from a Unit Disk Graph (UDG). We analytically study their properties including connectivity, planarity and degree bound. All these graphs are connected (provided the original graph is connected) planar. Hypocomb has unbounded degree while Reduced Hypocomb and Local Hypocomb have maximum degree 6 and 8, respectively. To our knowledge, Local Hypocomb is the first strictly-localized, degree-bounded planar graph computed using merely 1-hop neighbor position information. We present a construction algorithm for these graphs and analyze its time complexity. Hypocomb family graphs are promising for wireless ad hoc networking. We report our numerical results on their average degree and their impact on FACE routing. We discuss their potential applications and some open problems.

This paper presents the enforcement of control flow policies for Java bytecode devoted to open and constrained devices. On-device enforcement of security policies mostly relies on run-time monitoring or inline checking code, which is not appropriate for strongly constrained devices such as mobile phones and smart-cards. We present a proof-carrying code approach with on-device lightweight verification of control flow policies statically at loading- time. Our approach is suitable for evolving, open and constrained Java-based systems as it is compositional, to avoid re-verification of already verified bytecode upon loading of new bytecode, and it is regressive, to cleanly support bytecode unloading.

While mobile devices have become ubiquitous and generally multi-application capable, their operating systems provide few high level mechanisms to protect services offered by application vendors against potentially hostile applications coexisting on the device. In this paper, we tackle the issue of controlling application interactions including collusion in Java-based systems running on open, constrained devices such as smart cards or mobile phones. We present a model specially designed to be embedded in constrained devices to verify on-device at loading-time that interactions between applications abide by the security policies of each involved application without resulting in run-time computation overheads; this model deals with application (un)installations and policy changes in an incremental fashion. We sketch the application of our approach and its security enhancements on a multi-application use case for GlobalPlatform/Java Card smart cards.

In mobile-beacon assisted sensor localization, beacon mobility scheduling aims to determine the best beacon trajectory so that each sensor receives sufficient beacon signals with minimum delay. We propose a novel DeteRministic bEAcon Mobility Scheduling (DREAMS) algorithm, without requiring any prior knowledge of the sensory field. In this algorithm, beacon trajectory is defined as the track of depth-first traversal (DFT) of the network graph, thus deterministic. The mobile beacon performs DFT under the instruction of nearby sensors on the fly. It moves from sensor to sensor in an intelligent heuristic manner according to RSS (Received Signal Strength)-based distance measurements. We prove that DREAMS guarantees full localization (every sensor is localized) when the measurements are noise-free. Then we suggest to apply node elimination and topology control (Local Minimum Spanning Tree) to shorten beacon tour and reduce delay. Through simulation we show that DREAMS guarantees full localization even with noisy distance measurements. We evaluate its performance on localization delay and communication overhead in comparison with a previously proposed static path based scheduling method.

Electronic cash is an attempt to replace and reproduce paper cash in electronic transactions that faces competing challenges when used either online or offline. In effect, while effective protection against double spending for e-cash can be achieved in online payment environments through real-time detection, this comes at the expense of efficiency, the bank representing in such case a performance bottleneck and single point of failure. In contrast, in offline payment environments, while efficiency is improved, double spending can be detected only after the fact, which can be very costly. We propose in this paper a risk management approach for double spending protection which allows suitable tradeoffs between efficiency and effectiveness. This involves using the service of a trader, who is a trusted third party that will cover the risk involved in offline payment transactions, against some remuneration. The main goal is to provide full coverage to users against losses related to invalid coins while avoiding or minimizing interactions with the bank. Since the trader will incur some risk by guaranteeing coins while she cannot communicate with the bank, a winning strategy is devised for the trader to mitigate such risk.

In mobile-beacon assisted sensor localization, beacon mobility scheduling aims to determine the best beacon trajectory so that each sensor receives sufficient beacon signals and becomes localized with minimum delay. We propose a novel DeteRministic dynamic bEAcon Mobility Scheduling (DREAMS) algorithm, without requiring any prior knowledge of the sensory field. In this algorithm, the beacon trajectory is defined as the track of Depth-First Traversal (DFT) of the network graph, thus deterministic. The mobile beacon performs DFT dynamically, under the instruction of nearby sensors on the fly. It moves from sensor to sensor in an intelligent heuristic manner according to Received Signal Strength (RSS)-based distance measurements. We prove that DREAMS guarantees full localization (every sensor is localized) when the measurements are noise-free, and derive the upper bound of beacon total moving distance in this case. Then, we suggest to apply node elimination and Local Minimum Spanning Tree (LMST) to shorten beacon tour and reduce delay. Further, we extend DREAMS to multibeacon scenarios. Beacons with different coordinate systems compete for localizing sensors. Loser beacons agree on winner beacons' coordinate system, and become cooperative in subsequent localization. All sensors are finally localized in a commonly agreed coordinate systems. Through simulation we show that DREAMS guarantees full localization even with noisy distance measurements. We evaluate its performance on localization delay and communication overhead in comparison with a previously proposed static path-based scheduling method.

Telecommunication software systems, containing security vulnerabilities, continue to be created and released to consumers. We need to adopt improved software engineering practices to reduce the security vulnerabilities in modern systems. Contracts can provide a useful mechanism for the identification, tracking, and validation of security vulnerabilities. In this work, we propose a new contract-based security assertion monitoring framework (CB_SAMF) that is intended to reduce the number of security vulnerabilities that are exploitable across multiple software layers, and to be used in an enhanced systems development life cycle (SDLC). We show how contract-based security assertion monitoring can be achieved in a live environment on Linux. Through security activities integrated into the SDLC we can identify potential security vulnerabilities in telecommunication systems, which in turn are used for the creation of contracts defining security assertions. Our contract model is then applied, as runtime probes, against two common security related vulnerabilities in the form of a buffer overflow and a denial of service.

Extending the lifetime of wireless sensor networks remains the most challenging and demanding requirement that impedes large-scale deployments. The basic operation in WSNs is the systematic gathering and transmission of sensed data to a base station for further processing. During data gathering, the amount of data can be large sometimes, due to redundant data combined from different sensing nodes in the neighborhood. Thus the data gathered need to be processed before being transmitted, in order to detect and remove redundancy, which can impact the communication traffic and energy consumption of the network in a negative way. In this paper, we propose an algorithm to measure similarity between the data collected toward the base station(relative to a specific event monitoring), so that an aggregator sensor sends a minimum amount of information to the base station in a way that the latter can deduce the source information of sensing neighbors nodes. Further, our experimental results demonstrate that the communication traffic and the number of bits transmitted can be minimized while preserving accuracy on the base station estimations.

A primary purpose of sensing in a sensor network is to collect and aggregate information about a phenomenon of interest. The batteries on today's wireless sensor barely last a few days, and nodes typically expend a lot of energy in computation and wireless communication. Hence, the energy efficiency of the system is a major issue. Different representative mechanisms has been proposed to achieve a long lived sensors such as “clustering mechanisms” as well as Aggregation techniques to reduce the amount of data communication generated by sensors. Depending on the data type, ARMA series and forecasting are possible ways to reduce data transmission. In this work, we adopt single-hop clustering mechanism where all sensor nodes in a cluster communicate with their Cluster-Head (or sink) via single hop (such as In/On body sensors for personal health monitoring,..). We propose different data aggregation algorithms based on the AutoRegressive model, to predict local readings and reduce the communication traffic. We evaluate the performance of our work in terms of communication cost and energy consumption. We also extend our work to enhance the prediction accuracy by estimating dynamic prediction threshold. Our simulation shows that depending on data type, communication overhead and rate can be reduced and a considerable accuracy prediction can be obtained.

In this paper we present a flow-sensitive analysis for secure information flow for Java bytecode. Our approach consists of computing, at all program points, an abstract memory graph (AMG) which tracks how input values of a method may influence its outputs. This computation subsumes a points-to analysis (reflecting how objects depend on each other) by addressing dependencies arising from data of primitive types and from the control flow of the program. Our graph construction is proved to be sound for both intra-procedural and inter-procedural analysis by establishing a non-interference theorem stating that if an output value is unrelated to an input one in the AMG then the output remains unchanged when the input is modified. In contrast with many type-based information flow techniques, our approach does not require security levels to be known during the computation of the graph: security aspects of information flow are checked by labeling ”a posteriori” the AMG with security levels.

We propose a localized sensor localization scheme making full use of controlled mobility of a location-aware actor and the connectivity of the sensor network. It contains two new algorithms: a unscented particle filter (UPF) based localization algorithm and an actor mobility scheduling algorithm. The former is an application of UPF. It enables sensor self-localization using received signal strength indicator and actor position. The latter models actor mobility scheduling as traveling salesman problem and aims at fully localized network and minimized time delay. Navigated by sensors, the actor depth-first traverses a local minimum spanning tree of a connected 3-dominating set of the network.