[libre-riscv-dev] formal proof NLnet proposal in
hendrik at topoi.pooq.com
Mon Sep 23 12:32:01 BST 2019
On Mon, Sep 23, 2019 at 03:58:54AM +0100, Luke Kenneth Casson Leighton wrote:
> submitted. this is a proposal that we adopt formal mathematical
> proofs as the "default" unit test, exactly as samuel falvo did. does.
> and receive funds for doing so.
I'm not familiar with current work on hardware verification, but I find
myself doubtful of this project. My experience with formal verification
(admittedly dating back to the late 80's) indicates that it is very
It's possible that SymbiYosys takes advantage of typical hardware coding
patterns to greatly simplify and automate the entire process, but I'd be
wary of committing to a project of this scale for pay if the pay is only
available when the entire project is finished.
That said, I'm willing to have a look at the problem and see what I can do
in my so-called spare time.
The links in the project proposal give me somewhat more information about
the SymbiYosys. It appears to be a framework for xressing assertions and
calling on independently written theorem provers. Still, the text provided
gives little information about what its various provers actually do. It
suggests trying them out on sample problems to get a feeling for them.
"Trial and error can also be a useful method for evaluating engines."
But I do have doubts about using "feelings" when doing formal verification.
The links I see to code repositories for these provers don't seem to reach
much in the way of documentation. But maybe that's because I'm unfmiliar
with bitbucket and I have to actually install them before I see any.
I have a 16G RAM on my Purism laptop (yes, likely the same Purism that has
showed interest in our project). Unfortunately it has an intel processor,
so it cannot be secure.
Sometime in the next few weeks I'll try installing this stuff and see what
happens. I'll get a larger hard drive if necessary.
Or is there a system elsewhere I should be using for this?
> what that gives us is a greatly-simplified testing regime (as outlined
> and explained by sam). it also ensures that there's no 3rd party that
> needs to be approached in an independent audit of the code.
There are still issues -- the possibility that the prover may itself have
bugs, the possibility that one misunderstands just what the prover
guarantees to do, the possibility that we fail to write the correct
specifications. For example, the bounded model check just
checks that the system follows spec for a specified number of cycles.
Without knowing this, one might assume that passing the check accomplishes
complete verification. This limitation is documented. But there may be
other restrictions I haven't seen yet, given the sparsity of
the documentation I've located.
What are the limitations of the various provers? At present I do not know.
And I suspect that proving no information leaks will be very difficut
indeed. I do not know a formalism that can accomplish this. There may be
one -- anyone know? It would require statistical, probabilistic global
analysis. It may not be wise to promise this before payment. But
it would be lovely to accomplish it.
More information about the libre-riscv-dev