ORCID

0009-0003-7712-5055

Keywords

Session types, Formal Methods, Runtime Monitoring, Cyber Physical Systems, Theorem Proving

Subject Categories

Computer Sciences | Information Security | Theory and Algorithms

Abstract

Cyber-physical systems execute physical actions in response to software commands, making their communication protocols a primary attack surface. A stealthy attack is a sequence of individually valid messages that violates a required ordering, driving the system into an unsafe state without malware or protocol violation. Existing defenses examine messages or physical state in isolation, not protocol level sequences, and cannot prevent them. Preventing them requires enforcement that makes unsafe sequences unexecutable at the communication boundary.

Formal methods offer a principled path to enforcement, but no tool spans specification to safe deployed hardware. Model checking automates proofs but has no certified connection to the implementation and cannot handle complex systems. Theorem proving frameworks connect proofs to code but demand inductive proofs. No existing approach closes the gap between verified specification, application safety, and enforcement on legacy hardware.

This dissertation shows stealthy attacks are preventable before execution. Spectre enforces protocol behavioral contracts using Refined Multiparty Session Types through three formally connected components. Facet gives the first mechanized RMPST metatheory, deriving a statically checked OCaml endpoint and distributed enforcer validating traffic at the boundary. F*ACT closes the gap between protocol conformance and application safety, using model checking for bounded protocols and certified simulation for unbounded ones. Platum synthesizes flat C monitors as transparent legacy protocol proxies, cutting monitor latency 4x for deployment on ARM microcontrollers in UAV flight controllers. The three components share one RCFSM, so a safety property transfers to a deployment artifact once shown to admit only RCFSM conforming traces.

Completion Date

2026

Semester

Summer

Committee Chair

Paul Gazzillo

Degree

Doctor of Philosophy (Ph.D.)

College

College of Engineering and Computer Science

Department

Computer Science

Format

PDF

Document Type

Dissertation

Language

English

Download

Share

COinS
 

Accessibility Statement

This item was created or digitized prior to April 24, 2027, or is a reproduction of legacy media created before that date. It is preserved in its original, unmodified state specifically for research, reference, or historical recordkeeping. In accordance with the ADA Title II Final Rule, the University Libraries provides accessible versions of archival materials upon request. To request an accommodation for this item, please submit an accessibility request form.