A Hoare Logic for Rust

agentultra wrote: post #2

Very nice! Is work being done to produce a formal, verifiable specification? edit : I'm particularly interested in formal specifications and their use in open source software.

I know of a few efforts to better specify Rust in addition to ticki's (OP):

* https://github.com/nikomatsakis/rust-memory-model * http://plv.mpi-sws.org/rustbelt/ * https://kha.github.io/2016/07/22/formally-verifying-rusts-bi...

The first isn't using formal methods AFAIK, the second is, and the third is as well, but I think they're targeting safe code only.

Re: A Hoare Logic for Rust

#5

Post by lifthrasiir » Fri, Sep 30, 2016, 4:01 PM UTC

tudelo wrote: post #3

Very broken for me on Chrome. All the equations are randomly overlapping words. (Version 53.0.2785.116 m (64-bit))

Probably your connection to cdn.mathjax.org is somehow disabled or blocked.

Re: A Hoare Logic for Rust

#6

Post by mbrubeck » Fri, Sep 30, 2016, 4:03 PM UTC

dikaiosune wrote: post #4

agentultra wrote: post #2

Very nice! Is work being done to produce a formal, verifiable specification? edit : I'm particularly interested in formal specifications and their use in open source software.

I know of a few efforts to better specify Rust in addition to ticki's (OP): * https://github.com/nikomatsakis/rust-memory-model * http://plv.mpi-sws.org/rustbelt/ * https://kha.github.io/2016/07/22/formally-verifying-rusts-bi... The first isn't using formal methods AFAIK, the second is, and the third is as well, but I think they're targeting safe code only.

There was also Patina, which formalized a subset of safe Rust's semantics, though it was done on an older (pre-1.0) version of the language:

ftp://ftp.cs.washington.edu/tr/2015/03/UW-CSE-15-03-02.pdf

Re: A Hoare Logic for Rust

#7

Post by [deleted] » Fri, Sep 30, 2016, 4:03 PM UTC

tudelo wrote: post #3

Very broken for me on Chrome. All the equations are randomly overlapping words. (Version 53.0.2785.116 m (64-bit))

[deleted]

Re: A Hoare Logic for Rust

#8

Post by taktoa » Fri, Sep 30, 2016, 4:07 PM UTC

Tony Hoare meets Graydon Hoare :^)

Re: A Hoare Logic for Rust

#9

Post by cbHXBY1D » Fri, Sep 30, 2016, 5:05 PM UTC

Very cool. I've long that that having formal program verification built in to a language and run as part of the compiler is the way forward. Giving the pre and post-conditions for a function is much more reasonable than dropping down to a verification tool like Coq or TLA+. I know that AWS uses TLA+ to reason about the correctness of algorithms.

Re: A Hoare Logic for Rust

#10

Post by nickpsecurity » Fri, Sep 30, 2016, 5:20 PM UTC

Nice description and first steps. Ideal moves would probably be the following:

1.Modifying front-end for Frama-C flow or similar tool to take a subset of Rust with specs, generate the VC’s, and feed them to supported provers. He seems to be doing something similar but Im sure there’s some good tools to build on.

2. For manual and high-assurance, embed Rust into Simpl/HOL that seL4 used. Do an AutoCorres tool with that. You now have ability to pull similar effort with translation validation to machine code. Next, extend COGENT to generate Rust subset Simpl supports. You can now do, like their C example, a whole filesystem functionally that outputs verified Rust or machine code. Optionally extend the COGENT tool with QuickCheck, QuickSpec, etc esp where tests/specs can translate to Rust to. Quite a foundation for other Rust developments to build on. Including redoing Rust compiler in COGENT at least for certified, reference version. ;)