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

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

연구 분야: Verification

학회: International Symposium on Leveraging Applications of Formal Methods

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.