[hacs] x86 verification

[Lennart Beringer]

One of the issues is that manufacturers have traditionally been reluctant
to bless any independently developed formalization or publish their own one in
whatever proof assistant they prefer. The various CompCert backends also contain
assembly language specs, but at a slightly higher level of abstraction than is 
maybe desirable.

But there's hope: Peter Sewell's REMS project is collaborating with ARM - see the 
description of task 2 here: https://www.cl.cam.ac.uk/~pes20/rems/index-tasks.html.
Maybe this creates enough pressure to force other manufacturers to do the same...

Also, open architectures such as Risc-V don't present these administrative
challenges. Adam Chlipala's group is collaborating with the BlueSpec team to
enable the writing of specs for various processors, and to translate these 
in a provably correct way into circuit descriptions: http://deepspec.org/research/Kami.

Lennart.

----- Original Message -----
From: "Aaron Tomb" <atomb at galois.com>
To: hacs at moderncrypto.org
Sent: Wednesday, February 22, 2017 6:09:29 PM
Subject: Re: [hacs] x86 verification

A related bit of work created a separate model of x86 (in Coq instead
of the ACL2 cited below). They used a similar random testing approach
to validate the x86 model against real processors, and used the model
to prove that the structural code checks performed by the Google
Native Client are sufficient to get the isolation guarantees they
claim.

    http://www.cse.psu.edu/~gxt29/paper/rocksalt.pdf

There's also a similar bit of work in HOL4:

    https://www.cl.cam.ac.uk/~pes20/weakmemory/index3.html

So whichever theorem prover you want to use, there's an x86
description you can use. I wish there were some way to share an
instruction set definition between proof systems, though. It seems
like a lot of duplicated work.


On Wed, Feb 22, 2017 at 6:07 AM, Ben Laurie <ben at links.org> wrote:
> I haven't read it (yet), but seems interesting...
>
> Formal Verification of Application and System Programs Based on a
> Validated x86 ISA Model:
> http://www.cs.utexas.edu/~shigoel/x86isaInfo/Shilpi-Goel-Dissertation.pdf
> _______________________________________________
> Hacs mailing list
> Hacs at moderncrypto.org
> https://moderncrypto.org/mailman/listinfo/hacs
_______________________________________________
Hacs mailing list
Hacs at moderncrypto.org
https://moderncrypto.org/mailman/listinfo/hacs