Undergraduate/Graduate (Summer) Intern - Formal Verification Methods for Cybersecurity

National Renewable Energy Laboratory • Golden, CO

9d

About The Position

The intern will work on the formal verification of system-level properties of energy systems, with a specific focus on verifying the properties of communication paths connecting components of energy systems of systems. Using the Isabelle/HOL interactive theorem proving environment, the intern will help develop and apply Adversarial Logic frameworks to rigorously model and reason about the security of these communication paths. This research contributes directly to NLR's mission of delivering verifiable, high-assurance cybersecurity solutions for operational technology.

Requirements

• Must be enrolled as a full-time student in a Bachelor's, Master's or PhD degree program, or graduated in the past 12 months from an accredited institution. Candidates who have earned a degree may work for a period not to exceed 12 months.
• Must have a minimum of a 3.0 cumulative grade point average.
• Please Note: •You will need to upload official or unofficial school transcripts as part of the application process. •If selected for position, a letter of recommendation will be required as part of the hiring process.
• Must meet educational requirements prior to employment start date.
• Required background: Expect a candidate who has completed BS in computer science, or computer engineering, or applied mathematics, or electrical engineering. Or a candidate who is currently pursuing or completed a master’s in computer science, or applied mathematics, or computer engineering, or software engineering, or cybersecurity, or information security, or electrical engineering. Or a candidate who is currently pursuing a Ph.D. in computer science, or computer engineering, or applied mathematics, or electrical engineering, or cybersecurity.
• Required skills: familiarity with proof assistants such as Isabelle/HOL, or Lean, or Coq, etc.
• Required research experience: formal verification methods.

Responsibilities

• Use the Isabelle/HOL interactive theorem proving environment to formally specify and verify properties of communication paths in energy systems.
• Develop and apply Adversarial Logic models to reason about potential attack vectors and system vulnerabilities.
• Conduct literature reviews on formal methods, interactive theorem proving, and cybersecurity of operational technology systems.
• Collaborate with research staff to translate system-level cybersecurity requirements into formal specifications.
• Assist in documenting proof strategies, findings, and formal models for internal reports and potential publications.
• Participate in team meetings, present progress updates, and contribute to technical discussions on research directions.
• Support the development of reusable formal frameworks that can be applied to a range of energy system components and configurations.

Benefits

• Benefits include medical, dental, and vision insurance
• 403(b) Employee Savings Plan with employer match
• sick leave (where required by law).
• NLR employees may be eligible for, but are not guaranteed, performance-, merit-, and achievement- based awards that include a monetary component.
• Some positions may be eligible for relocation expense reimbursement.

What This Job Offers

• Job Type: Full-time
• Career Level: Intern