Email Gateway (Dec 09 2025 at 23:38): Email Gateway (Dec 09 2025 at 23:38):From: Meera Sridhar <cl-isabelle-users@lists.cam.ac.uk>
Project Description:
We are seeking a highly-motivated Postdoctoral Fellow to join our team for the
DARPA Bus-based Local Attack Detection and Elimination (BLADE) program, a
groundbreaking collaborative project between UNC Charlotte, Electric Power
Research Institute (EPRI) and NVIDIA, to secure critical hardware bus systems.
This position will lead the formal methods and verification thrust, focusing
on providing mathematical assurances for the security of bus-based
communications.
Key Responsibilities:
Formally model and verify the correctness of “Forensic Observation
Data” (FODs) to ensure they accurately detect specified vulnerabilities.
Investigate and define formal models of formal security properties of the
PCIe bus and NVIDIA’s DPU, CPU, and NIC for the purposes of security.
Explore the use of high-assurance languages and toolchains for the
implementation of a verified validation engine.
Collaborate closely with our systems and cybersecurity teams to integrate
formal analysis and verified components into the broader project.
Publish research in top-tier security and formal methods conferences and
journals.
Required Qualifications:
A Ph.D. (or anticipated completion) in Computer Science or a related field.
A strong research background in formal methods, with demonstrated experience
in model checking, theorem proving, or formal specification.
An interest in applying formal methods to real-world systems and security
challenges.
Preferred Qualifications:
Direct experience with formal specification and verification tools (e.g.,
Lean, TLA+, Coq, SMT solvers, etc.) is strongly preferred.
Familiarity with high-assurance languages or provably-correct software
development.
Knowledge of low-level hardware protocols (e.g., PCIe), computer
architecture, or systems security.
Understanding of vulnerability analysis or anomaly detection.
To apply, please submit the following materials to Dr. Meera Sridhar
(msridhar@charlotte.edu):
A Curriculum Vitae (CV).
A cover letter detailing your specific experience with formal methods tools
and your interest in systems security.
Contact information for three professional references.
One or two representative publications (preferably on formal verification or
security).
Last updated: Dec 21 2025 at 20:24 UTC