Seminar

The SILM seminar features up to two presentations, one day per month from September 2019 to March 2020 on the security at the software/hardware interface. Following the format of its siblings, presentations will take place at INRIA, Rennes, France.

Practical information

The seminar is usually held one Friday per month between 10h and 12h at INRIA, on the Beaulieu campus in Rennes (France).

Seminars are open to the public. But to be allowed to enter the building, please register first by sending a mail with your names and affiliation to Nadia Derouault (nadia.derouault@inria.fr) and present an ID at the front desk.

Register to the mailing list at https://sympa.inria.fr/sympa/subscribe/silm-seminar to get info on the next talks.

Videoconference (live stream)

To join :

– connect to https://visio.inria.fr (<login>@inria.fr) and “Meet” : seminaire.silm@visio.inria.fr (PIN : 4875#)

– for external collaborators : https://visio.inria.fr/invited.sf?secret=O3A9s9dvp2Mvl4xKwR8yWw&id=305424998

– from a visioconference endpoint : call visio.inria.fr then enter the call ID : 305424998# (PIN : 4875#)

– phone: +33 4 92 38 77 88 (77788), then enter 305424998# (PIN : 4875#)

Contacts

Ronan Lashermes, INRIA, (+33|0)2 99 84 72 84, ronan.lashermes@inria.fr

Guillaume Hiet, CentraleSupélec, guillaume.hiet@centralesupelec.fr

Upcoming presentations

Temporarily cancelled due to the coronavirus epidemic.

Past presentations

November 8th, 2019

Lucas Davi (University of Duisburg-Essen) : Memory Corruption Attacks in the Context of Trusted Execution Environments (slides, video)

ARM TrustZone and Intel Software Guard Extensions (SGX) offer hardware-assisted trusted execution environments (TEEs) to enable strong isolation of security-critical code and data. They also allow systems to perform remote attestation, where a device challenges another device to report its current state. In this talk, we elaborate on remote attestation schemes that do not only attest static properties, but also cover run-time control-flow behavior of applications based on ARM TrustZone. While TEEs enable secure attestation of control-flow behavior, memory corruption attacks (e.g., return-oriented programming) inside TEEs can undermine remote attestation schemes. This talk will elaborate on memory corruption attacks for the use-case of SGX and how we can develop analysis approaches to detect vulnerable TEE code.

January 17th, 2020

Billy Brumley (Tampere University of Technology) : Port Contention for Fun and Profit

Simultaneous Multithreading (SMT) architectures are attractive targets for attackers with side-channel expertise. SMT inherently offers a broader attack surface, exposing more microarchitecture components per physical core for fine-grain attacks. PortSmash (CVE-2018-5407) is a technique that abuses the execution units to exploit port contention, and creates a high-resolution timing side-channel capable of leaking confidential information. PortSmash affects both Intel and AMD architectures featuring SMT technology and due to its nature, it is capable of targetting shared libraries, static builds and even SGX enclaves.

Yann Loisel (SiFive, RISC-V) :  Embedded security around RISC-V cores (slides)

The security needs increase a lot in our connected world. Beyond the perception the software can satisfy the security requirements, it’s obvious that the best solutions could only be a combination of hardware and software mechanisms.
The huge activity around the RISC-V cores these last years is not only a buzz or for an unjustified reason. On the contrary, this ecosystem is more than only a new ISA: it is the ideal playground for applying the best practices in embedded security.
We will see in this talk what the RISC-V foundation and its academic and industrial members propose for making RISC-V a synonym of security at the core, in the software and at the system level.

February 18th, 2020

Guillaume Hiet (CentraleSupélec/CIDRE): SILM thematic semester presentation (slides)

Clémentine Maurice (CRNS/EMSEC): Software side-channel attacks and fault attacks on ARM devices (slides)

In the last years, mobile devices and smartphones have become the most important personal computing platform.
Besides phone calls and managing the personal address book, they are also used to approve bank transfers and digitally sign official documents, thus storing very sensitive secrets.
However, the large majority of research work in software side-channel attacks and fault attacks is targeting x86 CPUs (such as laptops and servers).
In this presentation, we will present side-channel attacks on microarchitecture and DRAM fault attacks on ARM devices, and we will highlight the main particulars of the platform and necessary adaptations of the attacks and defences.

Ronan Lashermes (INRIA/LHS&SED): Radically secure computing (slides)

Past experiences have shown that ensuring security in any computing system is a difficult task.
When software security is starting to mature, micro-architectural attacks sneak in! And physical attacks are not far.
Instead of blaming people for bad implementations, we will argue for a new radical solution to ensure secure computing: the instruction set architecture should ensure strong formal security guarantees by restricting the computational model.

David Pichardie (ENS-Rennes/CELTIQUE): Formal Verification of a Constant-Time Preserving C Compiler

Timing side-channels are arguably one of the main sources of vulnerabilities in cryptographic implementations.
One effective mitigation against timing side-channels is to write programs that do not perform secret-dependent branches and memory accesses.
This mitigation, known as “cryptographic constant-time”, is adopted by several popular cryptographic libraries.

This work focuses on compilation of cryptographic constant-time programs, and more specifically on the following question: is the code generated by a realistic compiler for a constant-time source program itself provably constant-time?
Surprisingly, we answer the question positively for a mildly modified version of the CompCert compiler, a formally verified and moderately optimizing compiler for C.
Concretely, we modify the CompCert compiler to eliminate sources of potential leakage.
Then, we instrument the operational semantics of CompCert intermediate languages so as to be able to capture cryptographic constant-time.
Finally, we prove that the modified CompCert compiler preserves constant-time.
Our mechanization maximizes reuse of the CompCert correctness proof, through the use of new proof techniques for proving preservation of constant-time.
These techniques achieve complementary trade-offs between generality and tractability of proof effort, and are of independent interest.

Lee Smith (Arm fellow), Frédéric Piry (Arm fellow), Arnaud de Grandmaison ( senior principal engineer ) : Fruitful security (and more) from CHERI to Morello (slides)

Security is the greatest challenge computing needs to address to meet its full potential. Memory safety issues have been for far too long and way too common in the field, with the first partially documented one dating from 1972 ! Almost 50 years later, it’s obvious the situation has only gotten worse, with for example Microsoft (and this is not specific to them) recognizing that 70% of all security bugs in their products are memory safety issues.

Capability-based (software managed but hardware enforced tokens of authority used to access memory) systems have been researched and used since the very beginning of computing, but they have been set aside by segmentation/pagination-based systems for price, performance and ease of implementation reasons. Arm has been working with the University of Cambridge for several years to come up with Morello, an Arm implementation of the CHERI architecture, to address security with strong fundamental principles. This is a big and critical project, as recognized by the large funding from the UK government (£70 million), and the £117 million additional contribution from the “Digital Security by Design” partners.

This presentation will first introduce capability-based systems in general, and CHERI specifically then focus on Morello. Transitioning to capabilities is challenging and disruptive enough, at all levels from the hardware up to the software, system, debug, … that this is the right time to look at those (not so) new systems again, hopefully benefiting from 50+ years of experience, if not errors, in security. This is effectively a call to arms (pun intended !) for a joint research – industry collaboration effort.

Guillaume Hiet (CentraleSupélec/CIDRE): HardBlare, a hardware/software co-design approach for Information Flow Control (slides)

HardBlare proposes a hardware/software solution to implement an anomaly-based approach to detect software attacks against confidentiality and integrity through Dynamic Information Flow Tracking (DIFT).
HardBlare combines fine-grained DIFT with OS-level tagging which allows end-user to specify security policies.
Main outcome at the hardware level of HardBlare is the design of a dedicated multi-core DIFT co-processor on FPGA that does not require any modification of the main CPU.  This contribution tackles one of the main challenges of the project.
To achieve this goal, information required for DIFT is obtained both at compile-time and run-time through pre-computation during the compilation step, hardware trace mechanisms and instrumentation at run-time.
Main outcome at the software level of HardBlare is the Linux kernel modification to handle file tags and to support communication between the instrumented code and the co-processor, a patch of the official Linux PTM driver, Linux loader (ld.so) modification to load annotations to the co-processor and a LLVM backend pass to compute the annotations and instrument applications.
All validation has been performed on the Digilent ZedBoard using Xilinx ZYNQ SoC which combines two hardcores (ARM Cortex-A9) with a Xilinx FPGA.
Through its achievements HardBlare demonstrates that a hardware/software co-design approach for Information Flow Control corresponds to an efficient and promising solution.

Annelie Heuser (CRNS/TAMIS): Physical side-channel analysis on STM32F{0,1,2,3,4}

Physical side-channel attacks use unintentionally omitted information of physical devices to predict internally processed data.
In this talk, we will present attacks using power consumption and electromagnetic emanations captured on STM32F0 to F4.
Interestingly, all devices present similar and yet different behaviours in terms of side-channel vulnerabilities.

Comments are closed.