Active Research
Security, Privacy, and Formal Methods in Healthcare Systems
My research sits at the intersection of healthcare systems, security, and formal methods.
I work on making health data infrastructure more robust — whether that means building
storage engines purpose-built for clinical monitoring, stress-testing voice agents that handle
protected health information, enabling privacy-preserving computation across institutional
boundaries, applying cryptographic proofs to genomic data, or formally verifying the data
models that underpin modern health information exchange.
EmberDB
FHIR-Native Time-Series Storage for Critical Care
- Specialized time-series database treating FHIR Observations as first-class citizens for ICU monitoring
- Chunked storage with FHIR-aware metric encoding, eliminating impedance mismatch between clinical data models and storage
- Integrated multivariate pattern detection — seasonal decomposition, change-point detection, anomaly scoring
- Benchmarked against InfluxDB, TimescaleDB, and QuestDB using MIMIC-III (330M observations, 38K patients)
Healthcare Voice Agent Security
Securing AI Voice Agents that Handle PHI
- Security evaluation of commercial and open-source voice AI platforms deployed in healthcare settings
- Novel testing framework with a FHIR-compliant EHR system for realistic attack simulation
- Covers authentication bypass, prompt injection, PHI extraction, and synthetic voice attacks
- Proposes a tiered security framework for reducing attack success rates while preserving clinical workflows
Privacy-Preserving Healthcare Cost Prediction
Secure Multiparty Computation for Cross-Institutional ML
- Custom SMPC protocol enabling joint model training across hospitals, insurers, and public health agencies
- Additive secret sharing with Beaver-triple-based multiplication and honest-majority assumption
- Commitment-based verification layer for detecting malicious participants
- Optimized for gradient-based ML workloads — fewer communication rounds than general-purpose frameworks
zkDNA
Zero-Knowledge Proofs for Negative STR DNA Match Verification
- Interactive ZK protocol allowing proof of DNA non-match without revealing actual genetic data
- Operates over committed STR allele values with locus-level inequality proofs
- Formal security analysis — completeness, soundness, and zero-knowledge properties
- Targeted at forensic investigations where suspects need privacy-preserving exclusion
Formal Verification of FHIR Resources
Lightweight Formal Methods for EHR Data Models
- Conceptual framework for applying formal verification to the HL7 FHIR Patient resource
- Formalizes structure, cardinality constraints, choice type invariants, and cross-field dependencies in Alloy
- Resource-centric verification boundary modeling external references as opaque types for tractable analysis
- Bounded model checking to exhaustively verify structural integrity, semantic consistency, and safety invariants
- Extensible compositionally to other FHIR resources and cross-resource workflows
Reading MUMPS at Scale
An Open Parser and an Empirical Study of VistA
- Open tree-sitter grammar for MUMPS that produces a reusable, analyzable concrete syntax tree
- Parses 98.6% of VistA's 33,951 routines (3.6M lines) with no error nodes; expression semantics verified by differential testing against YottaDB
- Call-graph and runtime-code-generation measurements over the OSEHRA VistA-M corpus
- Open-source artifact archived on Zenodo
