Talk: Designing Formally Correct Intermittent Systems

LIVE STREAM: https://uwmadison.zoom.us/j/94682556896?pwd=UmJMNGNEUCthTHJGOWQrS2hFOGttQT09 

Abstract: "Extreme edge computing" is an emerging computing paradigm targeting application domains like medical wearables, disaster-monitoring tiny satellites, or smart 
infrastructure. This paradigm brings sophisticated sensing and data processing 
into an embedded device's deployment environment, enabling computing in environments 
that are too harsh, inaccessible, or dense to support frequent communication 
with a central server. Batteryless, energy harvesting devices (EHDs) are key to 
enabling extreme edge computing; instead of using batteries, which may be too costly 
or even impossible to replace, they can operate solely off energy collected from 
their environment. However, harvested energy is typically too weak to power a 
device continuously, causing frequent, arbitrary power failures that break 
traditional software and make correct programming difficult. Given the high 
assurance requirements of the envisioned application domains, EHDs must execute 
software without bugs that could render the device inoperable or leak 
sensitive information. While researchers have developed intermittent systems 
to support programming EHDs, they rely on informal, undefined correctness 
notions that preclude proving such necessary correctness and security properties.

My research lays the foundation for designing formally correct intermittent 
systems that provide correctness guarantees. In this talk, I show how 
existing correctness notions are insufficient, leading to unaddressed bugs. 
I then present the first formal model of intermittent execution, 
along with correctness definitions for important memory consistency 
and timing properties. I use these definitions to design and implement both 
the language abstractions that programmers can use to specify their desired 
properties and the enforcement mechanisms that uphold them. Finally, I discuss 
my future research directions in intermittent system security 
and leveraging formal methods for full-stack correctness reasoning. 

Bio:  Milijana Surbatovich is a PhD Candidate in the Electrical and Computer Engineering Department at Carnegie Mellon University, co-advised by Professors Brandon Lucia and Limin Jia. Her research interests are in applied formal methods, programming languages, and systems for intermittent computing and non-traditional computing platforms broadly. She is excited by research problems that require reasoning about correctness and security across the architecture, system, and language stack. She was awarded CMU's CyLab Presidential Fellowship in 2021 and was selected as a 2022 Rising Star in EECS. Previously, she received an MS in ECE from CMU in 2020  and a BS in Computer Science from University of Rochester in 2017.