OpenRaiser/Intern-Atlas huggingface dataset:
Early recurrence enables figure border ownership
Venue: arXiv cs.CV 2019
Year: 2019

The face-vase illusion introduced by Rubin demonstrates how one can switch back and forth between two different interpretations depending on how the figure outlines are assigned [1]. This border ownership assignment is an important step in the perception of forms. Zhou et al. [2] found neurons in the visual cortex whose responses not only depend on the local features present in their classical receptive fields, but also on their contextual information. Various models proposed that feedback from higher ventral areas or lateral connections could provide the required contextual information. However, some studies [3, 4, 5] ruled out the plausibility of models exclusively based on lateral connections. In addition, further evidence [6] suggests that ventral feedback even from V4 is not fast enough to provide context to border ownership neurons in either V1 or V2. As a result, the border ownership assignment mechanism in the brain is a mystery yet to be solved. Here, we test with computational simulations the hypothesis that the dorsal stream provides the global information to border ownership cells in the ventral stream. Our proposed model incorporates early recurrence from the dorsal pathway as well as lateral modulations within the ventral stream. Our simulation experiments show that our model border ownership neurons, similar to their biological counterparts, exhibit different responses to figures on either side of the border.
The Capacity Achieving Distribution for the Amplitude Constrained Additive Gaussian Channel: An Upper Bound on the Number of Mass Points
Venue: arXiv cs.IT 2019
Year: 2019

This paper studies an $n$-dimensional additive Gaussian noise channel with a peak-power-constrained input. It is well known that, in this case, when $n=1$ the capacity-achieving input distribution is discrete with finitely many mass points, and when $n>1$ the capacity-achieving input distribution is supported on finitely many concentric shells. However, due to the previous proof technique, neither the exact number of mass points/shells of the optimal input distribution nor a bound on it was available. This paper provides an alternative proof of the finiteness of the number mass points/shells of the capacity-achieving input distribution and produces the first firm bounds on the number of mass points and shells, paving an alternative way for approaching many such problems. Roughly, the paper consists of three parts. The first part considers the case of $n=1$. The first result, in this part, shows that the number of mass points in the capacity-achieving input distribution is within a factor of two from the downward shifted capacity-achieving output probability density function (pdf). The second result, by showing a bound on the number of zeros of the downward shifted capacity-achieving output pdf, provides a first firm upper on the number of mass points. Specifically, it is shown that the number of mass points is given by $O(\mathsf{A}^2)$ where $\mathsf{A}$ is the constraint on the input amplitude. The second part generalizes the results of the first part to the case of $n>1$. In particular, for every dimension $n>1$, it is shown that the number of shells is given by $O(\mathsf{A}^2)$ where $\mathsf{A}$ is the constraint on the input amplitude. Finally, the third part provides bounds on the number of points for the case of $n=1$ with an additional power constraint.
FireLedger: A High Throughput Blockchain Consensus Protocol
Venue: arXiv cs.DC 2019
Year: 2019

Blockchains are distributed secure ledgers to which transactions are issued continuously and each block of transactions is tightly coupled to its predecessors. Permissioned blockchains place special emphasis on transactions throughput. In this paper we present FireLedger, which leverages the iterative nature of blockchains in order to improve their throughput in optimistic execution scenarios. FireLedger trades latency for throughput in the sense that in FireLedger the last f + 1 blocks of each node's blockchain are considered tentative, i.e., they may be rescinded in case one of the last f + 1 blocks proposers was Byzantine. Yet, when optimistic assumptions are met, a new block is decided in each communication step, which consists of a proposer that sends only its proposal and all other participants are sending a single bit each. Our performance study demonstrates that in a single Amazon data-center, FireLedger running on 10 mid-range Amazon nodes obtains a throughput of up to 160K transactions per second for (typical Bitcoin size) 512 bytes transactions. In a 10 nodes Amazon geo-distributed setting with 512 bytes transactions, FireLedger obtains a throughput of 30K tps. Moreover, on higher end Amazon machines, FireLedger obtains $20%-600%$ better throughput than state of the art protocols like HotStuff and BFT-SMaRt, depending on the exact configuration.
Robotics Evolution: from Remote Brain to Cloud
Venue: arXiv cs.RO 2019
Year: 2019

Robotic systems have been evolving since decades and touching almost all aspects of life, either for leisure or critical applications. Most of traditional robotic systems operate in well-defined environments utilizing pre-configured on-board processing units. However, modern and foreseen robotic applications ask for complex processing requirements that exceed the limits of on-board computing power. Cloud computing and the related technologies have high potential to overcome on-board hardware restrictions and can improve the performance efficiency. This research highlights the advancements in robotic systems with focus on cloud robotics as an emerging trend. There exists an extensive amount of effort to leverage the potentials of robotic systems and to handle arising shortcomings. Moreover, there are promising insights for future breed of intelligent, flexible, and autonomous robotic systems in the Internet of Things era.
Incentive-based integration of useful work into blockchains
Venue: arXiv cs.CR 2019
Year: 2019

Blockchains have recently gained popularity thanks to their ability to record "digital truth". They are designed to keep persistence, security, and avoid attacks which is useful for many applications. However, they are still problematic in their energy consumption, governance, and scalability Current solutions either require vast computing power via Proof-of-Work (PoW) or cannot directly utilize computing power as a resource in virtual mining. Here, we propose incentive-based protocols that use competitions to integrate computing power into blockchains. We introduce Proof-of-Accumulated-Work (PoAW): miners compete in costumer-submitted jobs, accumulate recorded work whenever they are successful, and, over time, are remunerated. The underlying competition replaces the standard hash puzzle-based competitions of PoW. A competition is managed by a dynamically-created small masternode network (dTMN) of invested miners. dTMNs allow for scalability as we do not need the entire network to manage the competition. Using careful design on incentives, our system preserves security, avoids attacks, and offers new markets to miners. When there are no costumers the system converges into a standard protocol. Our proposed solution improves the way by which the blockchain infrastructure works and makes use of its computing power. We also discuss how the protocol can be used by fields that require solving difficult optimization problems, such as Artificial Intelligence and Pattern Recognition in Big Data.
Cocon: Computation in Contextual Type Theory
Venue: arXiv cs.PL 2019
Year: 2019

We describe a Martin-Löf style dependent type theory, called Cocon, that allows us to mix the intensional function space that is used to represent higher-order abstract syntax (HOAS) trees with the extensional function space that describes (recursive) computations. We mediate between HOAS representations and computations using contextual modal types. Our type theory also supports an infinite hierarchy of universes and hence supports type-level computation -- thereby providing metaprogramming and (small-scale) reflection. Our main contribution is the development of a Kripke-style model for Cocon that allows us to prove normalization. From the normalization proof, we derive subject reduction and consistency. Our work lays the foundation to incorporate the methodology of logical frameworks into systems such as Agda and bridges the longstanding gap between these two worlds.
Large Scale Studies of Memory, Storage, and Network Failures in a Modern Data Center
Venue: arXiv cs.DC 2019
Year: 2019

The workloads running in the modern data centers of large scale Internet service providers (such as Amazon, Baidu, Facebook, Google, and Microsoft) support billions of users and span globally distributed infrastructure. Yet, the devices used in modern data centers fail due to a variety of causes, from faulty components to bugs to misconfiguration. Faulty devices make operating large scale data centers challenging because the workloads running in modern data centers consist of interdependent programs distributed across many servers, so failures that are isolated to a single device can still have a widespread effect on a workload. In this dissertation, we measure and model the device failures in a large scale Internet service company, Facebook. We focus on three device types that form the foundation of Internet service data center infrastructure: DRAM for main memory, SSDs for persistent storage, and switches and backbone links for network connectivity. For each of these device types, we analyze long term device failure data broken down by important device attributes and operating conditions, such as age, vendor, and workload. We also build and release statistical models to examine the failure trends for the devices we analyze. Our key conclusion in this dissertation is that we can gain a deep understanding of why devices fail---and how to predict their failure---using measurement and modeling. We hope that the analysis, techniques, and models we present in this dissertation will enable the community to better measure, understand, and prepare for the hardware reliability challenges we face in the future.
Deep Learning for Anomaly Detection: A Survey
Venue: arXiv cs.LG 2019
Year: 2019

Anomaly detection is an important problem that has been well-studied within diverse research areas and application domains. The aim of this survey is two-fold, firstly we present a structured and comprehensive overview of research methods in deep learning-based anomaly detection. Furthermore, we review the adoption of these methods for anomaly across various application domains and assess their effectiveness. We have grouped state-of-the-art research techniques into different categories based on the underlying assumptions and approach adopted. Within each category we outline the basic anomaly detection technique, along with its variants and present key assumptions, to differentiate between normal and anomalous behavior. For each category, we present we also present the advantages and limitations and discuss the computational complexity of the techniques in real application domains. Finally, we outline open issues in research and challenges faced while adopting these techniques.
Towards platform-independent specification and verification of the standard trigonometry functions
Venue: arXiv cs.LO 2019
Year: 2019

Research project "Platform-independent approach to formal specification and verification of standard mathematical functions" is aimed onto a development of an incremental combined approach to the specification and verification of the standard mathematical functions like sqrt, cos, sin, etc. Platform-independence means that we attempt to design a relatively simple axiomatization of the computer arithmetic in terms of real, rational, and integer arithmetic (i.e. the fields R and Q of real and rational numbers, the ring Z of integers) but don't specify neither base of the computer arithmetic, nor a format of numbers' representation. Incrementality means that we start with the most straightforward specification of the simplest easy to verify algorithm in real numbers and finish with a realistic specification and a verification of an algorithm in computer arithmetic. We call our approach combined because we start with a manual (pen-and-paper) verification of some selected algorithm in real numbers, then use these algorithm and verification as a draft and proof-outlines for the algorithm in computer arithmetic and its manual verification, and finish with a computer-aided validation of our manual proofs with some proof-assistant system (to avoid appeals to "obviousness" that are very common in human-carried proofs). In the paper we present first steps towards a platform-independent incremental combined approach to specification and verification of the standard functions cos and sin that implement mathematical trigonometric functions cos and sin.
Segmentation of Levator Hiatus Using Multi-Scale Local Region Active contours and Boundary Shape Similarity Constraint
Venue: arXiv cs.CV 2019
Year: 2019

In this paper, a multi-scale framework with local region based active contour and boundary shape similarity constraint is proposed for the segmentation of levator hiatus in ultrasound images. In this paper, we proposed a multiscale active contour framework to segment levator hiatus ultrasound images by combining the local region information and boundary shape similarity constraint. In order to get more precisely initializations and reduce the computational cost, Gaussian pyramid method is used to decompose the image into coarse-to-fine scales. A localized region active contour model is firstly performed on the coarsest scale image to get a rough contour of the levator hiatus, then the segmentation result on the coarse scale is interpolated into the finer scale image as the initialization. The boundary shape similarity between different scales is incorporate into the local region based active contour model so that the result from coarse scale can guide the contour evolution at finer scale. By incorporating the multi-scale and boundary shape similarity, the proposed method can precisely locate the levator hiatus boundaries despite various ultrasound image artifacts. With a data set of 90 levator hiatus ultrasound images, the efficiency and accuracy of the proposed method are validated by quantitative and qualitative evaluations (TP, FP, Js) and comparison with other two state-of-art active contour segmentation methods (C-V model, DRLSE model).
PiNcH: an Effective, Efficient, and Robust Solution to Drone Detection via Network Traffic Analysis
Venue: arXiv cs.CR 2019
Year: 2019

We propose PiNcH, a methodology to detect the presence of a drone, its current status, and its movements by leveraging just the communication traffic exchanged between the drone and its Remote Controller (RC). PiNcH is built applying standard classification algorithms to the eavesdropped traffic, analyzing features such as packets inter-arrival time and size. PiNcH is fully passive and it requires just cheap and general-purpose hardware. To evaluate the effectiveness of our solution, we collected real communication traces originated by a drone running the widespread ArduCopter open-source firmware, currently mounted on-board of a wide range (30+) of commercial amateur drones. We tested our solution against different publicly available wireless traces. The results prove that PiNcH can efficiently and effectively: (i) identify the presence of the drone in several heterogeneous scenarios; (ii) identify the current state of a powered-on drone, i.e., flying or lying on the ground; (iii) discriminate the movements of the drone; and, finally, (iv) enjoy a reduced upper bound on the time required to identify a drone with the requested level of assurance. The effectiveness of PiNcH has been also evaluated in the presence of both heavy packet loss and evasion attacks. In this latter case, the adversary modifies on purpose the profile of the traffic of the drone-RC link to avoid the detection. In both the cited cases, PiNcH continues enjoying a remarkable performance. Further, the comparison against state of the art solution confirms the superior performance of PiNcH in several scenarios. Note that all the drone-controller generated data traces have been released as open-source, to allow replicability and foster follow-up. Finally, the quality and viability of our solution, do prove that network traffic analysis can be successfully adopted for drone identification and status discrimination.
Somatic Practices for Understanding Real, Imagined, and Virtual Realities
Venue: arXiv cs.HC 2019
Year: 2019

In most VR experiences, the visual sense dominates other modes of sensory input, encouraging non-visual senses to respond as if the visual were real. The simulated visual world thus becomes a sort of felt actuality, where the 'actual' physical body and environment can 'drop away', opening up possibilities for designing entirely new kinds of experience. Most VR experiences place visual sensory input (of the simulated environment) in the perceptual foreground, and the physical body in the background. In what follows, we discuss methods for resolving the apparent tension which arises from VR's prioritization of visual perception. We specifically aim to understand how somatic techniques encouraging participants to 'attend to their attention' enable them to access more subtle aspects of sensory phenomena in a VR experience, bound neither by rigid definitions of vision-based virtuality nor body-based corporeality. During a series of workshops, we implemented experimental somatic-dance practices to better understand perceptual and imaginative subtleties that arise for participants whilst they are embedded in a multi-person VR framework. Our preliminary observations suggest that somatic methods can be used to design VR experiences which enable (i) a tactile quality or felt sense of phenomena in the virtual environment (VE), (ii) lingering impacts on participant imagination even after the VR headset is taken off, and (iii) an expansion of imaginative potential.
OFDMA-based DF Secure Cooperative Communication with Untrusted Users
Venue: arXiv cs.IT 2019
Year: 2019

In this letter we consider resource allocation for OFDMA-based secure cooperative communication by employing a trusted Decode and Forward (DF) relay among the untrusted users. We formulate two optimization problems, namely, (i) sum rate maximization subject to individual power constraints on source and relay, and (ii) sum power minimization subject to a fairness constraint in terms of per-user minimum support secure rate requirement. The optimization problems are solved utilizing the optimality of KKT conditions for pseudolinear functions.
ACMiner: Extraction and Analysis of Authorization Checks in Android's Middleware
Venue: arXiv cs.CR 2019
Year: 2019

Billions of users rely on the security of the Android platform to protect phones, tablets, and many different types of consumer electronics. While Android's permission model is well studied, the enforcement of the protection policy has received relatively little attention. Much of this enforcement is spread across system services, taking the form of hard-coded checks within their implementations. In this paper, we propose Authorization Check Miner (ACMiner), a framework for evaluating the correctness of Android's access control enforcement through consistency analysis of authorization checks. ACMiner combines program and text analysis techniques to generate a rich set of authorization checks, mines the corresponding protection policy for each service entry point, and uses association rule mining at a service granularity to identify inconsistencies that may correspond to vulnerabilities. We used ACMiner to study the AOSP version of Android 7.1.1 to identify 28 vulnerabilities relating to missing authorization checks. In doing so, we demonstrate ACMiner's ability to help domain experts process thousands of authorization checks scattered across millions of lines of code.
Coded Distributed Computing over Packet Erasure Channels
Venue: arXiv cs.IT 2019
Year: 2019

Coded computation is a framework which provides redundancy in distributed computing systems to speed up largescale tasks. Although most existing works assume an error-free scenarios in a master-worker setup, the link failures are common in current wired/wireless networks. In this paper, we consider the straggler problem in coded distributed computing with link failures, by modeling the links between the master node and worker nodes as packet erasure channels. When the master fails to detect the received signal, retransmission is required for each worker which increases the overall run-time to finish the task. We first investigate the expected overall run-time in this setting using an (n; k) maximum distance separable (MDS) code. We obtain the lower and upper bounds on the latency in closed-forms and give guidelines to design MDS code depending on the packet erasure probability. Finally, we consider a setup where the number of retransmissions is limited due to the bandwidth constraint. By formulating practical optimization problems related to latency, transmission bandwidth and probability of successful computation, we obtain achievable performance curves as a function of packet erasure probability.
Subcarrier Pairing as Channel Gain Tailoring: Joint Resource Allocation for Relay-Assisted Secure OFDMA with Untrusted Users
Venue: arXiv cs.IT 2019
Year: 2019

Joint resource allocation involving optimization of subcarrier allocation, subcarrier pairing (SCP), and power allocation in a cooperative secure orthogonal frequency division multiple access (OFDMA) communication system with untrusted users is considered. Both amplify and forward (AF), and decode and forward (DF) modes of operations are considered with individual power budget constraints for source and relay. After finding optimal subcarrier allocation for an AF relayed system, we prove the joint power allocation as a generalized convex problem, and solve it optimally. Compared to the conventional channel gain matching view, the optimal SCP is emphasized as a novel concept of channel gain tailoring. We prove that the optimal SCP pairs subcarriers such that the variance among the effective channel gains is minimized. For a DF relayed system, we show that depending on the power budgets of source and relay, SCP can either be in a subordinate role where it improves the energy efficiency, or in a main role where it improves the spectral efficiency of the system. In an AF relayed system we confirm that SCP plays a crucial role, and improves the spectral efficiency of the system. The channel gain tailoring property of SCP, various roles of SCP in improving the spectral and the energy efficiency of a cooperative communication system are validated with the help of simulation results.
SPFlow: An Easy and Extensible Library for Deep Probabilistic Learning using Sum-Product Networks
Venue: arXiv cs.LG 2019
Year: 2019

We introduce SPFlow, an open-source Python library providing a simple interface to inference, learning and manipulation routines for deep and tractable probabilistic models called Sum-Product Networks (SPNs). The library allows one to quickly create SPNs both from data and through a domain specific language (DSL). It efficiently implements several probabilistic inference routines like computing marginals, conditionals and (approximate) most probable explanations (MPEs) along with sampling as well as utilities for serializing, plotting and structure statistics on an SPN. Moreover, many of the algorithms proposed in the literature to learn the structure and parameters of SPNs are readily available in SPFlow. Furthermore, SPFlow is extremely extensible and customizable, allowing users to promptly distill new inference and learning routines by injecting custom code into a lightweight functional-oriented API framework. This is achieved in SPFlow by keeping an internal Python representation of the graph structure that also enables practical compilation of an SPN into a TensorFlow graph, C, CUDA or FPGA custom code, significantly speeding-up computations.