Given the popularity of low-end microcontrollers, manufacturers and researchers have proposed memory isolation mechanisms for these devices. However, current proposals face two main shortcomings. First, due to a lack of extensible reference implementations of commercial specifications, academic systems commonly use custom memory isolation mechanisms, reducing compatibility and the chance of real-world adoption. Second, recent research has demonstrated crucial and overlapping vulnerabilities, including in commercial systems. Unfortunately, efforts to mitigate and validate these issues are hindered by the disconnect in codebases.This paper proposes openIPE, an open research platform for extensible, industry-compliant hardware-software co-designs. Our platform introduces minimal hardware extensions for memory isolation based on Texas Instruments’ specification for Intellectual Property Encapsulation (IPE), alongside a versatile firmware layer enabling rapid prototyping of advanced security extensions. We establish a robust security testing infrastructure and demonstrate the capabilities of our framework through a comprehensive study on secure interrupt handling, an important research area for microcontrollers. Our evaluation shows that openIPE allows for the independent reproduction and comparison of existing proposals and enables a novel solution that achieves strong architectural and microarchitectural security with minimal hardware modifications and low overhead.

Threat modeling (TM) is essential to manage, prevent, and fix security and privacy issues in our society. TM requires a data model to represent threats and tools to exploit such data. Current TM data models and tools have significant limitations preventing their usage in real-world scenarios. For example, it is challenging to TM embedded devices with current data models and tools as they cannot model their hardware, firmware, and low-level software. Moreover, it is impossible to TM a device lifecycle or security-privacy tradeoffs as these data models and tools were developed for other use cases (e.g., software security or user privacy). We fill this relevant gap by presenting the AttackDefense Framework (ADF), which provides a novel data model and related tools to augment TM. ADF’s building block is the AD object that can be used to represent heterogeneous and complex threats. Moreover, ADF provides automations to process a collection of AD objects, including ways to create sets, maps, chains, trees, and wordclouds of AD objects. We present ADF , a toolkit implementing ADF composed of four modules (Catalog, Parse, Check, and Analyze). We confirm that the data model and tools provided by ADF are useful by running an extensive set of experiments while threat modeling a crypto wallet and its lifecycle. Our experiments involved seven expert groups from academia and industry, each using the ADF on an orthogonal threat class. The evaluation generated 175 high-quality ADs covering ISA/IEC 62433-4-1 SecDev Lifecycle, side-channels, fault injection, microarchitectural attacks, speculative execution, pre-silicon testing, invasive physical chip modifications, Bluetooth protocol and implementation threats, and FIDO2 authentication.

Control-flow leakage (CFL) attacks enable an attacker to expose control-flow decisions of a victim program via side-channel observations. Linearization (i.e. elimination) of secret-dependent control flow is the main countermeasure against these attacks, yet it comes at a non-negligible cost. Conversely, balancing secret-dependent branches often incurs a smaller overhead, but is notoriously insecure on high-end processors. Hence, linearization has been widely believed to be the only effective countermeasure against CFL attacks. In this paper, we challenge this belief and investigate an unexplored alternative: how to securely balance secret-dependent branches on higher-end processors?

The control flow of a program can often be observed through side-channel attacks. Hence, when control flow depends on secrets, attackers can learn information about these secrets. Widely used software-based countermeasures ensure that attacker-observable aspects of the control flow do not depend on secrets, relying on techniques like dummy execution (for balancing code) or conditional execution (for linearizing code). In the current state-of-practice, the primitives to implement these techniques have to be found in an existing instruction set architecture (ISA) that was not designed a priori to provide them, leading to performance, security, and portability issues. To counter these issues, this paper proposes lightweight hardware extensions for supporting these techniques in a principled way. We propose (1) a novel hardware mechanism (mimic execution), that executes an instruction stream only for its attacker-observable effects, and suppresses (most) architectural effects, and (2) ISA support (called AMi, for Architectural Mimicry) and programming models to effectively use mimic execution to balance or linearize code. We show the feasibility and benefits of our proposal by implementing mimic execution and AMi for a 32-bit out-of-order RISC-V core that leaks control flow in multiple ways (via e.g., the branch predictor, instruction timings, and the data cache). Our experimental evaluation shows that the hardware cost is low (most importantly, no impact on the processor′s critical path), and that AMi enables significant performance improvements. In particular, AMi reduces the overhead of state-of-the-art linearized code by 60% in our benchmarks.

Microarchitectural attacks typically rely on precise timing sources to uncover short-lived secret-dependent activity in the processor. In response, many browsers and even CPU vendors restrict access to fine-grained timers. While some attacks are still possible, several state-of-the-art microarchitectural attack vectors are actively hindered or even eliminated by these restrictions.

Preventing information leakage through microarchitectural side channels is notoriously challenging and, as a result, an important research question. Recent work has shown the viability of compiler-assisted instruction balancing for small, embedded processors with deterministic timing behavior. However, even in such small processors, more subtle microarchitectural side channels continue to be discovered, complicating mitigation efforts.We propose a methodology for augmenting an existing instruction set architecture (ISA) specification with instruction-specific microarchitectural leakage traces obtained through principled microarchitectural profiling. Building on this augmented ISA, it becomes possible to construct software tools to detect and mitigate certain side-channel vulnerabilities. As a case study, we instantiate our methodology on a recently uncovered microarchitectural side channel, which is based on cycle-level timing differences of direct memory access (DMA) requests on 16-bit openMSP430 processors. Using the augmented ISA obtained for this side channel through microarchitectural profiling, we develop practical attack scenarios and extend a state-of-the-art compiler-based mitigation and a binary validation tool, both of which originally targeted a coarser-grained, instruction-granular side channel. Our benchmarks show that our extended compiler mitigation, while still mitigating the instruction-granular leakage, also eliminates the cycle-accurate DMA information leakage without incurring any additional overhead.

The security claims of a system can be supported or refuted by different kinds of evidence. On the one hand, attack research uses empirical, experimental, inductive methods to refute security claims. If motivated and competent attackers do not succeed in breaking a specific security property, this provides some support (but no definite proof) that the system is secure.On the other hand, formal methods use mathematical, deductive methods that can prove the security of a model of the system. The process of constructing a proof can uncover vulnerabilities that can then be fixed. The use of formal methods can be very powerful and is attractive because it seems to provide irrefutable evidence of security. However, that evidence applies only to the mathematical model, not to any actual system, and, hence, it is important to understand the gap between the model and the real-world system.In this paper, we present a case study that examines this gap for two embedded security architectures that use formal methods to prove their security properties. Despite strong formal evidence for security, we discover numerous attacks against the implementations, all of which falsify proven security properties. These attacks range from exploiting simple programming errors to a novel DMA-based side-channel attack. The simple attacks demonstrate that the construction of systems and proofs is error-prone, while some of the more sophisticated attacks serve as examples to show that formal methods alone can never guarantee the security of a real-world system.From our case study, we also distill actionable guidelines on how to provide stronger evidence for the security of a system.