FM-Fuzz: Continuous Fuzzing and AI-based Bug Fixing for Formal Methods

About the Project

Formal Methods (FM), mathematically rigorous techniques to prove security and correctness, are experiencing a major resurgence. Large-scale applications include AWS’s Zelkova to ensure cloud security, Facebook's Infer for detecting security vulnerabilities, Microsoft's Project Everest for verified cryptography, and Huawei's use of formal verification in its TEE microkernel.

However, this renewed interest in FM poses major challenges. One of them is ensuring tool reliability. Guarantees offered by FM tools are only valid if the tools themselves are sound. For example, a model checker may prove that a piece of C code is safe wrt. use-after-free errors—a serious security vulnerability—but a bug in the checker could invalidate that guarantee. Moreover, many FM tools feature complex, highly optimized codebases under rapid development. Despite promising advances, using FM tools to verify themselves is currently out of reach.

To improve tool reliability, researchers have resorted to automated testing. Various fuzzing campaigns have been conducting, including on SMT solvers, program verifiers, model checkers, and Datalog engines. These efforts have lead to 4,000 bugs, of which 3,000+ have been fixed by tool developers. While effective, such campaigns are unsustainable. There are two main obstacles. First, fuzzing campaigns are rarely integrated into continuous integration. Researchers run large-scale campaigns for a few months, publish a paper, and stop shortly afterward. It is often unclear whether the proposed techniques would be effective under resource-constrained CI/CD settings. Second, fuzzers produce large numbers of bug reports placing a significant burden on developers.

The goal of this Ph.D. project is to overcome both obstacles. We aim to realize FM fuzz, a continuous fuzzing and AI-assisted bug fixing pipeline for FM tools. Inspired by portfolio solving in the SAT/SMT, we aim to invent techniques for best using available fuzzers under resource constraints. Moreover, we plan to invent new AI-based techniques for automatically fixing soundness issues in FM tools. We expect FM-Fuzz to have a major impact on the FM ecosystem benefiting both academia and industry.

Eligibility

Applicants should have, or expect to achieve, at least a 2.1 honours degree or a master’s (or international equivalent) in a relevant science or engineering related discipline.

Funding

This is a 3.5-year PhD. Excellent candidates will be nominated for competence-based funding.

At The University of Manchester, we offer a range of scholarships, studentships and awards at university, faculty and department level, to support both UK and overseas postgraduate researchers.

For more information, visit our funding page or search our funding database for specific scholarships, studentships and awards you may be eligible for. We recommend that you apply early as the advert will be removed once the position has been filled.

Before you apply

We strongly recommend that you contact the Dominik Winterer (fme.lab.recruiting@gmail.com) for this project before you apply. Please include details of your current level of study, academic background and any relevant experience and include a paragraph about your motivation to study this PhD project.

How to apply

Apply online through our website: https://uom.link/pgr-apply-2425

When applying, you’ll need to specify the full name of this project, the name of your supervisor, if you already having funding or if you wish to be considered for available funding through the university, details of your previous study, and names and contact details of two referees.

Your application will not be processed without all of the required documents submitted at the time of application, and we cannot accept responsibility for late or missed deadlines. Incomplete applications will not be considered.

After you have applied you will be asked to upload the following supporting documents:

• Final Transcript and certificates of all awarded university level qualifications
• Interim Transcript of any university level qualifications in progress
• CV
• Supporting statement: A one or two page statement outlining your motivation to pursue postgraduate research and why you want to undertake postgraduate research at Manchester, any relevant research or work experience, the key findings of your previous research experience, and techniques and skills you’ve developed. (This is mandatory for all applicants and the application will be put on hold without it).
• Contact details for two referees (please make sure that the contact email you provide is an official university/work email address as we may need to verify the reference)
• English Language certificate (if applicable)

If you have any questions about making an application, please contact our admissions team by emailing FSE.doctoralacademy.admissions@manchester.ac.uk.