[libre-riscv-dev] formal proof NLnet proposal in

[Hendrik Boom]

On Mon, Sep 23, 2019 at 03:58:54AM +0100, Luke Kenneth Casson Leighton wrote:
> https://libre-riscv.org/nlnet_2019_formal/
> 
> 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 
difficult.

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." 
(https://symbiyosys.readthedocs.io/en/latest/quickstart.html#selecting-the-right-engine)

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?

-- hendrik  

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

-- hendrik