[hacs] x86 verification

[Aaron Tomb]

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