Abstract We present Taco , a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. Our toolsuite implements three approaches for model checking threshold automata in different decidable fragments known from the literature and two semi-decision procedures going beyond these decidable fragments. Moreover, Taco is a modular, extensible, and well-documented framework for developing algorithms and tools for threshold automata. We present important features, give an overview of the implemented algorithms, and evaluate their performance experimentally.

Machine learning (ML) has become a crucial component in safety-critical systems, such as those used in autonomous vehicle perception. However, the correctness and, therefore, the safety of these systems can be compromised by out-of-distribution data, accidental faults, and security breaches. This paper investigates using a replicated ML architecture to mitigate the risks associated with complex single-points-of-failure. Additionally, it explores the application of rejuvenation to sustain healthy majorities when facing persistent threats. We evaluate the output reliability of the proposed architecture in two case studies: traffic sign detection and perception for autonomous driving. We adopt models and reliability functions, validating our findings using realistic data sets and fault injection experiments. We also evaluate driving safety using the proposed architecture in the CARLA simulator. Our results show that our models can present a good generalization and multi-version ML with proactive rejuvenation can improve correctness and, thus, safety despite faults and cyberattacks.

In modern blockchains, efficient, fair, and fault-tolerant information dissemination is critical for performance and security. Several stages of the transaction lifecycle are affected, from the creation and dissemination of transactions to the dissemination of blocks in the consensus layer. Mempool protocols, such as LØ, already address some of modern blockchains’ security threats. However, others remain unless fairness is embedded most fundamentally in the dissemination layer used by these protocols to share transactions and blocks and to reconcile mempools. This paper introduces HERMES, a novel dissemination protocol for mempools that leverages robust minimal structures to optimize data propagation, balance load, and ensure fairness despite faults and Byzantine actors. Specifically, we address front-running attacks by randomizing the choice of an overlay structure while forcing nodes to prove adherence to the mempools’ dissemination policies and the random choice made. Experimental results show significant performance improvements compared to traditional broadcast protocols for both permissioned and permissionless blockchains.

Abstract We present an algorithm for the repair of parameterized systems that can be represented as well-structured transition systems. The repair problem is, for a given process implementation, to find a refinement such that a given safety property is satisfied by the resulting parameterized system, and deadlocks are avoided. Our algorithm uses a parameterized model checker to determine the correctness of candidate solutions and employs a constraint system to rule out candidates. Parameterized systems that fall into our class include disjunctive systems, pairwise rendezvous systems, broadcast protocols, and certain global synchronization protocols. Moreover, we show that parameterized deadlock detection and similar global properties can be decided in EXPTIME for disjunctive systems, and that deadlock detection is in general undecidable for broadcast protocols.

Abstract Threshold automata are a computational model that has proven to be versatile in modeling threshold-based distributed algorithms and enabling their completely automatic parameterized verification. We present novel techniques for the verification of threshold automata, based on well-structured transition systems, that allow us to extend the expressiveness of both the computational model and the specifications that can be verified. In particular, we extend the model to allow decrements and resets of shared variables, possibly on cycles, and the specifications to general coverability. While these extensions of the model in general lead to undecidability, our algorithms provide a semi-decision procedure. We demonstrate the benefit of our extensions by showing that we can model complex round-based algorithms such as the phase king consensus algorithm and the Red Belly Blockchain protocol (published in 2019), and verify them fully automatically for the first time.

Safety Models for Autonomous Vehicles often neglect fault tolerance, relying on strong assumptions over vehicles’ actuation, such as Responsibility-Sensitive Safety (RSS), which relies on static notions over vehicle’ actuation. This paper proposes to enhance RSS’s proper responses to support fault tolerance during complex maneuvers, specifically overtaking. The proposed approach is carefully built to comply with the original RSS notion of evasive maneuvers. Thus, it can be applied to enable Fault-Tolerant capabilities without losing its original properties. Moreover, the proposed proper responses are modeled using Signal Temporal Logic to promote the verification of system traces using formal methods.

Geo-replication provides disaster recovery after catastrophic accidental failures or attacks, such as fires, blackouts or denial-of-service attacks to a data center or region. Naturally distributed data structures, such as Blockchains, when well designed, are immune against such disruptions, but they also benefit from leveraging locality. In this work, we consolidate the performance of geo-replicated consensus by leveraging novel insights about hierarchical consensus and a construction methodology that allows creating novel protocols from existing building blocks. In particular we show that cluster confirmation, paired with subgroup rotation, allows protocols to safely operate through situations where all members of the global consensus group are Byzantine. We demonstrate our compositional construction by combining the recent HotStuff and Damysus protocols into a hierarchical geo-replicated blockchain with global durability guarantees. We present a compositionality proof and demonstrate the correctness of our protocol, including its ability to tolerate cluster crashes. Our protocol — Orion1— achieves a 20% higher throughput than GeoBFT, the latest hierarchical Byzantine Fault-Tolerant (BFT) protocol.

Modern embedded systems integrate software components onto a single computing platform to meet stringent non-functional requirements of cost, space, weight, and power consumption, amongst others. Moreover, the growing demand for computational power pushed for the adoption of multicore platforms. At the same time, those platforms are often connected to the external world to support a variety of applications. In this context, Machine Learning-based Intrusion Detection Systems (IDS) are of significant importance to guarantee the system’s security during its operation. One approach to be adopted by IDS is to model the behavior of the applications on an embedded system through Performance Monitoring Counters (PMC) and operate during runtime by detecting deviations to the modeled behavior. Notwithstanding, the execution of multiple tasks onto the same multicore platform often incurs shared-resource contention between tasks, which may impair the execution of software components and possibly affect the behavior observed through PMC. In this paper, we assess the impacts of lacking proper resource isolation mechanisms on multicore embedded systems over two Machine Learning-based Intrusion Detection Systems (IDS) solutions that rely on PMC. We use a relevant dataset in the scope of embedded systems control with both tasks monitored while executing without and with the interference of shared-resources contention. Results demonstrate that the lack of isolation can lead to the IDS mechanism losing the ability to recognize the behavior of target software components.

Cooperation among autonomous vehicles is required whenever efficiency or safety prevents maneuvering based solely on the information of individuals. Intersection crossing is a prominent example of such a situation, where obstructed views create safety concerns and where driving on sight would lead to known inefficient solutions. However, communication, a prerequisite for cooperation, and, in general, the complexity of autonomous driving stacks elevate the threat surface beyond justifiable thresholds, creating the potential for cyberattacks to succeed, particularly when targeting the “brain”. Some of these attacks go undetected and may harm passengers, pedestrians, and other traffic participants in a vehicle's proximity. In this paper, we address a fundamental challenge of intrusion-resilient maneuver planning: the question of forming consensus groups given variations in the number$N$of vehicles that participate in complex maneuvers and given that in a larger group of cars, a larger number$F$may have already been compromised by an adversary. Introducing confirmed-location-based group membership, we show how trust-anchor-provided precise location information can be leveraged to establish a ground truth about N and$F$to efficiently solve and agree upon intersection crossing as representative of other complex maneuvers in an$F$fault-and-intrusion tolerant manner.

Collision-free time-triggered communication in distributed safety- and real-time-critical systems relies on approximately synchronized clocks, a-priori-defined communication schedules, and network guardians, synchronized in the same manner, which inhibit a node’s network access outside scheduled times. However, the ever-increasing complexity and interconnectivity of such systemsrender using contemporary network-aware guardians unsuitable: firstly, significant cost, complexity and certification efforts are incurred in developing new network protocol and topology specific guardian solutions. Secondly, contemporary network guardians lack the means to protect against repetitive cyberattacks that exhaust system synchrony.In this paper, we investigate a novel class of time-domain attacks, aimed at exhausting nodes by tampering with the synchrony of their network-agnostic guardians. We counter the attacks by introducing SyncGuard, the first, network-agnostic and time-domain attack-resilient guardian. SyncGuard-equipped systems avoid synchrony exhaustion attacks by jointly coordinating network access and node-rejuvenation.

Genome-wide Association Studies (GWASes) identify genomic variations that are statistically associated with a trait, such as a disease, in a group of individuals. Unfortunately, careless sharing of GWAS statistics might give rise to privacy attacks. Several works attempted to reconcile secure processing with privacy-preserving releases of GWASes. However, we highlight that these approaches remain vulnerable if GWASes utilize overlapping sets of individuals and genomic variations. In such conditions, we show that even when relying on state-of-the-art techniques for protecting releases, an adversary could reconstruct the genomic variations of up to 28.6% of participants, and that the released statistics of up to 92.3% of the genomic variations would enable membership inference attacks. We introduce I-GWAS, a novel framework that securely computes and releases the results of multiple possibly interdependent GWASes. I-GWAS continuously releases privacy-preserving and noise-free GWAS results as new genomes become available.

Genome-wide association studies (GWAS) identify correlations between the genetic variants and an observable characteristic such as a disease. Previous works presented privacy-preserving distributed algorithms for a federation of genome data holders that spans multiple institutional and legislative domains to securely compute GWAS results. However, these algorithms have limited applicability, since they still require a centralized instance to operate on the data and decide whether GWAS results can be safely disclosed, which violates privacy regulations, such as GDPR. In this work, we introduce GenDPR, a distributed middleware that leverages Trusted Execution Environments (TEEs) to securely determine a subset of the potential GWAS statistics that can be safely released. GenDPR achieves the same accuracy as centralized solutions, but requires transferring significantly less data because TEEs only exchange intermediary results but no genomes. Additionally, GenDPR can be configured to tolerate all-but-one honest-but-curious federation members colluding with the aim to expose genomes of correct members.

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.

Today, leveraging the enormous modular power, diversity and flexibility of manycore systems-on-a-chip (SoCs) requires careful orchestration of complex and heterogeneous resources, a task left to low-level software, e.g., hypervisors. In current architectures, this software forms a single point of failure and worthwhile target for attacks: once compromised, adversaries can gain access to all information and full control over the platform and the environment it controls. This article proposes Midir, an enhanced manycore architecture, effecting a paradigm shift from SoCs to distributed SoCs. Midir changes the way platform resources are controlled, by retrofitting tile-based fault containment through well known mechanisms, while securing low-overhead quorum-based consensus on all critical operations, in particular privilege management and, thus, management of containment domains. Allowing versatile redundancy management, Midir promotes resilience for all software levels, including at low level. We explain this architecture, its associated algorithms and hardware mechanisms and show, for the example of a Byzantine fault tolerant microhypervisor, that it outperforms the highly efficient MinBFT by one order of magnitude.

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. However, 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.

The advent of next-generation sequencing (NGS) machines made DNA sequencing cheaper, but also put pressure on the genomic life-cycle, which includes aligning millions of short DNA sequences, called reads, to a reference genome. On the performance side, efficient algorithms have been developed, and parallelized on public clouds. On the privacy side, since genomic data are utterly sensitive, several cryptographic mechanisms have been proposed to align reads more securely than the former, but with a lower performance. This paper presents DNA-SeAl a novel contribution to improving the privacy × performance product in current genomic workflows. First, building on recent works that argue that genomic data needs to be treated according to a threat-risk analysis, we introduce a multi-level sensitivity classification of genomic variations designed to prevent the amplification of possible privacy attacks. We show that the usage of sensitivity levels reduces future re-identification risks, and that their partitioning helps prevent linkage attacks. Second, after extending this classification to reads, we show how to align and store reads using different security levels. To do so, DNA-SeAl extends a recent reads filter to classify unaligned reads into sensitivity levels, and adapts existing alignment algorithms to the reads sensitivity. We show that using DNA-SeAl allows high performance gains whilst enforcing high privacy levels in hybrid cloud environments.

Much effort has been put into improving the predictability of real-time systems, especially in safety-critical environments, which provides designers with a rich set of methods and tools to attest safety in situations with no or a limited number of accidental faults. However, with increasing connectivity of real-time systems and a wide availability of increasingly sophisticated exploits, security and, in particular, the consequences of predictability on security become concerns of equal importance. Time-triggered scheduling with offline constructed tables provides determinism and simplifies timing inference, however, at the same time, time-triggered scheduling creates vulnerabilities by allowing attackers to target their attacks to specific, deterministically scheduled and possibly safety-critical tasks. In this paper, we analyze the severity of these vulnerabilities by assuming successful compromise of a subset of the tasks running in a real-time system and by investigating the attack potential that attackers gain from them. Moreover, we discuss two ways to mitigate direct attacks: slot-level online randomization of schedules, and offline schedule-diversification. We evaluate these mitigation strategies with a real-world case study to show their practicability for mitigating not only accidentally malicious behavior, but also malicious behavior triggered by attackers on purpose.

Our increasing dependence on complex and critical information infrastructures and the emerging threat of sophisticated attacks, ask for extended efforts to ensure the correctness and security of these systems. Byzantine fault-tolerant state-machine replication (BFT-SMR) provides a way to harden such systems. It ensures that they maintain correctness and availability in an application-agnostic way, provided that the replication protocol is correct and at least $$n-f$$ out of n replicas survive arbitrary faults. This paper presents Velisarios, a logic-of-events based framework implemented in Coq, which we developed to implement and reason about BFT-SMR protocols. As a case study, we present the first machine-checked proof of a crucial safety property of an implementation of the area’s reference protocol: PBFT.

Fully autonomous driving is one if not the killer application for the upcoming decade of real-time systems. However, in the presence of increasingly sophisticated attacks by highly skilled and well equipped adversarial teams, autonomous driving must not only guarantee timeliness and hence safety. It must also consider the dependability of the software concerning these properties while the system is facing attacks. For distributed systems, fault-and-intrusion tolerance toolboxes already offer a few solutions to tolerate partial compromise of the system behind a majority of healthy components operating in consensus. In this paper, we present a concept of an intrusion-tolerant architecture for autonomous driving. In such a scenario, predictability and recovery challenges arise from the inclusion of increasingly more complex software on increasingly less predictable hardware. We highlight how an intrusion tolerant design can help solve these issues by allowing timeliness to emerge from a majority of complex components being fast enough, often enough while preserving safety under attack through pre-computed fail safes.

Time-triggered real-time systems achieve deterministic behaviour, making them suitable for safety-critical environments. However, this determinism also allows attackers to finetune attacks after studying the system behaviour through side channels, targeting safety-critical victim tasks. Assuming fault independence, replication tolerates both random and malicious faults of up to f replicas. Yet, directed attacks violate the fault independence assumption. This violation possibly gives attackers the edge to compromise more than f replicas simultaneously, in particular if they can mount the attack from already compromised components. In this paper, we sketch mitigation strategies for time-triggered systems with task replication to withstand directed timing attacks and show preliminary results on their effectiveness and practicality.

Technologies such as Industry 4.0 or assisted/autonomous driving are relying on highly customized cyber-physical realtime systems. Those systems are designed to match functional safety regulations and requirements such as EN ISO 13849, EN IEC 62061 or ISO 26262. However, as systems – especially vehicles – are becoming more connected and autonomous, they become more likely to suffer from new attack vectors. New features may meet the corresponding safety requirements but they do not consider adversaries intruding through security holes with the purpose of bringing vehicles into unsafe states. As research goal, we want to bridge the gap between security and safety in cyber-physical real-time systems by investigating real-time-aware intrusion-tolerant architectures for automotive use-cases.

Sequencing thousands of human genomes has enabled breakthroughs in many areas, among them precision medicine, the study of rare diseases, and forensics. However, mass collection of such sensitive data entails enormous risks if not protected to the highest standards. In this article, we follow the position and argue that post-alignment privacy is not enough and that data should be automatically protected as early as possible in the genomics workflow, ideally immediately after the data is produced. We show that a previous approach for filtering short reads cannot extend to long reads and present a novel filtering approach that classifies raw genomic data (i.e., whose location and content is not yet determined) into privacy-sensitive (i.e., more affected by a successful privacy attack) and non-privacy-sensitive information. Such a classification allows the fine-grained and automated adjustment of protective measures to mitigate the possible consequences of exposure, in particular when relying on public clouds. We present the first filter that can be indistinctly applied to reads of any length, i.e., making it usable with any recent or future sequencing technologies. The filter is accurate, in the sense that it detects all known sensitive nucleotides except those located in highly variable regions (less than 10 nucleotides remain undetected per genome instead of 100,000 in previous works). It has far less false positives than previously known methods (10% instead of 60%) and can detect sensitive nucleotides despite sequencing errors (86% detected instead of 56% with 2% of mutations). Finally, practical experiments demonstrate high performance, both in terms of throughput and memory consumption.

We formalize the soundness theorem for differential dynamic logic, a logic for verifying hybrid systems. To increase confidence in the formalization, we present two versions: one in Isabelle/HOL and one in Coq. We extend the metatheory to include features used in practice, such as systems of differential equations and functions of multiple arguments. We demonstrate the viability of constructing a verified kernel for the hybrid systems theorem prover KeYmaera X by embedding proof checkers for differential dynamic logic in Coq and Isabelle. We discuss how different provers and libraries influence the design of the formalization.

Silicon nanowire reconfigurable field effect transistors (SiNW RFETs) abolish the physical separation of n-type and p-type transistors by taking up both roles in a configurable way within a doping-free technology. However, the potential of transistor-level reconfigurability has not been demonstrated in larger circuits, so far. In this paper, we present first steps to a new compact and efficient design of combinational circuits by employing transistor-level reconfiguration. We contribute new basic gates realized with silicon nanowires, such as 2/3-XOR and MUX gates. Exemplifying our approach with 4-bit, 8-bit and 16-bit conditional carry adders, we were able to reduce the number of transistors to almost one half. With our current case study we show that SiNW technology can reduce the required chip area by 16 despite larger size of the individual transistor, and improve circuit speed by 26%.

The world is becoming an immense critical information infrastructure, with the fast and increasing entanglement of utilities, telecommunications, Internet, cloud, and the emerging IoT tissue. This may create enormous opportunities, but also brings about similarly extreme security and dependability risks. We predict an increase in very sophisticated targeted attacks, or advanced persistent threats (APT), and claim that this calls for expanding the frontier of security and dependability methods and techniques used in our current CII. Extreme threats require extreme defenses: we propose resilience as a unifying paradigm to endow systems with the capability of dynamically and automatically handling extreme adversary power, and sustaining perpetual and unattended operation. In this position paper, we present this vision and describe our methodology, as well as the assurance arguments we make for the ultra-resilient components and protocols they enable, illustrated with case studies in progress.

In the last decade, the number of available cores increased and heterogeneity grew. In this work, we ask the question whether the design of the current operating systems (OSes) is still appropriate if these trends continue and lead to abundantly available but heterogeneous cores, or whether it forces a fundamental rethinking of how systems are designed. We argue that: 1. hiding heterogeneity behind a common hardware interface unifies, to a large extent, the control and coordination of cores and accelerators in the OS, 2. isolating at the network-on-chip rather than with processor features (like privileged mode, memory management unit, ...), allows running untrusted code on arbitrary cores, and 3. providing OS services via protocols over the network-on-chip, instead of via system calls, makes them accessible to arbitrary types of cores as well.

Cyber-physical systems (CPSs), due to their direct influence on the physical world, have to meet extended security and dependability requirements. This is particularly true for CPS that operate in close proximity to humans or that control resources that, when tampered with, put all our lives at stake. In this paper, we review the challenges and some early solutions that arise at the architectural and operating-system level when we require cyber-physical systems and CPS infrastructure to withstand advanced and persistent threats. We found that although some of the challenges we identified are already matched by rudimentary solutions, further research is required to ensure sustainable and dependable operation of physically exposed CPS infrastructure and, more importantly, to guarantee graceful degradation in case of malfunction or attack.

Many-core systems are increasingly used in real-time settings to meet the performance requirements of advanced applications such as the classification and tracking of dynamic objects for autonomous driving [1] or the generation of safe trajectories through rough terrain [2]. Task sets of these applications are often mixtures of short running, low latency tasks, such as the various filtering steps required for signal or image processing, and long running tasks, such as route planning, which occupy their assigned core for extended periods of time. Short running tasks often follow a data flow programming paradigm and are organized into directed acyclic graphs (DAG) based on their input-/output-dependencies. Once these dependencies are met, they execute without further task interactions until they complete producing outputs for subsequent tasks. Long running tasks on the other hand interact frequently with other tasks, accessing data located in the memories of remote cores or interacting with operating-system services. This demonstrator shows how both types of applications can be integrated into a single many-core architecture.

The unbelievable properties of our information processing capabilities regarding the processing of big data, resilience, and energy efficiency are inspiration sources for the optimization and the rethinking of the principles of electronic information processing. Here, we present an approach of integrated circuits intended to solve chemical problems by active processing of chemical information.

In the past, we have silently accepted that energy consumption in real-time and embedded systems is subordinate to time. That is, we have tried to reduce energy always under the constraint that all deadlines must be met. In mixed-criticality systems however, schedulers respect that some tasks are more important than others and guarantee their completion even at the expense of others. We believe in these systems the role of the energy budget has changed and it is time to ask whether energy has surpassed timeliness. Investigating energy as a further dimension of mixed-criticality systems, we show in a realistic scenario that a subordinate handling of energy can lead to violations of the mixed-criticality guarantees that can only be avoided if energy becomes an equally important resource as time.

Coordinating access to shared resources is a challenging task, in particular if real-time and security aspects have to be integrated into the same system. However, rather than exacerbating the problem, we found that considering real-time guarantees actually simplifies the security problem of preventing information leakage over shared-resource covert channels. We introduce a transformation for standard real-time resource locking protocols and show that protocols transformed in this way preserve the confidentiality guarantees of the schedulers on which they are based. Through this transformation, we were able to prove that four out of the seven investigated protocols are information-flow secure.

Energy has become the dominating concern for resource management. We advocate an energy-centered design approach for resource-management systems. To this end, we structure systems in layers, where layers implement higher-level resources using lower-level ones. For each layer, we describe the relation of the performance delivered for the higher layer to its demands on the lower layer and refer to that relation as demand/performance function. The lowest layers are rooted in hardware and express demand in terms of energy, the highest layers provide performance in terms of user-specific utility, thus leading to an Energy/Utility characterization of a complete system. We describe the overall approach, some research challenges and few initial results on the representation of demand/performance functions.

Recently, the application of virtual-machine technology to integrate real-time systems into a single host has received significant attention and caused controversy. Drawing two examples from mixed-criticality systems, we demonstrate that current virtualization technology, which handles guest scheduling as a black box, is incompatible with this modern scheduling discipline. However, there is a simple solution by exporting sufficient information for the host scheduler to overcome this problem. We describe the problem, the modification required on the guest and show on the example of two practical real-time operating systems how flattening the hierarchical scheduling problem resolves the issue. We conclude by showing the limitations of our technique at the current state of our research.

At WITS 2005, Warnier et al. published an algorithm to statically check confidentiality of programs with dynamic labels. Unlike prior approaches, their method allows for temporary breaches of confidentiality. However, they share the commonly made assumption that programs run entirely in private memory. Thus, interaction with and observationof the checked program is restricted to program start and termination respectively. This paper extends Warnier’s approach in two fundamental aspects: shared memory and synchronisation. Through shared memory other programs may observe and interact with the checked program at memory-access granularity. Synchronisation renders parts of the shared memory inaccessible to those programs which adhere to the locking policy. We provide a mechanically-checked soundness proof and show the effectiveness of a countermeasure to the AES cache side-channel attack.

A practically feasible modification to fixed-priority schedulers allows to avoid timing channels despite threads having access to precise clocks. This modification is rather simple: we compute at admission time a static predicate that states whether a thread may possibly leak information; if such a thread blocks we switch to the idle thread instead. We describe the modified scheduler, provide a mechanical PVS-based proof of noninterference and show how common admission algorithms can be reused to give real-time guarantees for this modified scheduler. While providing similar isolation guarantees, our approach outperforms timepartitioning schedulers in terms of achieved real-time guarantees.