Biblio

The design of modern computer hardware heavily relies on third-party intellectual property (IP) cores, which may contain malicious hardware Trojans that could be exploited by an adversary to leak secret information or take control of the system. Existing hardware Trojan detection methods either require a golden reference design for comparison or extensive functional testing to identify suspicious signals. In this paper, we propose a new formal verification method to verify the security of hardware designs. The proposed solution formalizes fine grained gate level information flow model for proving security properties of hardware designs in the Coq theorem prover environment. Compare with existing register transfer level (RTL) information flow security models, our model only needs to translate a small number of logic primitives to their formal representations without the need of supporting the rich RTL HDL semantics or dealing with complex conditional branch or loop structures. As a result, a gate level information flow model can be created at much lower complexity while achieving significantly higher precision in modeling the security behavior of hardware designs. We use the AES-T1700 benchmark from Trust-HUB to demonstrate the effectiveness of our solution. Experimental results show that our method can detect and pinpoint the Trojan.

With rapid advances in the fields of the Internet of Things and autonomous systems, the network security of cyber-physical systems(CPS) becomes more and more important. This paper focuses on the real-time security evaluation for unmanned aircraft systems which are cyber-physical systems relying on information communication and control system to achieve autonomous decision making. Our problem formulation is motivated by scenarios involving autonomous unmanned aerial vehicles(UAVs) working continuously under data-driven attacks when in an open, uncertain, and even hostile environment. Firstly, we investigated the state estimation method in CPS integrated with data-driven attacks model, and then proposed a real-time security scoring algorithm to evaluate the security condition of unmanned aircraft systems under different threat patterns, considering the vulnerability of the systems and consequences brought by data attacks. Our simulation in a UAV illustrated the efficiency and reliability of the algorithm.

A privately owned smart device connected to a corporate network using a USB connection creates a potential channel for malware infection and its subsequent spread. For example, air-gapped (a.k.a. isolated) systems are considered to be the most secure and safest places for storing critical datasets. However, unlike network communications, USB connection streams have no authentication and filtering. Consequently, intentional or unintentional piggybacking of a malware infected USB storage or a mobile device through the air-gap is sufficient to spread infection into such systems. Our findings show that the contact rate has an exceptional impact on malware spread and destabilizing free malware equilibrium. This work proposes a USB authentication and delegation protocol based on radiofrequency identification (RFID) in order to stabilize the free malware equilibrium in air-gapped networks. The proposed protocol is modelled using Coloured Petri nets (CPN) and the model is verified and validated through CPN tools.

Existing systems allow manufacturers to acquire factory floor data and perform analysis with cloud applications for machine health monitoring, product quality prediction, fault diagnosis and prognosis etc. However, they do not provide capabilities to perform testing of machine tools and associated components remotely, which is often crucial to identify causes of failure. This paper presents a fault diagnosis system in a cyber-physical manufacturing cloud (CPMC) that allows manufacturers to perform diagnosis and maintenance of manufacturing machine tools through remote monitoring and online testing using Machine Tool Communication (MTComm). MTComm is an Internet scale communication method that enables both monitoring and operation of heterogeneous machine tools through RESTful web services over the Internet. It allows manufacturers to perform testing operations from cloud applications at both machine and component level for regular maintenance and fault diagnosis. This paper describes different components of the system and their functionalities in CPMC and techniques used for anomaly detection and remote online testing using MTComm. It also presents the development of a prototype of the proposed system in a CPMC testbed. Experiments were conducted to evaluate its performance to diagnose faults and test machine tools remotely during various manufacturing scenarios. The results demonstrated excellent feasibility to detect anomaly during manufacturing operations and perform testing operations remotely from cloud applications using MTComm.

Numerous authorization models have been proposed for relational databases. On the other hand, several NoSQL databases used in Big Data applications use a new model appropriate to their requirements for structure, speed, and large amount of data. This model protects each individual cell in key-value databases by labeling them with authorization rights following a Role-Based Access Control model or similar. We present here a pattern to describe this model as it exists in several Big Data systems.

The high penetration of third-party intellectual property (3PIP) brings a high risk of malicious inclusions and data leakage in products due to the planted hardware Trojans, and system level security constraints have recently been proposed for MPSoCs protection against hardware Trojans. However, secret communication still can be established in the context of the proposed security constraints, and thus, another type of security constraints is also introduced to fully prevent such malicious inclusions. In addition, fulfilling the security constraints incurs serious overhead of schedule length, and a two-stage performance-constrained task scheduling algorithm is then proposed to maintain most of the security constraints. In the first stage, the schedule length is iteratively reduced by assigning sets of adjacent tasks into the same core after calculating the maximum weight independent set of a graph consisting of all timing critical paths. In the second stage, tasks are assigned to proper IP vendors and scheduled to time periods with a minimization of cores required. The experimental results show that our work reduces the schedule length of a task graph, while only a small number of security constraints are violated.

Cyber physical system (CPS) is often deployed at safety-critical key infrastructures and fields, fault tolerance policies are extensively applied in CPS systems to improve its credibility; the same physical backup of hardware redundancy (SPB) technology is frequently used for its simple and reliable implementation. To resolve challenges faced with in simulation test of SPB-CPS, this paper dynamically determines the test resources matched with the CPS scale by using the adaptive allocation policies, establishes the hierarchical models and inter-layer message transmission mechanism. Meanwhile, the collaborative simulation time sequence push strategy and the node activity test mechanism based on the sliding window are designed in this paper to improve execution efficiency of the simulation test. In order to validate effectiveness of the method proposed in this paper, we successfully built up a fault-tolerant CPS simulation platform. Experiments showed that it can improve the SPB-CPS simulation test efficiency.

CAPTCHAs have become an ubiquitous defense used to protect open web resources from being exploited at scale. Traditionally, attackers have developed automatic programs known as CAPTCHA solvers to bypass the mechanism. With the presence of cheap labor in developing countries, hackers now have options to use human solvers. In this research, we develop a game theoretical framework to model the interactions between the defender and the attacker regarding the design and countermeasure of CAPTCHA system. With the result of equilibrium analysis, both parties can determine the optimal allocation of software-based or human-based CAPTCHA solvers. Counterintuitively, instead of the traditional wisdom of making CAPTCHA harder and harder, it may be of best interest of the defender to make CAPTCHA easier. We further suggest a welfare-improving CAPTCHA business model by involving decentralized cryptocurrency computation.

We propose a novel cross-stack sensor framework for realizing lightweight, context-aware, high-interaction network and endpoint deceptions for attacker disinformation, misdirection, monitoring, and analysis. In contrast to perimeter-based honeypots, the proposed method arms production workloads with deceptive attack-response capabilities via injection of booby-traps at the network, endpoint, operating system, and application layers. This provides defenders with new, potent tools for more effectively harvesting rich cyber-threat data from the myriad of attacks launched by adversaries whose identities and methodologies can be better discerned through direct engagement rather than purely passive observations of probe attempts. Our research provides new tactical deception capabilities for cyber operations, including new visibility into both enterprise and national interest networks, while equipping applications and endpoints with attack awareness and active mitigation capabilities.

Fault Location, Isolation and System Restoration (FLISR) mechanisms allow for rapid restoration of power to customers that are not directly implicated by distribution network failures. However, depending on where the logic for the FLISR system is located, deployment may have security implications for the distribution network. This paper discusses alternative FLISR placements in terms of cyber security considerations, concluding that there is a case for both local and centralized FLISR solutions.

Neural networks are vulnerable to adversarial examples, which poses a threat to their application in security sensitive systems. We propose high-level representation guided denoiser (HGD) as a defense for image classification. Standard denoiser suffers from the error amplification effect, in which small residual adversarial noise is progressively amplified and leads to wrong classifications. HGD overcomes this problem by using a loss function defined as the difference between the target model's outputs activated by the clean image and denoised image. Compared with ensemble adversarial training which is the state-of-the-art defending method on large images, HGD has three advantages. First, with HGD as a defense, the target model is more robust to either white-box or black-box adversarial attacks. Second, HGD can be trained on a small subset of the images and generalizes well to other images and unseen classes. Third, HGD can be transferred to defend models other than the one guiding it. In NIPS competition on defense against adversarial attacks, our HGD solution won the first place and outperformed other models by a large margin.1

Large scale services have automated hardware remediation to maintain the infrastructure availability at a healthy level. In this paper, we share the current remediation flow at Facebook, and how it is being monitored. We discuss a class of hardware issues that are transient and typically have higher rates during heavy load. We describe how our remediation system was enhanced to be efficient in detecting this class of issues. As hardware and systems change in response to the advancement in technology and scale, we have also utilized machine learning frameworks for hardware remediation to handle the introduction of new hardware failure modes. We present an ML methodology that uses a set of predictive thresholds to monitor remediation efficiency over time. We also deploy a recommendation system based on natural language processing, which is used to recommend repair actions for efficient diagnosis and repair. We also describe current areas of research that will enable us to improve hardware availability further.

The aim of this work is to perform an analysis on Technology Transfer strategies for the development of Serious Games at Public National Universities. The results can be extrapolated to other research topics and institutions. First of all, the University role as a producer of knowledge is studied, and possible scenarios for Technology Transfer to third-parties are considered. Moreover, the actors involved in the research and development processes and their corresponding Intellectual Property rights on the Research Results are identified and analysed. Finally, an Intellectual Property Rights protection analysis is undertaken to the different components of a Serious Game type of product, through the modalities of invention patents, utility models, industrial models and designs, brands and author rights. The work concludes that public universities are best fitted as knowledge factories, and the most promising scenario in Technology Transfer is that universities manage their Intellectual Property Rights and licence them to third-party institutions to handle commercialization, while keeping favorable conditions to finance subsequent research and ensuring that products derived from Research Results will be reachable by the society.

Within “Industrie 4.0” approach 3D printing technology is characterized as one of the disruptive innovations. Conventional supply chains are replaced by value-added networks. The spatially distributed development of printed components, e.g. for the rapid delivery of spare parts, creates a new challenge when differentiating between “original part”, “copy” or “counterfeit” becomes necessary. This is especially true for safety-critical products. Based on these changes classic branded products adopt the characteristics of licensing models as we know them in the areas of software and digital media. This paper describes the use of digital rights management as a key technology for the successful transition to Additive Manufacturing methods and a key for its commercial implementation and the prevention of intellectual property theft. Risks will be identified along the process chain and solution concepts are presented. These are currently being developed by an 8-partner project named SAMPL (Secure Additive Manufacturing Platform).

Linear oscillating actuators are emerging electrical motors applied to direct-drive electromechanical systems. They merit high efficiency and quick dynamical property due to the unique structure of spring oscillator. Resonant principle is the base of their high performance, which however, is easily influenced by various load, complex environment and mechanical failure. This paper studies the modeling of linear oscillating actuators in multi-work condition. Three kinds of load are considered in performance evaluation model. Simulations are conducted at different frequencies to obtain the actuator behavior, especially at non-resonance frequencies. A method of constant impedance angle is proposed to search the best working points in sorts of conditions. Eventually, analytical results reflect that the resonant parameter would drift with load, while linear oscillating actuators exhibits robustness in efficiency performance. Several evaluating parameters are concluded to assess the actuator health status.

Just like bugs in single-threaded programs can lead to vulnerabilities, bugs in multithreaded programs can also lead to concurrency attacks. We studied 31 real-world concurrency attacks, including privilege escalations, hijacking code executions, and bypassing security checks. We found that compared to concurrency bugs' traditional consequences (e.g., program crashes), concurrency attacks' consequences are often implicit, extremely hard to be observed and diagnosed by program developers. Moreover, in addition to bug-inducing inputs, extra subtle inputs are often needed to trigger the attacks. These subtle features make existing tools ineffective to detect concurrency attacks. To tackle this problem, we present OWL, the first practical tool that models general concurrency attacks' implicit consequences and automatically detects them. We implemented OWL in Linux and successfully detected five new concurrency attacks, including three confirmed and fixed by developers, and two exploited from previously known and well-studied concurrency bugs. OWL has also detected seven known concurrency attacks. Our evaluation shows that OWL eliminates 94.1% of the reports generated by existing concurrency bug detectors as false positive, greatly reducing developers' efforts on diagnosis. All OWL source code, concurrency attack exploit scripts, and results are available on github.com/hku-systems/owl.

The IP address attribution information includes the geographical information, the network routing information, the agency information, Internet Content Provider (ICP) information, etc. Nowadays, the attribution information is important to the network traffic engineering, which needs to be obtained in real time in network traffic analysis system. The existing proposed methods for IP address attribution information lookup cannot be employed in actual systems efficiently due to their low scalability or bad performance. They cannot address the backbone network's requirements for real-time IP address attribution information lookup, and most lookup methods do not support custom IP address attribution lookup. In response to these challenges, we propose a novel high-speed approach for IP address attribution information lookup. We first devise a data structure of IP address attribution information search tree (PATIP-TREE) to store custom IP address attribution information. Based on the PATIP-TREE, an effective algorithm for IP information lookup is proposed, which can support custom IP addresses attribution information lookup in real time. The experimental results show that our method outperforms the existing methods in terms of higher efficiency. Our approach also provides high scalability, which is suitable for many kinds network address such as IPv4 address, IPv6 address, named data networking address, etc.

Question Answering system(QA) plays an increasingly important role in the Internet age. The proportion of using the QA is getting higher and higher for the Internet users to obtain knowledge and solve problems, especially in the modern agricultural filed. However, the answer quality in QA varies widely due to the agricultural expert's level. Answer quality assessment is important. Due to the lexical gap between questions and answers, the existing approaches are not quite satisfactory. A practical approach RCAS is proposed to rank the candidate answers, which utilizes the support sets to reduce the impact of lexical gap between questions and answers. Firstly, Similar questions are retrieved and support sets are produced with their high-quality answers. Based on the assumption that high quality answers would also have intrinsic similarity, the quality of candidate answers are then evaluated through their distance from the support sets. Secondly, Different from the existing approaches, previous knowledge from similar question-answer pairs are used to bridge the straight lexical and semantic gaps between questions and answers. Experiments are implemented on approximately 0.15 million question-answer pairs about agriculture, dietetics and food from Yahoo! Answers. The results show that our approach can rank the candidate answers more precisely.

The following topics are dealt with: security of data; risk management; decision making; computer crime; invasive software; critical infrastructures; data privacy; insurance; Internet of Things; learning (artificial intelligence).

Traditionally, power grid vulnerability assessment methods are separated to the study of nodes vulnerability and edges vulnerability, resulting in the evaluation results are not accurate. A framework for vulnerability assessment is still required for power grid. Thus, this paper proposes a universal method for vulnerability assessment of power grid by establishing a complex network model with uniform weight of nodes and edges. The concept of virtual edge is introduced into the distinct weighted complex network model of power system, and the selection function of edge weight and virtual edge weight are constructed based on electrical and physical parameters. In addition, in order to reflect the electrical characteristics of power grids more accurately, a weighted betweenness evaluation index with transmission efficiency is defined. Finally, the method has been demonstrated on the IEEE 39 buses system, and the results prove the effectiveness of the proposed method.

We revisit Physical-Layer Network Coding (PLNC) and the reasons preventing it from becoming a staple in wireless networks. We identify its strong coupling to the Two-Way Relay Channel (TWRC) as key among them due to its requiring crossing traffic flows and two-hop node coordination. We introduce SE-PLNC, a Source-Encoded PLNC scheme that is traffic pattern independent and involves coordination only among one-hop neighbors, making it significantly more practical to adopt PLNC in multi-hop wireless networks. To accomplish this, SE-PLNC introduces three innovations: it combines bit-level with physical-level network coding, it shifts most of the coding burden from the relay to the source of the PLNC scheme, and it leverages multi-path relaying opportunities available to a particular traffic flow. We evaluate SE-PLNC using theoretical analysis, proof-of-concept implementation on a Universal Software Radio Peripherals (USRP) testbed, and simulations. The theoretical analysis shows the scalability of SE-PLNC and its efficiency in large ad-hoc networks while the testbed experiments its real-life feasibility. Large-scale simulations show that TWRC PLNC barely boosts network throughput while SE-PLNC improves it by over 30%.

Securing Cyber-Physical Systems (CPS) against cyber-attacks is challenging due to the wide range of possible attacks - from stealthy ones that seek to manipulate/drop/delay control and measurement signals to malware that infects host machines that control the physical process. This has prompted the research community to address this problem through developing targeted methods that protect and check the run-time operation of the CPS. Since protecting signals and checking for errors result in performance penalties, they must be performed within the delay bounds dictated by the control loop. Due to the large number of potential checks that can be performed, coupled with various degrees of their effectiveness to detect a wide range of attacks, strategic assignment of these checks in the control loop is a critical endeavor. To that end, this paper presents a coherent runtime framework - which we coin BLOC - for orchestrating the CPS with check blocks to secure them against cyber attacks. BLOC capitalizes on game theoretical techniques to enable the defender to find an optimal randomized use of check blocks to secure the CPS while respecting the control-loop constraints. We develop a Stackelberg game model for stateless blocks and a Markov game model for stateful ones and derive optimal policies that minimize the worst-case damage from rational adversaries. We validate our models through extensive simulations as well as a real implementation for a HVAC system.

Formal security verification of firmware interacting with hardware in modern Systems-on-Chip (SoCs) is a critical research problem. This faces the following challenges: (1) design complexity and heterogeneity, (2) semantics gaps between software and hardware, (3) concurrency between firmware/hardware and between Intellectual Property Blocks (IPs), and (4) expensive bit-precise reasoning. In this paper, we present a co-verification methodology to address these challenges. We model hardware using the Instruction-Level Abstraction (ILA), capturing firmware-visible behavior at the architecture level. This enables integrating hardware behavior with firmware in each IP into a single thread. The co-verification with multiple firmware across IPs is formulated as a multi-threaded program verification problem, for which we leverage software verification techniques. We also propose an optimization using abstraction to prevent expensive bit-precise reasoning. The evaluation of our methodology on an industry SoC Secure Boot design demonstrates its applicability in SoC security verification.

Airports are at the forefront of technological innovation, mainly due to the fact that the number of air travel passengers is exponentially increasing every year. As a result, airports enhance infrastructure's intelligence and evolve as smart facilities to support growth, by offering a pleasurable travel experience, which plays a vital role in increasing revenue of aviation sector. New challenges are coming up, which aviation has to deal and adapt, such as the integration of Industrial IoT in airport facilities and the increased use of Bring Your Own Device from travelers and employees. Cybersecurity is becoming a key enabler for safety, which is paramount in the aviation context. Smart airports strive to provide optimal services in a reliable and sustainable manner, by working around the domains of growth, efficiency, safety andsecurity. This paper researches the implementation rate of cybersecurity measures and best practices to improve airports cyber resilience. With the aim to enhance operational practices anddevelop robust cybersecurity governance in smart airports, we analyze security gaps in different areas including technical, organizational practices and policies.

Modern high-level languages bring compelling productivity benefits to hardware design and verification. For example, hardware generation and simulation frameworks (HGSFs) use a single "host" language for parameterization, static elaboration, test bench generation, behavioral modeling, and simulation. Unfortunately, HGSFs often suffer from slow simulator performance which undermines their potential productivity benefits. In this paper, we introduce Mamba, a new Python-based HGSF that co-optimizes both the framework and a general-purpose just-in-time compiler. We conduct a quantitative comparison of Mamba vs. traditional and emerging hardware development frameworks across both simple and complex designs. Our results suggest Mamba is able to match the performance of commercial Verilog simulators and is 10× faster than existing HGSFs while still maintaining the productivity of using a high-level language in hardware design.