(she/her/hers)
Carnegie Mellon University
Intermittent Computing Systems, Programming Languages, Applied Formal Methods
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. Previously, she received an MS in ECE from CMU in 2020 while doing her PhD and a BS in Computer Science from University of Rochester in 2017. Her research interests are in applied formal methods, programming languages, and systems for intermittent computing. She is excited by research problems that requiring reasoning about correctness and security across the architecture, system, and language stack. She has been awarded CMU's CyLab Presidential Fellowship in 2021 and won first place in the PLDI 22 SRC for her project on developing a type system for safe intermittent computing.
A Type System for Safe Intermittent Computing
Batteryless, energy-harvesting devices (EHDs) are an emerging platform that enables computing in remote or inaccessible environments such as tiny satellites, smart city sensing, or even in-/on-body implants. Instead of using a battery, an EHD harvests energy from its environment into a buffer and operates intermittently, only as energy is available. This operational cycle causes the device to experience frequent, arbitrary power failures that make correct programming difficult. To make progress, an intermittent system must save execution state before power failure and restore it after the device reboots. Incorrectly determining which state must be saved and where a save point should be made causes software to exhibit memory and timing bugs that would not occur on continuously powered program executions. As EHDs are envisioned to be remotely-deployed, low-maintenance devices, programs must execute reliably, without memory consistency or timing violations. Unfortunately, existing systems rely on ad-hoc correctness notions, providing few correctness guarantees.
My research lays the groundwork for designing formally correct intermittent systems.My goal is to use rigorous, precise correctness reasoning to define correct intermittent execution and then transform these formal correctness criteria into system and programming language implementations that give programmers assurance their intermittent systems and applications will execute as intended. In my work, I showed that existing ad-hoc correctness notions of intermittent execution are insufficient, leading to unaddressed bugs. I then developed the first formal model of intermittent execution and used it to define correctness conditions for memory consistency and timing properties on intermittent systems, leveraging information flow and type theory reasoning. Once I had formal meanings of correctness, I designed both enforcement mechanisms, e.g., runtime restoration mechanisms or compiler transformation tools, and abstractions programmers can use to specify their desired properties, e.g., types or annotated policies. My research thus allows the development of intermittent systems that meet specified guarantees of time and memory consistency, improving reliability.