MAY 2022 |
|
|
“ Port Contention Goes Portable: Port Contention Side Channels in Web Browsers” by Thomas Rokicki (Univ Rennes, CNRS, IRISA) Date : 13 may 2022 Microarchitectural side-channel attacks can derive secrets from the execution of vulnerable programs. Their implementation in web browsers represents a considerable extension of their attack surface, as a user simply browsing a malicious website, or even a malicious third-party advertisement in a benign cross-origin isolated website, can be a victim.
|
|
APRIL 2022 |
|
|
“On MILP modelisations ” by Christina Boura (UVSQ, CNRS, LMV) Date : 29 april 2022 Modelizing a problem using linear constraints and solving it by some Mixed Integer Linear Programming (MILP) solver is a popular approach in many domains of computer science. In this talk we present and compare different new techniques to modelize any subset of {0,1}^n for MILP. We then discuss the efficiency of our models by applying them to the search of differential paths, a classical problem in symmetric cryptography.
|
|
MARCH 2022 |
|
|
“Built on sand: on the security of Collaborative Machine Learning ” by Dario PASQUINI (EPFL) Date : 25 march 2022 This talk is about inaccurate assumptions, unrealistic trust models, and flawed methodologies affecting current collaborative machine learning techniques. In the presentation, we cover different security issues concerning both emerging approaches and well-established solutions in privacy-preserving collaborative machine learning. We start by discussing the inherent insecurity of Split Learning and peer-to-peer collaborative learning. Then, we talk about the soundness of current Secure Aggregation protocols in Federated Learning, showing that those do not provide any additional level of privacy to users. Ultimately, the objective of this talk is to highlight the general errors and flawed approaches we all should avoid in devising and implementing “privacy-preserving collaborative machine learning”.
|
|
FEBRUARY 2022 |
|
|
“Search-Based Local Black-Box Deobfuscation: Understand, Improve and Mitigate” by Grégoire Menguy (CEA LIST) Date : 25 february 2022 Code obfuscation aims at protecting Intellectual Property and other secrets embedded into software from being retrieved. Recent works leverage advances in artificial intelligence (AI) with the hope of getting blackbox deobfuscators completely immune to standard (whitebox) protection mechanisms. While promising, this new field of AI-based, and more specifically search-based blackbox deobfuscation, is still in its infancy. We deepen the state of search-based blackbox deobfuscation in three key directions: understand the current state-of-the-art, improve over it and design dedicated protection mechanisms. In particular, we define a novel generic framework for search-based blackbox deobfuscation encompassing prior work and highlighting key components; we are the first to point out that the search space underlying code deobfuscation is too unstable for simulation-based methods (e.g., Monte Carlo Tree Search used in prior work) and advocate the use of robust methods such as S-metaheuristics; we propose the new optimized search-based blackbox deobfuscator Xyntia which significantly outperforms prior work in terms of success rate (especially with small time budget) while being completely immune to the most recent anti-analysis code obfuscation methods; and finally we propose two novel protections against search-based blackbox deobfuscation, allowing to counter Xyntia powerful attacks. This work has been published at ACM CCS 2021.
|
|
FEBRUARY 2022 |
|
|
“Model Stealing Attacks Against Inductive Graph Neural Networks” by Yufei Han (INRIA) Date : 18 february 2022 Many real-world data come in the form of graphs. Graph neural networks (GNNs), a new family of machine learning (ML) models, have been proposed to fully leverage graph data to build powerful applications. In particular, the inductive GNNs, which can generalize to unseen data, become mainstream in this direction. Machine learning models have shown great potential in various tasks and have been deployed in many real-world scenarios. To train a good model, a large amount of data as well as computational resources are needed, leading to valuable intellectual property. Previous research has shown that ML models are prone to model stealing attacks, which aim to steal the functionality of the target models. However, most of them focus on the models trained with images and texts. On the other hand, little attention has been paid to models trained with graph data, i.e., GNNs. In this paper, we fill the gap by proposing the first model stealing attacks against inductive GNNs. We systematically define the threat model and propose six attacks based on the adversary’s background knowledge and the responses of the target models. Our evaluation on six benchmark datasets shows that the proposed model stealing attacks against GNNs achieve promising performance.
|
|
JANUARY 2022 |
|
|
“Security and privacy in personal data management systems” by Nicolas Anciaux (INRIA) Date : 28 january 2022 Personal Data Management Systems (called PDMS) provide individuals with a hardware and/or software solution to manage their data under control. From a data management and security/privacy perspective, the issues involved are complex and differ significantly from the traditional database setting. The emergence of trusted execution environments (such as Intel SGX) could be a game changer. This presentation will aim to (1) review different approaches for PDMS and the potential contribution of trusted runtime environments, and (2) discuss some issues related to collective processing of personal data (citizen portability), compliance with user consents, or protection against information leakage at runtime.
|
|
JANUARY 2022 |
|
|
“ Browser fingerprinting: past, present and possible future” by Pierre Laperdrix (CRIStAL) Date : 21 january 2022 Browser fingerprinting has grown a lot since its debut in 2010. By collecting specific information in the browser, one can learn a lot about a device and its configuration. It has been shown in previous studies that it can even be used to track users online, bypassing current tracking methods like cookies. In this presentation, we will look at how this technique works and present an overview of the research performed in the domain over the past decade. We will see how this technique is currently used online before looking at its possible future.
|
|
NOVEMBER 2021 |
|
|
“ Ransomware Detection Using Markov Chain Models Over File Headers” by David Lubicz (DGA-MI) Date : 26 november 2021 In this paper, a new approach for the detection of ransomware based on the runtime analysis of their behaviour is presented. The main idea is to get samples by using a mini-filter to intercept write requests, then decide if a sample corresponds to a benign or a malicious write request. To do so, in a learning phase, statistical models of structured file headers are built using Markov chains. Then in a detection phase, a maximum likelihood test is used to decide if a sample provided by a write request is normal or malicious. We introduce new statistical distances between two Markov chains, which are variants of the Kullback-Leibler divergence, which measure the efficiency of a maximum likelihood test to distinguish between two distributions given by Markov chains. This distance and extensive experiments are used to demonstrate the relevance of our method.
|
|
NOVEMBER 2021 |
|
|
“ Formal security proofs in a post-quantum world” by Charlie Jacomme (CISPA) Date : 19 november 2021 In the recent years, formals methods for security and their associated tools have been used successfully both to find novel and complex attacks on many protocols [A] and to help in their standardization process. They however face a new challenge with the increasing probability of quantum computers coming into the real-world: we need to be able to provide guarantees against quantum attackers. [A] see, e.g., https://www.bbc.co.uk/news/technology-58719891 for a recent example |
|
OCTOBER 2021 |
|
|
“ Towards Security-Oriented Program analysis” by Sébastien Bardin (CEA LIST) Date : 29 october 2021 While digital security concerns increase, we face both a urging demand for more and more code-level security analysis and a shortage of security experts. Hence the need for techniques and tools able to automate part of these code-level security analyses. As source-level program analysis and formal methods for safety-critical applications have made tremendous progress in the past decades, it is extremely tempting to adapt them from safety to security. Yet, security is not safety and, while still useful, a direct adaptation of safety-oriented program analysis to security scenarios remains limited in its scope. In this talk, we will argue for the need of security-oriented program analysis. Especially, we will first present some of the challenges faced by formal methods and program analysis in the context of code-level security scenarios. For example, security-oriented code analysis is better performed at the binary level, the attacker must be taken into account and practical security properties deviate from standard reachability / invariance properties. Second, we will discuss some early results and achievements carried out within the BINSEC group at CEA LIST. Especially, we will show how techniques such as symbolic execution and SMT constraint solving can be tailored to a number of practical code-level security scenarios.
|
|
OCTOBER 2021 |
|
|
“ Les cyber opérations, entre opportunités stratégiques et contraintes opérationnelles” by Stéphane Taillat (Académie Militaire de Saint Cyr-Coëtquidan) Date : 01 october 2021 Le recours aux opérations numériques et au cyberespace s’est généralisé dans la gestion des crises et des conflits internationaux. Pour autant, aucune des cyber opérations étatiques ou prêtées à des États n’ont débouché sur des conflits armés ou sur une escalade significative des tensions. A ce titre, cette conférence cherche à s’interroger sur l’utilité stratégique des opérations numériques et du recours au cyberespace comme théâtre, enjeux et modalités des confrontations géopolitiques en se focalisant sur les contraintes politiques, opérationnelles et organisationnelles qui les encadrent.
|
|
APRIL 2021 |
|
|
“ Squirrel: a new approach to computer-assisted proofs of protocols in the computational model” by David Baelde (ENS Cachan) Date : 16 april 2021 Formal methods have brought several approaches for proving that security protocols ensure the expected security and privacy properties. Most of the resulting tools analyze protocols in symbolic models, aka. Dolev-Yao-style models. Security in the symbolic model does not imply security in the cryptographer’s standard model, the computational model, where attackers are arbitrary (PPTIME) Turing machines. Computer-assisted verification techniques for the computational model have appeared only recently, and are generally less flexible or less automated than in the symbolic model. In some recent work, several colleagues and myself have proposed a new approach, elaborating on the CCSA logic of Gergei Bana and Hubert Comon. We have implemented it in a new proof assistant, Squirrel, and validated it on a variety of case studies. In this talk, I will present this approach, its benefits, and some of the remaining challenges. This is based on work with Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos and Solène Moreau, which has been accepted at S&P’21. |
|
APRIL 2021 |
|
|
“ Les cyberopérations: entre technique et droit international. Attribution, preuve et responsabilité.” by Anne-Thida Norodom (Professeur de droit public, Université de Paris) Date : 02 april 2021 L’objet de cette intervention est de montrer à quel point le juridique est dépendant du technique lorsqu’il s’agit de réguler les cyberopérations. L’approche choisie sera celle du droit international public, c’est-à-dire du droit applicable entre Etats. Alors qu’il existe un consensus au niveau international sur l’applicabilité du droit international dans le domaine numérique, les négociations en cours, notamment à l’ONU, achoppent sur un certain nombre de questions relatives à la manière dont le droit international doit s’appliquer. Il s’agira de montrer que le droit international dispose déjà de règles suffisantes pour encadrer les cyberopérations mais que sa mise en oeuvre doit être affinée, notamment au regard de certaines difficultés techniques.
|
|
MARCH 2021 |
|
|
“ Does Facebook use sensitive data for advertising?” by José González Cabañas (Universidad Carlos III de Madrid, Spain) Date : 12 march 2021 Large online platforms use personal data, for example, your interests, to allow advertisers to reach you based on the things you like. But did you know some of these interests they use are associated with sensitive information directly linked to your social profile? In this talk, I will talk about the definition of sensitive data in terms of the General Data Protection Regulation in Europe (GDPR). What does the GDPR say about its use? And how large social networks like Facebook use it to deliver you ads? We will see how many Facebook users are labeled with sensitive information around the world. Our findings show that a significant portion of Facebook users is tagged with some potentially sensitive ad preferences onto their profiles. This is important in terms of privacy. We will check if there are differences between countries. And finally, I will discuss the risks associated with this undesirable use of our data.
|
|
FEBRUARY 2021 |
|
|
“ A formal study of injection-based attacks and some tools it will enable “by Pierre-François Gimenez (Inria Rennes, CentraleSupélec) Date : 19 february 2021 Many systems work by receiving instructions and processing them: e.g., a browser receives and then displays an HTML page and executes Javascript scripts, a database receives a query and then applies it to its data, an embedded system controlled through a protocol receives and then processes a message. When such instructions depend on user input, one generally constructs them with concatenation or insertion. It can lead to injection-based attacks: when the user input modifies the query’s intended semantics and leads to a security breach. Protections do exist but are not sufficient as they never tackle the origin of the problem: the language itself. We propose a new formal approach based on formal languages to assess risk, enhance static analysis, and enable new tools. This approach is general and can be applied to query, programming, and domain-specific languages as well as network protocols. We are setting up an ANR project to go into this subject in more depth.
|
|
DECEMBER 2020 |
|
|
“ Canadian and Québec approaches to contact tracing ” Date : 11 december 2020 Contact tracing applications have been deployed in many countries as a complementary measure to fight Covid-19 by enabling to automatically notify individuals who have been in contact with infected persons. However, the choice of the design of a particular application is not innocent as it has a direct impact on its security as well as on the privacy of its user. In this talk, I will review the proposition of contact tracing applications that have emerged in the last months in Canada and Québec, comparing in particular their security and privacy properties. Finally, I will conclude by discussing some ethical issues raised by the deployment of these applications.
|
|
NOVEMBER 2020 |
|
|
“ The PINED-RQ Family: Differentially Private Indexes for Range Query Processing in Clouds” Date : 13 november 2020 Performing non- aggregate range queries on cloud stored data, while achieving both privacy and efficiency is a challenging problem. With the PINED-RQ family of techniques, we propose constructing a differentially private index to an outsourced encrypted dataset. Efficiency is enabled by using a cleartext index structure to perform range queries. Security relies on both differential privacy (of the index) and semantic security (of the encrypted dataset). Our initial solution, PINED-RQ, develops algorithms for building and updating the differentially private index. Our recent proposals extend PINED-RQ with a parallel architecture for coping with high-rate incoming data. Compared to state-of-the-art secure index based range query processing approaches, PINED-RQ executes queries in the order of at least one magnitude faster. Moreover its parallel extensions increase its throughput by at least one order of magnitude. The security of the PINED-RQ solutions is proved and their efficiency is assessed by extensive experimental validations. In this talk, I will introduce the PINED-RQ family of techniques by presenting the initial PINED-RQ proposal and overviewing then its parallel extensions.
|
|
SEPTEMBER 2020 |
|
|
“ An evaluation of Symbolic Execution Systems and the benefits of compilation with SymCC” Date : 25 september 2020 In this talk I will discuss our recent work, together with Sebastian Poeplau, on Symbolic execution. Symbolic execution has become a popular technique for software testing and vulnerability detection, in particular, because it allows to generate test cases for difficult to reach program paths. However, a major impediment to practical symbolic execution is speed, especially when compared to near-native speed solutions like fuzz testing. SymCC received a distinguished paper award at Usenix Security 2020.
|
|
JUNE 2020 |
|
|
“ Intriguing Properties of Adversarial ML Attacks in the Problem Space” Date : 19 june 2020 Recent research efforts on adversarial ML have investigated problem-space attacks, focusing on the generation of real evasive objects in domains where, unlike images, there is no clear inverse mapping to the feature space (e.g., software). However, the design, comparison, and real-world implications of problem-space attacks remain underexplored. In this talk, I will present two major contributions from our recent IEEE Symp. S&P 2020 paper [1]. First, I will present our novel reformulation of adversarial ML evasion attacks for the problem-space, with more constraints to consider than the feature-space and with more light shed on the relationship between feature-space and problem-space attacks. Second, building on our reformulation, I will present our novel problem-space attack for generating end-to-end evasive Android malware, showing that it is feasible to generative evasive malware at scale that also evade feature-space defenses. [1] Fabio Pierazzi*, Feargus Pendlebury*, Jacopo Cortellazzi, Lorenzo Cavallaro. “Intriguing Properties of Adversarial ML Attacks in the Problem Space”. IEEE Symp. Security & Privacy (Oakland), 2020. Trailer of the talk |
|
MAY 2020 |
|
|
“ QUIC: que faut-il attendre de ce nouveau protocole de communication sécurisé ? ” Date : 29 may 2020 Depuis plusieurs années, les grands acteurs du web travaillent à l’amélioration des communications entre leurs utilisateurs et leurs services. Ces améliorations peuvent porter sur la vitesse des connexions ou sur la sécurité des échanges. QUIC fait partie des efforts en cours. Il s’agit d’un protocole en cours de standardisation à l’IETF, qu’on peut résumer à un protocole sur UDP fournissant les services de TCP/SCTP, TLS 1.3 et HTTP/2.
|
|
FEBRUARY 2020 |
|
|
“Cybersecurity of industrial systems. Open problems and some ideas.” Date : 7 february 2020 Research in cybersecurity of SCADA systems is a relatively recent field developed mainly into the last decade. Despite the manufacturers progress in hardening the security of device SCADA systems are still prone to severe vulnerabilities and specialized countermeasures are still incipient. This talk aims to present the open problems seen from the boundary between computer science and control systems I.e. the architectural view of system (IT/OT/process). We’ll focus mainly on system modelling and vulnerability search and intrusion detection.
|
|
JANUARY 2020 |
|
|
“Contemporary Issues in Digital Forensics” Date : 31 january 2020 The discipline of digital forensics, or as it was then known ‘forensic computing’, began with a focus on retrieving admissible evidence from computer systems (typically personal computers). However, with the increased pervasiveness of connected digital technologies in the last 20 years, a wide variety of new and complex sources of digital evidence have emerged. This has presented a range of opportunities and challenges for forensic practitioners.
|
|
DECEMBER 2019 |
|
|
“ Intrusion Detection Systems over an Encrypted Traffic: Problem and Solutions” Date : 6 december 2019 Privacy and data confidentiality are today at the heart of many discussions. But such data protection should not be done at the detriment of other security aspects. In the context of network traffic, intrusion detection system becomes in particular totally blind when the traffic is encrypted, making clients again vulnerable to known threats and attacks. Reconciling security and privacy is then one of the major topics for which we should find relevant and scalable solutions that can be deployed as soon as possible. In this context, several recent papers propose to perform Deep Packet Inspection over an encrypted traffic, based on different cryptographic techniques. In this talk, we introduce the main difficulties to design such solutions and give some details about two of them.
|
|
NOVEMBER 2019 |
|
|
“ La protection des flux en télévision numérique” Date : 22 november 2019 En télévision numérique, des flux numériques comportant de la vidéo sont mis à la disposition des utilisateurs via différents média (cable, satellite, TNT, IP…) et différentes techniques (broadcast, multicast, unicast, support numérique…). Pour garantir les revenus des opérateurs de télévision à péage proposant des contenus à forte valeur ajoutée, il est essentiel que seuls les consommateurs ayant payé pour accéder à ces services puissent réellement y accéder. Rien que pour la France, certains estiment la perte de revenu liée au piratage à 1,3 milliard d’euros annuels.
“ Présentation des fondamentaux du management du risque et d’EBIOS Risk Manager ” Date : 29 november 2019 Résumé : La présentation théorique sera complétée avec un atelier pratique couvrant les sujets suivants :
|
|
OCTOBER 2019 |
|
|
“ Subject Access Request and Proof of Ownership” Date : 25 october 2019 The GDPR (General Data Protection Regulation) provides rights on our data: access, rectification, objection, etc. However, this regulation is not binding on how we can exercise these rights. Data controllers have therefore deployed various methods to authenticate subject requests. We have analyzed how this authentication process can fail and examined its consequences. Our study shows that a key concept is missing in the GDPR: Proof of ownership for our data.
|
|
JUNE 2019 |
|
|
“ A Formal Analysis of 5G Authentication ” Date : 3 june 2019 Mobile communication networks connect much of the world’s population. The security of users’ calls, text messages, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose. |
|
MARCH 2019 |
|
|
“ Voting : You Can’t Have Privacy without Individual Verifiability ” Date : 1 march 2019 Electronic voting typically aims at two main security goals: vote privacy and verifiability. These two goals are often seen as antagonistic and some national agencies even impose a hierarchy between them: first privacy, and then verifiability as an additional feature. Verifiability typically includes individual verifiability (a voter can check that her ballot is counted); universal verifiability (anyone can check that the result corresponds to the published ballots); and eligibility verifiability (only legitimate voters may vote). We show that actually, privacy implies individual verifiability. In other words, systems without individual verifiability cannot achieve privacy (under the same trust assumptions). To demonstrate the generality of our result, we show this implication in two different settings, namely cryptographic and symbolic models, for standard notions of privacy and individual verifiability. Our findings also highlight limitations in existing privacy definitions in cryptographic settings.
|
|
FEBRUARY 2019 |
|
|
“A Compositional and Complete approach to Verifying Privacy Properties using the Applied Pi-calculus ” Date : 8 february 2019 The pi-calculus was introduced for verifying cryptographic protocols by Abadi and Fournet in 2001. They proposed an equivalence technique, called bisimilarity, useful for verify privacy properties. It is widely acknowledged (cf. Paige and Tarjan 1987), that bisimilarity is more efficient to check than trace equivalence; however, surprisingly, tools based on the applied pi-calculus typically still implement trace equivalence. I suggest this may be attributed to two problems:
|
|
JANUARY 2019 |
|
|
“Privacy in The 5G-AKA Authentication Protocol ” Date : 18 january 2019 The 5G mobile communications standards are being finalized, and drafts are now available. This standard describes the 5G-AKA authentication and key exchange protocol. The previous version of AKA (3G and 4G) are well-known for their lack of privacy against an active adversary (e.g. a user can be massively tracked using IMSI-catcher). This new version of AKA tries to offer more privacy, notably through the use of asymmetric randomized encryption of the users permanent identities. Our first contribution is to show that, while this prevents the mass surveillance coming from IMSI-catchers, this is not sufficient for privacy. In particular, all the other known privacy attacks against 3G and 4G-AKA carry over to 5G-AKA. We also found a new type of vulnerabilities of stateful authentication protocols.
|
|
DECEMBER 2018 |
|
|
“Splitting the Linux Kernel for Fun and Profit ” Date : 7 december 2018 This talk looks at a pragmatic attempt at strengthening the security properties of Linux by introducing a degree of intra-kernel protection into the Linux kernel (supported by CPU Virtualization silicon features). Consider it, if you like, an attempt at retrofitting a ‘micro-kernel’ interface into traditionally monolithic Linux whilst maintaining a single linux code base (yes it’s still Linux), no need for a hypervisor and with reasonable performance characteristics. The motivation for the work was the frightening increase in reliance on the security properties of the Linux kernel driven by trends away from full-virtualization solutions such as VMWare and KVM and towards lighter weight containment approaches led by Docker, et al for application hosting, deployment and consolidation.
|
|
NOVEMBER 2018 |
|
|
“Machine Learning for Computer Security Detection Systems: Practical Feedback and Solutions ” Date : 30 november 2018 Machine learning based detection models can strengthen detection, but there remain some significant barriers to the widespread deployment of such techniques in operational detection systems. In this presentation, we identify the main challenges to overcome and we provide both methodological guidance and practical solutions to address them. The solutions we present are completely generic to be beneficial to any detection problem on any data type and are freely available in SecuML.
|
|
SEPTEMBER 2018 |
|
|
“Binary Edwards Curves for intrinsically secure ECC implementations for the IoT” Date: 7 september 2018 Even if recent advances in public key cryptography tend to focus on algorithms able to survive the post quantum era, at present, there is a urgent need to propose fast, low power and securely implemented cryptography to address the immediate security challenges of the IoT. In this talk, we present a new set of Binary Edwards Curves which have been defined to achieve the highest security levels (up to 284-bit security level) and whose parameters have been defined to fit IoT devices embedding 32-bit general purpose processors. We optimized the choice of the point generator with the w-coordinate to save a multiplication in the addition and doubling formulae. We manage to compute one step of the Montgomery Ladder in 4 multiplications and 4 squares. On top of the performance benefits, cryptography over such curves have some intrinsic security properties against physical attacks.
|
|
JULY 2018
|
|
|
“How to decrypt without keys with GlobalPlatform SCP02 protocol” Date: 6 july 2018 The GlobalPlatform SCP02 protocol is a security protocol implemented in smart cards, and used by transport companies, in the banking world and by mobile network operators (UICC/SIM cards). We describe how to perform a padding oracle attack against SCP02. The attack allows an adversary to efficiently retrieve plaintext bytes from an encrypted data field. We provide results of our experiments done with 10 smart cards from six different card manufacturers, and show that, in our experimental setting, the attack is fully practical. Given that billions SIM cards are produced every year, the number of affected cards, although difficult to estimate, is potentially high. To the best of our knowledge, this is the first practical attack against SCP02.
|
|
JUNE 2018 |
|
|
“A theory of assertions for Dolev-Yao models” Date: 8 june 2018 We undertake an abstract study of certification in security protocols, concentrating on the logical properties and derivability of certificates. Specifically, we extend the Dolev-Yao model with a new class of objects called ‘assertions’, along with an associated algebra for deriving new assertions from old ones. We obtain complexity results for the derivability problem and active intruder problem for this model, and provide a case study via the FOO e-voting protocol.
|
|
MARCH 2018
|
|
|
“Anonymous Server-Aided Verification” Date: 30 march 2018 Server-Aided Verification (SAV) is a method that can be employed to speed up the process of verifying signatures by letting the verifier outsource part of its computation load to a third party. Achieving fast and reliable verification under the presence of an untrusted server is an attractive goal in cloud computing and internet of things scenarios.
“Automated verification of privacy-type properties for security protocols” Date: 16 march 2018 The applied pi-calculus is a powerful framework to model protocols and to define security properties. In this symbolic model, it is possible to verify automatically complex security properties such as strong secrecy, anonymity and unlinkability properties which are based on equivalence of processes.
“The Internet of Backdoors“ Date: 7 march 2018 Complex embedded devices are becoming ever prevalent in our everyday lives, yet only a tiny amount of people consider the potential security and privacy implications of attaching such devices to our home, business and government networks. As demonstrated through recent publications from academia and blog posts from numerous industry figures, these devices are plagued by poor design choices concerning end-user security. What’s even more worrying, are reports of manufacturers inserting backdoor-like functionality into the production firmware of those devices.
|
|
FEBRUARY 2018 |
|
|
“When Good Components Go Bad: Formally Secure CompilationDespite Dynamic Compromise” by Catalin Hritcu (Inria Paris) Date: 5 february 2018 We propose a new formal criterion for secure compilation, providing strong end-to-end security guarantees for components written in unsafe, low-level languages with C-style undefined behavior. Our criterion is the first to model dynamic compromise in a system of mutually distrustful components running with least privilege. Each component is protected from all the others until it becomes compromised by exhibiting undefined behavior, opening the door for an attacker to take control over the component and to use the component’s privileges to attack the remaining uncompromised components. More precisely, we ensure that dynamically compromised components cannot break the safety properties of the system at the target level any more than equally privileged components without undefined behavior already could in the source language. To illustrate this model, we build a secure compilation chain for an unsafe language with buffers, procedures, and components. We compile this to a simple RISC abstract machine with built-in compartmentalization and provide machine-checked proofs in Coq showing that this compiler satisfies our secure compilation criterion. Finally, we show that the protection guarantees offered by the compartmentalized abstract machine can be achieved at the machine-code level using either software fault isolation or tag-based reference monitoring.
“Breaking and fixing HB+DB: A Short Tale of Provable vs Experimental Security and Lightweight Designs” Date: 2 february 2018 HB+ is a well-know authentication scheme purposely designed to be lightweight. However, HB+ is vulnerable to a key-recovery, man-in-the-middle (MiM) attack dubbed GRS. To this end, at WiSec2015, the HB+DB protocol added a distance-bounding dimension to HB+, which was experimentally shown to counteract the GRS attack.
|
