CS Events

Computer Science Department Colloquium

Designing Formally Correct Intermittent Systems

 

Download as iCal file

Thursday, March 23, 2023, 10:30am - 12:00pm
 

Speaker: Milijana Surbatovich

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.

Location : CoRE 301

: 

Event Type: Computer Science Department Colloquium

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.

: 

Contact  Yipeng Huang

Livestream available via Zoom:
https://rutgers.zoom.us/j/92060421647?pwd=UUMrek81TnVPY0Jma2ZielIwYzdIdz09