Next talks

DECEMBER 2022

Programmable Network Security – Challenges and Opportunitiesby Sandra Scott-Hayward (Queen’s University Belfast)

Date : 02 december 2022
Place : Web-conference – https://bbb.inria.fr/all-t0p-qjq-9em (Access code: 192737)

Society’s dependence on communication networks for all aspects of day-to-day living; business, education, entertainment etc. makes “the network” a very attractive target for malicious attack, which cyber criminals are only too eager to exploit, attempting to limit or block access to essential services (e.g., healthcare, banking, critical infrastructure etc.), disrupting our daily lives and causing high cost to businesses and individuals. Advances in networking such as Software-Defined Networking (SDN) and Network Functions Virtualization (NFV) have enabled the network availability and scalability required to support massive global connectivity. With SDN and programmable networks, we introduce flexibility to the control and processing of network traffic, which may be leveraged for in-network security functions. However, as we explore the use of network programmability frameworks and languages such as P4 to accelerate packet processing functions for the flexible and scalable connectivity in next-generation networks, we cannot lose sight of the security of the programmable network itself. Indeed, this flexibility and programmability potentially exposes the network devices to compromise.

This talk will explore the opportunities and challenges of programmable network security, developments in the field, and our related research at CSIT/QUB.

DECEMBER 2022

Thwarting covert adversaries in FHE pipelinesby Sylvain Chatel (EPFL)

Date : 09 december 2022
Room : Aurigny

Fully Homomorphic Encryption (FHE) enables computations to be executed directly on encrypted data without decryption, thus it is becoming an auspicious solution to protect the confidentiality of sensitive data without impeding its usability for the purpose of analytics. While many practical systems rely on FHE to achieve strong privacy guarantees, their constructions only consider an honest-but-curious threat model by default, FHE provides no guarantees that the cryptographic material has been honestly generated nor that the computation was executed correctly on the encrypted data. In particular, in multiparty settings with numerous clients providing data and one or several servers performing the computation, this threat-model becomes even less realistic. Only recently, the cryptographic community has started analysing the guarantees of FHE under stronger adversaries and proposed solutions tailored to the malicious threat-model, however these efforts have remained theoretical and not applicable to real-life scenarios.

In our work, we aim at reducing this gap by considering covert adversaries that are malicious but rational (i.e., they do not want to be detected when cheating) and we build different systems that protect the FHE pipeline against such entities. We first propose an efficient solution to prove the correctness of homomorphic operations performed by a server without compromising the expressiveness of the FHE scheme. Then, we propose different protocols to secure input verification and correct encryption in settings where the client encrypting its data is not trusted. Our constructions provide baselines to evaluate the impact of the threat model change in FHE pipelines with real-life implementation constraints.

DECEMBER 2022

Not so AdHoc testing: formal methods in the standardization of the EDHOC protocolby Charlie Jacomme (Inria Paris)

Date : 16 december 2022
Room : Métivier

We believe that formal methods in security should be leveraged in all the standardisation’s of security protocols in order to strengthen their guarantees. To be effective, such analyses should be:
* maintainable: the security analysis should be performed on every step of the way, i.e. each iteration of the draft;
* pessimistic: all possible threat models, notably all sort of compromise should be considered;
* precise: the analysis should notably include as many real life weaknesses of the concrete cryptographic primitives specified.

In this talk, we illustrate how such a goal may be approached by detailing our analysis of the current IETF draft standard of the EDHOC protocol, as well as our subsequent interactions with its LAKE working group. We will proceed in three steps, first introducing the Sapic+ platform that allows from a single modeling of a protocol to benefit from all the capabilities of multiple automated verification tools (ProVerif, Tamarin, DeepSec). We will then introduce multiple recent advances on how to better model the cryptographic primitives and their real life weaknesses. We will finally show how we leveraged Sapic+ along with the advanced primitive models to analyze the EDHOC protocol and provide feedback to the LAKE working group that has been integrated in latter drafts.

 

Comments are closed.