Refine Search Clear All


Career Areas


Experience Level


Employment Type


Location


Organization


Security Clearance

Keyword Search

Back to open positions

Formal Methods/Binary Analysis Research Scientist – Postdoctoral Researcher

Entry Level | Full-time
Postdoctoral/Fellowship | livermore, CA | 06/11/2021

Apply Now  

Company Description

Join us and make YOUR mark on the World!

Are you interested in joining some of the brightest talent in the world to strengthen the United States’ security? Come join Lawrence Livermore National Laboratory (LLNL) where our employees apply their expertise to create solutions for BIG ideas that make our world a better place.

We are committed to a diverse and equitable workforce with an inclusive culture that values and celebrates the diversity of our people, talents, ideas, experiences, and perspectives. This is essential to innovation and creativity for continued success of the Laboratory’s mission.

Job Description

We have one opening for a Postdoctoral Research Staff Member to engage in the research, design, and deployment of formal methods in the verification of binary code.  You will work as a technical expert in a team developing a framework applying concepts of proof-carrying code.  The goal of this project is to develop techniques that allow a device to verify formal evidence that firmware updates conform to a stated security policy.  This position is in the Center for Applied Scientific Computing (CASC) Division within the Computing Directorate.

In this role you will

  • Research, design, implement, and apply techniques for formal analysis of binary code.
  • Develop and apply lightweight techniques for proof verification.
  • Propose and implement predicate rewriting techniques to reduce the size and complexity of required proofs.
  • Contribute to grant proposals and collaborate with others in a multidisciplinary team environment, including academic and industrial partners, to accomplish research goals.
  • Pursue independent (but complementary) research interests and interact with a broad spectrum of scientists internal and external to the Laboratory.
  • Perform other duties as assigned.

Qualifications

  • Ph.D. in Computer Science, Mathematics or a related field.
  • Experience developing, implementing and applying formal methods using interactive theorem proving system such as Isabelle/HOL or Coq.
  • Experience modeling program semantics using formal methods.
  • Ability to conduct research, as documented by publications, reports, and presentations.
  • Analytical problem-solving and decision-making skills needed to craft creative solutions and independently solve complex problems.
  • Proficient verbal and written communication skills necessary to effectively collaborate in a multidisciplinary team environment, present and explain technical information to technical as well non-technical audiences, document work and write research papers.

Qualifications We Desire

  • Experience with program verification.
  • Experience with compiler internals.
  • Demonstrated technical leadership in fields related to program verification and binary analysis.

Additional Information

Why Lawrence Livermore National Laboratory?

  • Included in 2021 Best Places to Work by Glassdoor!
  • Work for a premier innovative national Laboratory
  • Comprehensive Benefits Package
  • Flexible schedules (*depending on project needs)
  • Collaborative, creative, inclusive, and fun team environment

Learn more about our company, selection process, position types and security clearances by visiting our Career site

Security Clearance

LLNL is a Department of Energy (DOE) and National Nuclear Security Administration (NNSA) Laboratory.  Some positions will require a DOE L or Q clearance (please reference Security Clearance requirement above).  If you are selected and a clearance is required, we will initiate a Federal background investigation to determine if you meet eligibility requirements for access to classified information or matter. In addition, all L or Q cleared employees are subject to random drug testing.  An L or Q clearance requires U.S. citizenship.  For additional information please see DOE Order 472.2.

Equal Employment Opportunity

LLNL is an affirmative action and equal opportunity employer that values and hires a diverse workforce. All qualified applicants will receive consideration for employment without regard to race, color, religion, marital status, national origin, ancestry, sex, sexual orientation, gender identity, disability, medical condition, pregnancy, protected veteran status, age, citizenship, or any other characteristic protected by applicable laws.

If you need assistance and/or a reasonable accommodation during the application or the recruiting process, please submit a request via our online form

California Privacy Notice

The California Consumer Privacy Act (CCPA) grants privacy rights to all California residents. The law also entitles job applicants, employees, and non-employee workers to be notified of what personal information LLNL collects and for what purpose. The Employee Privacy Notice can be accessed here.

Apply Now