Biblio

Software-defined networks offer a promising framework for the implementation of cross-layer data-centric security policies in military systems. An important aspect of the design process for such advanced security solutions is the thorough experimental assessment and validation of proposed technical concepts prior to their deployment in operational military systems. In this paper, we describe an OpenFlow-based testbed, which was developed with a specific focus on validation of SDN security mechanisms - including both the mechanisms for protecting the software-defined network layer and the cross-layer enforcement of higher level policies, such as data-centric security policies. We also present initial experimentation results obtained using the testbed, which confirm its ability to validate simulation and analytic predictions. Our objective is to provide a sufficiently detailed description of the configuration used in our testbed so that it can be easily re-plicated and re-used by other security researchers in their experiments.

We propose a multi-level CSI quantization and key reconciliation scheme for physical layer security. The noisy wireless channel estimates obtained by the users first run through a transformation, prior to the quantization step. This enables the definition of guard bands around the quantization boundaries, tailored for a specific efficiency and not compromising the uniformity required at the output of the quantizer. Our construction results in an better key disagreement and initial key generation rate trade-off when compared to other level-crossing quantization methods.

The area of secure compilation aims to design compilers which produce hardened code that can withstand attacks from low-level co-linked components. So far, there is no formal correctness criterion for secure compilers that comes with a clear understanding of what security properties the criterion actually provides. Ideally, we would like a criterion that, if fulfilled by a compiler, guarantees that large classes of security properties of source language programs continue to hold in the compiled program, even as the compiled program is run against adversaries with low-level attack capabilities. This paper provides such a novel correctness criterion for secure compilers, called trace-preserving compilation (TPC). We show that TPC preserves a large class of security properties, namely all safety hyperproperties. Further, we show that TPC preserves more properties than full abstraction, the de-facto criterion used for secure compilation. Then, we show that several fully abstract compilers described in literature satisfy an additional, common property, which implies that they also satisfy TPC. As an illustration, we prove that a fully abstract compiler from a typed source language to an untyped target language satisfies TPC.

Security protocols are critical components for the construction of secure and dependable distributed applications, but their implementation is challenging and error prone. Therefore, tools for formal modelling and analysis of security protocols can be potentially very useful to support software engineers. However, despite such tools have been available for a long time, their adoption outside the research community has been very limited. In fact, most practitioners find such applications too complex and hardly usable for their daily work. In this paper, we present an Integrated Development Environment for the design, verification and implementation of security protocols, aimed at lowering the adoption barrier of formal methods tools for security. In the spirit of Model Driven Development, the environment supports the user in the specification of the model using the simple and intuitive language AnB (and its extension AnBx). Moreover, it provides a push-button solution for the formal verification of the abstract and concrete models, and for the automatic generation of Java implementation. This Eclipse-based IDE leverages on existing languages and tools for modelling and verification of security protocols, such as the AnBx Compiler and Code Generator, the model checker OFMC and the protocol verifier ProVerif.

Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant. Using the supercop framework, we evaluate the Jasmin compiler on representative cryptographic routines and conclude that the code generated by the compiler is as efficient as fast, hand-crafted, implementations. Moreover, the framework includes highly automated tools for proving memory safety and constant-time security (for protecting against cache-based timing attacks). We also demonstrate the effectiveness of the verification tools on a large set of cryptographic routines.

We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i. a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao's SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012). We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.

Word representation is one of the basic word repressentation methods in natural language processing, which mapped a word into a dense real-valued vector space based on a hypothesis: words with similar context have similar meanings. Models like NNLM, C&W, CBOW, Skip-gram have been designed for word embeddings learning, and get widely used in many NLP tasks. However, these models assume that one word had only one semantics meaning which is contrary to the real language rules. In this paper we pro-pose a new word unit with multiple meanings and an algorithm to distinguish them by it's context. This new unit can be embedded in most language models and get series of efficient representations by learning variable embeddings. We evaluate a new model MCBOW that integrate CBOW with our word unit on word similarity evaluation task and some downstream experiments, the result indicated our new model can learn different meanings of a word and get a better result on some other tasks.

Modern databases contain an enormous amount of information stored in a structured format. This information is processed to acquire knowledge. However, the process of information extraction from a Database System is cumbersome for non-expert users as it requires an extensive knowledge of DBMS languages. Therefore, an inevitable need arises to bridge the gap between user requirements and the provision of a simple information retrieval system whereby the role of a specialized Database Administrator is annulled. In this paper, we propose a methodology for building an Intelligent Querying System (IQS) by which a user can fire queries in his own (natural) language. The system first parses the input sentences and then generates SQL queries from the natural language expressions of the input. These queries are in turn mapped with the desired information to generate the required output. Hence, it makes the information retrieval process simple, effective and reliable.

This paper describes a video fingerprinting system that is highly robust to audio and video transformations. The proposed system adapts a robust audio fingerprint extraction approach to video fingerprinting. The audio fingerprinting system converts the spectrogram into binary images, and then encodes the positions of salient regions selected from each binary image. Visual features are extracted in a similar way from the video images. We propose two visual fingerprint generation methods where fingerprints encode the positions of salient regions of greyscale video images. Salient regions of the first method are selected based on the intensity values of the image, while the second method identifies the regions that represent the highest variations between two successive images. The similarity between two fingerprints is defined as the intersection between their elements. The search algorithm is speeded up by an efficient implementation on a Graphics Processing Unit (GPU). We evaluate the performance of the proposed video system on TRECVID 2009 and 2010 datasets, and we show that this system achieves promising results and outperforms other state-of-the-art video copy detection methods for queries that do not includes geometric transformations. In addition, we show the effectiveness of this system for a challenging audio+video copy detection task.

Nowadays the adoption of IoT solutions is gaining high momentum in several fields, including energy, home and environment monitoring, transportation, and manufacturing. However, cybersecurity attacks to low-cost end-user devices can severely undermine the expected deployment of IoT solutions in a broad range of scenarios. To face these challenges, emerging software-based networking features can introduce new security enablers, providing further scalability and flexibility required to cope with massive IoT. In this paper, we present a novel framework aiming to exploit SDN/NFV-based security features and devise new efficient integration with existing IoT security approaches. The potential benefits of the proposed framework is validated in two case studies. Finally, a feasibility study is presented, accounting for potential interactions with open-source SDN/NFV projects and relevant standardization activities.

Integer errors in C/C++ are caused by arithmetic operations yielding results which are unrepresentable in certain type. They can lead to serious safety and security issues. Due to the complicated semantics of C/C++ integers, integer errors are widely harbored in real-world programs and it is error-prone to repair them even for experts. An automatic tool is desired to 1) automatically generate fixes which assist developers to correct the buggy code, and 2) provide sufficient hints to help developers review the generated fixes and better understand integer types in C/C++. In this paper, we present a tool IntPTI that implements the desired functionalities for C programs. IntPTI infers appropriate types for variables and expressions to eliminate representation issues, and then utilizes the derived types with fix patterns codified from the successful human-written patches. IntPTI provides a user-friendly web interface which allows users to review and manage the fixes. We evaluate IntPTI on 7 real-world projects and the results show its competitive repair accuracy and its scalability on large code bases. The demo video for IntPTI is available at: https://youtu.be/9Tgd4A\_FgZM.

Quantum Key Distribution (QKD) is a revolutionary technology which leverages the laws of quantum mechanics to distribute cryptographic keying material between two parties with theoretically unconditional security. Terrestrial QKD systems are limited to distances of \textbackslashtextless;200 km in both optical fiber and line-of-sight free-space configurations due to severe losses during single photon propagation and the curvature of the Earth. Thus, the feasibility of fielding a low Earth orbit (LEO) QKD satellite to overcome this limitation is being explored. Moreover, in August 2016, the Chinese Academy of Sciences successfully launched the world's first QKD satellite. However, many of the practical engineering performance and security tradeoffs associated with space-based QKD are not well understood for global secure key distribution. This paper presents several system-level considerations for modeling and studying space-based QKD architectures and systems. More specifically, this paper explores the behaviors and requirements that researchers must examine to develop a model for studying the effectiveness of QKD between LEO satellites and ground stations.

Software Defined Networks (SDNs) have gained prominence recently due to their flexible management and superior configuration functionality of the underlying network. SDNs, with OpenFlow as their primary implementation, allow for the use of a centralised controller to drive the decision making for all the supported devices in the network and manage traffic through routing table changes for incoming flows. In conventional networks, machine learning has been shown to detect malicious intrusion, and classify attacks such as DoS, user to root, and probe attacks. In this work, we extend the use of machine learning to improve traffic tolerance for SDNs. To achieve this, we extend the functionality of the controller to include a resilience framework, ReSDN, that incorporates machine learning to be able to distinguish DoS attacks, focussing on a neptune attack for our experiments. Our model is trained using the MIT KDD 1999 dataset. The system is developed as a module on top of the POX controller platform and evaluated using the Mininet simulator.

We present a neural network technique for the analysis and extrapolation of time-series data called Neural Decomposition (ND). Units with a sinusoidal activation function are used to perform a Fourier-like decomposition of training samples into a sum of sinusoids, augmented by units with nonperiodic activation functions to capture linear trends and other nonperiodic components. We show how careful weight initialization can be combined with regularization to form a simple model that generalizes well. Our method generalizes effectively on the Mackey-Glass series, a dataset of unemployment rates as reported by the U.S. Department of Labor Statistics, a time-series of monthly international airline passengers, and an unevenly sampled time-series of oxygen isotope measurements from a cave in north India. We find that ND outperforms popular time-series forecasting techniques including LSTM, echo state networks, (S)ARIMA, and SVR with a radial basis function.

Lithium Ion batteries usually degrade to an unacceptable capacity level after hundreds or even thousands of cycles. The continuously observed capacity fade data over time and their internal structure can be informative for constructing capacity fade models. This paper applies a mean-covariance decomposition modeling method to analyze the capacity fade data. The proposed approach directly examines the variances and correlations in data of interest and express the correlation matrix in hyper-spherical coordinates using angles and trigonometric functions. The proposed method is applied to model and predict key batteries performance metrics using testing data under various testing conditions.

In this paper, a novel quantum encryption algorithm for color image is proposed based on multiple discrete chaotic systems. The proposed quantum image encryption algorithm utilize the quantum controlled-NOT image generated by chaotic logistic map, asymmetric tent map and logistic Chebyshev map to control the XOR operation in the encryption process. Experiment results and analysis show that the proposed algorithm has high efficiency and security against differential and statistical attacks.

The chaotic system and cryptography have some common features. Due to the close relationship between chaotic system and cryptosystem, researchers try to combine the chaotic system with cryptosystem. In this study, security analysis of an encryption algorithm which aims to encrypt the data with ECG signals and chaotic functions was performed using the Logistic map in text encryption and Henon map in image encryption. In the proposed algorithm, text and image data can be encrypted at the same time. In addition, ECG signals are used to determine the initial conditions and control parameters of the chaotic functions used in the algorithm to personalize of the encryption algorithm. In this cryptanalysis study, the inadequacy of the mentioned process and the weaknesses of the proposed method have been determined. Encryption algorithm has not sufficient capacity to provide necessary security level of key space and secret key can be obtained with only one plaintext/ciphertext pair with chosen-plaintext attack.

To enhance the encryption and anti-translation capability of the information, we constructed a five-dimensional chaotic system. Combined with the Lü system, a time-switched system with multiple chaotic attractors is realized in the form of a digital circuit. Some characteristics of the five-dimensional system are analyzed, such as Poincare mapping, the Lyapunov exponent spectrum, and bifurcation diagram. The analysis shows that the system exhibits chaotic characteristics for a wide range of parameter values. We constructed a time-switched expression between multiple chaotic attractors using the communication between a microcontroller unit (MCU) and field programmable gate array (FPGA). The system can quickly switch between different chaotic attractors within the chaotic system and between chaotic systems at any time, leading to signal sources with more variability, diversity, and complexity for chaotic encryption.

In this paper, we propose a new color image encryption and compression algorithm based on the DNA complementary rule and the Chinese remainder theorem, which combines the DNA complementary rule with quantum chaotic map. We use quantum chaotic map and DNA complementary rule to shuffle the color image and obtain the shuffled image, then Chinese remainder theorem from number theory is utilized to diffuse and compress the shuffled image simultaneously. The security analysis and experiment results show that the proposed encryption algorithm has large key space and good encryption result, it also can resist against common attacks.

The MgO-based magnetic tunnel junction (MTJ) is the basis of modern hard disk drives' magnetic read sensors. Within its operating bandwidth, the sensor's performance is significantly affected by nonlinear and oscillating behavior arising from the MTJ's magnetization dynamics at microwave frequencies. Static I-V curve measurements are commonly used to characterize sensor's nonlinear effects. Unfortunately, these do not sufficiently capture the MTJ's magnetization dynamics. In this paper, we demonstrate the use of the two-tone measurement technique for full treatment of the sensor's nonlinear effects in conjunction with dynamic ones. This approach is new in the field of magnetism and magnetic materials, and it has its challenges due to the nature of the device. Nevertheless, the experimental results demonstrate how the two-tone measurement technique can be used to characterize magnetic sensor nonlinear properties.

In a number of information security scenarios, human beings can be better than technical security measures at detecting threats. This is particularly the case when a threat is based on deception of the user rather than exploitation of a specific technical flaw, as is the case of spear-phishing, application spoofing, multimedia masquerading and other semantic social engineering attacks. Here, we put the concept of the human-as-a-security-sensor to the test with a first case study on a small number of participants subjected to different attacks in a controlled laboratory environment and provided with a mechanism to report these attacks if they spot them. A key challenge is to estimate the reliability of each report, which we address with a machine learning approach. For comparison, we evaluate the ability of known technical security countermeasures in detecting the same threats. This initial proof of concept study shows that the concept is viable.

Genetic Algorithms are group of mathematical models in computational science by exciting evolution in AI techniques nowadays. These algorithms preserve critical information by applying data structure with simple chromosome recombination operators by encoding solution to a specific problem. Genetic algorithms they are optimizer, in which range of problems applied to it are quite broad. Genetic Algorithms with its global search includes basic principles like selection, crossover and mutation. Data structures, algorithms and human brain inspiration are found for classification of data and for learning which works using Neural Networks. Artificial Intelligence (AI) it is a field, where so many tasks performed naturally by a human. When AI conventional methods are used in a computer it was proved as a complicated task. Applying Neural Networks techniques will create an internal structure of rules by which a program can learn by examples, to classify different inputs than mining techniques. This paper proposes a phishing websites classifier using improved polynomial neural networks in genetic algorithm.

To address increasing problems caused by cyber attacks, we leverage Software Defined networks and Network Function Virtualisation governed by a SARNET-agent to enable autonomous response and attack mitigation. A Secure Autonomous Response Network (SARNET) uses a control loop to constantly assess the security state of the network by means of observables. Using a prototype we introduce the metrics impact and effectiveness and show how they can be used to compare and evaluate countermeasures. These metrics become building blocks for self learning SARNET which exhibit true autonomous response.

The introduction of automation in cyber-physical systems (CPS) has raised major safety and security concerns. One attack vector is the sensing unit whose measurements can be manipulated by an adversary through attacks such as denial of service and delay injection. To secure an autonomous CPS from such attacks, we use a challenge response authentication (CRA) technique for detection of attack in active sensors data and estimate safe measurements using the recursive least square algorithm. For demonstrating effectiveness of our proposed approach, a car-follower model is considered where the follower vehicle's radar sensor measurements are manipulated in an attempt to cause a collision.

Internet of Things (IoT) and its various application domains are radically changing the lives of people, providing smart services which will ultimately constitute integral components of the living environment. The services of IoT operate based on the data flows collected from the different sensors and actuators. In this respect, the correctness and security of the sensor data transported over the IoT system is a crucial factor in ensuring the correct functioning of the IoT services. In this work, we present a method that can detect abnormal sensor events based on “apriori” knowledge of the behavior of the monitored process. The main advantage of the proposed methodology is that it builds on well-established theoretical works, while delivering a practical technique with low computational requirements. As a result, the developed technique can be hosted on various components of an IoT system. The developed approach is evaluated through real-world use-cases.