Biblio

Model checking is one of the most commonly used technique in formal verification. However, the exponential scale state space renders exhaustive state enumeration inefficient even for a moderate System on Chip (SoC) design. In this paper, we propose a method that leverages symbolic execution to accelerate state space search and pinpoint security vulnerabilities. We automatically convert the hardware design to functionally equivalent C++ code and utilize the KLEE symbolic execution engine to perform state exploration through heuristic search. To reduce the search space, we symbolically represent essential input signals while making non-critical inputs concrete. Experiment results have demonstrated that our method can precisely identify security vulnerabilities at significantly lower computation cost.

With the development of artificial intelligence, the need for data sharing is becoming more and more urgent. However, the existing data sharing methods can no longer fully meet the data sharing needs. Privacy breaches, lack of motivation and mutual distrust have become obstacles to data sharing. We design a privacy-preserving, decentralized data sharing method based on blockchain smart contracts, named PPDS. To protect data privacy, we transform the data sharing problem into a model sharing problem. This means that the data owner does not need to directly share the raw data, but the AI model trained with such data. The data requester and the data owner interact on the blockchain through a smart contract. The data owner trains the model with local data according to the requester's requirements. To fairly assess model quality, we set up several model evaluators to assess the validity of the model through voting. After the model is verified, the data owner who trained the model will receive reward in return through a smart contract. The sharing of the model avoids direct exposure of the raw data, and the reasonable incentive provides a motivation for the data owner to share the data. We describe the design and workflow of our PPDS, and analyze the security using formal verification technology, that is, we use Coloured Petri Nets (CPN) to build a formal model for our approach, proving its security through simulation execution and model checking. Finally, we demonstrate effectiveness of PPDS by developing a prototype with its corresponding case application.

The fifth-generation (5G) standard is the last telecommunication technology, widely considered to have the most important characteristics in the future network industry. The 5G system infrastructure contains three principle interfaces, each one follows a set of protocols defined by the 3rd Generation Partnership Project group (3GPP). For the next generation network, 3GPP specified two authentication methods systematized in two protocols namely 5G Authentication and Key Agreement (5G-AKA) and Extensible Authentication Protocol (EAP). Such protocols are provided to ensure the authentication between system entities. These two protocols are critical systems, thus their reliability and correctness must be guaranteed. In this paper, we aim to formally re-examine 5G-AKA protocol using micro Common Representation Language 2 (mCRL2) language to verify such a security protocol. The mCRL2 language and its associated toolset are formal tools used for modeling, validation, and verification of concurrent systems and protocols. In this context, the authentication protocol 5G-AKA model is built using Algebra of Communication Processes (ACP), its properties are specified using Modal mu-Calculus and the properties analysis exploits Model-Checker provided with mCRL2. Indeed, we propose a new mCRL2 model of 3GPP specification considering 5G-AKA protocol and we specify some properties that describe necessary requirements to evaluate the correctness of the protocol where the parsed properties of Deadlock Freedom, Reachability, Liveness and Safety are positively assessed.

Always-On Denial of Service (DoS) Trojans with power drain payload can be disastrous in systems where on-chip power resources are limited. These Trojans are designed so that they have no impact on system behavior and hence, harder to detect. A formal verification method is presented to detect sequential always-on DoS Trojans in pipelined circuits and pipelined microprocessors. Since the method is proof-based, it provides a 100% accurate classification of sequential Trojan components. Another benefit of the approach is that it does not require a reference model, which is one of the requirements of many Trojan detection techniques (often a bottleneck to practical application). The efficiency and scalability of the proposed method have been evaluated on 36 benchmark circuits. The most complex of these benchmarks has as many as 135,898 gates. Detection times are very efficient with a 100% rate of detection, i.e., all Trojan sequential elements were detected and all non-trojan sequential elements were classified as such.

The advent of 5G, one of the most recent and promising technologies currently under deployment, fulfills the emerging needs of mobile subscribers by introducing several new technological advancements. However, this may lead to numerous attacks in the emerging 5G networks. Thus, to guarantee the secure transmission of user data, 5G Authentication protocols such as Extensible Authentication Protocol - Authenticated Key Agreement Protocol (EAP-AKA) were developed. These protocols play an important role in ensuring security to the users as well as their data. However, there exists no guarantees about the security of the protocols. Thus formal verification is necessary to ensure that the authentication protocols are devoid of vulnerabilities or security loopholes. Towards this goal, we formally verify the security of the 5G EAP-AKA protocol using an automated verification tool called ProVerif. ProVerif identifies traces of attacks and checks for security loopholes that can be accessed by the attackers. In addition, we model the complete architecture of the 5G EAP-AKA protocol using the language called typed pi-calculus and analyze the protocol architecture through symbolic model checking. Our analysis shows that some cryptographic parameters in the architecture can be accessed by the attackers which cause the corresponding security properties to be violated.

The semaphore mechanism is an important part of the embedded operating system. Therefore, it is very necessary to ensure its safety. Traditional software testing methods are difficult to ensure 100% coverage of the program. Therefore, it is necessary to adopt a formal verfication method which proves the correctness of the program theoretically. This paper proposes a proof framework based on the theorem proof tool Coq: modeling the semaphore mechanism, extracting important properties from the requirement documents, and finally verifying that the semaphore mechanism can meet these properties, which means the correctness of the semaphore mechanism is proved and also illustrates the feasibility of the verification framework proposed in this paper, which lays a foundation for the verification of other modules of operating systems.

Safety- and security-critical developers have long recognized the importance of applying a high degree of scrutiny to a system’s (or subsystem’s) I/O messages. However, lack of care in the development of message-handling components can lead to an increase, rather than a decrease, in the attack surface. On the DARPA Cyber-Assured Systems Engineering (CASE) program, we have focused our research effort on identifying cyber vulnerabilities early in system development, in particular at the Architecture development phase, and then automatically synthesizing components that mitigate against the identified vulnerabilities from high-level specifications. This approach is highly compatible with the goals of the LangSec community. Advances in formal methods have allowed us to produce hardware/software implementations that are both performant and guaranteed correct. With these tools, we can synthesize high-assurance “building blocks” that can be composed automatically with high confidence to create trustworthy systems, using a method we call Security-Enhancing Architectural Transformations. Our synthesis-focused approach provides a higherleverage insertion point for formal methods than is possible with post facto analytic methods, as the formal methods tools directly contribute to the implementation of the system, without requiring developers to become formal methods experts. Our techniques encompass Systems, Hardware, and Software Development, as well as Hardware/Software Co-Design/CoAssurance. We illustrate our method and tools with an example that implements security-improving transformations on system architectures expressed using the Architecture Analysis and Design Language (AADL). We show how message-handling components can be synthesized from high-level regular or context-free language specifications, as well as a novel specification language for self-describing messages called Contiguity Types, and verified to meet arithmetic constraints extracted from the AADL model. Finally, we guarantee that the intent of the message processing logic is accurately reflected in the application binary code through the use of the verified CakeML compiler, in the case of software, or the Restricted Algorithmic C toolchain with ACL2-based formal verification, in the case of hardware/software co-design.

Equivalence checking is one of the most scalable and useful verification techniques in industry. NULL Convention Logic (NCL) circuits utilize dual-rail signals (i.e., two wires to represent one bit of DATA), where the wires are inverses of each other during a DATA wavefront. In this paper, a technique that exploits this invariant at NCL register boundaries is proposed to improve the efficiency of equivalence verification of NCL circuits.

Security is one of the most important problems in the engineering of online service-oriented systems. The current best practice in security design is a pattern-oriented approach. A large number of security design patterns have been identified, categorised and documented in the literature. The design of a security solution for a system starts with identification of security requirements and selection of appropriate security design patterns; these are then composed together. It is crucial to verify that the composition of security design patterns is valid in the sense that it preserves the features, semantics and soundness of the patterns and correct in the sense that the security requirements are met by the design. This paper proposes a methodology that employs the algebraic specification language SOFIA to specify security design patterns and their compositions. The specifications are then translated into the Alloy formalism and their validity and correctness are verified using the Alloy model checker. A tool that translates SOFIA into Alloy is presented. A case study with the method and the tool is also reported.

The Internet of Things enables interaction between IoT devices and users through the cloud. The cloud provides services such as account monitoring, device management, and device control. As the center of the IoT platform, the cloud provides services to IoT devices and IoT applications through APIs. Therefore, the permission verification of the API is essential. However, we found that some APIs are unverified, which allows unauthorized users to access cloud resources or control devices; it could threaten the security of devices and cloud. To check for unauthorized access to the API, we developed IoT-APIScanner, a framework to check the permission verification of the cloud API. Through observation, we found there is a large amount of interactive information between IoT application and cloud, which include the APIs and related parameters, so we can extract them by analyzing the code of the IoT application, and use this for mutating API test cases. Through these test cases, we can effectively check the permissions of the API. In our research, we extracted a total of 5 platform APIs. Among them, the proportion of APIs without permission verification reached 13.3%. Our research shows that attackers could use the API without permission verification to obtain user privacy or control of devices.

Vulnerabilities in privileged software layers have been exploited with severe consequences. Recently, Trusted Execution Environments (TEEs) based technologies have emerged as a promising approach since they claim strong confidentiality and integrity guarantees regardless of the trustworthiness of the underlying system software. In this paper, we consider one of the most prominent TEE technologies, referred to as Intel Software Guard Extensions (SGX). Despite many formal approaches, there is still a lack of formal proof of some critical processes of Intel SGX, such as remote attestation. To fill this gap, we propose a fully automated, rigorous, and sound formal approach to specify and verify the Enhanced Privacy ID (EPID)-based remote attestation in Intel SGX under the assumption that there are no side-channel attacks and no vulnerabilities inside the enclave. The evaluation indicates that the confidentiality of attestation keys is preserved against a Dolev-Yao adversary in this technology. We also present a few of the many inconsistencies found in the existing literature on Intel SGX attestation during formal specification.

One of the main security issues in telecare medecine information systems is the remote user authentication and key agreement between healthcare professionals and patient's medical sensors. Many of the proposed approaches are based on multiple factors (password, token and possibly biometrics). Two-factor authentication protocols do not resist to many possible attacks. As for three-factor authentication schemes, they usually come with high resource consumption. Since medical sensors have limited storage and computational capabilities, ensuring a minimal resources consumption becomes a major concern in this context. In this paper, we propose a secure and lightweight three-factor authentication and key generation scheme for securing communications between healtcare professional and patient's medical sensors. Thanks to formal verification, we prove that this scheme is robust enough against known possible attacks. A comparison with the most relevant related work's schemes shows that our protocol ensures an optimised resource consumption level.

This paper is related to dissemination and exploitation of the InFoCPS PhD research project: Failure of Cyber-Physical Systems (CPS) may cause extensive damage. Safety standards emphasize the use of formal analysis in CPS development processes. Performance degradation assessment and estimation of lifetime of energy storage (electric batteries) are vital in supporting maintenance decisions and guaranteeing CPS reliability. Existing formal analysis techniques mainly focus on specifying energy constraints in simplified manners and checking whether systems operate within given energy bounds. Leading to overlooked energy features that impede development of trustworthy CPS. Prognostics and health management (PHM) estimate energy uncertainty and predict remaining life of systems. We aim to utilize PHM techniques to rigorously model dynamic energy behaviors; resulting models are amenable to formal analysis. This project will increase the degree of maintenance of CPS while (non)-functional requirements are preserved correctly.

E- Health systems, specifically, Telecare Medical Information Systems (TMIS), are deployed in order to provide patients with specific diseases with healthcare services that are usually based on remote monitoring. Therefore, making an efficient, convenient and secure connection between users and medical servers over insecure channels within medical services is a rather major issue. In this context, because of the biometrics' characteristics, many biometrics-based three factor user authentication schemes have been proposed in the literature to secure user/server communication within medical services. In this paper, we make a brief study of the most interesting proposals. Then, we propose a new three-factor authentication and key agreement scheme for TMIS. Our scheme tends not only to fix the security drawbacks of some studied related work, but also, offers additional significant features while minimizing resource consumption. In addition, we perform a formal verification using the widely accepted formal security verification tool AVISPA to demonstrate that our proposed scheme is secure. Also, our comparative performance analysis reveals that our proposed scheme provides a lower resource consumption compared to other related work's proposals.

It is important to be able to establish formal performance bounds for autonomous systems. However, formal verification techniques require a model of the environment in which the system operates; a challenge for autonomous systems, especially those expected to operate over longer timescales. This paper describes work in progress to automate the monitor and repair of ROS-based autonomous robot software written for an apriori partially known and possibly incorrect environment model. A taint analysis method is used to automatically extract the dataflow sequence from input topic to publish topic, and instrument that code. A unique reinforcement learning approximation of MDP utility is calculated, an empirical and non-invasive characterization of the inherent objectives of the software designers. By comparing design (a-priori) utility with deploy (deployed system) utility, we show, using a small but real ROS example, that it's possible to monitor a performance criterion and relate violations of the criterion to parts of the software. The software is then patched using automated software repair techniques and evaluated against the original off-line utility.

Ensuring security to IoT devices is important in order to provide privacy and quality of services. Proposing a security solution is considered an important step towards achieving protection, however, proving the soundness of the solution is also crucial. In this paper, we propose a methodology for the performance evaluation of lightweight IoT-based authentication protocols based on execution time. Then, a formal verification test is conducted on a lightweight protocol proposed in the literature. The formal verification test conducted with Scyther tool proofs that the model provides mutual authentication, authorization, integrity, confidentiality, non-repudiation, and accountability. The protocol also was proven to provide protection from various attacks.

Securing cyber-physical systems (CPS) and Internet of Things (IoT) systems requires the identification of how interdependence among existing atomic vulnerabilities may be exploited by an adversary to stitch together an attack that can compromise the system. Therefore, accurate attack graphs play a significant role in systems security. A manual construction of the attack graphs is tedious and error-prone, this paper proposes a model-checking-based automated attack graph generator and visualizer (A2G2V). The proposed A2G2V algorithm uses existing model-checking tools, an architecture description tool, and our own code to generate an attack graph that enumerates the set of all possible sequences in which atomic-level vulnerabilities can be exploited to compromise system security. The architecture description tool captures a formal representation of the networked system, its atomic vulnerabilities, their pre-and post-conditions, and security property of interest. A model-checker is employed to automatically identify an attack sequence in the form of a counterexample. Our own code integrated with the model-checker parses the counterexamples, encodes those for specification relaxation, and iterates until all attack sequences are revealed. Finally, a visualization tool has also been incorporated with A2G2V to generate a graphical representation of the generated attack graph. The results are illustrated through application to computer as well as control (SCADA) networks.

Most modern cloud and web services are programmatically accessed through REST APIs. This paper discusses how an attacker might compromise a service by exploiting vulnerabilities in its REST API. We introduce four security rules that capture desirable properties of REST APIs and services. We then show how a stateful REST API fuzzer can be extended with active property checkers that automatically test and detect violations of these rules. We discuss how to implement such checkers in a modular and efficient way. Using these checkers, we found new bugs in several deployed production Azure and Office365 cloud services, and we discuss their security implications. All these bugs have been fixed.

With the widespread application of distributed information processing, information processing security issues have become one of the important research topics; CAPTCHA technology is often used as the first security barrier for distributed information processing and it prevents the client malicious programs to attack the server. The experiment proves that the existing “request / response” mode of CAPTCHA has great security risks. “The text-based CAPTCHA solution without network flow consumption” proposed in this paper avoids the “request / response” mode and the verification logic of the text-based CAPTCHA is migrated to the client in this solution, which fundamentally cuts off the client's attack facing to the server during the verification of the CAPTCHA and it is a high-security text-based CAPTCHA solution without network flow consumption.

Cyber-physical systems are characterized by strong interactions between their physical and computation parts. The increasing complexity of such systems, now used in numerous application domains (e.g., aeronautics, healthcare), in conjunction with hard to predict surrounding environments or the use of non-traditional middleware and with the presence of non-deterministic or non-explainable software outputs, tend to make traditional Verification and Validation (V&V) techniques ineffective. This paper presents the H2020 ADVANCE project, which aims precisely at addressing the Verification and Validation challenges that the next-generation of cyber-physical systems bring, by exploring techniques, methods and tools for achieving the technical objective of improving the overall efficiency and effectiveness of the V&V process. From a strategic perspective, the goal of the project is to create an international network of expertise on the topic of V&V of cyber-physical systems.

In this paper, System Theoretic Process Analysis (STPA) method was used to analyze the security of Temporary Speed Restriction (TSR) sending scenario in train control system based on vehicle-vehicle communication. The security of this scenario was analyzed according to the analysis process of STPA method. Firstly, Unsafe Control Actions (UCAs) in this scenario were identified and Control Defects (CDs) were analyzed. After that, the corresponding Security Design Requirements (SDRs) were formulated according to the obtained control defects. Finally, the time automata network model of TSR sending scenario was established to verify SDRs. The result shows that: STPA method is suitable to discover the unsafe factors and safety hazards of train control system and take corresponding safety measures to prevent the occurrence of accidents.

Industrial Control Security (ICS) plays an important role in protecting Industrial assets and processed from being tampered by attackers. Recent years witness the fast development of ICS technology. However there are still shortage of techniques and measures to verify the effectiveness of ICS approaches. In this paper, we propose a verification framework named vICS, for security measures in industrial environments. vICS does not requires installing any agent in industrial environments, and could be viewed as a non-intrusive way. We use vICS to evaluate the effectiveness of classic ICS techniques and measures through several experiments. The results shown that vICS provide an feasible solution for verifying the effectiveness of classic ICS techniques and measures for industrial environments.

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.

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%.

Runtime cloud security auditing plays a vital role in mitigating security concerns in a cloud. However, there currently does not exist a comprehensive solution that can protect a cloud tenant against the threats rendered from the multiple levels (e.g., user, virtual, and physical) of the cloud design. Furthermore, most of the existing solutions suffer from slow response time and require significant manual efforts. Therefore, a simple integration of the existing solutions for different levels is not a practical solution. In this paper, we propose a multilevel proactive security auditing system, which overcomes all the above-mentioned limitations. To this end, our main idea is to automatically build a predictive model based on the dependency relationships between cloud events, proactively verify the security policies related to different levels of a cloud by leveraging this model, and finally enforce those policies on the cloud based on the verification results. Our experiments using both synthetic and real data show the practicality and effectiveness of this solution (e.g., responding in a few milliseconds to verify each level of the cloud).