OpenRaiser/Intern-Atlas huggingface dataset:
Towards the Automated Verification of Cyber-Physical Security Protocols: Bounding the Number of Timed Intruders
Venue: arXiv cs.CR 2016
Year: 2016

Timed Intruder Models have been proposed for the verification of Cyber-Physical Security Protocols (CPSP) amending the traditional Dolev-Yao intruder to obey the physical restrictions of the environment. Since to learn a message, a Timed Intruder needs to wait for a message to arrive, mounting an attack may depend on where Timed Intruders are. It may well be the case that in the presence of a great number of intruders there is no attack, but there is an attack in the presence of a small number of well placed intruders. Therefore, a major challenge for the automated verification of CPSP is to determine how many Timed Intruders to use and where should they be placed. This paper answers this question by showing it is enough to use the same number of Timed Intruders as the number of participants. We also report on some preliminary experimental results in discovering attacks in CPSP.
Dialogue Concerning The Two Chief World Views
Venue: arXiv cs.GL 2016
Year: 2016

In 1632, Galileo Galilei wrote a book called \textit{Dialogue Concerning the Two Chief World Systems} which compared the new Copernican model of the universe with the old Ptolemaic model. His book took the form of a dialogue between three philosophers, Salviati, a proponent of the Copernican model, Simplicio, a proponent of the Ptolemaic model, and Sagredo, who was initially open-minded and neutral. In this paper, I am going to use Galileo's idea to present a dialogue between three modern philosophers, Mr. Spock, a proponent of the view that $\mathsf{P} \neq \mathsf{NP}$, Professor Simpson, a proponent of the view that $\mathsf{P} = \mathsf{NP}$, and Judge Wapner, who is initially open-minded and neutral.
TensorFlow: A system for large-scale machine learning
Venue: arXiv cs.DC 2016
Year: 2016

TensorFlow is a machine learning system that operates at large scale and in heterogeneous environments. TensorFlow uses dataflow graphs to represent computation, shared state, and the operations that mutate that state. It maps the nodes of a dataflow graph across many machines in a cluster, and within a machine across multiple computational devices, including multicore CPUs, general-purpose GPUs, and custom designed ASICs known as Tensor Processing Units (TPUs). This architecture gives flexibility to the application developer: whereas in previous "parameter server" designs the management of shared state is built into the system, TensorFlow enables developers to experiment with novel optimizations and training algorithms. TensorFlow supports a variety of applications, with particularly strong support for training and inference on deep neural networks. Several Google services use TensorFlow in production, we have released it as an open-source project, and it has become widely used for machine learning research. In this paper, we describe the TensorFlow dataflow model in contrast to existing systems, and demonstrate the compelling performance that TensorFlow achieves for several real-world applications.
Remixing as a Pathway to Computational Thinking
Venue: arXiv cs.CY 2016
Year: 2016

Theorists and advocates of "remixing" have suggested that appropriation can act as a pathway for learning. We test this theory quantitatively using data from more than 2.4 million multimedia programming projects shared by more than 1 million users in the Scratch online community. First, we show that users who remix more often have larger repertoires of programming commands even after controlling for the numbers of projects and amount of code shared. Second, we show that exposure to computational thinking concepts through remixing is associated with increased likelihood of using those concepts. Our results support theories that young people learn through remixing, and have important implications for designers of social computing systems.
Bridging the Capacity Gap Between Interactive and One-Way Communication
Venue: arXiv cs.IT 2016
Year: 2016

We study the communication rate of coding schemes for interactive communication that transform any two-party interactive protocol into a protocol that is robust to noise. Recently, Haeupler (FOCS '14) showed that if an $ε> 0$ fraction of transmissions are corrupted, adversarially or randomly, then it is possible to achieve a communication rate of $1 - \widetilde{O}(\sqrtε)$. Furthermore, Haeupler conjectured that this rate is optimal for general input protocols. This stands in contrast to the classical setting of one-way communication in which error-correcting codes are known to achieve an optimal communication rate of $1 - Θ(H(ε)) = 1 - \widetildeΘ(ε)$. In this work, we show that the quadratically smaller rate loss of the one-way setting can also be achieved in interactive coding schemes for a very natural class of input protocols. We introduce the notion of average message length, or the average number of bits a party sends before receiving a reply, as a natural parameter for measuring the level of interactivity in a protocol. Moreover, we show that any protocol with average message length $\ell = Ω(\mathrm{poly}(1/ε))$ can be simulated by a protocol with optimal communication rate $1 - Θ(H(ε))$ over an oblivious adversarial channel with error fraction $ε$. Furthermore, under the additional assumption of access to public shared randomness, the optimal communication rate is achieved ratelessly, i.e., the communication rate adapts automatically to the actual error rate $ε$ without having to specify it in advance. This shows that the capacity gap between one-way and interactive communication can be bridged even for very small (constant in $ε$) average message lengths, which are likely to be found in many applications.
Data-driven software security: Models and methods
Venue: arXiv cs.CR 2016
Year: 2016

For computer software, our security models, policies, mechanisms, and means of assurance were primarily conceived and developed before the end of the 1970's. However, since that time, software has changed radically: it is thousands of times larger, comprises countless libraries, layers, and services, and is used for more purposes, in far more complex ways. It is worthwhile to revisit our core computer security concepts. For example, it is unclear whether the Principle of Least Privilege can help dictate security policy, when software is too complex for either its developers or its users to explain its intended behavior. This paper outlines a data-driven model for software security that takes an empirical, data-driven approach to modern software, and determines its exact, concrete behavior via comprehensive, online monitoring. Specifically, this paper briefly describes methods for efficient, detailed software monitoring, as well as methods for learning detailed software statistics while providing differential privacy for its users, and, finally, how machine learning methods can help discover users' expectations for intended software behavior, and thereby help set security policy. Those methods can be adopted in practice, even at very large scales, and demonstrate that data-driven software security models can provide real-world benefits.
Computational Estimate Visualisation and Evaluation of Agent Classified Rules Learning System
Venue: arXiv cs.CY 2016
Year: 2016

Student modelling and agent classified rules learning as applied in the development of the intelligent Preassessment System has been presented in [10],[11]. In this paper, we now demystify the theory behind the development of the pre-assessment system followed by some computational experimentation and graph visualisation of the agent classified rules learning algorithm in the estimation and prediction of classified rules. In addition, we present some preliminary results of the pre-assessment system evaluation. From the results, it is gathered that the system has performed according to its design specification.
Reimagining the Living Room
Venue: arXiv cs.CY 2016
Year: 2016

An attempt to seek out and understand emerging trends and some of the challenges we face when dealing with an increasing amount and complexity of entertainment technologies in our homes, particularly in spaces that are both private and public. Accepting the premise that this influx of technologies will continue, the author identified some of the challenges that consumers, manufacturers, distributors and creators of content are facing today in incorporating these technologies into home life. Anticipating an imminent transformation, the author proposes a new approach to smart homes and an updated model for content distribution.
Optimal Scalar Linear Index Codes for One-Sided Neighboring Side-Information Problems
Venue: arXiv cs.IT 2016
Year: 2016

The capacity of symmetric instance of the multiple unicast index coding problem with neighboring antidotes (side-information) with number of messages equal to the number of receivers was given by Maleki \textit{et al.} In this paper, we construct matrices of size $ m \times n (m \geq n)$ over $F_q$ such that any $n$ adjacent rows of the matrix are linearly independent. By using such matrices, we give an optimal scalar linear index codes over $F_q$ for the symmetric one-sided antidote problems considered by Maleki \textit{et al.} for any given number of messages and one-sided antidotes. The constructed codes are independent of field size and hence works over every field.
A Self-Managed Architecture for Sensor Networks Based on Real Time Data Analysis
Venue: arXiv cs.SY 2016
Year: 2016

Wireless sensor networks (WSNs) have been adopted as merely data producers for years. However, the data collected by WSNs can also be used to manage their operation and avoid unnecessary measurements that do not provide any new knowledge about the environment. The benefits are twofold because wireless sensor nodes may save their limited energy resources and also reduce the wireless medium occupancy. We present a self-managed platform that collects and stores data from sensor nodes, analyzes its contents and uses the built knowledge to adjust the operation of the entire network. The system architecture facilitates the incorporation of traditional WSNs into the Internet of Things by abstracting the lower communication layers and allowing decisions based on the data relevance. Finally, we demonstrate the platform optimizing a WSN's operation at runtime, based on different real-time data analysis.
Semi-supervised Zero-Shot Learning by a Clustering-based Approach
Venue: arXiv cs.CV 2016
Year: 2016

In some of object recognition problems, labeled data may not be available for all categories. Zero-shot learning utilizes auxiliary information (also called signatures) describing each category in order to find a classifier that can recognize samples from categories with no labeled instance. In this paper, we propose a novel semi-supervised zero-shot learning method that works on an embedding space corresponding to abstract deep visual features. We seek a linear transformation on signatures to map them onto the visual features, such that the mapped signatures of the seen classes are close to labeled samples of the corresponding classes and unlabeled data are also close to the mapped signatures of one of the unseen classes. We use the idea that the rich deep visual features provide a representation space in which samples of each class are usually condensed in a cluster. The effectiveness of the proposed method is demonstrated through extensive experiments on four public benchmarks improving the state-of-the-art prediction accuracy on three of them.
A survey of systems for massive stream analytics
Venue: arXiv cs.DC 2016
Year: 2016

The immense growth of data demands switching from traditional data processing solutions to systems, which can process a continuous stream of real time data. Various applications employ stream processing systems to provide solutions to emerging Big Data problems. Open-source solutions such as Storm, Spark Streaming, and S4 are the attempts to answer key stream processing questions. The recent introduction of real time stream processing commercial solutions such as Amazon Kinesis, IBM Infosphere Stream reflect industry requirements. The system and application related challenges to handle massive stream of real time data analytics are an active field of research. In this paper, we present a comparative analysis of the existing state-of-the-art stream processing solutions. We also include various application domains, which are transforming their business model to benefit from these large scale stream processing systems.
Network Resource Sharing Games with Instantaneous Reciprocity
Venue: arXiv cs.GT 2016
Year: 2016

We propose a generic strategic network resource sharing game between a set of players representing operators. The players negotiate which sets of players share given resources, serving users with varying sensitivity to interference. We prove that the proposed game has a Nash equilibrium, to which a greedily played game converges. Furthermore, simulation results show that, when applied to inter-operator spectrum sharing in small-cell indoor office environment, the convergence is fast and there is a significant performance improvement for the operators when compared to the default resource usage configuration.
Going Deeper for Multilingual Visual Sentiment Detection
Venue: arXiv cs.MM 2016
Year: 2016

This technical report details several improvements to the visual concept detector banks built on images from the Multilingual Visual Sentiment Ontology (MVSO). The detector banks are trained to detect a total of 9,918 sentiment-biased visual concepts from six major languages: English, Spanish, Italian, French, German and Chinese. In the original MVSO release, adjective-noun pair (ANP) detectors were trained for the six languages using an AlexNet-styled architecture by fine-tuning from DeepSentiBank. Here, through a more extensive set of experiments, parameter tuning, and training runs, we detail and release higher accuracy models for detecting ANPs across six languages from the same image pool and setting as in the original release using a more modern architecture, GoogLeNet, providing comparable or better performance with reduced network parameter cost. In addition, since the image pool in MVSO can be corrupted by user noise from social interactions, we partitioned out a sub-corpus of MVSO images based on tag-restricted queries for higher fidelity labels. We show that as a result of these higher fidelity labels, higher performing AlexNet-styled ANP detectors can be trained using the tag-restricted image subset as compared to the models in full corpus. We release all these newly trained models for public research use along with the list of tag-restricted images from the MVSO dataset.
Feature Extraction from Segmentations of Neuromuscular Junctions
Venue: arXiv cs.CG 2016
Year: 2016

Segmentations are often necessary for the analysis of image data. They are used to identify different objects, for example cell nuclei, mitochondria, or complete cells in microscopic images. There might be features in the data, that cannot be detected by segmentation approaches directly, because they are not characterized by their texture of boundaries, which are properties most segmentation techniques rely on, but morphologically. In this report we will introduce our algorithm for the extraction of suchlike morphological features of segmented objects from segmentations of neuromuscular junctions and its interface for informed parameter tuning.
On the Fundamental Importance of Gauss-Newton in Motion Optimization
Venue: arXiv cs.RO 2016
Year: 2016

Hessian information speeds convergence substantially in motion optimization. The better the Hessian approximation the better the convergence. But how good is a given approximation theoretically? How much are we losing? This paper addresses that question and proves that for a particularly popular and empirically strong approximation known as the Gauss-Newton approximation, we actually lose very little--for a large class of highly expressive objective terms, the true Hessian actually limits to the Gauss-Newton Hessian quickly as the trajectory's time discretization becomes small. This result both motivates it's use and offers insight into computationally efficient design. For instance, traditional representations of kinetic energy exploit the generalized inertia matrix whose derivatives are usually difficult to compute. We introduce here a novel reformulation of rigid body kinetic energy designed explicitly for fast and accurate curvature calculation. Our theorem proves that the Gauss-Newton Hessian under this formulation efficiently captures the kinetic energy curvature, but requires only as much computation as a single evaluation of the traditional representation. Additionally, we introduce a technique that exploits these ideas implicitly using Cholesky decompositions for some cases when similar objective terms reformulations exist but may be difficult to find. Our experiments validate these findings and demonstrate their use on a real-world motion optimization system for high-dof motion generation.
Computing backup forwarding rules in Software-Defined Networks
Venue: arXiv cs.NI 2016
Year: 2016

The past century of telecommunications has shown that failures in networks are prevalent. Although much has been done to prevent failures, network nodes and links are bound to fail eventually. Failure recovery processes are therefore needed. Failure recovery is mainly influenced by (1) detection of the failure, and (2) circumvention of the detected failure. However, especially in SDNs where controllers recompute network state reactively, this leads to high delays. Hence, next to primary rules, backup rules should be installed in the switches to quickly detour traffic once a failure occurs. In this work, we propose algorithms for computing an all-to-all primary and backup network forwarding configuration that is capable of circumventing link and node failures. Omitting the high delay invoked by controller recomputation through preconfiguration, our proposal's recovery delay is close to the detection time which is significantly below the 50 ms rule of thumb. After initial recovery, we recompute network configuration to guarantee protection from future failures. Our algorithms use packet-labeling to guarantee correct and shortest detour forwarding. The algorithms and labeling technique allow packets to return to the primary path and are able to discriminate between link and node failures. The computational complexity of our solution is comparable to that of all-to-all-shortest paths computations. Our experimental evaluation on both real and generated networks shows that network configuration complexity highly decreases compared to classic disjoint paths computations. Finally, we provide a proof-of-concept OpenFlow controller in which our proposed configuration is implemented, demonstrating that it readily can be applied in production networks.
A Solver for a Theory of Strings and Bit-vectors
Venue: arXiv cs.LO 2016
Year: 2016

We present a solver for a many-sorted first-order quantifier-free theory $T_{w,bv}$ of string equations, string length represented as bit-vectors, and bit-vector arithmetic aimed at formal verification, automated testing, and security analysis of C/C++ applications. Our key motivation for building such a solver is the observation that existing string solvers are not efficient at modeling the string/bit-vector combination. Current approaches either reduce strings to bit-vectors and use a bit-vector solver as a backend, or model bit-vectors as natural numbers and use a solver for the combined theory of strings and natural numbers. Both these approaches are inefficient for different reasons. Modeling strings as bit-vectors destroys structure inherent in string equations thus missing opportunities for efficiently deciding such formulas, and modeling bit-vectors as natural numbers is known to be inefficient. Hence, there is a clear need for a solver that models strings and bit-vectors natively. Our solver Z3strBV is a decision procedure for the theory $T_{w,bv}$ combining solvers for bit-vector and string equations. We demonstrate experimentally that Z3strBV is significantly more efficient than reduction of string/bit-vector constraints to strings/natural numbers. Additionally, we prove decidability for the theory $T_{w,bv}$. We also propose two optimizations which can be adapted to other contexts. The first accelerates convergence on a consistent assignment of string lengths, and the second, dubbed library-aware SMT solving, fixes summaries for built-in string functions (e.g., {\tt strlen} in C/C++), which Z3strBV uses directly instead of analyzing the functions from scratch each time. Finally, we demonstrate experimentally that Z3strBV is able to detect nontrivial overflows in real-world system-level code, as confirmed against 7 security vulnerabilities from CVE and Mozilla database.
Psychologically based Virtual-Suspect for Interrogative Interview Training
Venue: arXiv cs.AI 2016
Year: 2016

In this paper, we present a Virtual-Suspect system which can be used to train inexperienced law enforcement personnel in interrogation strategies. The system supports different scenario configurations based on historical data. The responses presented by the Virtual-Suspect are selected based on the psychological state of the suspect, which can be configured as well. Furthermore, each interrogator's statement affects the Virtual-Suspect's current psychological state, which may lead the interrogation in different directions. In addition, the model takes into account the context in which the statements are made. Experiments with 24 subjects demonstrate that the Virtual-Suspect's behavior is similar to that of a human who plays the role of the suspect.
Efficiency of research performance and the glass researcher
Venue: arXiv cs.DL 2016
Year: 2016

Abramo and D'Angelo (in press) doubt the validity of established size-independent indicators measuring citation impact and plead in favor of measuring scientific efficiency (by using the Fractional Scientific Strength indicator). This note is intended to comment on some questionable and a few favorable approaches in the paper by Abramo and D'Angelo (in press).
Counting in One-Hop Beeping Networks
Venue: arXiv cs.DC 2016
Year: 2016

We consider networks of processes which interact with beeps. In the basic model defined by Cornejo and Kuhn, which we refer to as the $BL$ variant, processes can choose in each round either to beep or to listen. Those who beep are unable to detect simultaneous beeps. Those who listen can only distinguish between silence and the presence of at least one beep. Beeping models are weak in essence and even simple tasks may become difficult or unfeasible with them. In this paper, we address the problem of computing how many participants there are in a one-hop network: the {\em counting} problem. We first observe that no algorithm can compute this number with certainty in $BL$, whether the algorithm be deterministic or even randomised (Las Vegas). We thus consider the stronger variant where beeping nodes are able to detect simultaneous beeps, referred to as $B_{cd}L$ (for {\em collision detection}). We prove that at least $n$ rounds are necessary in $B_{cd}L$, and we present an algorithm whose running time is $O(n)$ rounds with high probability. Further experimental results show that its expected running time is less than $10n$. Finally, we discuss how this algorithm can be adapted in other beeping models. In particular, we show that it can be emulated in $BL$, at the cost of a logarithmic slowdown and of trading its Las Vegas nature (result certain, time uncertain) against Monte Carlo (time certain, result uncertain).