Visible to the public Biblio

Filters: Keyword is safety-critical software  [Clear All Filters]
Höfig, K., Klug, A..  2018.  SEnSE – An Architecture for a Safe and Secure Integration of Safety-Critical Embedded Systems. 2018 26th International Conference on Software, Telecommunications and Computer Networks (SoftCOM). :1–5.

Embedded systems that communicate with each other over the internet and build up a larger, loosely coupled (hardware) system with an unknown configuration at runtime is often referred to as a cyberphysical system. Many of these systems can become, due to its associated risks during their operation, safety critical. With increased complexity of such systems, the number of configurations can either be infinite or even unknown at design time. Hence, a certification at design time for such systems that documents a safe interaction for all possible configurations of all participants at runtime can become unfeasible. If such systems come together in a new configuration, a mechanism is required that can decide whether or not it is safe for them to interact. Such a mechanism can generally not be part of such systems for the sake of trust. Therefore, we present in the following sections the SEnSE device, short for Secure and Safe Embedded, that tackles these challenges and provides a secure and safe integration of safety-critical embedded systems.

Nichols, W., Hawrylak, P. J., Hale, J., Papa, M..  2018.  Methodology to Estimate Attack Graph System State from a Simulation of a Nuclear Research Reactor. 2018 Resilience Week (RWS). :84-87.
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.
Kang, K., Baek, Y., Lee, S., Son, S. H..  2017.  An Attack-Resilient Source Authentication Protocol in Controller Area Network. 2017 ACM/IEEE Symposium on Architectures for Networking and Communications Systems (ANCS). :109–118.

While vehicle to everything (V2X) communication enables safety-critical automotive control systems to better support various connected services to improve safety and convenience of drivers, they also allow automotive attack surfaces to increase dynamically in modern vehicles. Many researchers as well as hackers have already demonstrated that they can take remote control of the targeted car by exploiting the vulnerabilities of in-vehicle networks such as Controller Area Networks (CANs). For assuring CAN security, we focus on how to authenticate electronic control units (ECUs) in real-time by addressing the security challenges of in-vehicle networks. In this paper, we propose a novel and lightweight authentication protocol with an attack-resilient tree algorithm, which is based on one-way hash chain. The protocol can be easily deployed in CAN by performing a firmware update of ECU. We have shown analytically that the protocol achieves a high level of security. In addition, the performance of the proposed protocol is validated on CANoe simulator for virtual ECUs and Freescale S12XF used in real vehicles. The results show that our protocol is more efficient than other authentication protocol in terms of authentication time, response time, and service delay.

Pasareanu, C..  2017.  Symbolic execution and probabilistic reasoning. 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). :1–1.
Summary form only given. Symbolic execution is a systematic program analysis technique which explores multiple program behaviors all at once by collecting and solving symbolic path conditions over program paths. The technique has been recently extended with probabilistic reasoning. This approach computes the conditions to reach target program events of interest and uses model counting to quantify the fraction of the input domain satisfying these conditions thus computing the probability of event occurrence. This probabilistic information can be used for example to compute the reliability of an aircraft controller under different wind conditions (modeled probabilistically) or to quantify the leakage of sensitive data in a software system, using information theory metrics such as Shannon entropy. In this talk we review recent advances in symbolic execution and probabilistic reasoning and we discuss how they can be used to ensure the safety and security of software systems.
Nashaat, M., Ali, K., Miller, J..  2017.  Detecting Security Vulnerabilities in Object-Oriented PHP Programs. 2017 IEEE 17th International Working Conference on Source Code Analysis and Manipulation (SCAM). :159–164.

PHP is one of the most popular web development tools in use today. A major concern though is the improper and insecure uses of the language by application developers, motivating the development of various static analyses that detect security vulnerabilities in PHP programs. However, many of these approaches do not handle recent, important PHP features such as object orientation, which greatly limits the use of such approaches in practice. In this paper, we present OOPIXY, a security analysis tool that extends the PHP security analyzer PIXY to support reasoning about object-oriented features in PHP applications. Our empirical evaluation shows that OOPIXY detects 88% of security vulnerabilities found in micro benchmarks. When used on real-world PHP applications, OOPIXY detects security vulnerabilities that could not be detected using state-of-the-art tools, retaining a high level of precision. We have contacted the maintainers of those applications, and two applications' development teams verified the correctness of our findings. They are currently working on fixing the bugs that lead to those vulnerabilities.

Fellmuth, J., Herber, P., Pfeffer, T. F., Glesner, S..  2017.  Securing Real-Time Cyber-Physical Systems Using WCET-Aware Artificial Diversity. 2017 IEEE 15th Intl Conf on Dependable, Autonomic and Secure Computing, 15th Intl Conf on Pervasive Intelligence and Computing, 3rd Intl Conf on Big Data Intelligence and Computing and Cyber Science and Technology Congress(DASC/PiCom/DataCom/CyberSciTech). :454–461.

Artificial software diversity is an effective way to prevent software vulnerabilities and errors to be exploited in code-reuse attacks. This is achieved by lowering the individual probability of a successful attack to a level that makes the attack unfeasible. Unfortunately, the existing approaches are not applicable to safety-critical real-time systems as they induce unacceptable performance overheads, they violate safety and timing guarantees, or they assume hardware resources which are typically not available in embedded systems. To overcome these problems, we propose a safe diversity approach that preserves the timing properties of real-time processes by controlling its impact on the worst case execution time (WCET). Our main idea is to use block-level diversity with a large, but fixed set of movable instruction sequences, and to use static WCET analysis to identify non-critical areas of code where it can safely be split into more movable instruction sequences.

Benthall, S..  2017.  Assessing Software Supply Chain Risk Using Public Data. 2017 IEEE 28th Annual Software Technology Conference (STC). :1–5.

The software supply chain is a source of cybersecurity risk for many commercial and government organizations. Public data may be used to inform automated tools for detecting software supply chain risk during continuous integration and deployment. We link data from the National Vulnerability Database (NVD) with open version control data for the open source project OpenSSL, a widely used secure networking library that made the news when a significant vulnerability, Heartbleed, was discovered in 2014. We apply the Alhazmi-Malaiya Logistic (AML) model for software vulnerability discovery to this case. This model predicts a sigmoid cumulative vulnerability discovery function over time. Some versions of OpenSSL do not conform to the predictions of the model because they contain a temporary plateau in the cumulative vulnerability discovery plot. This temporary plateau feature is an empirical signature of a security failure mode that may be useful in future studies of software supply chain risk.

Schulz, T., Golatowski, F., Timmermann, D..  2017.  Evaluation of a Formalized Encryption Library for Safety-Critical Embedded Systems. 2017 IEEE International Conference on Industrial Technology (ICIT). :1153–1158.

Complex safety-critical devices require dependable communication. Dependability includes confidentiality and integrity as much as safety. Encrypting gateways with demilitarized zones, Multiple Independent Levels of Security architectures and the infamous Air Gap are diverse integration patterns for safety-critical infrastructure. Though resource restricted embedded safety devices still lack simple, certifiable, and efficient cryptography implementations. Following the recommended formal methods approach for safety-critical devices, we have implemented proven cryptography algorithms in the qualified model based language Scade as the Safety Leveraged Implementation of Data Encryption (SLIDE) library. Optimization for the synchronous dataflow language is discussed in the paper. The implementation for public-key based encryption and authentication is evaluated for real-world performance. The feasibility is shown by execution time benchmarks on an industrial safety microcontroller platform running a train control safety application.

Resch, S., Paulitsch, M..  2017.  Using TLA+ in the Development of a Safety-Critical Fault-Tolerant Middleware. 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). :146–152.

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.

Brunner, M., Huber, M., Sauerwein, C., Breu, R..  2017.  Towards an Integrated Model for Safety and Security Requirements of Cyber-Physical Systems. 2017 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :334–340.

Increasing interest in cyber-physical systems with integrated computational and physical capabilities that can interact with humans can be identified in research and practice. Since these systems can be classified as safety- and security-critical systems the need for safety and security assurance and certification will grow. Moreover, these systems are typically characterized by fragmentation, interconnectedness, heterogeneity, short release cycles, cross organizational nature and high interference between safety and security requirements. These properties combined with the assurance of compliance to multiple standards, carrying out certification and re-certification, and the lack of an approach to model, document and integrate safety and security requirements represent a major challenge. In order to address this gap we developed a domain agnostic approach to model security and safety requirements in an integrated view to support certification processes during design and run-time phases of cyber-physical systems.

Kwiatkowska, M..  2016.  Advances and challenges of quantitative verification and synthesis for cyber-physical systems. 2016 Science of Security for Cyber-Physical Systems Workshop (SOSCYPS). :1–5.

We are witnessing a huge growth of cyber-physical systems, which are autonomous, mobile, endowed with sensing, controlled by software, and often wirelessly connected and Internet-enabled. They include factory automation systems, robotic assistants, self-driving cars, and wearable and implantable devices. Since they are increasingly often used in safety- or business-critical contexts, to mention invasive treatment or biometric authentication, there is an urgent need for modelling and verification technologies to support the design process, and hence improve the reliability and reduce production costs. This paper gives an overview of quantitative verification and synthesis techniques developed for cyber-physical systems, summarising recent achievements and future challenges in this important field.

Dutta, R. G., Guo, Xiaolong, Zhang, Teng, Kwiat, K., Kamhoua, C., Njilla, L., Jin, Y..  2017.  Estimation of safe sensor measurements of autonomous system under attack. 2017 54th ACM/EDAC/IEEE Design Automation Conference (DAC). :1–6.
The introduction of automation in cyber-physical systems (CPS) has raised major safety and security concerns. One attack vector is the sensing unit whose measurements can be manipulated by an adversary through attacks such as denial of service and delay injection. To secure an autonomous CPS from such attacks, we use a challenge response authentication (CRA) technique for detection of attack in active sensors data and estimate safe measurements using the recursive least square algorithm. For demonstrating effectiveness of our proposed approach, a car-follower model is considered where the follower vehicle's radar sensor measurements are manipulated in an attempt to cause a collision.
Alqahtani, S. S., Eghan, E. E., Rilling, J..  2017.  Recovering Semantic Traceability Links between APIs and Security Vulnerabilities: An Ontological Modeling Approach. 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST). :80–91.

Over the last decade, a globalization of the software industry took place, which facilitated the sharing and reuse of code across existing project boundaries. At the same time, such global reuse also introduces new challenges to the software engineering community, with not only components but also their problems and vulnerabilities being now shared. For example, vulnerabilities found in APIs no longer affect only individual projects but instead might spread across projects and even global software ecosystem borders. Tracing these vulnerabilities at a global scale becomes an inherently difficult task since many of the existing resources required for such analysis still rely on proprietary knowledge representation. In this research, we introduce an ontology-based knowledge modeling approach that can eliminate such information silos. More specifically, we focus on linking security knowledge with other software knowledge to improve traceability and trust in software products (APIs). Our approach takes advantage of the Semantic Web and its reasoning services, to trace and assess the impact of security vulnerabilities across project boundaries. We present a case study, to illustrate the applicability and flexibility of our ontological modeling approach by tracing vulnerabilities across project and resource boundaries.

Petullo, W.M., Wenyuan Fei, Solworth, J.A., Gavlin, P..  2014.  Ethos' Deeply Integrated Distributed Types. Security and Privacy Workshops (SPW), 2014 IEEE. :167-180.

Programming languages have long incorporated type safety, increasing their level of abstraction and thus aiding programmers. Type safety eliminates whole classes of security-sensitive bugs, replacing the tedious and error-prone search for such bugs in each application with verifying the correctness of the type system. Despite their benefits, these protections often end at the process boundary, that is, type safety holds within a program but usually not to the file system or communication with other programs. Existing operating system approaches to bridge this gap require the use of a single programming language or common language runtime. We describe the deep integration of type safety in Ethos, a clean-slate operating system which requires that all program input and output satisfy a recognizer before applications are permitted to further process it. Ethos types are multilingual and runtime-agnostic, and each has an automatically generated unique type identifier. Ethos bridges the type-safety gap between programs by (1) providing a convenient mechanism for specifying the types each program may produce or consume, (2) ensuring that each type has a single, distributed-system-wide recognizer implementation, and (3) inescapably enforcing these type constraints.