Ultra-resilient minimal roots-of-trust and enclaves

Research in the area of trustworthy embedded components, focusing on ultra-resilient computing bases: hardened subsystem architectures and code bases that can be re-used in several target systems. Investigation of reference fault and intrusion tolerant mechanisms based on many-cores and SoC. Integration of some of such components as trusted-trustworthy hybrids of hybridization-aware architectures.

Hybridisation-aware distributed algorithms, models, and architectures

Intrusion tolerant middleware and infrastructures, focusing on frameworks for building dependable and secure services, leveraging modular and distributed systems hybridization.

In the area of innovative BFT algorithms and systems: rethinking BFT-SMR protocol construction for distributed systems in general, in relation to reconfiguration, which can open the door to climbing the next step in the resilience ladder, adaptation.

In the area of cyber-physical systems with R/T communication networks under timing uncertainties and malicious attacks: investigation of Byzantine resilient communication and consensus, like reliable and atomic broadcast as well as state-machine replication protocols, fulfilling real-time requirements whilst being tolerant of Byzantine faults.

In the area of intrusion tolerant middleware for low-level cyber-physical systems (CPS), such as found in in-car vehicle controller architectures: bridging the safety-security gap in ECU-level networks.

In the area of software defined networking (SDN) security and dependability: analyzing the threat plane to SDN, and investigating solution frameworks promoting automatic (unattended) secure and dependable operation. We investigate logically-centralized security and/or dependability architectures for Software-Defined Networks, which we plan in a later stage, to make resilient to faults and attacks.

High-confidence vertical verification of mid-sized software

As part of the general objectives of the lab, we plan to develop verification techniques based on proof assistants, applied to fault and intrusion tolerant (FIT) protocols. We will leverage on the Coq ecosystem, to produce vertical verification (from the high level specification down to the machine code) of the fundamental pieces of the FIT suites we design, and those designed by others, e.g. the precursor PBFT, through mechanical proofs of fundamental properties.

We also plan to enhance the Coq-based framework to reason about Byzantine faults, liveness and more importantly, timeliness (fundamental in R/T systems), as well as to support reasoning about rejuvenation and group membership.

Privacy- and integrity-preserving decentralised data processing

Analysis of the problems of data privacy and integrity in highly sensitive sectors for citizens and organisations, such as those concerned with biomedical, and with financial data. Investigation of infrastructure-aware data storage and processing algorithms and protocols.

In the area of biomedical data privacy and integrity: we are investigating e-health architectures as ecosystems that allow reconciling data sharing with high levels of privacy, and algorithms powering those architectures.

One objective is to identify and filter sensitive genomic sequences immediately they are generated (i.e. at the mouth of the NGS machine) to segregate and protect them appropriately, drawing from and improving recent research in this area, namely with a view on long reads.

With regard to alignment, we wish to improve the privacy x performance product of genome alignment, which currently is either secure and slow, or fast and insecure. We propose to classify genomic information in risk categories, and use alignment algorithms with different security-speed tradeoffs, to process the different categories.

Concerning secure data processing, we look into the problematic of SGX-enclave-based genome alignment, namely situations causing the undesired leakage of sensitive genomic information from SGX enclaves.

In the area of Blockchain/Bitcoin analysis and threat mitigation, and authentication and key management in critical information infrastructures: we have been working on adapting Byzantine fault tolerance and post-compromise security techniques to address these problems.

We are investigating techniques to improve existing blockchain systems, neutralising attacks from powerful adversaries, leveraging Byzantine fault tolerance algorithms to prevent uncertainties, either constraining the formation of colluding cliques that control the network, or guaranteeing the correct operation even when the former temporarily dominated the network. We are investigating as well, mechanisms that take the long-term performance and reliability of a miner into account, preventing flash attacks. Additionally, we intend these techniques to not constrain performance of blockchain, but rather enhance it.

On key infrastructures and authentication, we have been researching on the detection of endpoint compromise and of misuse of secrets, and on authenticating compromisable storage systems.