CAREER: Formally Verified Intermittent Systems with Tiered Trust

Batteryless, energy-harvesting, intermittent computing platforms can be deployed indefinitely in environments that are unsuitable for traditional embedded devices, such as disaster zones, body implants, or even tiny satellites, enabling exciting new applications across bio-medical, disaster monitoring, and defense domains. The major challenge hindering this advancement is that harvested energy is unreliable and causes frequent power failures that introduce new errors and bugs in software running on the platform. Such errors make these platforms unsafe for applications, e.g., in health and defense spaces, where bugs could cause significant harm, either by accident or by a malicious party exploiting the bug. The goal of this project is to build up both theory and practical tools to create an embedded operating system (OS) that is verified (i.e., proven by machine) to execute applications correctly and securely through power failures. The project's novelties are that it defines the first formal model of an intermittence-safe OS and develops new programming languages and verification frameworks for proving that intermittent system implementations satisfy their correctness and security requirements. Such verification tools integrate into AI-based code generation workflows and make writing correct software much easier, as coding agents can write proofs and developers can check that AI-generated code meets requirements. The project's impacts are that it makes intermittent computing platforms trustworthy to run sophisticated safety-critical applications in previously inaccessible deployment environments; that it gives developers tools to write verified intermittent system software, either directly or through AI workflows; and that it supports the education of a future workforce who can create provably well-behaved system software, reducing costly bugs and cyber-attack vectors. To accomplish its objectives, the project pursues four major thrusts. The first thrust develops foundational models of an intermittent OS, including precisely defined abstraction layers that allow delineated tiers of trust and modular verification of components. The second thrust creates domain specific languages for writing intermittent systems code, leveraging ownership type systems to get basic correctness and security assurances "by construction", making it easier for coding agents and non-expert programmers to write intermittent system software. The third thrust develops libraries for the Rocq and Verus verification frameworks that are specifically designed to reason about effects of intermittent execution, making it possible to have correctness proofs that apply directly to intermittent system implementations. Finally, to evaluate the framework, the fourth thrust ports a slice of the TOCK embedded OS to run provably safely intermittently, leveraging the theory, languages, and verification libraries crafted by the first three thrusts. Together, these contributions push the state-of-the-art in both the complexity of the intermittent system that can be formally proven correct and secure, and in the rigor and practicality of proof tooling, bringing safety-critical applications across bio-medical, remote monitoring, and defense domains to new deployment frontiers. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria. NSF Award ID: 2543611 | Program: 01002930DB NSF RESEARCH & RELATED ACTIVIT,01003031DB NSF RESEARCH & RELATED ACTIVIT,01002627DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Milijana Surbatovich | Institution: University of Maryland, College Park, COLLEGE PARK, MD | Award Amount: $399,522 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2543611 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2543611.html