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.

Side-channel attacks are a powerful class of attacks targeting cryptographic devices. Masking is a popular protection technique to thwart such attacks as it can be theoretically proven secure. However, correctly implementing masking schemes is a non-trivial task and error-prone. If several techniques have been proposed to formally verify masked implementations, they all come with limitations regarding expressiveness, scalability or accuracy. In this work, we propose a symbolic approach, based on a variant of the classical substitution method, for formally verifying arithmetic and boolean masked programs. This approach is more accurate and scalable than existing approaches thanks to a careful design and implementation of key heuristics, algorithms and data structures involved in the verification process. We present all the details of this approach and the open-source tool calledLeakageVerifwhich implements it as a python library, and which offers constructions for symbolic expressions and functions for their verification. We compareLeakageVerifto three existing state-of-the-art tools on a set of 46 masked programs, and we show that it has very good scalability and accuracy results while providing all the necessary constructs for describing algorithmic to assembly masking schemes. Finally, we also provide the set of 46 benchmarks, namedMaskedVerifBenchsand written for comparing the different verification tools, in the hope that they will be useful to the community for future comparisons.

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 powerful attacks for retrieving secret data by exploiting physical measurements, such as power consumption or electromagnetic emissions. Masking is a popular countermeasure as it can be proven secure against an attacker model. In practice, software-masked implementations suffer from a security reduction due to a mismatch between the considered leakage sources in the security proof and the real ones, which depend on the microarchitecture. We propose ARMISTICE, a framework for formally verifying the absence of leakage in first-order masked implementations taking into account modeled microarchitectural sources of leakage. As a proof of concept, we present the modeling of an Arm Cortex-M3 core from its RTL description and leakage test vectors, as well as the modeling of the memory of an STM32F1 board, exclusively using leakage test vectors. We show that, with these models, ARMISTICE pinpoints vulnerable instructions in real-world masked implementations and helps the design of masked software implementations which are practically secure.

Software protections against side-channel and physical attacks are essential to the development of secure applications. Such protections are meaningful at machine code or micro-architectural level, but they typically do not carry observable semantics at source level. This renders them susceptible to miscompilation, and security engineers embed input/output side-effects to prevent optimizing compilers from altering them. Yet these side-effects are error-prone and compiler-dependent. The current practice involves analyzing the generated machine code to make sure security or privacy properties are still enforced. These side-effects may also be too expensive in fine-grained protections such as control-flow integrity. We introduce observations of the program state that are intrinsic to the correct execution of security protections, along with means to specify and preserve observations across the compilation flow. Such observations complement the input/output semantics-preservation contract of compilers. We introduce an opacification mechanism to preserve and enforce a partial ordering of observations. This approach is compatible with a production compiler and does not incur any modification to its optimization passes. We validate the effectiveness and performance of our approach on a range of benchmarks, expressing the secure compilation of these applications in terms of observations to be made at specific program points.

Annotations and assertions capturing static program properties are ubiquitous, from robust software engineering to safety-critical or secure code. These may be functional or non-functional properties of control and data flow, memory usage, I/O and real time. We propose an approach to encode, translate, and preserve the semantics of both functional and non-functional properties along the optimizing compilation of C to machine code. The approach involves (1) capturing and translating source-level properties through lowering passes and intermediate representations, such that data and control flow optimizations will preserve their consistency with the transformed program, and (2) carrying properties and their translation as debug information down to machine code. Our experiments using LLVM validate the soundness, expressiveness and efficiency of the approach, considering a reference suite of functional properties as well as established security properties and applications hardened against side-channel attacks.

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.

In the area of physical attacks, system-on-chip (SoC) designs have not received the same level of attention as simpler micro-controllers. We try to model the behavior of secure software running on a superscalar out-of-order microprocessor typical of more complex SoC, in the presence of electromagnetic (EM) pulses. We first show that it is possible, in a black box approach, to corrupt the loop iteration count of both original and hardened versions of two sensitive loops. We propose a characterization methodology based on very simple codes, to understand and classify the fault effects at the level of the instruction set architecture (ISA). The resulting classification includes the well established instruction skip and register corruption models, as well as new effects specific to more complex processors, such as operand substitution, multiple correlated register corruptions, advanced control-flow hijacking, and combinations of all reported effects. This diversity and complexity of effects can lead to powerful attacks. The proposed methodology and fault classification at ISA level is a first step towards a more complete characterization. It is also a tool supporting the designers of software and hardware countermeasures.

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.

In this paper we present a hardware based solution to verify simultaneously Code and Control-Flow Integrity (CCFI), aiming at protecting microcontrollers against both cyber-and physical attacks. This solution is non-intrusive as it does not require any modification of the CPU core. It relies on two additional hardware blocks external to the CPU: The first one – called CCFI-cache – acts as a dedicated cache for the storage of information to check the code and control-flow integrity, and the second one – CCFI-checker – performs control-flow and code integrity verification. Based on a RISC-V platform implementation, we show that the proposed scheme is able to perform online CCFI validation at the price of a small hardware area overhead and doubling the size of the. text section. In most cases, the impact on the run-time performance is on average 32 percent, offering for the first time a generic and practical hardware-enabled cyber-security solution.

Secure elements widely used in smartphones, digital consumer electronics, and payment systems are subject to fault attacks. To thwart such attacks, software protections are manually inserted requiring experts and time. The explosion of the Internet of Things (IoT) in home, business, and public spaces motivates the hardening of a wider class of applications and the need to offer security solutions to non-experts. This article addresses the automated protection of loops at compilation time, covering the widest range of control- and data-flow patterns, in both shape and complexity. The security property we consider is that a sensitive loop must always perform the expected number of iterations; otherwise, an attack must be reported. We propose a generic compile-time loop hardening scheme based on the duplication of termination conditions and of the computations involved in the evaluation of such conditions. We also investigate how to preserve the security property along the compilation flow while enabling aggressive optimizations. We implemented this algorithm in LLVM 4.0 at the Intermediate Representation (IR) level in the backend. On average, the compiler automatically hardens 95% of the sensitive loops of typical security benchmarks, and 98% of these loops are shown to be robust to simulated faults. Performance and code size overhead remain quite affordable, at 12.5% and 14%, respectively.

Dynamic task-parallel programming models are popular on shared-memory systems, promising enhanced scalability, load balancing and locality. Yet these promises are undermined by non-uniform memory access (NUMA). We show that using NUMA-aware task and data placement, it is possible to preserve the uniform abstraction of both computing and memory resources for task-parallel programming models while achieving high data locality. Our data placement scheme guarantees that all accesses to task output data target the local memory of the accessing core. The complementary task placement heuristic improves the locality of task input data on a best effort basis. Our algorithms take advantage of data-flow style task parallelism, where the privatization of task data enhances scalability by eliminating false dependences and enabling fine-grained dynamic control over data placement. The algorithms are fully automatic, application-independent, performance-portable across NUMA machines, and adapt to dynamic changes. Placement decisions use information about inter-task data dependences readily available in the run-time system and placement information from the operating system. We achieve 94% of local memory accesses on a 192-core system with 24 NUMA nodes, up to 5x higher performance than NUMA-aware hierarchical work-stealing, and even 5.6x compared to static interleaved allocation. Finally, we show that state-of-the-art dynamic page migration by the operating system cannot catch up with frequent affinity changes between cores and data and thus fails to accelerate task-parallel applications.

This paper studies the interactive visualization and post-mortem analysis of execution traces generated by task-parallel programs. We focus on the detection of performance anomalies inaccessible to state-of-the-art performance analysis techniques, including anomalies deriving from the interaction of multiple levels of software abstractions, anomalies associated with the hardware, and anomalies resulting from interferences between optimizations in the application and run-time system. Building on our practical experience with the performance debugging of representative task-parallel applications and run-time systems for dynamic dependent task graphs, we designed a new tool called Aftermath. This tool enables the visualization of intricate anomalies involving multiple layers and components in the system. It also supports filtering, aggregation and joint visualization of key metrics and performance indicators, such as task duration, run-time state, hardware performance counters and data transfers. The tool also relates this information to the machine's topology. While not specifically designed for non-uniform memory access (NUMA) architectures, Aftermath takes advantage of the explicit memory regions and dependence information in dependent task models to precisely capture long-distance and inter-core effects. Aftermath supports traces of up to several gigabytes, with fast and intuitive navigation and the on-line configuration of new derived metrics. As it has proven invaluable to optimize both run-time environments and applications, we illustrate Aftermath on genuine cases encountered in the OpenStream project.

Dynamic task parallelism is a popular programming model on shared-memory systems. Compared to data parallel loop-based concurrency, it promises enhanced scalability, load balancing and locality. These promises, however, are undermined by non-uniform memory access (NUMA) systems. We show that it is possible to preserve the uniform hardware abstraction of contemporary task-parallel programming models, for both computing and memory resources, while achieving near-optimal data locality. Our run-time algorithms for NUMA-aware task and data placement are fully automatic, application-independent, performance-portable across NUMA machines, and adapt to dynamic changes. Placement decisions use information about inter-task data dependences and reuse. This information is readily available in the run-time systems of modern task-parallel programming frameworks, and from the operating system regarding the placement of previously allocated memory. Our algorithms take advantage of data-flow style task parallelism, where the privatization of task data enhances scalability through the elimination of false dependences and enables fine-grained dynamic control over the placement of application data. We demonstrate that the benefits of dynamically managing data placement outweigh the privatization cost, even when comparing with target-specific optimizations through static, NUMA-aware data interleaving. Our implementation and the experimental evaluation on a set of high-performance benchmarks executing on a 192-core system with 24 NUMA nodes show that the fraction of local memory accesses can be increased to more than 99%, resulting in a speedup of up to 5× compared to a NUMA-aware hierarchical work-stealing baseline.

We present a joint scheduling and memory allocation algorithm for efficient execution of task-parallel programs on non-uniform memory architecture (NUMA) systems. Task and data placement decisions are based on a static description of the memory hierarchy and on runtime information about intertask communication. Existing locality-aware scheduling strategies for fine-grained tasks have strong limitations: they are specific to some class of machines or applications, they do not handle task dependences, they require manual program annotations, or they rely on fragile profiling schemes. By contrast, our solution makes no assumption on the structure of programs or on the layout of data in memory. Experimental results, based on the OpenStream language, show that locality of accesses to main memory of scientific applications can be increased significantly on a 64-core machine, resulting in a speedup of up to 1.63× compared to a state-of-the-art work-stealing scheduler.

Injection of transient faults as a way to attack cryptographic implementations has been largely studied in the last decade. Several attacks that use electromagnetic fault injection against hardware or software architectures have already been presented. On micro controllers, electromagnetic fault injection has mostly been seen as a way to skip assembly instructions or subroutine calls. However, to the best of our knowledge, no precise study about the impact of an electromagnetic glitch fault injection on a micro controller has been proposed yet. The aim of this paper is twofold: providing a more in-depth study of the effects of electromagnetic glitch fault injection on a state-of-the-art micro controller and building an associated register-transfer level fault model.

Smart card software has to implement software countermeasures to face attacks. Some of these attacks are physical disruptions of chip components that cause a misbehavior in the code execution. A successful functional attack may reveal a secret or grant an undesired authorization. In this paper, we propose to model fault attacks at source level and then simulate these attacks to find out which ones are harmful. After discussing the effects of physical attacks at assembly level and going back to their consequences at source code level, the paper focuses on control flow attacks. Such attacks are good candidates for the proposed model that can be used to exhaustively test the robustness of the attacked program. On the bzip2 software, the paper's results show that up to 21% of the assembly simulated control flow attacks are covered by the C model with 30 times less test cases.

Abstract Embedded systems are increasingly expected to provide good performance at low cost. As the characteristics of compiled code can have an impact on the overall cost of an embedded system, a compilation strategy must be cost aware as well as achieve high performance. As one major factor for system cost is memory size, code size becomes an important issue in code generation. Thus, cost‐effective optimization strategies that are able to perform a good trade‐off between code size and performance improvement are needed. In this paper, we propose a novel method based on Integer Linear Programming for computing efficient unroll factors for collections of loop nests with control over code size and side‐effects of the transformation. We define a notion of trade‐off between code size and performance. Experiments on the Philips Trimedia show that our method achieves excellent trade‐offs. Copyright © 2006 John Wiley & Sons, Ltd.

The design of an embedded system is often heavily constrained by its performance objective and budget envelope. Software code compression may reduce the instruction memory space and then the overall cost of the system. However, it may also induce performance degradation. Previous studies proposed selective code compression using profile information in order to reduce the performance penalty. In this paper, we go one step further. We propose a software-only compression system, called SCS, that automatically finds trade-offs between code size and performance. Through an iterative approach, SCS automatically determines which functions to be compressed given a performance constraint and/or a code size constraint in order to guarantee a minimal performance and a maximal code size for an application. Experimentations illustrate that even with a non-optimal software decompression approach, SCS achieves a high compression rate with a minimal performance degradation.