Formal Verification of Machine / Assembly Language

[Steven Bellock]

Has any work been done on the formal verification of RISC-V machine / assembly language code? I am running into cases where I'd like to prove that machine code cannot access certain registers and whatnot. 

Thanks

[Tommy Murphy]

Is this of any use?

https://riscv.org/blog/2020/05/getting-started-with-risc-v-verification/

---

From: Steven Bellock <sbel...@nvidia.com>
Sent: Tuesday, February 9, 2021 10:07:16 PM
To: RISC-V SW Dev <sw-...@groups.riscv.org>
Subject: [sw-dev] Formal Verification of Machine / Assembly Language

 

Has any work been done on the formal verification of RISC-V machine / assembly language code? I am running into cases where I'd like to prove that machine code cannot access certain registers and whatnot. 

Thanks

--
You received this message because you are subscribed to the Google Groups "RISC-V SW Dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to sw-dev+un...@groups.riscv.org.
To view this discussion on the web visit https://groups.google.com/a/groups.riscv.org/d/msgid/sw-dev/6e889ca7-3182-41d9-8dd4-1584fc642681n%40groups.riscv.org.

[Steven Bellock]

Negative. That’s for formal verification of a hardware implementation. I’m looking to see if a formal tool exists that takes as its inputs

1. RISC-V machine code (.hex, .s19)
2. Properties / assertions written against the code

and the tool would prove whether the properties / assertions are true or provide counter-examples.

 

While it’s true that this could possibly be accomplished with a specific RISC-V implementation in RTL and formal HW tools, I don’t need cycle accuracy. In addition I’d like to not wait hours / days for a result.

 

From: Tommy Murphy <tommy_...@hotmail.com>
Sent: Tuesday, February 9, 2021 3:31 PM
To: RISC-V SW Dev <sw-...@groups.riscv.org>; Steven Bellock <sbel...@nvidia.com>
Subject: Re: [sw-dev] Formal Verification of Machine / Assembly Language

 

External email: Use caution opening links or attachments

 

To view this discussion on the web visit https://groups.google.com/a/groups.riscv.org/d/msgid/sw-dev/LNXP123MB3675516F818C945279C805E3F98E9%40LNXP123MB3675.GBRP123.PROD.OUTLOOK.COM.

[Thomas Bourgeat]

Hi, 

A non-exhaustive  list of work that comes to my mind, and how they may be relevant:

https://github.com/uw-unsat/serval

in this work the authors developed a framework that contains among other things a symbolic interpreter for riscv, it relies on rosette that itself hook into z3 or other solvers to prove obligations.

They used their system to characterize several pieces of machine code.

https://github.com/anishathalye/notary (I have an institutional conflict of interest)

in this work, among other things, the authors proved that a piece of code running at the beginning  of a machine was guaranteed to put the machine in a deterministic initial state after it finished running (it zeroed out part of the memory, initialize registers in a deterministic way etc...).

Their work operate at a lower level than the previous work: their proof is about running the boot program on the RTL of a specific small machine (so the proof is at the RTL semantics).

https://github.com/mit-plv/riscv-coq ( conflict of interest, I contributed),

This is a Coq formalization of riscv which mainly supports  a base rv32/64i (minus complete support for exceptions/interrupts and some system instructions), at the base of an other project https://github.com/mit-plv/bedrock2 , in which colleagues have proven a simple compiler from a minimal imperative language to riscv, so it is their bread and butter to prove that certain snippets of assembly  do what they are expected to do.

All the best,

Thomas

[Jim Wilson]

On Tue, Feb 9, 2021 at 3:50 PM Steven Bellock <sbel...@nvidia.com> wrote:

Negative. That’s for formal verification of a hardware implementation. I’m looking to see if a formal tool exists that takes as its inputs

1. RISC-V machine code (.hex, .s19)
2. Properties / assertions written against the code

 You can find info on formal specs here.

    https://github.com/riscv/ISA_Formal_Spec_Public_Review

The Sail one was adopted as the official RISC-V International formal spec, and claims 300K instructions per second on a fast x86-64 machine.  But some of the others might be interesting to you also.  See the comparison table.

Jim