About

I am a Ph.D. candidate in Computer Science at the University of Central Florida, advised by Dr. Gary T. Leavens. Since 2022 I have been a formal methods researcher at Idaho National Laboratory's National and Homeland Security Directorate, and more recently at the CyManII Cybersecurity Manufacturing Innovation Institute.

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), a framework for constructing formally verified, runtime-enforced safety monitors for cyber-physical communication protocols.

The core idea: you write a protocol specification as a Refined Multiparty Session Type (RMPST) — a type-theoretic formalism that describes the full choreography of a protocol, including data-dependent safety predicates discharged by an SMT solver. SPECTRE then produces three certified deployment paths from that specification:

• · Static (Facet): certified OCaml endpoint extraction with compile-time checking
• · Dynamic distributed (Facet): lightweight runtime monitors at each participant
• · Dynamic centralized (Platum): synthesized C FSMs for legacy embedded retrofit, running in O(1) memory at ~13 µs/message on ARM hardware

A composition theorem connects protocol conformance across all three paths to physical safety invariants — meaning the proof object and the deployed monitor are the same object. I have validated SPECTRE on MAVLink (ArduPilot, PX4) and Modbus, with 100% detection of behavioral attacks at under 10% latency overhead on a physical chemical mixing testbed.

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 — deadlock-free, with 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 — 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.