|
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.
|
