Towards Automated Security Hardening Using Timed Path Conditions in Shared Bus Systems

Becker-Kupczok, Jonas; Herber, Paula

Research article in edited proceedings (conference) | Peer reviewed

Abstract

Traditionally, many embedded systems are considered to be safety-critical, as they are used in cars, airplanes, or power plants. As embedded systems are more and more connected to the internet, they are becoming increasingly security-critical as well. At the same time, many applications, including in-vehicle networks, internally use shared bus systems that connect many components with varying security levels. While this provides very efficient means for internal communication, it also comes with the risk that confidential information is leaked to components that communicate over the internet and thus might be the target of malicious attacks, or that such components gain access to safety-critical functionality. In this paper, we present initial ideas on how to use timed path conditions for automatic security hardening with regards to violations of information flow security, i.e. confidentiality or integrity of information, in shared bus systems. We propose to enrich ordinary path conditions, obtained from an information flow analysis, with timing information. Then, we use these conditions to find and automatically correct timing errors that may result in illegal information flow. To illustrate our approach, we conduct this method on an example system where concurrently executed components communicate over a time-shared bus, modeled in the system level description language SystemC.

Details about the publication

PublisherMargaria, Tiziana; Steffen, Bernhard
Book titleLeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies - 12th International Symposium, ISoLA 2024, Crete, Greece, October 27-31, 2024, Proceedings, Part IV
Page range115-131
Publishing companySpringer
Place of publicationCham
Title of seriesLecture Notes in Computer Science
Volume of series15222
StatusPublished
Release year2024
Language in which the publication is writtenEnglish
ConferenceLeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies - 12th International Symposium, ISoLA 2024, Crete, Greece
DOI10.1007/978-3-031-75387-9_8
KeywordsAutomatic reengineering; Security hardening; Path conditions; Information flow analysis; Timing

Authors from the University of Münster

Becker-Kupczok, Jonas Lennard
Professorship for practical comuter science
Herber, Paula
Professorship for practical comuter science