Biblio

Data Distribution Service (DDS) is a realtime peer-to-peer protocol that serves as a scalable middleware between distributed networked systems found in many Industrial IoT domains such as automotive, medical, energy, and defense. Since the initial ratification of the standard, specifications have introduced a Security Model and Service Plugin Interface (SPI) architecture, facilitating authenticated encryption and data centric access control while preserving interoperable data exchange. However, as Secure DDS v1.1, the default plugin specifications presently exchanges digitally signed capability lists of both participants in the clear during the crypto handshake for permission attestation; thus breaching confidentiality of the context of the connection. In this work, we present an attacker model that makes use of network reconnaissance afforded by this leaked context in conjunction with formal verification and model checking to arbitrarily reason about the underlying topology and reachability of information flow, enabling targeted attacks such as selective denial of service, adversarial partitioning of the data bus, or vulnerability excavation of vendor implementations.

Self-timed circuits can be modeled in a link-joint style using a formally defined hardware description language. It has previously been shown how functional properties of these models can be formally verified with the ACL2 theorem prover using a scalable, hierarchical method. Here we extend that method to parameterized circuit families that may have loops and non-deterministic outputs. We illustrate this extension with iterative self-timed circuits that calculate the greatest common divisor of two natural numbers, with circuits that perform arbitrated merges non-deterministically, and with circuits that combine both of these.

The design methods and the detection methods for Hardware Trojan develop rapidly. Existing trustiness verification methods are effective to obviously malicious HT but no effect on Stealthy Trojan. Stealthy Trojan is an advanced attack form and hard to be detected. In this paper, we analyze the characteristic of stealthy Trojan and propose a static detection method based on feature analysis. The results on ISCAS benchmarks show that the proposed method can detect the Stealthy Trojan node and is convenient to be implanted into other scalable verification framework.

Formally verifying functional and security properties of a large-scale production operating system is highly desirable. However, it is challenging as such OSes are often written in multiple source languages that have no formal semantics - a prerequisite for formal reasoning. To avoid expensive formalization of the semantics of multiple high-level source languages, we present a lightweight and rigorous verification toolchain that verifies OS code at the binary level, targeting ARM machines. To reason about ARM instructions, we first translate the ARM Specification Language that describes the semantics of the ARMv8 ISA into the PVS7 theorem prover and verify the translation. We leverage the radare2 reverse engineering tool to decode ARM binaries into PVS7 and verify the translation. Our translation verification methodology is a lightweight formal validation technique that generates large-scale instruction emulation test lemmas whose proof obligations are automatically discharged. To demonstrate our verification methodology, we apply the technique on two OSes: Google's Zircon and a subset of Linux. We extract a set of 370 functions from these OSes, translate them into PVS7, and verify the correctness of the translation by automatically discharging hundreds of thousands of proof obligations and tests. This took 27.5 person-months to develop.

In the component-based software system, certain behaviours of components and their composition may affect system reliability at runtime. This problem can be early detected through the automated verification of software architecture design, by which model checking is one of the techniques to achieve this. However, its practicality and performance issue remain challenges. This paper presents a scalable approach for the software architecture verification. The modelling is proposed to manifest the behaviours in the software component, in order to detect problematic behaviours, such as circular dependency and performance bottleneck. The outcome of the verification identifies the problem and the scenarios that cause it. In order to mitigate the verification performance issue, the parallelism is applied to the verification process so that multiple decomposed models can be simultaneously verified on a multi-threaded environment. As some software systems are designed as the monolithic architecture, we present a method that helps to automatically decompose a large monolithic model into a set of smaller sub-models. Our approach was evaluated and proved to enhance the performance of the verification process for the large-scale complex software systems.

In a diagnosability verifier with polynomial complexity, a non-diagnosable system generates uncertain loops. Such forbidden loops are in this paper transformed to forbidden states by simple detector automata. The forbidden state problem is trivially transformed to a nonblocking problem by considering all states except the forbidden ones as marked states. This transformation is combined with one of the most efficient abstractions for modular systems called conflict equivalence, where nonblocking properties are preserved. In the resulting abstraction, local events are hidden and more local events are achieved when subsystems are synchronized. This incremental abstraction is applied to a scalable production system, including parallel lines where buffers and machines in each line include some typical failures and feedback flows. For this modular system, the proposed diagnosability algorithm shows great results, where diagnosability of systems including millions of states is analyzed in less than a second.

Virtual Prototypes (VPs) at the Electronic System Level (ESL) written in SystemC language using its Transaction Level Modeling (TLM) framework are increasingly adopted by the semiconductor industry. The main reason is that VPs are much earlier available, and their simulation is orders of magnitude faster in comparison to the hardware models implemented at lower levels of abstraction (e.g. RTL). This leads designers to use VPs as reference models for an early design verification. Hence, the correctness assurance of these reference models (VPs) is critical as undetected faults may propagate to less abstract levels in the design process, increasing the fixing cost and effort. In this paper, we propose a novel simulation-based verification approach to automatically validate the simulation behavior of a given SystemC VP against both the TLM-2.0 rules and its specifications (i.e. functional and timing behavior of communications in the VP). The scalability and the efficiency of the proposed approach are demonstrated using an extensive set of experiments including a real-word VP.

We present two novel sound and complete netlist transformations, which substantially improve verification scalability while enabling very efficient trace reconstruction. First, we present a 2QBF variant of input reparameterization, capable of eliminating inputs without introducing new logic and without complete range computation. While weaker in reduction potential, it yields up to 4 orders of magnitude speedup to trace reconstruction when used as a fast-and-lossy preprocess to traditional reparameterization. Second, we present a novel scalable approach to leverage sequential unateness to merge selective inputs, in cases greatly reducing netlist size and verification complexity. Extensive benchmarking demonstrates the utility of these techniques. Connectivity verification particularly benefits from these reductions, up to 99.8%.

Due to the importance of securing electronic transactions, many cryptographic protocols have been employed, that mainly depend on distributed keys between the intended parties. In classical computers, the security of these protocols depends on the mathematical complexity of the encoding functions and on the length of the key. However, the existing classical algorithms 100% breakable with enough computational power, which can be provided by quantum machines. Moving to quantum computation, the field of security shifts into a new area of cryptographic solutions which is now the field of quantum cryptography. The era of quantum computers is at its beginning. There are few practical implementations and evaluations of quantum protocols. Therefore, the paper defines a well-known quantum key distribution protocol which is BB84 then provides a practical implementation of it on IBM QX software. The practical implementations showed that there were differences between BB84 theoretical expected results and the practical implementation results. Due to this, the paper provides a statistical analysis of the experiments by comparing the standard deviation of the results. Using the BB84 protocol the existence of a third-party eavesdropper can be detected. Thus, calculations of the probability of detecting/not detecting a third-party eavesdropping have been provided. These values are again compared to the theoretical expectation. The calculations showed that with the greater number of qubits, the percentage of detecting eavesdropper will be higher.

Recently, the increase of different services makes the design of routing protocols more difficult in mobile ad hoc networks (MANETs), e.g., how to guarantee the QoS of different types of traffics flows in MANETs with resource constrained and malicious nodes. opportunistic routing (OR) can make full use of the broadcast characteristics of wireless channels to improve the performance of MANETs. In this paper, we propose a traffic-differentiated secure opportunistic routing from a game theoretic perspective, DSOR. In the proposed scheme, we use a novel method to calculate trust value, considering node's forwarding capability and the status of different types of flows. According to the resource status of the network, we propose a service price and resource price for the auction model, which is used to select optimal candidate forwarding sets. At the same time, the optimal bid price has been proved and a novel flow priority decision for transmission is presented, which is based on waiting time and requested time. The simulation results show that the network lifetime, packet delivery rate and delay of the DSOR are better than existing works.

Routing protocols in wireless sensor network are vulnerable to various malicious security attacks that can degrade network performance and lifetime. This becomes more important in cluster routing protocols that is composed of multiple node and cluster head, such as low energy adaptive clustering hierarchy (LEACH) protocol. Namely, if an attack succeeds in failing the cluster head, then the entire set of nodes fail. Therefore, it is necessary to develop robust recovery schemes to overcome security attacks and recover packets at short times. Hence this paper proposes a detection and recovery scheme for selective forwarding attacks in wireless sensor networks using LEACH protocol. The proposed solution features near-instantaneous recovery times, without the requirement for feedback or retransmissions once an attack occurs.

Traditional power grid security schemes are being replaced by highly advanced and efficient smart security schemes due to the advancement in grid structure and inclusion of cyber control and monitoring tools. Smart attackers create physical, cyber, or cyber-physical attacks to gain the access of the power system and manipulate/override system status, measurements and commands. In this paper, we formulate the environment for the attacker-defender interaction in the smart power grid. We provide a strategic analysis of the attacker-defender strategic interaction using a game theoretic approach. We apply repeated game to formulate the problem, implement it in the power system, and investigate for optimal strategic behavior in terms of mixed strategies of the players. In order to define the utility or cost function for the game payoffs calculation, generation power is used. Attack-defense budget is also incorporated with the attacker-defender repeated game to reflect a more realistic scenario. The proposed game model is validated using IEEE 39 bus benchmark system. A comparison between the proposed game model and the all monitoring model is provided to validate the observations.

The deployment of smart devices in IoT applications are increasing with tremendous pace causing severe security concerns, as it trade most of private information. To counter that security issues in low resource applications, lightweight cryptographic algorithms have been introduced in recent past. In this paper we propose efficient hardware architecture of piccolo lightweight algorithm uses 64 bits block size with variable key size of length 80 and 128 bits. This paper introduces novel hardware architecture of piccolo-80, to supports high speed RFID security applications. Different design strategies are there to optimize the hardware metrics trade-off for particular application. The algorithm is implemented on different family of FPGAs with different devices to analyze the performance of design in 4 input LUTs and 6 input LUTs implementations. In addition, the results of hardware design are evaluated and compared with the most relevant lightweight block ciphers, shows the proposed architecture finds its utilization in terms of speed and area optimization from the hardware resources. The increment in throughput with optimized area of this architecture suggests that piccolo can applicable to implement for ultra-lightweight applications also.

Profiled DPA is a new method combined with machine learning method in side channel attack which is put forward by Whitnall in CHES 2015.[1]The most important part lies in effectiveness of extracting information. This paper introduces a new rule Explained Local Variance (ELV) to extract information in profiled stage for profiled DPA. It attracts information effectively and shields noise to get better accuracy than the original rule. The ELV enables an attacker to use less power traces to get the same result as before. It also leads to 94.6% space reduction and 29.2% time reduction for calculation. For security circuit implementation, a high order masking scheme in modelsim is implemented. A new exchange network is put forward. 96.9% hardware resource is saved due to the usage of this network.

With the application of integrated circuits (ICs) appears in all aspects of life, whether an IC is security and reliable has caused increasing worry which is of significant necessity. An attacker can achieve the malicious purpose by adding or removing some modules, so called hardware Trojans (HTs). In this paper, we use side-channel analysis (SCA) and support vector machine (SVM) classifier to determine whether there is a Trojan in the circuit. We use SAKURA-G circuit board with Xilinx SPARTAN-6 to complete our experiment. Results show that the Trojan detection rate is up to 93% and the classification accuracy is up to 91.8475%.

In this paper, we focuses on an access control issue in the Internet of Things (IoT). Generally, we firstly propose a decentralized IoT system based on blockchain. Then we establish a secure fine-grained access control strategies for users, devices, data, and implement the strategies with smart contract. To trigger the smart contract, we design different transactions. Finally, we use the multi-index table struct for the access right's establishment, and store the access right into Key-Value database to improve the scalability of the decentralized IoT system. In addition, to improve the security of the system we also store the access records on the blockchain and database.

New IoT applications are demanding for more and more performance in embedded devices while their deployment and operation poses strict power constraints. We present the security concept for a customizable Internet of Things (IoT) platform based on the RISC-V ISA and developed by several Fraunhofer Institutes. It integrates a range of peripherals with a scalable computing subsystem as a three dimensional System-in-Package (3D-SiP). The security features aim for a medium security level and target the requirements of the IoT market. Our security architecture extends given implementations to enable secure deployment, operation, and update. Core security features are secure boot, an authenticated watchdog timer, and key management. The Universal Sensor Platform (USeP) SoC is developed for GLOBALFOUNDRIES' 22FDX technology and aims to provide a platform for Small and Medium-sized Enterprises (SMEs) that typically do not have access to advanced microelectronics and integration know-how, and are therefore limited to Commercial Off-The-Shelf (COTS) products.

State-of-the-art security frameworks have been extensively addressing security issues for web resources, agents and services in the Semantic Web. The provision of Stream Reasoning as a new area spanning Semantic Web and Data Stream Management Systems has eventually opened up new challenges. Namely, their decentralized nature, the metadata descriptions, the number of users, agents, and services, makes securing Stream Reasoning systems difficult to handle. Thus, there is an inherent need of developing new security models which will handle security and automate security mechanism to a more autonomous system that supports complex and dynamic relationships between data, clients and service providers. We plan to validate our proposed security model on a typical application of stream data, on Wireless Sensor Networks (WSNs). In particular, WSNs for water quality monitoring will serve as a case study. The proposed model can be a guide when deploying and maintaining WSNs in different contexts. Moreover, this model will point out main segments which are most important in ensuring security in semantic stream reasoning systems, and their interrelationships. In this paper we propose a security framework to handle most important issues of security within WSN. The security model in itself should be an incentive for other researchers in creating other models to improve information security within semantic stream reasoning systems.

This paper presents a novel logic locking security assessment method based on linear regression, by means of modeling between the distribution probabilities of key-inputs and observable outputs. The algorithm reveals a weakness of the encrypted circuit since the assessment can revoke the key-inputs within several iterations. The experiment result shows that the proposed assessment can be applied to varies of encrypted combinational benchmark circuits, which exceeds 85% of correctness after revoking the encrypted key-inputs.

Based on Markov chain analysis method, the situation prediction of smart grid security and stability can be judged in this paper. First component state transition probability matrix and component state prediction were defined. A fast derivation method of Markov state transition probability matrix using in system state prediction was proposed. The Matlab program using this method was compiled to analyze and obtain the future state probability distribution of grid system. As a comparison the system state distribution was simulated based on sequential Monte Carlo method, which was in good agreement with the state transition matrix, and the validity of the method was verified. Furthermore, the situation prediction of the six-node example was analyzed, which provided an effective prediction and analysis tool for the security situation.

The integrity of information and services is one of the more evident concerns in the world of global information security, due to the fact that it has economic repercussions on the digital industry. For this reason, big companies spend a lot of money on systems that protect them against cyber-attacks like Denial of Service attacks. In this article, we will use all the attributes of the data-set NSL-KDD to train and test a Support Vector Machine model. This model will then be applied to a method of feature selection to obtain the most relevant attributes within the aforementioned data-set and train the model again. The main goal is comparing the results obtained in both instances of training and validate which was more efficient.

A novel supervised machine learning system is developed to classify network traffic whether it is malicious or benign. To find the best model considering detection success rate, combination of supervised learning algorithm and feature selection method have been used. Through this study, it is found that Artificial Neural Network (ANN) based machine learning with wrapper feature selection outperform support vector machine (SVM) technique while classifying network traffic. To evaluate the performance, NSL-KDD dataset is used to classify network traffic using SVM and ANN supervised machine learning techniques. Comparative study shows that the proposed model is efficient than other existing models with respect to intrusion detection success rate.

The Distributed Denial of Service attack is one of the most common attacks and it is hard to mitigate, however, it has become more difficult while dealing with the Low-rate DoS (LDoS) attacks. The LDoS exploits the vulnerability of TCP congestion-control mechanism by sending malicious traffic at the low constant rate and influence the victim machine. Recently, machine learning approaches are applied to detect the complex DDoS attacks and improve the efficiency and robustness of the intrusion detection system. In this research, the algorithm is designed to balance the detection rate and its efficiency. The detection algorithm combines the Power Spectral Density (PSD) entropy function and Support Vector Machine to detect LDoS traffic from normal traffic. In our solution, the detection rate and efficiency are adjustable based on the parameter in the decision algorithm. To have high efficiency, the detection method will always detect the attacks by calculating PSD-entropy first and compare it with the two adaptive thresholds. The thresholds can efficiently filter nearly 19% of the samples with a high detection rate. To minimize the computational cost and look only for the patterns that are most relevant for detection, Support Vector Machine based machine learning model is applied to learn the traffic pattern and select appropriate features for detection algorithm. The experimental results show that the proposed approach can detect 99.19% of the LDoS attacks and has an O (n log n) time complexity in the best case.

To efficiently provide the ancient ceramic composition analysis and testing services, it is necessary to efficiently classify the ancient ceramics in ceramic cloud service platform. In this paper, we get the 8 kinds of major chemical contents of the body and glaze in each sample according to analyze 35 samples. After establishing of the classification model of two samples, the results indicate: as long as choosing SVM algorithm correctly, the classification results of body and glaze samples will be quite ideal, and the support vector machine is a very valuable new method which can process ancient porcelains data.

The traditional smart-home is designed to integrate the concept of the Internet of Things(IoT) into our home environment, and to improve the comfort of home. It connects electrical products and household goods to the network, and then monitors and controls them. However, this paper takes home safety as the main axis of research. It combines the past concept of smart-home and technology of machine learning to improve the whole system of smart-home. Through systematic self-learning, it automatically figure out whether it is normal or abnormal, and reports to remind building occupants safety. At the same time, it saves the cost of human resources preservation. This paper make a set of rules table as the basic criteria first, and then classify a part of data which collected by traditional Internet of Things of smart-home by manual way, which includes the opening and closing of doors and windows, the starting and stopping of motors, the connection and interruption of the system, and the time of sending each data to label, then use Support Vector Machine(SVM) algorithm to classify and build models, and then train it. The executed model is applied to our smart-home system. Finally, we verify the Accuracy of anomaly reporting in our system.