OpenRaiser/Intern-Atlas huggingface dataset:
The Third Offset and a Fifth Domain? Balancing Game-Changing Innovation and Cyber Risk Mitigation
Venue: arXiv cs.CY 2016
Year: 2016

Cyber has changed the scope of the national security mission and is placing new strains on our diplomatic, warfighting, legal, and economic/budgetary processes. Cybersecurity processes and techniques are increasingly critical to our warfighting missions, but they can also inhibit the pace and potential for high impact, game-changing innovation. Throughout its history, the Navy has shown the ability of innovation (in policy, process, and technology) to change the game when our security is on the line. We believe the Navy is capable of dramatically impacting not only the U.S. capabilities in cyber conflict and information operations, but also in cyber defense and information assurance, as well as cybersecurity for our society. While cyber risk management is challenging, the transition from DoD Information Assurance Certification and Accreditation Process (DIACAP) to the Risk Management Framework (RMF) has the potential to harmonize our cybersecurity efforts with our need (and demonstrated ability to provide) for game-changing strategies, tactics, and technologies. We offer a foundation for the foregoing assertions and recommendations on ways to encourage innovation in the context of effective cyber risk management.
An Analysis of Attacks on Blockchain Consensus
Venue: arXiv cs.CR 2016
Year: 2016

We present and validate a novel mathematical model of the blockchain mining process and use it to conduct an economic evaluation of the double-spend attack, which is fundamental to all blockchain systems. Our analysis focuses on the value of transactions that can be secured under a conventional double-spend attack, both with and without a concurrent eclipse attack. Our model quantifies the importance of several factors that determine the attack's success, including confirmation depth, attacker mining power, and any confirmation deadline set by the merchant. In general, the security of a transaction against a double-spend attack increases roughly logarithmically with the depth of the block, made easier by the increasing sum of coin turned-over (between individuals) in the blocks, but more difficult by the increasing proof of work required. In recent blockchain data, we observed a median block turnover value of 6 BTC. Based on this value, a merchant requiring a single confirmation is protected against only attackers that can increase the current mining power by 1% or less. However, similar analysis shows that a merchant that requires a much longer 72 confirmations (~12 hours) will eliminate all potential profit for any double-spend attacker adding mining power less than 40% of the current mining power.
On Fractional Linear Network Coding Solution of Multiple-Unicast Networks
Venue: arXiv cs.IT 2016
Year: 2016

It is known that there exists a multiple-unicast network which has a rate $1$ linear network coding solution if and only if the characteristic of the finite field belongs to a given finite or co-finite set of primes. In this paper, we show that for any non-zero positive rational number $\frac{k}{n}$, there exists a multiple-unicast network which has a rate $\frac{k}{n}$ fractional linear network coding solution if and only if the characteristic of the finite field belongs to a given finite or co-finite set of primes.
Savu: A Python-based, MPI Framework for Simultaneous Processing of Multiple, N-dimensional, Large Tomography Datasets
Venue: arXiv cs.DC 2016
Year: 2016

Diamond Light Source (DLS), the UK synchrotron facility, attracts scientists from across the world to perform ground-breaking x-ray experiments. With over 3000 scientific users per year, vast amounts of data are collected across the experimental beamlines, with the highest volume of data collected during tomographic imaging experiments. A growing interest in tomography as an imaging technique, has led to an expansion in the range of experiments performed, in addition to a growth in the size of the data per experiment. Savu is a portable, flexible, scientific processing pipeline capable of processing multiple, n-dimensional datasets in serial on a PC, or in parallel across a cluster. Developed at DLS, and successfully deployed across the beamlines, it uses a modular plugin format to enable experiment-specific processing and utilises parallel HDF5 to remove RAM restrictions. The Savu design, described throughout this paper, focuses on easy integration of existing and new functionality, flexibility and ease of use for users and developers alike.
Bounded Model Checking and Feature Omission Diversity
Venue: arXiv cs.SE 2016
Year: 2016

In this paper we introduce a novel way to speed up the discovery of counterexamples in bounded model checking, based on parallel runs over versions of a system in which features have been randomly disabled. As shown in previous work, adding constraints to a bounded model checking problem can reduce the size of the verification problem and dramatically decrease the time required to find counterexample. Adapting a technique developed in software testing to this problem provides a simple way to produce useful partial verification problems, with a resulting decrease in average time until a counterexample is produced. If no counterexample is found, partial verification results can also be useful in practice.
Efficient Polar Code Construction for Higher-Order Modulation
Venue: arXiv cs.IT 2016
Year: 2016

An efficient algorithm for the construction of polar codes for higher-order modulation is presented based on information-theoretic principles. The bit reliabilities after successive demapping are estimated using the LM-rate, an achievable rate for mismatched decoding. The successive demapper bit channels are then replaced by binary input Additive White Gaussian Noise (biAWGN) surrogate channels and polar codes are constructed using the Gaussian approximation (GA). This LM-rate Demapper GA (LM-DGA) construction is used to construct polar codes for several demapping strategies proposed in literature. For all considered demappers, the LM-DGA constructed polar codes have the same performance as polar codes constructed by Monte Carlo (MC) simulation. The proposed LM-DGA construction is much faster than the MC construction. For 64-QAM, spectral efficiency 3 bits/s/Hz, and block length 1536 bits, simulation results show that LM-DGA constructed polar codes with cyclic redundancy check and successive cancellation list decoding are 1 dB more power efficient than state-of-the-art AR4JA low-density parity-check codes.
Sound Probabilistic #SAT with Projection
Venue: arXiv cs.LO 2016
Year: 2016

We present an improved method for a sound probabilistic estimation of the model count of a boolean formula under projection. The problem solved can be used to encode a variety of quantitative program analyses, such as concerning security of resource consumption. We implement the technique and discuss its application to quantifying information flow in programs.
Logical Characterization of Bisimulation Metrics
Venue: arXiv cs.LO 2016
Year: 2016

Bisimulation metrics provide a robust and accurate approach to study the behavior of nondeterministic probabilistic processes. In this paper, we propose a logical characterization of bisimulation metrics based on a simple probabilistic variant of the Hennessy-Milner logic. Our approach is based on the novel notions of mimicking formulae and distance between formulae. The former are a weak version of the well known characteristic formulae and allow us to characterize also (ready) probabilistic simulation and probabilistic bisimilarity. The latter is a 1-bounded pseudometric on formulae that mirrors the Hausdorff and Kantorovich lifting the defining bisimilarity pseudometric. We show that the distance between two processes equals the distance between their own mimicking formulae.
MELA: Modelling in Ecology with Location Attributes
Venue: arXiv cs.LO 2016
Year: 2016

Ecology studies the interactions between individuals, species and the environment. The ability to predict the dynamics of ecological systems would support the design and monitoring of control strategies and would help to address pressing global environmental issues. It is also important to plan for efficient use of natural resources and maintenance of critical ecosystem services. The mathematical modelling of ecological systems often includes nontrivial specifications of processes that influence the birth, death, development and movement of individuals in the environment, that take into account both biotic and abiotic interactions. To assist in the specification of such models, we introduce MELA, a process algebra for Modelling in Ecology with Location Attributes. Process algebras allow the modeller to describe concurrent systems in a high-level language. A key feature of concurrent systems is that they are composed of agents that can progress simultaneously but also interact - a good match to ecological systems. MELA aims to provide ecologists with a straightforward yet flexible tool for modelling ecological systems, with particular emphasis on the description of space and the environment. Here we present four example MELA models, illustrating the different spatial arrangements which can be accommodated and demonstrating the use of MELA in epidemiological and predator-prey scenarios.
Word Embeddings and Their Use In Sentence Classification Tasks
Venue: arXiv cs.LG 2016
Year: 2016

This paper have two parts. In the first part we discuss word embeddings. We discuss the need for them, some of the methods to create them, and some of their interesting properties. We also compare them to image embeddings and see how word embedding and image embedding can be combined to perform different tasks. In the second part we implement a convolutional neural network trained on top of pre-trained word vectors. The network is used for several sentence-level classification tasks, and achieves state-of-art (or comparable) results, demonstrating the great power of pre-trainted word embeddings over random ones.
Things Bayes can't do
Venue: arXiv cs.LG 2016
Year: 2016

The problem of forecasting conditional probabilities of the next event given the past is considered in a general probabilistic setting. Given an arbitrary (large, uncountable) set C of predictors, we would like to construct a single predictor that performs asymptotically as well as the best predictor in C, on any data. Here we show that there are sets C for which such predictors exist, but none of them is a Bayesian predictor with a prior concentrated on C. In other words, there is a predictor with sublinear regret, but every Bayesian predictor must have a linear regret. This negative finding is in sharp contrast with previous results that establish the opposite for the case when one of the predictors in $C$ achieves asymptotically vanishing error. In such a case, if there is a predictor that achieves asymptotically vanishing error for any measure in C, then there is a Bayesian predictor that also has this property, and whose prior is concentrated on (a countable subset of) C.
An Improved Approach for Prediction of Parkinson's Disease using Machine Learning Techniques
Venue: arXiv cs.LG 2016
Year: 2016

Parkinson's disease (PD) is one of the major public health problems in the world. It is a well-known fact that around one million people suffer from Parkinson's disease in the United States whereas the number of people suffering from Parkinson's disease worldwide is around 5 million. Thus, it is important to predict Parkinson's disease in early stages so that early plan for the necessary treatment can be made. People are mostly familiar with the motor symptoms of Parkinson's disease, however, an increasing amount of research is being done to predict the Parkinson's disease from non-motor symptoms that precede the motor ones. If an early and reliable prediction is possible then a patient can get a proper treatment at the right time. Nonmotor symptoms considered are Rapid Eye Movement (REM) sleep Behaviour Disorder (RBD) and olfactory loss. Developing machine learning models that can help us in predicting the disease can play a vital role in early prediction. In this paper, we extend a work which used the non-motor features such as RBD and olfactory loss. Along with this the extended work also uses important biomarkers. In this paper, we try to model this classifier using different machine learning models that have not been used before. We developed automated diagnostic models using Multilayer Perceptron, BayesNet, Random Forest and Boosted Logistic Regression. It has been observed that Boosted Logistic Regression provides the best performance with an impressive accuracy of 97.159 % and the area under the ROC curve was 98.9%. Thus, it is concluded that these models can be used for early prediction of Parkinson's disease.
A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
Venue: arXiv cs.CR 2016
Year: 2016

Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. A secure communication has a different meaning depending on the underlying application. It ranges from the confidentiality of a data to e.g. verifiability in electronic voting systems. Another example of a security notion is privacy. Formal symbolic models have proved their usefulness for analysing the security of protocols. Until quite recently, most results focused on trace properties like confidentiality or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require a notion of behavioural equivalence. Typical examples are anonymity, and privacy related properties. During the last decade, several results and verification tools have been developed to analyse equivalence-based security properties. We propose here a synthesis of decidability and undecidability results for equivalence-based security properties. Moreover, we give an overview of existing verification tools that may be used to verify equivalence-based security properties.
Social Groups and Pedestrian Crowds: Experiment on Dyads in a Counter Flow Scenario
Venue: arXiv cs.MA 2016
Year: 2016

The calibration and validation of pedestrian simulations require the acquisition of empirical evidences of human behaviour. The current work presents the results of an experiment focused on the potentially combined effect of counter flow and grouping on pedestrian dynamics. In particular, we focused on: (i) four different configurations of flow ratio (the rate between the minor flow and the total flow in bidirectional scenarios); (ii) dyads, as the most frequently observed and basic social groups of crowds. Results showed that the increase of flow ratio negatively impacted the speed of pedestrians. Dyads walked significantly slower than singletons, due to the difficulty in movement coordination among group members (proxemics) in case of counter flow. The collected results represent an useful contribution towards the validation of pedestrian simulations.
Distortion Contribution Analysis with the Best Linear Approximation
Venue: arXiv cs.SY 2016
Year: 2016

A Distortion Contribution Analysis (DCA) obtains the distortion at the output of an analog electronic circuit as a sum of distortion contributions of its sub-circuits. Similar to a noise analysis, a DCA helps a designer to pinpoint the actual source of the distortion. Classically, the DCA uses the Volterra theory to model the circuit and its sub-circuits. This DCA has been proven useful for small circuits or heavily simplified examples. In more complex circuits however, the amount of contributions increases quickly, making the interpretation of the results difficult. In this paper, the Best Linear Approximation (BLA) is used to perform the DCA instead. The BLA represents the behaviour of a sub-circuit as a linear circuit with the unmodelled distortion represented by a noise source. Combining the BLA with a classic noise analysis yields a DCA that is simple to understand, yet capable to handle complex excitation signals and complex strongly non-linear circuits.
Exploiting Structure Sparsity for Covariance-based Visual Representation
Venue: arXiv cs.CV 2016
Year: 2016

The past few years have witnessed increasing research interest on covariance-based feature representation. A variety of methods have been proposed to boost its efficacy, with some recent ones resorting to nonlinear kernel technique. Noting that the essence of this feature representation is to characterise the underlying structure of visual features, this paper argues that an equally, if not more, important approach to boosting its efficacy shall be to improve the quality of this characterisation. Following this idea, we propose to exploit the structure sparsity of visual features in skeletal human action recognition, and compute sparse inverse covariance estimate (SICE) as feature representation. We discuss the advantage of this new representation on dealing with small sample, high dimensionality, and modelling capability. Furthermore, utilising the monotonicity property of SICE, we efficiently generate a hierarchy of SICE matrices to characterise the structure of visual features at different sparsity levels, and two discriminative learning algorithms are then developed to adaptively integrate them to perform recognition. As demonstrated by extensive experiments, the proposed representation leads to significantly improved recognition performance over the state-of-the-art comparable methods. In particular, as a method fully based on linear technique, it is comparable or even better than those employing nonlinear kernel technique. This result well demonstrates the value of exploiting structure sparsity for covariance-based feature representation.
PCM and APCM Revisited: An Uncertainty Perspective
Venue: arXiv cs.CV 2016
Year: 2016

In this paper, we take a new look at the possibilistic c-means (PCM) and adaptive PCM (APCM) clustering algorithms from the perspective of uncertainty. This new perspective offers us insights into the clustering process, and also provides us greater degree of flexibility. We analyze the clustering behavior of PCM-based algorithms and introduce parameters $σ_v$ and $α$ to characterize uncertainty of estimated bandwidth and noise level of the dataset respectively. Then uncertainty (fuzziness) of membership values caused by uncertainty of the estimated bandwidth parameter is modeled by a conditional fuzzy set, which is a new formulation of the type-2 fuzzy set. Experiments show that parameters $σ_v$ and $α$ make the clustering process more easy to control, and main features of PCM and APCM are unified in this new clustering framework (UPCM). More specifically, UPCM reduces to PCM when we set a small $α$ or a large $σ_v$, and UPCM reduces to APCM when clusters are confined in their physical clusters and possible cluster elimination are ensured. Finally we present further researches of this paper.
Real-time optimal control via Deep Neural Networks: study on landing problems
Venue: arXiv cs.SY 2016
Year: 2016

Recent research on deep learning, a set of machine learning techniques able to learn deep architectures, has shown how robotic perception and action greatly benefits from these techniques. In terms of spacecraft navigation and control system, this suggests that deep architectures may be considered now to drive all or part of the on-board decision making system. In this paper this claim is investigated in more detail training deep artificial neural networks to represent the optimal control action during a pinpoint landing, assuming perfect state information. It is found to be possible to train deep networks for this purpose and that the resulting landings, driven by the trained networks, are close to simulated optimal ones. These results allow for the design of an on-board real time optimal control system able to cope with large sets of possible initial states while still producing an optimal response.
The Probabilistic Model Checker Storm (Extended Abstract)
Venue: arXiv cs.SE 2016
Year: 2016

We present a new probabilistic model checker Storm. Using state-of-the-art libraries, we aim for both high performance and versatility. This extended abstract gives a brief overview of the features of Storm.
Combining Usability and Privacy Protection in Free-Access Public Cloud Storage Servers: Review of the Main Threats and Challenges
Venue: arXiv cs.CR 2016
Year: 2016

The 21st century belongs to the world of computing, specially as a result of the so-called cloud computing. This technology enables ubiquitous information management and thus people can access all their data from any place and at any time. In this landscape, the emergence of cloud storage has had an important role in the last five years. Nowadays, several free-access public cloud storage services make it possible for users to have a free backup of their assets and to manage and share them, representing a low-cost opportunity for Small and Medium Companies (SME). However, the adoption of cloud storage involves data outsourcing, so a user does not have the guarantee about the way her data will be processed and protected. Therefore, it seems necessary to endow public cloud storage with a set of means to protect users' confidentiality and privacy, to assess data integrity and to guarantee a proper backup of information assets. Along this paper we discuss the main challenges to achieve such a goal, underlining the set of functionalities already implemented in the most popular public cloud storage services.
Cross-Modal Scene Networks
Venue: arXiv cs.CV 2016
Year: 2016

People can recognize scenes across many different modalities beyond natural images. In this paper, we investigate how to learn cross-modal scene representations that transfer across modalities. To study this problem, we introduce a new cross-modal scene dataset. While convolutional neural networks can categorize scenes well, they also learn an intermediate representation not aligned across modalities, which is undesirable for cross-modal transfer applications. We present methods to regularize cross-modal convolutional neural networks so that they have a shared representation that is agnostic of the modality. Our experiments suggest that our scene representation can help transfer representations across modalities for retrieval. Moreover, our visualizations suggest that units emerge in the shared representation that tend to activate on consistent concepts independently of the modality.
Compressive Holographic Video
Venue: arXiv cs.CV 2016
Year: 2016

Compressed sensing has been discussed separately in spatial and temporal domains. Compressive holography has been introduced as a method that allows 3D tomographic reconstruction at different depths from a single 2D image. Coded exposure is a temporal compressed sensing method for high speed video acquisition. In this work, we combine compressive holography and coded exposure techniques and extend the discussion to 4D reconstruction in space and time from one coded captured image. In our prototype, digital in-line holography was used for imaging macroscopic, fast moving objects. The pixel-wise temporal modulation was implemented by a digital micromirror device. In this paper we demonstrate $10\times$ temporal super resolution with multiple depths recovery from a single image. Two examples are presented for the purpose of recording subtle vibrations and tracking small particles within 5 ms.