Characterization of bugs and attack vectors is in many practical scenarios as important as their finding. Recently, Girol et al. have introduced the concept of robust reachability , which ensures a perfect reproducibility of the reported violations by distinguishing inputs that are under the control of the attacker ( controlled inputs ) from those that are not ( uncontrolled inputs ), and proposed first automated analysis for it. While it is a step toward distinguishing severe bugs from benign ones, it fails for example to describe violations that are mostly reproducible, i.e., when triggering conditions are likely to happen, meaning that they happen for all uncontrolled inputs but a few corner cases. To address this issue, we propose to leverage theory-agnostic abduction techniques to generate constraints on the uncontrolled program inputs that ensure that a target property is robustly satisfied . Our proposal comes with an extension of robust reachability that is generic on the type of trace property and on the technology used to verify the properties. We show that our approach is complete w.r.t. its inference language , and we additionally discuss strategies for the efficient exploration of the inference space. We demonstrate the feasibility of the method and its practical ability to refine the notion of robust reachability with an implementation that uses robust reachability oracles to generate constraints on standard benchmarks from software verification and security analysis. We illustrate the use of our implementation to a vulnerability characterization problem in the context of fault injection attacks. Our method overcomes a major limitation of the initial proposal of robust reachability, without complicating its definition. From a practical view, this is a step toward new verification tools that are able to characterize program violations through high-level feedback.

Fault injection attacks represent an effective threat to embedded systems. Recently, Laurent et al. have reported that fault injection attacks can leverage faults inside the microarchitecture. However, state-of-the-art countermeasures, hardware-only or with hardware support, do not consider the integrity of microarchitecture control signals that are the target of these faults. We present MAFIA, a microarchitecture protection against fault injection attacks. MAFIA ensures integrity of pipeline control signals through a signature-based mechanism, and ensures fine-grained control-flow integrity with a complete indirect branch support and code authenticity. We analyze the security properties of two different implementations with different security/overhead tradeoffs: one with a CBC-MAC/Prince signature function, and another one with a CRC32. We present our implementation of MAFIA in a RISC-V processor, supported by a dedicated compiler toolchain based on LLVM/Clang. We report a hardware area overhead of 23.8% and 6.5% for the CBC-MAC/Prince and CRC32, respectively. The average code size and execution time overheads are 29.4% and 18.4%, respectively, for the CRC32 implementation and are 50% and 39% for the CBC-MAC/Prince.

Fault injection attacks have become a serious threat against embedded systems. Recently, Laurent et al. have reported that some faults inside the microarchitecture escape all typical software fault models and so software counter-measures. Moreover, state-of-the-art counter-measures, hardware-only or with hardware support, do not consider the integrity of microarchitectural control signals that are the target of these faults. We present SCI-FI, a counter-measure for Control Signal, Code, and Control-Flow Integrity against Fault Injection attacks. SCI-FI combines the protection of pipeline control signals with a fine-grained code and control-flow integrity mechanism, and can additionally provide code authentication. We evaluate SCI-FI by extending a RISC-V core. The average hardware area overheads range from 6.5% to 23.8%, and the average code size and execution time increase by 25.4% and 17.5% respectively.

This paper introduces a formal workflow for modeling software/hardware systems in order to explore the effects of fault injections and evaluate the robustness to fault injection attacks. We illustrate this workflow on four versions of a PIN authentication code, embedding different software countermeasures. The code is symbolically evaluated on two implementations of the RISC-V CV32E40P core: the original implementation from the OpenHW group and an implementation that integrates protection of the pipeline control signals. On the original, unprotected core, our formal workflow exposes various vulnerabilities, including previously unknown ones, whereas, on the protected core, it confirms the effectiveness of the proposed countermeasures.

Side-channel attacks are amongst the major threats for embedded systems and IoT devices. Masking is one of the most used countermeasure against such attacks, but its application remains a difficult process. We propose a target-independent approach for applying a first-order Boolean masking countermeasure during compilation, on the static single assignment (SSA) form. Contrary to the state-of-the art automated approaches that require to simplify the control flow of the input program, our approach supports regular control-flow program structures. Moreover, our compiler is the first to automatically mask table lookups using a polynomial interpolation approach. We also present new optimizations to speedup the evaluation of polynomials: we reduce the number of terms of the polynomial, and we accelerate finite-field multiplication. We show that our approach is faster than the standard masked table approach with mask refresh after each access, with speedups up to ×2.4 in our experiments. Finally, using a formal verification approach, we show that the compiled machine code is secure, i.e., that all intermediate computations are statistically independent of the secrets.

We present an approach and a tool to answer the need for effective, generic, and easily applicable protections against side-channel attacks. The protection mechanism is based on code polymorphism, so that the observable behaviour of the protected component is variable and unpredictable to the attacker. Our approach combines lightweight specialized runtime code generation with the optimization capabilities of static compilation. It is extensively configurable. Experimental results show that programs secured by our approach present strong security levels and meet the performance requirements of constrained systems.

International audience

International audience

In this paper we explore, by means of three pilot observational studies using virtual objects, how direct perception through action of multi-sensory audio-visual and haptic object properties support the creation of new categories of believable and plausible objects than can be perceived as being different from those that were presented The three experiments are based on variations of "Pebble boxes" and consist in the exploration and the manipulation of multiple moving multi-sensory objects (the Pebbles). Results from observations and informal interviews with participants illustrate how an inferred scene is apparently constructed from experience, as assumed in the cognitive Enactive concept, by means of three complementary strategies: the Emergent Exploratory Procedures, Dynamic Manipulation Adaptation, and Adaptive Experimental Learning. Findings also illustrate the complementarities between the so-called ergotic and semiotic situations with respect to the strategies that were apparently successful in inferring a believable and plausible scene.Several fundamental questions arise which are relevant to the Enactive assumption with respect to the coupling between perceiving and acting, some of which are discussed here.