Postdoc Formal Methods for Hardware Security UNC Charlotte

Stream: job postings

[Meera Sridhar]

Postdoctoral Fellow: Formal Methods for Hardware-Level Security (DARPA BLADE)

Location: University of North Carolina Charlotte

Position Type: Full-time Postdoctoral Researcher

Duration: 2-year term, with possibility of extension

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):

1.

2.

A Curriculum Vitae (CV).

A cover letter detailing your specific experience with formal methods tools and your interest in

systems security.

3. 4. Contact information for three professional references.

One or two representative publications (preferably on formal verification or security).