Biblio

Creating and implementing fault-tolerant distributed algorithms is a challenging task in highly safety-critical industries. Using formal methods supports design and development of complex algorithms. However, formal methods are often perceived as an unjustifiable overhead. This paper presents the experience and insights when using TLA+ and PlusCal to model and develop fault-tolerant and safety-critical modules for TAS Control Platform, a platform for railway control applications up to safety integrity level (SIL) 4. We show how formal methods helped us improve the correctness of the algorithms, improved development efficiency and how part of the gap between model and implementation has been closed by translation to C code. Additionally, we describe how we gained trust in the formal model and tools by following a specific design process called property-driven design, which also implicitly addresses software quality metrics such as code coverage metrics.

VisorFlow aims to monitor the flow of information between processes without requiring modifications to the operating system kernel or its userspace. VisorFlow runs in a privileged Xen domain and monitors the system calls executing in other domains running either Linux or Windows. VisorFlow uses its observations to prevent confidential information from leaving a local network. We describe the design and implementation of VisorFlow, describe how we used VisorFlow to confine na\"ıve users and malicious insiders during the 2017 Cyber-Defense Exercise, and provide performance measurements. We have released VisorFlow and its companion library, libguestrace, as open-source software.

As the adaptive steganography selects edge and texture area for loading, the theoretical analysis is limited by modeling difficulty. This paper introduces a novel method to study pixel-value difference (PVD) embedding scheme. First, the difference histogram values of cover image are used as parameters, and a variance formula for PVD stego noise is obtained. The accuracy of this formula has been verified through analysis with standard pictures. Second, the stego noise is divided into six kinds of pixel regions, and the regional noise variances are utilized to compare the security between PVD and least significant bit matching (LSBM) steganography. A mathematical conclusion is presented that, with the embedding capacity less than 2.75 bits per pixel, PVD is always not safer than LSBM under the same embedding rate, regardless of region selection. Finally, 10000 image samples are used to observe the validity of mathematical conclusion. For most images and regions, the data are also shown to be consistent with the prior judgment. Meanwhile, the cases of exception are analyzed seriously, and are found to be caused by randomness of pixel selection and abandoned blocks in PVD scheme. In summary, the unity of theory and practice completely indicates the effectiveness of our new method.

In-vehicle networks like Controller Area Network, FlexRay, Ethernet are now subjected to huge security threats where unauthorized entities can take control of the whole vehicle. This can pose very serious threats including accidents. Security features like encryption, message authentication are getting implemented in vehicle networks to counteract these issues. This paper is proposing a set of novel validation techniques to ensure that vehicle network security is fool proof. Security validation against requirements, security validation using white box approach, black box approach and grey box approaches are put forward. Test system architecture, validation of message authentication, decoding the patterns from vehicle network data, using diagnostics as a security loophole, V2V V2X loopholes, gateway module security testing are considered in detail. Aim of this research paper is to put forward a set of tools and methods for finding and reporting any security loopholes in the in-vehicle network security implementation.

Delegated authorization protocols have become wide-spread to implement Web applications and services, where some popular providers managing people identity information and personal data allow their users to delegate third party Web services to access their data. In this paper, we analyze the risks related to untrusted providers not behaving correctly, and we solve this problem by proposing the first verifiable delegated authorization protocol that allows third party services to verify the correctness of users data returned by the provider. The contribution of the paper is twofold: we show how delegated authorization can be cryptographically enforced through authenticated data structures protocols, we extend the standard OAuth2 protocol by supporting efficient and verifiable delegated authorization including database updates and privileges revocation.

In the verifiable database (VDB) model, a computationally weak client (database owner) delegates his database management to a database service provider on the cloud, which is considered untrusted third party, while users can query the data and verify the integrity of query results. Since the process can be computationally costly and has a limited support for sophisticated query types such as aggregated queries, we propose in this paper a framework that helps bridge the gap between security and practicality trade-offs. The proposed framework remodels the verifiable database problem using Stackelberg security game. In the new model, the database owner creates and uploads to the database service provider the database and its authentication structure (AS). Next, the game is played between the defender (verifier), who is a trusted party to the database owner and runs scheduled randomized verifications using Stackelberg mixed strategy, and the database service provider. The idea is to randomize the verification schedule in an optimized way that grants the optimal payoff for the verifier while making it extremely hard for the database service provider or any attacker to figure out which part of the database is being verified next. We have implemented and compared the proposed model performance with a uniform randomization model. Simulation results show that the proposed model outperforms the uniform randomization model. Furthermore, we have evaluated the efficiency of the proposed model against different cost metrics.

Verifying attacks against cyber physical systems can be a costly and time-consuming process. By using a simulated environment, attacks can be verified quickly and accurately. By combining the simulation of a cyber physical system with a hybrid attack graph, the effects of a series of exploits can be accurately analysed. Furthermore, the use of a simulated environment to verify attacks may uncover new information about the nature of the attacks.

We consider the automatic verification of information flow security policies of web-based workflows, such as conference submission systems like EasyChair. Our workflow description language allows for loops, non-deterministic choice, and an unbounded number of participating agents. The information flow policies are specified in a temporal logic for hyperproperties. We show that the verification problem can be reduced to the satisfiability of a formula of first-order linear-time temporal logic, and provide decidability results for relevant classes of workflows and specifications. We report on experimental results obtained with an implementation of our approach on a series of benchmarks.

Vehicular Ad Hoc Networks (VANETs) enable vehicle-to-vehicle (V2V) and vehicle-to-infrastructure (V2I) communications that bring many benefits and conveniences to improve the road safety and drive comfort in future transportation systems. Sybil attack is considered one of the most risky threats in VANETs since a Sybil attacker can generate multiple fake identities with false messages to severely impair the normal functions of safety-related applications. In this paper, we propose a novel Sybil attack detection method based on Received Signal Strength Indicator (RSSI), Voiceprint, to conduct a widely applicable, lightweight and full-distributed detection for VANETs. To avoid the inaccurate position estimation according to predefined radio propagation models in previous RSSI-based detection methods, Voiceprint adopts the RSSI time series as the vehicular speech and compares the similarity among all received time series. Voiceprint does not rely on any predefined radio propagation model, and conducts independent detection without the support of the centralized infrastructure. It has more accurate detection rate in different dynamic environments. Extensive simulations and real-world experiments demonstrate that the proposed Voiceprint is an effective method considering the cost, complexity and performance.

Security in virtualised environments is becoming increasingly important for institutions, not only for a firm's own on-site servers and network but also for data and sites that are hosted in the cloud. Today, security is either handled globally by the cloud provider, or each customer needs to invest in its own security infrastructure. This paper proposes a Virtual Security Operation Center (VSOC) that allows to collect, analyse and visualize security related data from multiple sources. For instance, a user can forward log data from its firewalls, applications and routers in order to check for anomalies and other suspicious activities. The security analytics provided by the VSOC are comparable to those of commercial security incident and event management (SIEM) solutions, but are deployed as a cloud-based solution with the additional benefit of using big data processing tools to handle large volumes of data. This allows us to detect more complex attacks that cannot be detected with todays signature-based (i.e. rules) SIEM solutions.

This paper considers a framework of electrical cyber-physical systems (ECPSs) in which each bus and branch in a power grid is equipped with a controller and a sensor. By means of measuring the damages of cyber attacks in terms of cutting off transmission lines, three solution approaches are proposed to assess and deal with the damages caused by faults or cyber attacks. Splitting incident is treated as a special situation in cascading failure propagation. A new simulation platform is built for simulating the protection procedure of ECPSs under faults. The vulnerability of ECPSs under faults is analyzed by experimental results based on IEEE 39-bus system.

Trustworthy operation of industrial control systems depends on secure and real-time code execution on the embedded programmable logic controllers (PLCs). The controllers monitor and control the critical infrastructures, such as electric power grids and healthcare platforms, and continuously report back the system status to human operators. We present Zeus, a contactless embedded controller security monitor to ensure its execution control flow integrity. Zeus leverages the electromagnetic emission by the PLC circuitry during the execution of the controller programs. Zeus's contactless execution tracking enables non-intrusive monitoring of security-critical controllers with tight real-time constraints. Those devices often cannot tolerate the cost and performance overhead that comes with additional traditional hardware or software monitoring modules. Furthermore, Zeus provides an air-gap between the monitor (trusted computing base) and the target (potentially compromised) PLC. This eliminates the possibility of the monitor infection by the same attack vectors. Zeus monitors for control flow integrity of the PLC program execution. Zeus monitors the communications between the human machine interface and the PLC, and captures the control logic binary uploads to the PLC. Zeus exercises its feasible execution paths, and fingerprints their emissions using an external electromagnetic sensor. Zeus trains a neural network for legitimate PLC executions, and uses it at runtime to identify the control flow based on PLC's electromagnetic emissions. We implemented Zeus on a commercial Allen Bradley PLC, which is widely used in industry, and evaluated it on real-world control program executions. Zeus was able to distinguish between different legitimate and malicious executions with 98.9% accuracy and with zero overhead on PLC execution by design.

This paper develops a model for Wells turbine using Xilinx system generator (XSG)toolbox of Matlab. The Wells turbine is very popular in oscillating water column (OWC) wave energy converters. Mostly, the turbine behavior is emulated in a controlled DC or AC motor coupled with a generator. Therefore, it is required to model the OWC and Wells turbine in real time software like XSG. It generates the OWC turbine behavior in real time. Next, a PI control scheme is suggested for controlling the DC motor so as to emulate the Wells turbine efficiently. The overall performance of the system is tested with asquirrel cage induction generator (SCIG). The Pierson-Moskowitz and JONSWAP irregular wave models have been applied to validate the OWC model. Finally, the simulation results for Wells turbine and PI controller have beendiscussed.

Logic locking is an intellectual property (IP) protection technique that prevents IP piracy, reverse engineering and overbuilding attacks by the untrusted foundry or end-users. Existing logic locking techniques are all based on locking the functionality; the design/chip is nonfunctional unless the secret key has been loaded. Existing techniques are vulnerable to various attacks, such as sensitization, key-pruning, and signal skew analysis enabled removal attacks. In this paper, we propose a tenacious and traceless logic locking technique, TTlock, that locks functionality and provably withstands all known attacks, such as SAT-based, sensitization, removal, etc. TTLock protects a secret input pattern; the output of a logic cone is flipped for that pattern, where this flip is restored only when the correct key is applied. Experimental results confirm our theoretical expectations that the computational complexity of attacks launched on TTLock grows exponentially with increasing key-size, while the area, power, and delay overhead increases only linearly. In this paper, we also coin ``parametric locking," where the design/chip behaves as per its specifications (performance, power, reliability, etc.) only with the secret key in place, and an incorrect key downgrades its parametric characteristics. We discuss objectives and challenges in parametric locking.

Recently, cellular operators have started migrating to IPv6 in response to the increasing demand for IP addresses. With the introduction of IPv6, cellular middleboxes, such as firewalls for preventing malicious traffic from the Internet and stateful NAT64 boxes for providing backward compatibility with legacy IPv4 services, have become crucial to maintain stability of cellular networks. This paper presents security problems of the currently deployed IPv6 middleboxes of five major operators. To this end, we first investigate several key features of the current IPv6 deployment that can harm the safety of a cellular network as well as its customers. These features combined with the currently deployed IPv6 middlebox allow an adversary to launch six different attacks. First, firewalls in IPv6 cellular networks fail to block incoming packets properly. Thus, an adversary could fingerprint cellular devices with scanning, and further, she could launch denial-of-service or over-billing attacks. Second, vulnerabilities in the stateful NAT64 box, a middlebox that maps an IPv6 address to an IPv4 address (and vice versa), allow an adversary to launch three different attacks: 1) NAT overflow attack that allows an adversary to overflow the NAT resources, 2) NAT wiping attack that removes active NAT mappings by exploiting the lack of TCP sequence number verification of firewalls, and 3) NAT bricking attack that targets services adopting IP-based blacklisting by preventing the shared external IPv4 address from accessing the service. We confirmed the feasibility of these attacks with an empirical analysis. We also propose effective countermeasures for each attack.

Dynamic spectrum sharing techniques applied in the UHF TV band have been developed to allow secondary WiFi transmission in areas with active TV users. This technique of dynamically controlling the exclusion zone enables vastly increasing secondary spectrum re-use, compared to the "TV white space" model where TV transmitters determine the exclusion zone and only "idle" channels can be re-purposed. However, in current such dynamic spectrum sharing systems, the sensitive operation parameters of both primary TV users (PUs) and secondary users (SUs) need to be shared with the spectrum database controller (SDC) for the purpose of realizing efficient spectrum allocation. Since such SDC server is not necessarily operated by a trusted third party, those current systems might cause essential threatens to the privacy requirement from both PUs and SUs. To address this privacy issue, this paper proposes a privacy-preserving spectrum sharing system between PUs and SUs, which realizes the spectrum allocation decision process using efficient multi-party computation (MPC) technique. In this design, the SDC only performs secure computation over encrypted input from PUs and SUs such that none of the PU or SU operation parameters will be revealed to SDC. The evaluation of its performance illustrates that our proposed system based on efficient MPC techniques can perform dynamic spectrum allocation process between PUs and SUs efficiently while preserving users' privacy.

We propose $μ$Leech, a new embedded trusted platform module for next generation power scavenging devices. Such power scavenging devices are already widely deployed. For instance, the Square point-of-sale reader uses the microphone/speaker interface of a smartphone for communications and as power supply. While such devices are used as trusted devices in security critical applications in the wild, they have not been properly evaluated yet. $μ$Leech can securely store keys and provide cryptographic services to any connected smart phone. Our design also facilitates physical security analysis by providing interfaces to facilitate acquisition of power traces and clock manipulation attacks. Thus $μ$Leech empowers security researchers to analyze leakage in next generation embedded and IoT devices and to evaluate countermeasures before deployment.

The Distributed Denial of Service (DDoS) attack is a main concern in network security. Since the attackers have developed different techniques and methods, preventing DDoS attacks has become more difficult. Traditional firewall is ineffective in preventing DDoS attacks. In this paper, we propose a new type of firewall named XFirewall to defend against DDoS attacks. XFirewall is a temporary firewall and is created when an attack occurs. Also, XFirewall will be configured with dynamic rules based on real-time traffic analysis. We will discuss in detail the design and algorithm for generating an XFirewall.

Intrusion Detection Systems (IDS) have been in existence for many years now, but they fall short in efficiently detecting zero-day attacks. This paper presents an organic combination of Semantic Link Networks (SLN) and dynamic semantic graph generation for the on the fly discovery of zero-day attacks using the Spark Streaming platform for parallel detection. In addition, a minimum redundancy maximum relevance (MRMR) feature selection algorithm is deployed to determine the most discriminating features of the dataset. Compared to previous studies on zero-day attack identification, the described method yields better results due to the semantic learning and reasoning on top of the training data and due to the use of collaborative classification methods. We also verified the scalability of our method in a distributed environment.

Symmetry ergodic matrices exponentiation (SEME) problem is to find x, given CxMDx, where C and D are the companion matrices of primitive polynomials and M is an invertible matrix over finite field. This paper proposes a new zero-knowledge identification scheme based on SEME problem. It is perfect zero-knowledge for honest verifiers. The scheme could provide a candidate cryptographic primitive in post quantum cryptography. Due to its simplicity and naturalness, low-memory, low-computation costs, the proposed scheme is suitable for using in computationally limited devices for identification such as smart cards.

The accessibility of on-chip embedded infrastructure for test, reconfiguration, or debug poses a serious security problem. Access mechanisms based on IEEE Std 1149.1 (JTAG), and especially reconfigurable scan networks (RSNs), as allowed by IEEE Std 1500, IEEE Std 1149.1-2013, and IEEE Std 1687 (IJTAG), require special care in the design and development. This work studies the threats to trustworthy data transmission in RSNs posed by untrusted components within the RSN and external interfaces. We propose a novel scan pattern generation method that finds trustworthy access sequences to prevent sniffing and spoofing of transmitted data in the RSN. For insecure RSNs, for which such accesses do not exist, we present an automated transformation that improves the security and trustworthiness while preserving the accessibility to attached instruments. The area overhead is reduced based on results from trustworthy access pattern generation. As a result, sensitive data is not exposed to untrusted components in the RSN, and compromised data cannot be injected during trustworthy accesses.

Lots of traditional embedded systems can be called closed systems in that they do not connect and communicate with systems or devices outside of the entities they are embedded, and some part of these systems are designed based on proprietary protocols or standards. Open embedded systems connect and communicate with other systems or devices through the Internet or other networks, and are designed based on open protocols and standards. This paper discusses two types of security challenges facing open embedded systems: the security of the devices themselves that host embedded systems, and the security of information collected, processed, communicated, and consumed by embedded systems. We also discuss solution techniques to address these challenges.

Authentication and encryption within an embedded system environment using cameras, sensors, thermostats, autonomous vehicles, medical implants, RFID, etc. is becoming increasing important with ubiquitious wireless connectivity. Hardware-based authentication and encryption offer several advantages in these types of resource-constrained applications, including smaller footprints and lower energy consumption. Bitstring and key generation implemented with Physical Unclonable Functions or PUFs can further reduce resource utilization for authentication and encryption operations and reduce overall system cost by eliminating on-chip non-volatile-memory (NVM). In this paper, we propose a dynamic partial reconfiguration (DPR) strategy for implementing both authentication and encryption using a PUF for bitstring and key generation on FPGAs as a means of optimizing the utilization of the limited area resources. We show that the time and energy penalties associated with DPR are small in modern SoC-based architectures, such as the Xilinx Zynq SoC, and therefore, the overall approach is very attractive for emerging resource-constrained IoT applications.

Verifying that hardware design implementations adhere to specifications is a time intensive and sometimes intractable problem due to the massive size of the system's state space. Formal methods techniques can be used to prove certain tractable specification properties; however, they are expensive, and often require subject matter experts to develop and solve. Nonetheless, hardware verification is a critical process to ensure security and safety properties are met, and encapsulates problems associated with trust and reliability. For complex designs where coverage of the entire state space is unattainable, prioritizing regions most vulnerable to security or reliability threats would allow efficient allocation of valuable verification resources. Stackelberg security games model interactions between a defender, whose goal is to assign resources to protect a set of targets, and an attacker, who aims to inflict maximum damage on the targets after first observing the defender's strategy. In equilibrium, the defender has an optimal security deployment strategy, given the attacker's best response. We apply this Stackelberg security framework to synthesized hardware implementations using the design's network structure and logic to inform defender valuations and verification costs. The defender's strategy in equilibrium is thus interpreted as a prioritization of the allocation of verification resources in the presence of an adversary. We demonstrate this technique on several open-source synthesized hardware designs.

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.