CritiX Space Safety and Security Lab: a path towards trustworthy space systems

Speeches/Talks (2023)

Space systems security is an emerging discipline in cyberphysical systems security domain. The research conducted in the field has to be done using realistic assumptions and pieces of equipment that take ... [more ▼]

Space systems security is an emerging discipline in cyberphysical systems security domain. The research conducted in the field has to be done using realistic assumptions and pieces of equipment that take into account multi-disciplinary character of space systems. In CritiX, we've built the Space Systems Safety and Security lab to facilitate the research on space systems and to support the education of future generation of space systems security specialists. [less ▲]

Security Modeling and Analysis of Moving Target Defense in Software Defined Networks

in Security Modeling and Analysis of Moving Target Defense in Software Defined Networks (2022, November 28)

The use of traditional defense mechanisms or intrusion detection systems presents a disadvantage for defenders against attackers since these mechanisms are essentially reactive. Moving target defense (MTD ... [more ▼]

The use of traditional defense mechanisms or intrusion detection systems presents a disadvantage for defenders against attackers since these mechanisms are essentially reactive. Moving target defense (MTD) has emerged as a proactive defense mechanism to reduce this disadvantage by randomly and continuously changing the attack surface of a system to confuse attackers. Although significant progress has been made recently in analyzing the security effectiveness of MTD mechanisms, critical gaps still exist, especially in maximizing security levels and estimating network reconfiguration speed for given attack power. In this paper, we propose a set of Petri Net models and use them to perform a comprehensive evaluation regarding key security metrics of Software-Defined Network (SDNs) based systems adopting a time-based MTD mechanism. We evaluate two use-case scenarios considering two different types of attacks to demonstrate the feasibility and applicability of our models. Our analyses showed that a time-based MTD mechanism could reduce the attackers’ speed by at least 78% compared to a system without MTD. Also, in the best-case scenario, it can reduce the attack success probability by about ten times. [less ▲]

From Graphs to the Science Computer of a Space Telescope. The power of Petri Nets in Systems Engineering

in Graczyk, Rafal; Bujwan, Waldemar; Darmetko, Marcin (Eds.) et al From Graphs to the Science Computer of a Space Telescope. The power of Petri Nets in Systems Engineering (2022, June 23)

Space system engineering has to follow a rigorous design process to manage performance/risk trade-offs at each development stage and possibly across several functional and organizational domains. The ... [more ▼]

Space system engineering has to follow a rigorous design process to manage performance/risk trade-offs at each development stage and possibly across several functional and organizational domains. The process is further complicated by the co-development of multiple solutions, each contributing differently to the goal and with different tradeoffs. Moreover, the design process is iterative, involving both changing requirements and specifications along the different ways that lead to the set goal of the mission. The above requires rigorous modeling that, in addition, must be easily extendible and maintainable across organizational units. On the example of the PROBA-3 science computer (instrument control unit, CCB DPU), we show how Petri Nets can serve as such a simple-to-maintain, holistic model, combining finite-state characterizations with dynamic system behavior caused by hardware-software interactions, to express the component-state dependent end-to-end performance characteristics of the system. The paper elaborates on how the proposed Petri-Net modeling scheme allows for system architecture optimization that result in safely reduced technical margins and in turn substantial savings in components costs. We show that performance metrics, obtained from simulation, correlate well with the real performance characteristics of the flight model of PROBA-3's science computer. [less ▲]

To verify or tolerate, that’s the question

Scientific Conference (2021, December 06)

Formal verification carries the promise of absolute correctness, guaranteed at the highest level of assurance known today. However, inherent to many verification attempts is the assumption that the ... [more ▼]

Formal verification carries the promise of absolute correctness, guaranteed at the highest level of assurance known today. However, inherent to many verification attempts is the assumption that the underlying hardware, the code-generation toolchain and the verification tools are correct, all of the time. While this assumption creates interesting recursive verification challenges, which already have been executed successfully for all three of these elements, the coverage of this assumption remains incomplete, in particular for hardware. Accidental faults, such as single-event upsets, transistor aging and latchups keep causing hardware to behave arbitrarily in situations where such events occur and require other means (e.g., tolerance) to safely operate through them. Targeted attacks, especially physical ones, have a similar potential to cause havoc. Moreover, faults of the above kind may well manifest in such a way that their effects extend to all software layers, causing incorrect behavior, even in proven correct ones. In this position paper, we take a holistic system-architectural point of view on the role of trusted-execution environments (TEEs), their implementation complexity and the guarantees they can convey and that we want to be preserved in the presence of faults. We find that if absolute correctness should remain our visionary goal, TEEs can and should be constructed differently with tolerance embedded at the lowest levels and with verification playing an essential role. Verification should both assure the correctness of the TEE construction protocols and mechanisms as well as help protecting the applications executing inside the TEEs. [less ▲]

Threat Adaptive Byzantine Fault Tolerant State-Machine Replication

Scientific Conference (2021, September)

Critical infrastructures have to withstand advanced and persistent threats, which can be addressed using Byzantine fault tolerant state-machine replication (BFT-SMR). In practice, unattended cyberdefense ... [more ▼]

Critical infrastructures have to withstand advanced and persistent threats, which can be addressed using Byzantine fault tolerant state-machine replication (BFT-SMR). In practice, unattended cyberdefense systems rely on threat level detectors that synchronously inform them of changing threat levels. How- ever, to have a BFT-SMR protocol operate unattended, the state- of-the-art is still to configure them to withstand the highest possible number of faulty replicas f they might encounter, which limits their performance, or to make the strong assumption that a trusted external reconfiguration service is available, which introduces a single point of failure. In this work, we present ThreatAdaptive the first BFT-SMR protocol that is automatically strengthened or optimized by its replicas in reaction to threat level changes. We first determine under which conditions replicas can safely reconfigure a BFT-SMR system, i.e., adapt the number of replicas n and the fault threshold f, so as to outpace an adversary. Since replicas typically communicate with each other using an asynchronous network they cannot rely on consensus to decide how the system should be reconfigured. ThreatAdaptive avoids this pitfall by proactively preparing the reconfiguration that may be triggered by an increasing threat when it optimizes its performance. Our evaluation shows that ThreatAdaptive can meet the latency and throughput of BFT baselines configured statically for a particular level of threat, and adapt 30% faster than previous methods, which make stronger assumptions to provide safety. [less ▲]

PriLok:Citizen-protecting distributed epidemic tracing

E-print/Working paper (2020)

Contact tracing is an important instrument for national health services to fight epidemics. As part of the COVID-19 situation, many proposals have been made for scaling up contract tracing capacities with ... [more ▼]

Contact tracing is an important instrument for national health services to fight epidemics. As part of the COVID-19 situation, many proposals have been made for scaling up contract tracing capacities with the help of smartphone applications, an important but highly critical endeavor due to the privacy risks involved in such solutions. Extending our previously expressed concern, we clearly articulate in this article, the functional and non-functional requirements that any solution has to meet, when striving to serve, not mere collections of individuals, but the whole of a nation, as required in face of such potentially dangerous epidemics. We present a critical information infrastructure, PriLock, a fully-open preliminary architecture proposal and design draft for privacy preserving contact tracing, which we believe can be constructed in a way to fulfill the former requirements. Our architecture leverages the existing regulated mobile communication infrastructure and builds upon the concept of "checks and balances", requiring a majority of independent players to agree to effect any operation on it, thus preventing abuse of the highly sensitive information that must be collected and processed for efficient contact tracing. This is enforced with a largely decentralised layout and highly resilient state-of-the-art technology, which we explain in the paper, finishing by giving a security, dependability and resilience analysis, showing how it meets the defined requirements, even while the infrastructure is under attack. [less ▲]