Séminaire SILM / ARM

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

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/SED&LHS): Radically secure computing

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, Frédéric Piry, Arnaud de Grandmaison (Arm): Fruitful security (and more) from CHERI to Morello

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

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.