| 1. |
- Horga, Adrian, 1989-
(författare)
-
Performance and Security Analysis for GPU-Based Applications
- 2022
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Graphics Processing Units (GPUs) are becoming more and more prevalent in general-purpose computing. GPUs are used in areas from embedded systems to super-computing. With applications ranging from fluid dynamics simulations to image processing, machine learning, and encryption, GPU programs need to satisfy not only performance requirements but also various other non-functional constraints. Besides the aspects regarding performance, also security and the worst case execution time (WCET) need to be considered for such GPU applications. In our work, we study such non-functional properties and present approaches to detect and solve issues regarding them.First, we focus on the performance of GPU applications by detecting cache related performance bottlenecks. We detect the root causes of such bottlenecks and provide solutions to reduce their negative impact on performance. We also discuss and compare the impact of cache replacement policies and thread scheduling policies on the performance of GPU applications.Then, we present a measurement-based technique, which combines symbolic execution and genetic algorithms, and is used for estimating the WCET of GPU programs. Our proposed technique helps to produce test inputs that lead towards the WCET of a program. We also propose solutions to alleviate the inherent complexity of GPU programs due to branching behavior and high number of threads running in parallel.In continuation, we propose a technique to expose the side-channel leakage of shared memory in GPU implementations of cryptographic algorithms. We evaluate the robustness of such algorithms in the context of shared memory side-channel leakage. Also, we discuss the security and side-channel leakage for different implementations of the same algorithm.Finally, a formal approach is presented for the detection of GPU shared memory bank conflicts. We explore and discuss the impact of such conflicts on the performance and security of GPU applications. We show how our approach can help in producing inputs that can lead towards the WCET. We also discuss how our approach can be used to evaluate the leakage of the shared memory side-channel for GPU implementations of cryptographic algorithms.
|
|
| 2. |
- Ganjei, Zeinab, 1989-
(författare)
-
Parameterized Verification of Synchronized Concurrent Programs
- 2021
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- There is currently an increasing demand for concurrent programs. Checking the correctness of concurrent programs is a complex task due to the interleavings of processes. Sometimes, violation of the correctness properties in such systems causes human or resource losses; therefore, it is crucial to check the correctness of such systems. Two main approaches to software analysis are testing and formal verification. Testing can help discover many bugs at a low cost. However, it cannot prove the correctness of a program. Formal verification, on the other hand, is the approach for proving program correctness. Model checking is a formal verification technique that is suitable for concurrent programs. It aims to automatically establish the correctness (expressed in terms of temporal properties) of a program through an exhaustive search of the behavior of the system. Model checking was initially introduced for the purpose of verifying finite‐state concurrent programs, and extending it to infinite‐state systems is an active research area.In this thesis, we focus on the formal verification of parameterized systems. That is, systems in which the number of executing processes is not bounded a priori. We provide fully-automatic and parameterized model checking techniques for establishing the correctness of safety properties for certain classes of concurrent programs. We provide an open‐source prototype for every technique and present our experimental results on several benchmarks.First, we address the problem of automatically checking safety properties for bounded as well as parameterized phaser programs. Phaser programs are concurrent programs that make use of the complex synchronization construct of Habanero Java phasers. For the bounded case, we establish the decidability of checking the violation of program assertions and the undecidability of checking deadlock‐freedom. For the parameterized case, we study different formulations of the verification problem and propose an exact procedure that is guaranteed to terminate for some reachability problems even in the presence of unbounded phases and arbitrarily many spawned processes. Second, we propose an approach for automatic verification of parameterized concurrent programs in which shared variables are manipulated by atomic transitions to count and synchronize the spawned processes. For this purpose, we introduce counting predicates that related counters that refer to the number of processes satisfying some given properties to the variables that are directly manipulated by the concurrent processes. We then combine existing works on the counter, predicate, and constrained monotonic abstraction and build a nested counterexample‐based refinement scheme to establish correctness. Third, we introduce Lazy Constrained Monotonic Abstraction for more efficient exploration of well‐structured abstractions of infinite‐state non‐monotonic systems. We propose several heuristics and assess the efficiency of the proposed technique by extensive experiments using our open‐source prototype. Lastly, we propose a sound but (in general) incomplete procedure for automatic verification of safety properties for a class of fault‐tolerant distributed protocols described in the Heard‐Of (HO for short) model. The HO model is a popular model for describing distributed protocols. We propose a verification procedure that is guaranteed to terminate even for unbounded number of the processes that execute the distributed protocol.
|
|
| 3. |
- Zhou, Yuanbin, 1991-
(författare)
-
Synthesis of Safety-Critical Real-Time Systems
- 2022
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Modern safety-critical real-time systems are becoming more and more complex, due to sophisticated applications such as advanced driving assistance, automated driving, advanced infotainment, and applications involving machine learning and deep learning. This has led to increased requirements for the communication infrastructures. Real-time bus-based communication techniques, such as CAN and FlexRay, have been widely adopted for decades, due to their low cost and reliable communication capability. However, the bandwidth provided by these technologies is often not enough for modern safety-critical systems. Time-Sensitive Networking (TSN) is a promising technique that can handle the increasing bandwidth requirements, while meeting real-time constraints and providing Ethernet compatible solutions. We have studied the synthesis of schedules and routes for TSN, in order to fulfill timing and reliability requirements for safety-critical systems. Functional safety is an important goal for such systems, to ensure that no unreasonable risks are taken. This involves handling random and systematic faults, both of which are considered in this work. We synthesize schedules and routes for TSN so that the probability of faulty transmission due to random faults is below a certain threshold.ASIL Decomposition, introduced in the automotive industry, is applied to handle systematic faults, while achieving overall cost minimization. In order to improve schedulability, preemption support in TSN has also been studied. Heuristic algorithms are proposed for all the above contributions to address scalability issues characterized for the constrained synthesis and optimization problem addressed.Traditional designs for safety-critical systems usually deploy a federated architecture, where several processors are available and each processor implements one dedicated function. An important goal is to achieve fault containment. However, due to the increasing complexity of modern safety-critical systems, this architecture is no longer scalable. Therefore, several tasks with different criticality levels are usually integrated on the same computing platform. A key aspect for such systems is to achieve the required independence between tasks at different criticality levels and to guarantee that they do not interfere each other. We have developed a partitioned scheduling technique for mixed-criticality systems to achieve temporal independence, while minimizing the CPU usage.
|
|
| 4. |
- Bujosa Mateu, Daniel
(författare)
-
Enhancing TSN Adoption by Industry : Tools to Support Migrating Ethernet-based Legacy Networks into TSN
- 2023
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- New technologies present opportunities and challenges for industries. One major challenge is the ease, or even feasibility, of its adoption. The Time-Sensitive Networking (TSN) standards offer a range of features relevant to various applications and are key for the transition to Industry 4.0. These features include deterministic zero-jitter, low-latency data transmission, transmission of traffic with various levels of time-criticality on the same network, fault tolerance mechanisms, and advanced network management allowing dynamic reconfiguration.This thesis aims to develop tools that enable the industry to adopt TSN easily and efficiently. Specifically, we create tools that facilitate the migration of legacy networks to TSN, enabling the preservation of most of the legacy systems and solutions while reducing costs and adoption time. Firstly, we introduce LETRA (Legacy Ethernet-based Traffic Mapping Tool), a tool for mapping Ethernet-based legacy traffic to the new TSN traffic classes. Secondly, we develop HERMES (Heuristic Multi-queue Scheduler), a heuristic Time-Triggered (TT) traffic scheduler that can meet the characteristics of legacy systems and provide quick results suitable for reconfiguration. Thirdly, we develop TALESS (TSN with Legacy End-Stations Synchronization), a mechanism to avoid adverse consequences caused by the lack of synchronization between legacy systems and TSN-based ones, as not all legacy systems need to support the TSN synchronization mechanisms. Finally, we improve Stream Reservation Protocol (SRP) to enhance Audio-Video Bridging (AVB) traffic configuration in terms of termination and consistency.
|
|
| 5. |
- Mahfouzi, Rouhollah, 1989-
(författare)
-
Security-Aware Design of Cyber-Physical Systems for Control Applications
- 2021
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- With cyber-physical systems opening to the outside world, security can no longer be considered a secondary issue. In this work, we focus on security threats to control applications in cyber-physical systems. We provide detection, prevention, and mitigation solutions to attacks considering the stringent resource constraints and important properties of such systems. First, we highlight some important properties of control applications that are used to design an intrusion detection and mitigation mechanism. We show how the control laws, derived from the physical properties of control applications, can facilitate the intrusion detection mechanism. We also use a resource management approach to maintain the performance of the control application under attack. Second, we elaborate on the challenges derived from sharing a processor among several controller tasks. We investigate the counter-intuitive timing anomalies that result from such resource sharing and introduce the Butterfly attack which exploits these anomalies. With the Butterfly attack, the adversary interferes with a low criticality and less protected task to change the timing behavior of the other tasks sharing the same platform. We experimentally show how this attack can indirectly destabilize a high criticality and, potentially, more protected task. Then, we consider real-time communication of control applications over a Time-Triggered Ethernet network. We demonstrate the impact of varying delays on control stability and identify the route and schedule constraints that are necessary to guarantee stability. On top of that, we study the impact of encryption and decryption delays on stability and employ a design space exploration approach to maximize security while continuing to satisfy stability guarantees.
|
|
