Milijana Surbatovich “Designing Formally Correct Intermittent Systems”

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 the University of Rochester in 2017.

Details

• Date: Tuesday, April 4
• Time: 11:00 am - 12:00 pm
• Category: Special Seminar
• Location: 34-401A

Host

• Adam Chlipala