Trustworthy Tools
Home | About Us | Projects | HOL-Omega | Publications | Dissertation | Divine Support

Bounty available for soundness bugs in HOL-Omega

There is a $100.00 bounty available (U.S. dollars) for new soundness bugs discovered in the HOL-Omega kernel.  By soundness bugs, we mean vulnerabilities in the HOL-Omega kernel that can be exploited to prove the theorem |- F in HOL-Omega.  The HOL-Omega version to be examined is the current developer version. Both the standard kernel in src/0 and the experimental kernel in src/experimental-kernel are possible sources.
This bounty does not cover tricks such as manipulating the HOL-Omega parser or prettyprinter of theorems, such as printing the constant T as F.  Protecting against such attacks are part of the purpose of the HOL Zero theorem prover, but not HOL-Omega. Any exploit that would also work in principle with the HOL4 theorem prover is also excluded.   Furthermore, this bounty does not cover known methods for proving arbitrary theorems in HOL4, such as mk_thm or external oracles.  Rather, this is intended to find real errors in the code that would imperil its security.
Multiple bugs that are small variations of each other will be rewarded as a single conceptual bug.  In case of multiple people finding the same bug, the first one to report it to this author by email will be the recipient of the bounty.
The purpose of this bounty is to accelerate the normal process of maturity for the HOL-Omega kernel, and to strengthen its reliability.  It is not intended as a statement of overconfidence in the kernel being bug-free; rather, it is an acknowledgement that correct software is hard to write.
In addition to the financial reward, the discoverers of such soundness bugs will have their names and discoveries listed on this web page.
This bounty is inspired by the example of HOL Zero by Mark Adams of Proof Technologies Ltd.

List of soundness bugs discovered:

Making formal methods into normal methods.