skip to main content

Title: Modal Crash Types for Intermittent Computing
Intermittent computing is gaining traction in application domains such as Energy Harvesting Devices (EHDs) that experience arbitrary power failures during program execution. To make progress, programs require system support to checkpoint state and re-execute after power failure by restoring the last saved state. This re-execution should be correct, i.e., simulated by a continuously-powered execution. We study the logical underpinning of intermittent computing and model checkpoint, crash, restore, and re-execution operations as computation on Crash types. We draw inspiration from adjoint logic and define Crash types by introducing two adjoint modality operators to model persistent and transient memory values of partial (re-)executions and the transitions between them caused by checkpoints and restoration. We define a Crash type system for a core calculus. We prove the correctness of intermittent systems by defining a novel logical relation for Crash types.  more » « less
Award ID(s):
Author(s) / Creator(s):
; ; ;
Date Published:
Journal Name:
European Symposium on Programming
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Energy harvesters have enabled widespread utilization of ultra-low-power devices that operate solely based on the energy harvested from the environment. Due to the unpredictable nature of harvested energy, these devices experience frequent power outages. They resume execution after a power loss by utilizing intermittent computing techniques and non-volatile memory. In embedded devices, intermittent computing refers to a class of computing that stores a snapshot of the system and application state, as a checkpoint, in non-volatile memory, which is used to restore the system and application state in case of power loss. Although non-volatile memory provides tolerance against power failures, they introduce new vulnerabilities to the data stored in them. Sensitive data, stored in a checkpoint, is available to an attacker after a power loss, and the state-of-the-art intermittent computing techniques fail to consider the security of checkpoints. In this paper, we utilize the vulnerabilities introduced by the intermittent computing techniques to enable various implementation attacks. For this study, we focus on TI’s Compute Through Power Loss utility as an example of the state-of-the-art intermittent computing solution. First, we analyze the security, or lack thereof, of checkpoints in the latest intermittent computing techniques. Then, we attack the checkpoints and locate sensitive data in non-volatile memory. Finally, we attack AES using this information to extract the secret key. To the best of our knowledge, this work presents the first systematic analysis of the seriousness of security threats present in the field of intermittent computing. 
    more » « less
  2. Intermittent systems operate embedded devices without a source of constant reliable power, relying instead on an unreliable source such as an energy harvester. They overcome the limitation of intermittent power by retaining and restoring system state as checkpoints across periods of power loss. Previous works have addressed a multitude of problems created by the intermittent paradigm, but do not consider securing intermittent systems. In this paper, we address the security concerns created through the introduction of checkpoints to an embedded device. When the non-volatile memory that holds checkpoints can be tampered, the checkpoints can be replayed or duplicated. We propose secure application continuity as a defense against these attacks. Secure application continuity provides assurance that an application continues where it left off upon power loss. In our secure continuity solution, we define a protocol that adds integrity, authenticity, and freshness to checkpoints. We develop two solutions for our secure checkpointing design. The first solution uses a hardware accelerated implementation of AES, while the second one is based on a software implementation of a lightweight cryptographic algorithm, Chaskey. We analyze the feasibility and overhead of these designs in terms of energy consumption, execution time, and code size across several application configurations. Then, we compare this overhead to a non-secure checkpointing system. We conclude that securing application continuity does not come cheap and that it increases the overhead of checkpoint restoration from 3.79 μJ to 42.96 μJ with the hardware accelerated solution and 57.02 μJ with the software based solution. To our knowledge, no one has yet considered the cost to provide security guarantees for intermittent operations. Our work provides future developers with an empirical evaluation of this cost, and with a problem statement for future research in this area. 
    more » « less
  3. Intermittent computing applications in the IoT space, such as long-term monitoring of the structural integrity of infrastructures, rely on battery-less computing systems powered through scavenged energy. For such systems, power-loss is a fact of life, and there is a need for a secure power transition mechanism to convert the active system state into a protected nonvolatile form and back. We evaluate the architectural needs to secure these power transitions and to adapt computations based on the scavenged energy. Our objective is to enforce confidentiality, integrity, freshness, and authenticity over the system state across power loss. We observe that secure power transitions are delicate and complex. We need secure checkpoints which are expensive to compute, and which may require hardware-accelerated cryptography and isolated secure non-volatile storage. Next, we observe that in intermittent systems, the energy subsystem does not adapt to the needs of the application. Rather, the application must adjust its computing pattern to the available energy. We define an energy-harvester subsystem interface to optimize the run-time activity of the intermittent system. The interface drives the optimized execution of a secure communication protocol (covering key-exchange and bulk encryption), such that wasted energy is eliminated and that run-time performance is improved. We report results from several prototyping experiments. 
    more » « less
  4. Intermittent computing systems execute long-running tasks under a transient power supply such as an energy harvesting power source. During a power loss, they save intermediate program state as a checkpoint into write-efficient non-volatile memory. When the power is restored, the system state is reconstructed from the checkpoint, and the long-running computation continues. We analyze the security risks when power interruption is used as an attack vector, and we demonstrate the need to protect the integrity, authenticity, confidentiality, continuity, and freshness of checkpointed data. We propose a secure checkpointing technique called the Se-cure Intermittent Computing Protocol (SICP). The proposed protocol has the following properties. First, it associates every checkpoint with a unique power-on state to checkpoint replay. Second, every checkpoint is cryptographically chained to its predecessor, providing continuity, which enables the programmer to carry run-time security properties such as attested program images across power loss events. Third, SICP is atomic and resistant to power loss. We demonstrate a prototype implementation of SICP on an MSP430 microcontroller, and we investigate the overhead of SICP for several cryptographic kernels. To the best of our knowledge, this is the first work to provide a robust solution to secure intermittent computing. 
    more » « less
  5. Task-based intermittent software systems always re-execute peripheral input/output (I/O) operations upon power failures since tasks have all-or-nothing semantics. Re-executed I/O wastes significant time and energy and risks memory inconsistency. This paper presents EaseIO, a new task-based intermittent system that remedies these problems. EaseIO programming interface introduces re-execution semantics for I/O operations to facilitate safe and efficient I/O management for intermittent applications. EaseIO compiler front-end considers the programmer-annotated I/O re-execution semantics to preserve the task's energy efficiency and idem-potency. EaseIO runtime introduces regional privatization to eliminate memory inconsistency caused by idempotence bugs. Our evaluation shows that EaseIO reduces the wasted useful I/O work by up to 3× and total execution time by up to 44% by avoiding 76% of the redundant I/O operations, as compared to the state-of-the-art approaches for intermittent computing. Moreover, for the first time, EaseIO ensures memory consistency during DMA-based I/O operations. 
    more » « less