Biblio

Risk assessment of cyber-physical systems, such as power plants, connected devices and IT-infrastructures has always been challenging: safety (i.e., absence of unintentional failures) and security (i. e., no disruptions due to attackers) are conditions that must be guaranteed. One of the traditional tools used to help considering these problems is attack trees, a tree-based formalism inspired by fault trees, a well-known formalism used in safety engineering. In this paper we define and implement the translation of attack-fault trees (AFTs) to a new extension of timed automata, called parametric weighted timed automata. This allows us to parametrize constants such as time and discrete costs in an AFT and then, using the model-checker IMITATOR, to compute the set of parameter values such that a successful attack is possible. Using the different sets of parameter values computed, different attack and fault scenarios can be deduced depending on the budget, time or computation power of the attacker, providing helpful data to select the most efficient counter-measure.

After suffering decades of high-profile attacks, the need for formal verification of security-critical software has never been clearer. Verification-oriented programming languages like F* are now being used to build high-assurance cryptographic libraries and implementations of standard protocols like TLS. In this paper, we seek to apply these verification techniques to modern Web applications, like WhatsApp, that embed sophisticated custom cryptographic components. The problem is that these components are often implemented in JavaScript, a language that is both hostile to cryptographic code and hard to reason about. So we instead target WebAssembly, a new instruction set that is supported by all major JavaScript runtimes. We present a new toolchain that compiles Low*, a low-level subset of the F* programming language, into WebAssembly. Unlike other WebAssembly compilers like Emscripten, our compilation pipeline is focused on compactness and auditability: we formalize the full translation rules in the paper and implement it in a few thousand lines of OCaml. Using this toolchain, we present two case studies. First, we build WHACL*, a WebAssembly version of the existing, verified HACL* cryptographic library. Then, we present LibSignal*, a brand new, verified implementation of the Signal protocol in WebAssembly, that can be readily used by messaging applications like WhatsApp, Skype, and Signal.

Hardware vulnerabilities are often due to design mistakes because the designer does not sufficiently consider potential security vulnerabilities at the design stage. As a result, various security solutions have been developed to protect ICs, among which the language-based hardware security verification serves as a promising solution. The verification process will be performed while compiling the HDL of the design. However, similar to other formal verification methods, the language-based approach also suffers from scalability issue. Furthermore, existing solutions either lead to hardware overhead or are not designed for vulnerable or malicious logic detection. To alleviate these challenges, we propose a new language based framework, QIF-Verilog, to evaluate the trustworthiness of a hardware system at register transfer level (RTL). This framework introduces a quantified information flow (QIF) model and extends Verilog type systems to provide more expressiveness in presenting security rules; QIF is capable of checking the security rules given by the hardware designer. Secrets are labeled by the new type and then parsed to data flow, to which a QIF model will be applied. To demonstrate our approach, we design a compiler for QIF-Verilog and perform vulnerability analysis on benchmarks from Trust-Hub and OpenCore. We show that Trojans or design faults that leak information from circuit outputs can be detected automatically, and that our method evaluates the security of the design correctly.

In this work, we synthesize collaboration protocols for human-unmanned aerial vehicle (H-UAV) command and control systems, where the human operator aids in securing the UAV by intermittently performing geolocation tasks to confirm its reported location. We first present a stochastic game-based model for the system that accounts for both the operator and an adversary capable of launching stealthy false-data injection attacks, causing the UAV to deviate from its path. We also describe a synthesis challenge due to the UAV's hidden-information constraint. Next, we perform human experiments using a developed RESCHU-SA testbed to recognize the geolocation strategies that operators adopt. Furthermore, we deploy machine learning techniques on the collected experimental data to predict the correctness of a geolocation task at a given location based on its geographical features. By representing the model as a delayed-action game and formalizing the system objectives, we utilize off-the-shelf model checkers to synthesize protocols for the human-UAV coalition that satisfy these objectives. Finally, we demonstrate the usefulness of the H-UAV protocol synthesis through a case study where the protocols are experimentally analyzed and further evaluated by human operators.

Manufacturers often buy and/or license communication ICs from third-party suppliers. These communication ICs are then integrated into a complex computational system, resulting in a wide range of potential hardware-software security issues. This work proposes a compact supervisory circuit to classify the Bluetooth profile operation of a Bluetooth System-on-Chip (SoC) at low frequencies by monitoring the radio frequency (RF) output power of the Bluetooth SoC. The idea is to inexpensively manufacture an RF envelope detector to monitor the RF output power and a profile classification algorithm on a custom low-frequency integrated circuit in a low-cost legacy technology. When the supervisory circuit observes unexpected behavior, it can shut off power to the Bluetooth SoC. In this preliminary work, we proto-type the supervisory circuit using off-the-shelf components to collect a sufficient data set to train 11 different Machine Learning models. We extract smart descriptive time-domain features from the envelope of the RF output signal. Then, we train the machine learning models to classify three different Bluetooth operation profiles: sensor, hands-free, and headset. Our results demonstrate 100% classification accuracy with low computational complexity.

In order to solve privacy protection problem in the Internet of Vehicles environment, a message authentication scheme based on proxy re-signature is proposed using elliptic curves, which realizes privacy protection by transforming the vehicle's signature of the message into the roadside unit's signature of the same message through the trusted center. And through the trusted center traceability, to achieve the condition of privacy protection, and the use of batch verification technology, greatly improve the efficiency of authentication. It is proved that the scheme satisfies unforgeability in ECDLP hard problem in the random oracle model. The efficiency analysis shows that the scheme meets the security and efficiency requirements of the Internet of Vehicles and has certain practical significance.

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.

Verification of security policies represents one of the most critical, complex, and expensive steps of modern SoC design validation. SoC security policies are typically implemented as part of functional design flow, with a diverse set of protection mechanisms sprinkled across various IP blocks. An obvious upshot is that their verification requires comprehension and analysis of the entire system, representing a scalability bottleneck for verification tools. The scale and complexity of industrial SoC is far beyond the analysis capacity of state-of-the-art formal tools; even simulation-based security verification is severely limited in effectiveness because of the need to exercise subtle corner-cases across the entire system. We address this challenge by developing a novel security architecture that accounts for verification needs from the ground up. Our framework, ArtiFact, provides an alternative architecture for security policy implementation that exploits a flexible, centralized, infrastructure IP and enables scalable, streamlined verification of these policies. With our architecture, verification of system-level security policies reduces to analysis of this single IP and its interfaces, enabling off-the-shelf formal tools to successfully verify these policies. We introduce a CAD flow that supports both formal and dynamic (simulation-based) verification, and is built on top of such off-the-shelf tools. Our approach reduces verification time by over 62X and bug detection time by 34X for illustrative policies.

As the technology reliance increases, computer networks are getting bigger and larger and so are threats and attacks. Therefore Network security becomes a major concern during this last decade. Network Security requires a combination of hardware devices and software applications. Namely, Firewalls and IPsec gateways are two technologies that provide network security protection and repose on security policies which are maintained to ensure traffic control and network safety. Nevertheless, security policy misconfigurations and inconsistency between the policy's rules produce errors and conflicts, which are often very hard to detect and consequently cause security holes and compromise the entire system functionality. In This paper, we review the related approaches which have been proposed for security policy management along with surveying the literature for conflicts detection and resolution techniques. This work highlights the advantages and limitations of the proposed solutions for security policy verification in IPsec and Firewalls and gives an overall comparison and classification of the existing approaches.

pubcrawl, Network on Chip Security, Scalability, resiliency, resilience, metrics, Vulnerabilities and design flaws in Network-on-Chip (NoC) routers can be exploited in order to spy, modify and constraint the sensitive communication inside the Multi-Processors Systems-on-Chip (MPSoCs). Although previous works address the NoC threat, finding secure and efficient solutions to verify the security is still a challenge. In this work, we propose for the first time a method to formally verify the correctness and the security properties of a NoC router in order to provide the proper communication functionality and to avoid NoC attacks. We present a generalized verification flow that proves a wide set of implementation-independent security-related properties to hold. We employ unbounded model checking techniques to account for the highly-sequential behaviour of the NoC systems. The evaluation results demonstrate the feasibility of our approach by presenting verification results of six different NoC routing architectures demonstrating the vulnerabilities of each design.

The growth of the internet has brought along positive gains such as the emergence of a highly interconnected world. However, on the flip side, there has been a growing concern on how secure distributed systems can be built effectively and tested for security vulnerabilities prior to deployment. Developing a secure software product calls for a deep technical understanding of some complex issues with regards to the software and its operating environment, as well as embracing a systematic approach of analyzing the software. This paper proposes a method for identifying software security vulnerabilities from software requirement specifications written in Structured Object-oriented Formal Language (SOFL). Our proposed methodology leverages on the concept of providing an early focus on security by identifying potential security vulnerabilities at the requirement analysis and verification phase of the software development life cycle.

Formal verification of infinite-state systems, and distributed systems in particular, is a long standing research goal. In the deductive verification approach, the programmer provides inductive invariants and pre/post specifications of procedures, reducing the verification problem to checking validity of logical verification conditions. This check is often performed by automated theorem provers and SMT solvers, substantially increasing productivity in the verification of complex systems. However, the unpredictability of automated provers presents a major hurdle to usability of these tools. This problem is particularly acute in case of provers that handle undecidable logics, for example, first-order logic with quantifiers and theories such as arithmetic. The resulting extreme sensitivity to minor changes has a strong negative impact on the convergence of the overall proof effort.

This paper presents an assessment of continuous verification using linguistic style as a cognitive biometric. In stylometry, it is widely known that linguistic style is highly characteristic of authorship using representations that capture authorial style at character, lexical, syntactic, and semantic levels. In this work, we provide a contrast to previous efforts by implementing a one-class classification problem using Isolation Forests. Our approach demonstrates the usefulness of this classifier for accurately verifying the genuine user, and yields recognition accuracy exceeding 98% using very small training samples of 50 and 100-character blocks.

As a decentralized and distributed secure storage technology, the notion of blockchain is now widely used for electronic trading in finance, for issuing digital certificates, for copyrights management, and for many other security-critical applications. With applications in so many domains with high-assurance requirements, the formalization and verification of safety and security properties of blockchain becomes essential, and the aim of the present paper. We present the model-based formalization, simulation and verification of a blockchain protocol by using the SDL formalism of Telelogic Tau. We consider the hierarchical and modular SDL model of the blockchain protocol and exercise a methodology to formally simulate and verify it. This way, we show how to effectively increase the security and safety of blockchain in order to meet high assurance requirements demanded by its application domains. Our work also provides effective support for assessing different network consensus algorithms, which are key components in blockchain protocols, as well as on the topology of blockchain networks. In conclusion, our approach contributes to setting up a verification methodology for future blockchain standards in digital trading.

In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability logic theorem prover to generate a correct-by-construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts.

Industrial control systems are changing from monolithic to distributed and interconnected architectures, entering the era of industrial IoT. One fundamental issue is that security properties of such distributed control systems are typically only verified empirically, during development and after system deployment. We propose a novel modelling framework for the security verification of distributed industrial control systems, with the goal of moving towards early design stage formal verification. In our framework we model industrial IoT infrastructures, attack patterns, and mitigation strategies for countering attacks. We conduct model checking-based formal analysis of system security through scenario execution, where the analysed system is exposed to attacks and implement mitigation strategies. We study the applicability of our framework for large systems using a scalability analysis.

Hardware information flow analysis detects security vulnerabilities resulting from unintended design flaws, timing channels, and hardware Trojans. These information flow models are typically generated in a general way, which includes a significant amount of redundancy that is irrelevant to the specified security properties. In this work, we propose a property specific approach for information flow security. We create information flow models tailored to the properties to be verified by performing a property specific search to identify security critical paths. This helps find suspicious signals that require closer inspection and quickly eliminates portions of the design that are free of security violations. Our property specific trimming technique reduces the complexity of the security model; this accelerates security verification and restricts potential security violations to a smaller region which helps quickly pinpoint hardware security vulnerabilities.

This article describes a privacy policy framework that can represent and reason about complex privacy policies. By using a Common Data Model together with a formal shareability theory, this framework enables the specification of expressive policies in a concise way without burdening the user with technical details of the underlying formalism. We also build a privacy policy decision engine that implements the framework and that has been deployed as the policy decision point in a novel enterprise privacy prototype system. Our policy decision engine supports two main uses: (1) interfacing with user interfaces for the creation, validation, and management of privacy policies; and (2) interfacing with systems that manage data requests and replies by coordinating privacy policy engine decisions and access to (encrypted) databases using various privacy enhancing technologies.

With the development of large scale integrated circuits, the functions of the IoT chips have been increasingly perfect. The verification work has become one of the most important aspects. On the one hand, an efficient verification platform can ensure the correctness of the design. On the other hand, it can shorten the chip design cycle and reduce the design cost. In this paper, based on a transmission protocol of the IoT node, we propose a verification method which combines simulation verification and FPGA-based prototype verification. We also constructed a system verification platform for the IoT smart node chip combining two kinds of verification above. We have simulated and verificatied the related functions of the node chip using this platform successfully. It has a great reference value.

This Since the past century, the digital design industry has performed an outstanding role in the development of electronics. Hence, a great variety of designs are developed daily, these designs must be submitted to high standards of verification in order to ensure the 100% of reliability and the achievement of all design requirements. The Universal Verification Methodology (UVM) is the current standard at the industry for the verification process due to its reusability, scalability, time-efficiency and feasibility of handling high-level designs. This research proposes a functional verification framework using UVM for an AES encryption module based on a very detailed and robust verification plan. This document describes the complete verification process as done in the industry for a popular module used in information-security applications in the field of cryptography, defining the basis for future projects. The overall results show the achievement of the high verification standards required in industry applications and highlight the advantages of UVM against System Verilog-based functional verification and direct verification methodologies previously developed for the AES module.

Hybrid attack graphs are a powerful tool when analyzing the cybersecurity of a cyber-physical system. However, it is important to ensure that this tool correctly models reality, particularly when modelling safety-critical applications, such as a nuclear reactor. By automatically verifying that a simulation reaches the state predicted by an attack graph by analyzing the final state of the simulation, this verification procedure can be accomplished. As such, a mechanism to estimate if a simulation reaches the expected state in a hybrid attack graph is proposed here for the nuclear reactor domain.

As safety-critical systems become increasingly interconnected, a system's operations depend on the reliability and security of the computing components and the interconnections among them. Therefore, a growing body of research seeks to tie safety analysis to security analysis. Specifically, it is important to analyze system safety under different attacker models. In this paper, we develop generic parameterizable state automaton templates to model the effects of an attack. Then, given an attacker model, we generate a state automaton that represents the system operation under the threat of the attacker model. We use a railway signaling system as our case study and consider threats to the communication protocol and the commands issued to physical devices. Our results show that while less skilled attackers are not able to violate system safety, more dedicated and skilled attackers can affect system safety. We also consider several countermeasures and show how well they can deter attacks.

Exclusive-or (XOR) operations are common in cryptographic protocols, in particular in RFID protocols and electronic payment protocols. Although there are numerous applications, due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. The Tamarin prover is a state-of-the-art verification tool for cryptographic protocols in the symbolic model. In this paper, we improve the underlying theory and the tool to deal with an equational theory modeling XOR operations. The XOR theory can be freely combined with all equational theories previously supported, including user-defined equational theories. This makes Tamarin the first tool to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.

Often, analysts have to face a challenging situation when formally verifying the implementation of a security protocol: they need to build a model of the protocol from only poorly or not documented code, and with little or no help from the developers to better understand it. Security protocols implementations frequently use services provided by libraries coded in the C programming language; automatic tools for codelevel reverse engineering offer good support to comprehend the behavior of code in object-oriented languages but are ineffective to deal with libraries in C. Here we propose a systematic, yet human-dependent approach, which combines the capabilities of state-of-the-art tools in order to help the analyst to retrieve, step by step, the security protocol specifications from a library in C. Those specifications can then be used to create the formal model needed to carry out the analysis.

A well-defined structure is essential in all software development, thus providing an avenue for smooth execution of the processes involved during various software development phases. One of the potential benefits provided by a well-defined structure is systematic reuse of software artifacts. Requirements pattern approach provides guidelines and modality that enables a systematic way of specifying and documenting requirements, which in turn supports a systematic reuse. Although there is a great deal of research concerning requirements pattern in the literature, the research focuses are not on requirement engineering (RE) activities of SPLE. In this paper, we proposed a software requirement pattern (SRP) structure based on RePa Requirements Pattern Template, which was adapted to best suit RE activities in SPLE. With this requirement pattern structure, RE activities such as elicitation and identification of common and variable requirements as well as the specification, documentation, and reuse in SPLE could be substantially improved.