OpenRaiser/Intern-Atlas huggingface dataset:
Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution
Venue: arXiv cs.CR 2011
Year: 2011

Consider the problem of verifying security properties of a cryptographic protocol coded in C. We propose an automatic solution that needs neither a pre-existing protocol description nor manual annotation of source code. First, symbolically execute the C program to obtain symbolic descriptions for the network messages sent by the protocol. Second, apply algebraic rewriting to obtain a process calculus description. Third, run an existing protocol analyser (ProVerif) to prove security properties or find attacks. We formalise our algorithm and appeal to existing results for ProVerif to establish computational soundness under suitable circumstances. We analyse only a single execution path, so our results are limited to protocols with no significant branching. The results in this paper provide the first computationally sound verification of weak secrecy and authentication for (single execution paths of) C code.
Integral Value Transformations: A Class of Discrete Dynamical Systems
Venue: arXiv cs.DM 2011
Year: 2011

Here the Integral Value Transformations (IVTs) are considered to be Discrete Dynamical System map in the space\mathbb{N}_(0). In this paper, the dynamics of IVTs is deciphered through the light of Topological Dynamics.
Misbehavior in Mobile Application Markets
Venue: arXiv cs.CR 2011
Year: 2011

Mobile application markets facilitate the distribution of applications and thus help developers advertise their work and customers find useful applications. In addition, the operators of mobile application markets can control the quality and the content of the applications. These markets are growing rapidly with more than 300'000 application in the App Store of Apple and more than 100'000 in the Android Market of Google. This is not only a great opportunity for phone manufacturers to earn money but also for indie developers (single or small teams of developers with small financial support) who can thus have a great distribution channel. Steve Demeter, the Trim game developer for iPhone, became millionaire with a single puzzle game . Obviously, as new markets generate a lot of money, the temptation of misbehavior to steal part of the benefits is big. The first famous case was the one of Molinker who self-rated his applications with 5 stars to pump up his ranking in order to increase its revenue stream. In this report, we will consider the problem of misbehavior in mobile application markets. We will investigate multiple attacks by misbehaving developers, users or network operators that aim at breaking rules for their own benefit, managing to outwit the operators' control on which applications can be installed. We notably suggest novel attacks that may affect mobile markets in the future: in particular, we show that it is possible to get revenue for applications created by someone else, trick a user to download and buy an application and new ways to pump up an application's ranking. We will also discuss possible solutions against spyware applications and cheating developer
SERIMI - Resource Description Similarity, RDF Instance Matching and Interlinking
Venue: arXiv cs.DB 2011
Year: 2011

The interlinking of datasets published in the Linked Data Cloud is a challenging problem and a key factor for the success of the Semantic Web. Manual rule-based methods are the most effective solution for the problem, but they require skilled human data publishers going through a laborious, error prone and time-consuming process for manually describing rules mapping instances between two datasets. Thus, an automatic approach for solving this problem is more than welcome. In this paper, we propose a novel interlinking method, SERIMI, for solving this problem automatically. SERIMI matches instances between a source and a target datasets, without prior knowledge of the data, domain or schema of these datasets. Experiments conducted with benchmark collections demonstrate that our approach considerably outperforms state-of-the-art automatic approaches for solving the interlinking problem on the Linked Data Cloud.
Estimation of Sparse MIMO Channels with Common Support
Venue: arXiv cs.NI 2011
Year: 2011

We consider the problem of estimating sparse communication channels in the MIMO context. In small to medium bandwidth communications, as in the current standards for OFDM and CDMA communication systems (with bandwidth up to 20 MHz), such channels are individually sparse and at the same time share a common support set. Since the underlying physical channels are inherently continuous-time, we propose a parametric sparse estimation technique based on finite rate of innovation (FRI) principles. Parametric estimation is especially relevant to MIMO communications as it allows for a robust estimation and concise description of the channels. The core of the algorithm is a generalization of conventional spectral estimation methods to multiple input signals with common support. We show the application of our technique for channel estimation in OFDM (uniformly/contiguous DFT pilots) and CDMA downlink (Walsh-Hadamard coded schemes). In the presence of additive white Gaussian noise, theoretical lower bounds on the estimation of SCS channel parameters in Rayleigh fading conditions are derived. Finally, an analytical spatial channel model is derived, and simulations on this model in the OFDM setting show the symbol error rate (SER) is reduced by a factor 2 (0 dB of SNR) to 5 (high SNR) compared to standard non-parametric methods - e.g. lowpass interpolation.
Algorithms for Synthesizing Priorities in Component-based Systems
Venue: arXiv cs.LO 2011
Year: 2011

We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority synthesis, namely (a) data abstraction to reduce component complexities, (b) alphabet abstraction and #-deadlock to ignore components, and (c) automated assumption learning for compositional priority synthesis.
Performance of Local Information Based Link Prediction: A Sampling Perspective
Venue: arXiv cs.SI 2011
Year: 2011

Link prediction is pervasively employed to uncover the missing links in the snapshots of real-world networks, which are usually obtained from kinds of sampling methods. Contrarily, in the previous literature, in order to evaluate the performance of the prediction, the known edges in the sampled snapshot are divided into the training set and the probe set randomly, without considering the diverse sampling approaches beyond. However, different sampling methods might lead to different missing links, especially for the biased ones. For this reason, random partition based evaluation of performance is no longer convincing if we take the sampling method into account. Hence, in this paper, aim at filling this void, we try to reevaluate the performance of local information based link predictions through sampling methods governed division of the training set and the probe set. It is interesting that we find for different sampling methods, each prediction approach performs unevenly. Moreover, most of these predictions perform weakly when the sampling method is biased, which indicates that the performance of these methods is overestimated in the prior works.
On fuzzy syndrome hashing with LDPC coding
Venue: arXiv cs.IT 2011
Year: 2011

The last decades have seen a growing interest in hash functions that allow some sort of tolerance, e.g. for the purpose of biometric authentication. Among these, the syndrome fuzzy hashing construction allows to securely store biometric data and to perform user authentication without the need of sharing any secret key. This paper analyzes this model, showing that it offers a suitable protection against information leakage and several advantages with respect to similar solutions, such as the fuzzy commitment scheme. Furthermore, the design and characterization of LDPC codes to be used for this purpose is addressed.
Prostate biopsy tracking with deformation estimation
Venue: arXiv cs.CV 2011
Year: 2011

Transrectal biopsies under 2D ultrasound (US) control are the current clinical standard for prostate cancer diagnosis. The isoechogenic nature of prostate carcinoma makes it necessary to sample the gland systematically, resulting in a low sensitivity. Also, it is difficult for the clinician to follow the sampling protocol accurately under 2D US control and the exact anatomical location of the biopsy cores is unknown after the intervention. Tracking systems for prostate biopsies make it possible to generate biopsy distribution maps for intra- and post-interventional quality control and 3D visualisation of histological results for diagnosis and treatment planning. They can also guide the clinician toward non-ultrasound targets. In this paper, a volume-swept 3D US based tracking system for fast and accurate estimation of prostate tissue motion is proposed. The entirely image-based system solves the patient motion problem with an a priori model of rectal probe kinematics. Prostate deformations are estimated with elastic registration to maximize accuracy. The system is robust with only 17 registration failures out of 786 (2%) biopsy volumes acquired from 47 patients during biopsy sessions. Accuracy was evaluated to 0.76$\pm$0.52mm using manually segmented fiducials on 687 registered volumes stemming from 40 patients. A clinical protocol for assisted biopsy acquisition was designed and implemented as a biopsy assistance system, which allows to overcome the draw-backs of the standard biopsy procedure.
Click Efficiency: A Unified Optimal Ranking for Online Ads and Documents
Venue: arXiv cs.GT 2011
Year: 2011

Traditionally the probabilistic ranking principle is used to rank the search results while the ranking based on expected profits is used for paid placement of ads. These rankings try to maximize the expected utilities based on the user click models. Recent empirical analysis on search engine logs suggests a unified click models for both ranked ads and search results. The segregated view of document and ad rankings does not consider this commonality. Further, the used models consider parameters of (i) probability of the user abandoning browsing results (ii) perceived relevance of result snippets. But how to consider them for improved ranking is unknown currently. In this paper, we propose a generalized ranking function---namely "Click Efficiency (CE)"---for documents and ads based on empirically proven user click models. The ranking considers parameters (i) and (ii) above, optimal and has the same time complexity as sorting. To exploit its generality, we examine the reduced forms of CE ranking under different assumptions enumerating a hierarchy of ranking functions. Some of the rankings in the hierarchy are currently used ad and document ranking functions; while others suggest new rankings. While optimality of ranking is sufficient for document ranking, applying CE ranking to ad auctions requires an appropriate pricing mechanism. We incorporate a second price based pricing mechanism with the proposed ranking. Our analysis proves several desirable properties including revenue dominance over VCG for the same bid vector and existence of a Nash Equilibrium in pure strategies. The equilibrium is socially optimal, and revenue equivalent to the truthful VCG equilibrium. Further, we relax the independence assumption in CE ranking and analyze the diversity ranking problem. We show that optimal diversity ranking is NP-Hard in general, and that a constant time approximation is unlikely.
Medium Access Control for Wireless Networks with Peer-to-Peer State Exchange
Venue: arXiv cs.IT 2011
Year: 2011

Distributed medium access control (MAC) protocols are proposed for wireless networks assuming that one-hop peers can periodically exchange a small amount of state information. Each station maintains a state and makes state transitions and transmission decisions based on its state and recent state information collected from its one-hop peers. A station can adapt its packet length and the size of its state space to the amount of traffic in its neighborhood. It is shown that these protocols converge to a steady state, where stations take turns to transmit in each neighborhood without collision. In other words, an efficient time-division multiple access (TDMA) like schedule is formed in a distributed manner, as long as the topology of the network remains static or changes slowly with respect to the execution of the protocol.
Interference Networks with General Message Sets: A Random Coding Scheme
Venue: arXiv cs.IT 2011
Year: 2011

In this paper, the Interference Network with General Message Sets (IN-GMS) is introduced in which several transmitters send messages to several receivers: Each subset of transmitters transmit an individual message to each subset of receivers. For such a general scenario, an achievability scheme is presented using the random coding. This scheme is systematically built based on the capacity achieving scheme for the Multiple Access Channel (MAC) with common message as well as the best known achievability scheme for the Broadcast Channel (BC) with common message. A graphical illustration of the random codebook construction procedure is also provided, by using which the achievability scheme is easily understood. Some benefits of the proposed achievability scheme are described. It is also shown that the resulting rate region is optimal for a class of orthogonal INs-GMS, which yields the capacity region. Finally, it is demonstrated that how this general achievability scheme can be used to derive capacity inner bounds for interference networks with different distribution of messages; in most cases, the proposed achievability scheme leads to the best known capacity inner bound for the underlying channel. Capacity inner bounds can also be derived for new communication scenarios.
Utility Optimal Coding for Packet Transmission over Wireless Networks - Part I: Networks of Binary Symmetric Channels
Venue: arXiv cs.IT 2011
Year: 2011

We consider multi--hop networks comprising Binary Symmetric Channels ($\mathsf{BSC}$s). The network carries unicast flows for multiple users. The utility of the network is the sum of the utilities of the flows, where the utility of each flow is a concave function of its throughput. Given that the network capacity is shared by the flows, there is a contention for network resources like coding rate (at the physical layer), scheduling time (at the MAC layer), etc., among the flows. We propose a proportional fair transmission scheme that maximises the sum utility of flow throughputs subject to the rate and the scheduling constraints. This is achieved by {\em jointly optimising the packet coding rates of all the flows through the network}.
Link Scheduling in Multi-Transmit-Receive Wireless Networks
Venue: arXiv cs.NI 2011
Year: 2011

This paper investigates the problem of link scheduling to meet traffic demands with minimum airtime in a multi-transmit-receive (MTR) wireless network. MTR networks are a new class of networks, in which each node can simultaneously transmit to a number of other nodes, or simultaneously receive from a number of other nodes. The MTR capability can be enabled by the use of multiple directional antennas or multiple channels. Potentially, MTR can boost the network capacity significantly. However, link scheduling that makes full use of the MTR capability must be in place before this can happen. We show that optimal link scheduling can be formulated as a linear program (LP). However, the problem is NP-hard because we need to find all the maximal independent sets in a graph first. We propose two computationally efficient algorithms, called Heavy-Weight-First (HWF) and Max-Degree-First (MDF) to solve this problem. Simulation results show that both HWF and MDF can achieve superior performance in terms of runtime and optimality.
Enhanced Genetic Algorithm approach for Solving Dynamic Shortest Path Routing Problems using Immigrants and Memory Schemes
Venue: arXiv cs.NE 2011
Year: 2011

In Internet Routing, the static shortest path (SP) problem has been addressed using well known intelligent optimization techniques like artificial neural networks, genetic algorithms (GAs) and particle swarm optimization. Advancement in wireless communication lead more and more mobile wireless networks, such as mobile networks [mobile ad hoc networks (MANETs)] and wireless sensor networks. Dynamic nature of the network is the main characteristic of MANET. Therefore, the SP routing problem in MANET turns into dynamic optimization problem (DOP). Here the nodes ae made aware of the environmental condition, thereby making it intelligent, which goes as the input for GA. The implementation then uses GAs with immigrants and memory schemes to solve the dynamic SP routing problem (DSPRP) in MANETS. In our paper, once the network topology changes, the optimal solutions in the new environment can be searched using the new immigrants or the useful information stored in the memory. Results shows GA with new immigrants shows better convergence result than GA with memory scheme.
A Packet Scheduling Strategy in Sensor Networks with SGMH Protocol
Venue: arXiv cs.NI 2011
Year: 2011

Data communication in sensor networks can have timing constraints like end to end deadlines. If the deadlines are not met either a catastrophe can happen in hard real time systems or performance deterioration can occur in soft real time systems. In real time sensor networks, the recovery of data through retransmission should be minimized due to the stringent requirements on the worst case time delays. This paper presents the application of Stop and Go Multihop protocol (SGMH) at node level in wireless sensor networks for scheduling and hence to meet the hard real time routing requirements. SGMH is a distributed multihop packet delivery algorithm. The fractions of the total available bandwidth on each channel is assigned to several traffic classes by which the time it takes to traverse each of the hops from the source to the destination is bounded. It is based on the notion of time frames (Tfr). In sensor networks packets can have different delay guarantees. Multiple frame sizes can be assigned for different traffic classes.
Stegobot: construction of an unobservable communication network leveraging social behavior
Venue: arXiv cs.CR 2011
Year: 2011

We propose the construction of an unobservable communications network using social networks. The communication endpoints are vertices on a social network. Probabilistically unobservable communication channels are built by leveraging image steganography and the social image sharing behavior of users. All communication takes place along the edges of a social network overlay connecting friends. We show that such a network can provide decent bandwidth even with a far from optimal routing mechanism such as restricted flooding. We show that such a network is indeed usable by constructing a botnet on top of it, called Stegobot. It is designed to spread via social malware attacks and steal information from its victims. Unlike conventional botnets, Stegobot traffic does not introduce new communication endpoints between bots. We analyzed a real-world dataset of image sharing between members of an online social network. Analysis of Stegobot's network throughput indicates that stealthy as it is, it is also functionally powerful -- capable of channeling fair quantities of sensitive data from its victims to the botmaster at tens of megabytes every month.
Rule-based query answering method for a knowledge base of economic crimes
Venue: arXiv cs.AI 2011
Year: 2011

We present a description of the PhD thesis which aims to propose a rule-based query answering method for relational data. In this approach we use an additional knowledge which is represented as a set of rules and describes the source data at concept (ontological) level. Queries are posed in the terms of abstract level. We present two methods. The first one uses hybrid reasoning and the second one exploits only forward chaining. These two methods are demonstrated by the prototypical implementation of the system coupled with the Jess engine. Tests are performed on the knowledge base of the selected economic crimes: fraudulent disbursement and money laundering.
Interference Focusing for Simplified Optical Fiber Models with Dispersion
Venue: arXiv cs.IT 2011
Year: 2011

A discrete-time two-user interference channel model is developed that captures non-linear phenomena that arise in optical fiber communication employing wavelength-division multiplexing (WDM). The effect of non-linearity is that an amplitude variation on one carrier induces a phase variation on the other carrier. Moreover, the model captures the effect of group velocity mismatch that introduces memory in the channel. It is shown that both users can achieve the maximum pre-log factor of 1 simultaneously by using an interference focusing technique introduced in an earlier work.
Bidimensionality and Geometric Graphs
Venue: arXiv cs.DS 2011
Year: 2011

In this paper we use several of the key ideas from Bidimensionality to give a new generic approach to design EPTASs and subexponential time parameterized algorithms for problems on classes of graphs which are not minor closed, but instead exhibit a geometric structure. In particular we present EPTASs and subexponential time parameterized algorithms for Feedback Vertex Set, Vertex Cover, Connected Vertex Cover, Diamond Hitting Set, on map graphs and unit disk graphs, and for Cycle Packing and Minimum-Vertex Feedback Edge Set on unit disk graphs. Our results are based on the recent decomposition theorems proved by Fomin et al [SODA 2011], and our algorithms work directly on the input graph. Thus it is not necessary to compute the geometric representations of the input graph. To the best of our knowledge, these results are previously unknown, with the exception of the EPTAS and a subexponential time parameterized algorithm on unit disk graphs for Vertex Cover, which were obtained by Marx [ESA 2005] and Alber and Fiala [J. Algorithms 2004], respectively. We proceed to show that our approach can not be extended in its full generality to more general classes of geometric graphs, such as intersection graphs of unit balls in R^d, d >= 3. Specifically we prove that Feedback Vertex Set on unit-ball graphs in R^3 neither admits PTASs unless P=NP, nor subexponential time algorithms unless the Exponential Time Hypothesis fails. Additionally, we show that the decomposition theorems which our approach is based on fail for disk graphs and that therefore any extension of our results to disk graphs would require new algorithmic ideas. On the other hand, we prove that our EPTASs and subexponential time algorithms for Vertex Cover and Connected Vertex Cover carry over both to disk graphs and to unit-ball graphs in R^d for every fixed d.
Scaling Behavior of Convolutional LDPC Ensembles over the BEC
Venue: arXiv cs.IT 2011
Year: 2011

We study the scaling behavior of coupled sparse graph codes over the binary erasure channel. In particular, let 2L+1 be the length of the coupled chain, let M be the number of variables in each of the 2L + 1 local copies, let l be the number of iterations, let Pb denote the bit error probability, and let ε denote the channel parameter. We are interested in how these quantities scale when we let the blocklength (2L + 1)M tend to infinity. Based on empirical evidence we show that the threshold saturation phenomenon is rather stable with respect to the scaling of the various parameters and we formulate some general rules of thumb which can serve as a guide for the design of coding systems based on coupled graphs.