Biblio

The design of attacks for cyber physical systems is critical to assess CPS resilience at design time and run-time, and to generate rich datasets from testbeds for research. Attacks against cyber physical systems distinguish themselves from IT attacks in that the main objective is to harm the physical system. Therefore, both cyber and physical system knowledge are needed to design such attacks. The current practice to generate attacks either focuses on the cyber part of the system using IT cyber security existing body of knowledge, or uses heuristics to inject attacks that could potentially harm the physical process. In this paper, we present a systematic approach to automatically generate integrity attacks from the CPS safety and control specifications, without knowledge of the physical system or its dynamics. The generated attacks violate the system operational and safety requirements, hence present a genuine test for system resilience. We present an algorithm to automate the malware payload development. Several examples are given throughout the paper to illustrate the proposed approach.

Static system configuration provides a significant advantage for the adversaries to discover the assets and launch attacks. Configuration-based moving target defense (MTD) reverses the cyber warfare asymmetry by mutating certain configuration parameters to disrupt the attack planning or increase the attack cost significantly. In this research, we present a methodology for the formal verification of MTD techniques. We formally modeled MTD techniques and verified them against constraints. We use Random Host Mutation (RHM) as a case study for MTD formal verification. The RHM transparently mutates the IP addresses of end-hosts and turns into untraceable moving targets. We apply the formal methodology to verify the correctness, safety, mutation, mutation quality, and deadlock-freeness of RHM using the model checking tool. An adversary is also modeled to validate the effectiveness of the MTD technique. Our experimentation validates the scalability and feasibility of the formal verification methodology.

Humans are a key part of software development, including customers, designers, coders, testers and end users. In this keynote talk I explain why incorporating human-centric issues into software engineering for next-generation applications is critical. I use several examples from our recent and current work on handling human-centric issues when engineering various `smart living' cloud- and edge-based software systems. This includes using human-centric, domain-specific visual models for non-technical experts to specify and generate data analysis applications; personality impact on aspects of software activities; incorporating end user emotions into software requirements engineering for smart homes; incorporating human usage patterns into emerging edge computing applications; visualising smart city-related data; reporting diverse software usability defects; and human-centric security and privacy requirements for smart living systems. I assess the usefulness of these approaches, highlight some outstanding research challenges, and briefly discuss our current work on new human-centric approaches to software engineering for smart living applications.

Web application services have gradually become an important support of Internet services, but are also facing increasingly serious security problems. It is extremely necessary to evaluate the security of Web application services to deal with attacks against them effectively. In this paper, in view of the characteristics of the current attack of Web application services, a Web security analysis model based on the kill chain is established, and the possible attacks against Web application services are analyzed in depth from the perspective of the kill chain. Then, the security of Web application services is evaluated in a quantitative manner. In this way, it can make up the defects of insufficient inspection by the existing security vulnerability model and the security specification of the tracking of Web application services, so as to realize the objective and scientific evaluation of the security state of Web application services.

Although OpenFlow-based SDN networks make it easier to design and test new protocols, when you think of clean slate architectures, their use is quite limited because the parameterization of its flows resides primarily in TCP/IP protocols. Besides, despite the many benefits that SDN offers, some aspects have not yet been adequately addressed, such as management plane activities, network startup, and options for connecting the data plane to the control plane. Based on these issues and limitations, this work presents a bootstrap protocol for SDN-based networks, which allows, beyond the network topology discovery, automatic configuration of an inband control plane. The protocol is designed to act only on layer two, in an autonomous, distributed and deterministic way, with low overhead and has the intent to be the basement for the implementation of other management plane related activities. A formal specification of the protocol is provided. In addition, an analytical model was created to preview the number of required messages to establish the control plane. According to this model, the proposed protocol presents less overhead than similar de-facto protocols used to topology discovery in SDN networks.

Today's highly interconnected and technology reliant environment places great emphasis on the need for secure cyber-physical systems. This work addresses this need by detailing a top down systems security requirements analysis approach for understanding and eliciting security requirements for a notional space system. More specifically, the System-Theoretic Process Analysis approach for Security (STPA-Sec) is used to understand and elicit systems security requirements during the conceptual stage of development. This work employs STPA-Sec in a notional space system to detail the development of functional-level security requirements, design-level engineering considerations, and architectural-level security specifications early in the system life cycle when the solution trade-space is largest rather than merely examining components and adding protections during system operation, maintenance, or sustainment. Lastly, this approach employs a holistic viewpoint which aligns with the systems and software engineering processes as detailed in ISO/IEC/IEEE 152SS and NIST SP SOO-160 Volume 1. This work seeks to advance the science of systems security by providing insight into a viable systems security requirements analysis approach which results in traceable security, safety, and resiliency requirements that can be designed-for, built-to, and verified with confidence.

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.

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.

Engineering complex distributed systems is challenging. Recent solutions for the development of cyber-physical systems (CPS) in industry tend to rely on architectural designs based on service orientation, where the constituent components are deployed according to their service behavior and are to be understood as loosely coupled and mostly independent. In this paper, we develop a workflow that combines contract-based and CPS model-based specifications with service orientation, and analyze the resulting model using fault injection to assess the dependability of the systems. Compositionality principles based on the contract specification help us to make the analysis practical. The presented techniques are evaluated on two case studies.

The Smart Grid is the leading example when talking about complex and critical System-of-Systems (SoS). Specifically regarding the Smart Grids criticality, dependability is a central quality attribute to strive for. Combined with the desire of agility in modern development, conventional systems engineering methods reach their limits in coping with these requirements. However, approaches from model-based or model-driven engineering can reduce complexity and encourage development with rapidly changing requirements. Model-Driven Engineering (MDE) is known to be more successful in a domain specific manner. For that reason, an approach for Domain Specific Systems Engineering (DSSE) in the Smart Grid has already been specially investigated. This Model-Driven Architecture (MDA) approach especially aims the comprehensibility of complex systems. In this context, the traceability of requirements is a centrally pursued attribute. However, achieving continuing traceability between the model of a system and the concrete implementation is still an open issue. To close this gap, the present research paper introduces a Model-Centric Software Development (MCSD) solution for Smart Grid applications. Based on two exploratory case studies, the focus finally lies on the automated generation of partial implementation artifacts and the evaluation of traceability, based on dedicated functional aspects.

The intelligent production line is a complex application with a large number of independent equipment network integration. In view of the characteristics of CPS, the existing modeling methods cannot well meet the application requirements of large scale high-performance system. a formal simulation verification framework and verification method are designed for the performance constraints such as the real-time and security of the intelligent production line based on soft bus. A model-based service-oriented integration approach is employed, which adopts a model-centric way to automate the development course of the entire software life cycle. Developing experience indicate that the proposed approach based on the formal modeling and verification framework in this paper can improve the performance of the system, which is also helpful to achieve the balance of the production line and maintain the reasonable use rate of the processing equipment.

This paper presents an overview of the H2020 project VESSEDIA [9] aimed at verifying the security and safety of modern connected systems also called IoT. The originality relies in using Formal Methods inherited from high-criticality applications domains to analyze the source code at different levels of intensity, to gather possible faults and weaknesses. The analysis methods are mostly exhaustive an guarantee that, after analysis, the source code of the application is error-free. This paper is structured as follows: after an introductory section 1 giving some factual data, section 2 presents the aims and the problems addressed; section 3 describes the project's use-cases and section 4 describes the proposed approach for solving these problems and the results achieved until now; finally, section 5 discusses some remaining future work.

Modern large scale technical systems often face iterative changes on their behaviours with the requirement of validated quality which is not easy to achieve completely with traditional testing. Regression verification is a powerful tool for the formal correctness analysis of software-driven systems. By proving that a new revision of the software behaves similarly as the original version of the software, some of the trust that the old software and system had earned during the validation processes or operation histories can be inherited to the new revision. This trust inheritance by the formal analysis relies on a number of implicit assumptions which are not self-evident but easy to miss, and may lead to a false sense of safety induced by a misunderstood regression verification processes. This paper aims at pointing out hidden, implicit assumptions of regression verification in the context of cyber-physical systems by making them explicit using practical examples. The explicit trust inheritance analysis would clarify for the engineers to understand the extent of the trust that regression verification provides and consequently facilitate them to utilize this formal technique for the system validation.

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.

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.

Public key infrastructures (PKIs) are one of the main building blocks for securing communications over the Internet. Currently, PKIs are under the control of centralized authorities, which is problematic as evidenced by numerous incidents where they have been compromised. The distributed, fault tolerant log of transactions provided by blockchains and more recently, smart contract platforms, constitutes a powerful tool for the decentralization of PKIs. To verify the validity of identity records, blockchain-based identity systems store on chain either all identity records, or, a small (or even constant) sized amount of data for verifying identity records stored off chain. However, as most of these systems have never been implemented, there is little information regarding the practical implications of each design's tradeoffs. In this work, we first implement and evaluate the only provably secure, smart contract based PKI of Patsonakis et al. on top of Ethereum. This construction incurs constant-sized storage at the expense of computational complexity. To explore this tradeoff, we propose and implement a second construction which, eliminates the need for trusted setup, preserves the security properties of Patsonakis et al. and, as illustrated through our evaluation, is the only version with constant-sized state that can be deployed on the live chain of Ethereum. Furthermore, we compare these two systems with the simple approach of most prior works, e.g., the Ethereum Name Service, where all identity records are stored on the smart contract's state, to illustrate several shortcomings of Ethereum and its cost model. We propose several modifications for fine tuning the model, which would be useful to be considered for any smart contract platform like Ethereum so that it reaches its full potential to support arbitrary distributed applications.

Denial of Service (DoS) attacks have been a serious security concern, as no service is, in principle, protected against them. Although a Dolev-Yao intruder with unlimited resources can trivially render any service unavailable, DoS attacks do not necessarily have to be carried out by such (extremely) powerful intruders. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable even to resource-bounded intruders that cannot generate or intercept arbitrary large volumes of traffic. This paper proposes a novel, more refined intruder model where the intruder can only consume at most some specified amount of resources in any given time window. Additionally, we propose protocol theories that may contain timeouts and specify service resource usage during protocol execution. In contrast to the existing resource-conscious protocol verification models, our model allows finer and more subtle analysis of DoS problems. We illustrate the power of our approach by representing a number of classes of DoS attacks, such as, Slow, Asymmetric and Amplification DoS attacks, exhausting different types of resources of the target, such as, number of workers, processing power, memory, and network bandwidth. We show that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems. Finally, we implemented our formal verification model in the rewriting logic tool Maude and analyzed a number of DoS attacks in Maude using Rewriting Modulo SMT in an automated fashion.

Since cyber-physical systems are inherently vulnerable to information leaks, software architects need to reason about security policies to define desired and undesired information flow through a system. The microservice architectural style requires the architects to refine a macro-level security policy into micro-level policies for individual microservices. However, when policies are refined in an ill-formed way, information leaks can emerge on composition of microservices. Related approaches to prevent such leaks do not take into account characteristics of cyber-physical systems like real-time behavior or message passing communication. In this paper, we enable the refinement and verification of information-flow security policies for cyber-physical microservice architectures. We provide architects with a set of well-formedness rules for refining a macro-level policy in a way that enforces its security restrictions. Based on the resulting micro-level policies, we present a verification technique to check if the real-time message passing of microservices is secure. In combination, our contributions prevent information leaks from emerging on composition. We evaluate the accuracy of our approach using an extension of the CoCoME case study.

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.

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

This study introduces formal methods for detection of vulnerabilities in binary code. It considers the transformation of binary code into behavior algebra expressions and formalization of vulnerabilities. The detection method has two levels: behavior matching and symbolic execution with vulnerability pattern matching. This enables more efficient performance.

Modern automotive embedded software is mostly designed using model-based design tools such as Simulink or SCADE, and source code is generated automatically from the models. Formal proof using symbolic model checking has been integrated in these tools and can provide a higher assurance by proving safety-critical properties. Our experience shows that proving properties involving time is rather challenging when they involve long durations and timers. These properties are generally not inductive and even advanced techniques such as PDR/IC3 are unable to handle them on production models in reasonable time. In this paper, we first present our industrial use case and comment on the results obtained with the existing model checkers. Then we present our invariant generator and methodology for selecting invariants according to physical dimensions. They enable the proof of properties with long-running timers. Finally, we discuss their implementation and benchmarks.

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

Today's highly interconnected and technology reliant environment places greater emphasis on the need for dependably secure systems. This work addresses this problem by detailing a systems security analysis approach for understanding and eliciting security requirements for complex cyber-physical systems. First, a readily understandable description of key architectural analysis definitions and desirable characteristics is provided along with a survey of commonly used security architecture analysis approaches. Next, a tailored version of the System-Theoretic Process Analysis approach for Security (STPA-Sec) is detailed in three phases which supports the development of functional-level security requirements, architectural-level engineering considerations, and design-level security criteria. In particular, these three phases are aligned with the systems and software engineering processes defined in the security processes of NIST SP 800-160. Lastly, this work is important for advancing the science of systems security by providing a viable systems security analysis approach for eliciting, defining, and analyzing traceable security, safety, and resiliency requirements which support evaluation criteria that can be designed-for, built-to, and verified with confidence.