About

I recently defended my Ph.D. dissertation in Computer Science at the University of Central Florida, advised by Dr. Gary T. Leavens. Since 2022, I have been a Ph.D. intern at Idaho National Laboratory's National and Homeland Security Directorate, including a joint appointment with the CyManII Cybersecurity Manufacturing Innovation Institute. I have accepted a Research Scientist, System Security Researcher position at MIT Lincoln Laboratory.

My research sits at the intersection of programming language theory and cyber-physical systems security. The specific threat I focus on is the stealthy attack: a sequence of individually valid, authenticated commands that drives a physical system into an unsafe state. These attacks are invisible to signature-based intrusion detection (which checks individual messages) and to physics-based anomaly detectors (which have no notion of protocol structure). My goal is to close that gap with machine-checked, formally verified guarantees.

My dissertation introduces SPECTRE, Safety-enforcing Protocol Checking through Type-theoretic Runtime Enforcement. It is a unified F* framework that turns one high-level protocol specification into a shared refined communicating finite state machine, or RCFSM, for verification and deployment.

A user writes a Refined Multiparty Session Type, or RMPST, that specifies the complete communication choreography and its data-dependent safety conditions. Facet extracts the shared RCFSM from that specification. F*ACT proves that RCFSM-conforming traces preserve a system safety invariant. Platum and Facet then derive enforcement artifacts from the same model, so safety is not restated for each deployment target.

• · Facet, checked OCaml endpoints and distributed protocol enforcers for new or externally controlled endpoints
• · F*ACT, automated application-safety checking through generated nuXmv models or kernel-checked guard implications discharged with Z3
• · Platum, allocation-free C finite state machine monitors for retrofitting legacy systems without changing endpoint firmware

The composition theorem makes the connection explicit. If an artifact admits only traces permitted by the shared RCFSM, a safety result proved for that RCFSM transfers to the deployed artifact. This lets a single specification support verified endpoints, distributed protocol enforcers, and centralized C proxy monitors. I have applied SPECTRE to MAVLink, ArduPilot, PX4, and Modbus. Platum reduced monitor latency by four times over DATUM in ArduPilot SITL, while the Modbus work detected behavioral attacks on a physical chemical mixing testbed with less than ten percent latency overhead.

Multiparty session types are a type-theoretic formalism for specifying communication protocols as global interaction schemas. A global type describes the full choreography: who sends what to whom, in what order, subject to what conditions. Local types, projected from the global type, describe each participant's individual behavior. The theory guarantees that if every participant follows their local type, the global protocol is respected. The participants remain deadlock free and have no communication mismatches.

Refined session types add data-dependent predicates. In a UAV protocol, a refinement might say the next waypoint index must be strictly greater than the current one. These predicates are checked by an SMT solver at runtime, blocking sequences that appear individually valid but would drive the physical system into an unsafe state.

Mechanizing this theory in F* means these properties are not pen-and-paper claims. They are machine-checked proofs that the extraction pipeline carries through to the deployed monitor.

SPECTRE assumes an adversary who can inject, replay, or reorder messages at the network level, and who may have compromised one or more system components, including the ground control station, the autopilot OS, or a PLC. The adversary cannot break cryptographic message integrity, and operates within the protocol's message vocabulary (stealthy, not brute-force).

What SPECTRE guarantees: no trace accepted by the monitor drives the physical system to an unsafe state, regardless of the adversary's message sequence.

What SPECTRE does not guarantee: liveness under denial-of-service, or protection against adversaries who have compromised the monitor itself. The latter is addressed for dynamic deployments by composing monitors with seL4 microkernel isolation.