A Hoare Logic for Rust | Hacker News Reader

A Hoare Logic for Rust

ticki.github.io

193 pointssteveklabnik43 comments

Nice. It makes sense to try to formalize the semantics of Rust's new intermediate representation, MIR. It's much easier to get unambiguous semantics at that level. All name issues such as shadowing are gone, type issues have been resolved, and operations are machine-level unambiguous (not "+", "32 bit unsigned add").

An old project I worked on, the Pascal-F verifier,[1] from the early 1980s, worked in a similar way. We took the output from the first pass of the compiler, which was something like Java bytecode, and verified from that.

I found some old 9-track tapes of the sources recently, and I'm going to run them through a data recovery service in Morgan Hill next week and see if I can bring the system back to life. It's a historical curiosity, but should be fun to play with on today's machines. It was just too slow in 1982. Meanwhile, I brought the original Boyer-Moore theorem prover back to life and put it on Github.[2]

Some of our lessons learned were:

1. Integrate the verification statements into the programming language. Don't try to do it with comments. You want the language's regular syntax, type and variable checking to apply to the verification statements. We added the keywords ASSERT, ENTRY, EXIT, MEASURE, STATE, EFFECT, INVARIANT, DEPTH, and PROOF, EXTRA, and RULE.

2. Make verification program-like, not math-like. For example, if we wanted to verify the structure of a tree, we would add fields for a back-pointer and a tree depth to the data structure each node. We'd put in all the code to maintain them, and verify that the forward pointers and back pointers were consistent and that child objects always had a greater depth than their parents. This would all be done by writing ordinary-looking code with ASSERT statements. But the new data fields would have the EXTRA attribute, and the code manipulating those fields would have PROOF in front of it. This meant it was there only for verification purposes. No executable code could depend on that data, so it could all be stripped out for execution.

3. Use two theorem provers. One prover was an Oppen-Nelson decision procedure. This is fully automatic proving for integer +, -, multiplication by constants, inequalities, conditionals, logic operators, structures, and arrays. This subset of mathematics is decidable and there's a fast, complete decision procedure for it. That knocks off all the easy stuff automatically. Easy stuff usually includes subscript checks and overflow checks. The second prover was the Boyer-Moore prover, which is semi-automatic; you have to propose lemmas to help it along. This is hard. By using ASSERT statements to narrow the area of trouble, you could reach the point where you had two successive ASSERTs, one of which should imply the other, but the Oppen-Nelson prover couldn't prove it and there was no previously proved rule on file to cover it. But now the problem had been narrowed to an abstract mathematical problem - prove the second ASSERT from the first. Someone could work on that in the Boyer-Moore prover and then export the rule for use in the main system. This provided a separation of functions - you could have mathematically oriented people to struggle with the theorem prover, independent of the code. You could reuse that rule elsewhere, and change other code without having to re-prove it. Today, we'd put files of useful theorems on Github. We never let the user add "axioms". That opens a huge hole.

4. Expect to do a lot of compiler-type analysis and bookkeeping as part of the verification process. For example, the static analysis to determine that a function is pure ("pure" means x = y implies f(x) = f(y), and no side effects.) is something to do as a routine compiler operation. Potential aliasing has to be discovered. Do this using compiler techniques; don't dump it into the theorems-to-be-proved mill, where it's much harder to give the programmer good error messages.

5. Don't fall in love with the formalism. Too much work in verification has been done by people who wanted to publish math papers, not kill program bugs. This is about creating bug-free code. I think people will get this now, but when I was doing this, everybody else involved was an academic.

[1] http://www.animats.com/papers/verifier/verifiermanual.pdf [2] https://github.com/John-Nagle/nqthm/tree/master/nqthm-1992

> Nice. It makes sense to try to formalize the semantics of Rust's new intermediate representation, not MIR.

I'm no expert, but according to this: https://blog.rust-lang.org/2016/04/19/MIR.html, MIR /is/ Rust's new intermediate representation.

Oops, put an unwanted "not" in there. Yes, formalize MIR. Don't try to formalize the source language.

Thanks for this.

Too much work in verification has been done by people who wanted to publish math papers, not kill program bugs. This is about creating bug-free code. I think people will get this now,

This might be right, but when I go areading I still find all the maths-orriented stuff.

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

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.

Design by Contract: http://c2.com/cgi/wiki?DesignByContract

Which is a key element of the Eiffel language ( https://en.wikipedia.org/wiki/Eiffel_(programming_language) ).

SPARK Ada also includes this concept of pre/post conditions: https://en.wikipedia.org/wiki/SPARK_(programming_language)

I haven't programmed in the latter, but I'd like to. Since I'm often in the maintenance end of the software cycle I don't have much opportunity (professionally) to introduce new languages (new tools, yes, but not new languages).

I have a coworker who thinks we do this with asserts (in C and C++), but it's only half the battle. The asserts only tell us that our exercised version of the program (through our non-comprehensive testing) hasn't failed pre/post-conditions. It's helpful, but not sufficient.

Design by contract has nothing to do with formal verification, though.

Respectfully, I have to disagree. Design by contract is, or can be, a component of formal verification. If it's all you've got, it's probably better than nothing.

Design by contract brings the concept of using preconditions, postconditions, invariants, and other contractual objects into the design and implementation of the software. These are able (depending on implementation) to be analyzed statically by machine or by hand, or dynamically during testing (with some systems the tests can be automatically generated to exercise the contracts). This may not be the limit or ideal of formal verification, but it is certainly a part of it and a good measure forward compared to the typical approaches used in our industry.

EDIT:

Let's settle a pertinent question first: Is Hoare logic a tool/approach for formal verification? If it is, then design by contract (being largely based on the concept of Hoare logic) is also a tool/approach for formal verification.

The potential points of disagreement, as I see them, are that Hoare logic is not a tool for formal verification, or that design by contract is not based on Hoare logic. Is there something else that I've missed or are these the points of disagreement?

Design by contract forces you to be explicit about your intended preconditions and postconditions. But “intended” isn't the same thing as “actual”. Verification is making sure that the preconditions and postconditions actually hold, in every possible case where the statement (or procedure or whatever) could be reached.

EDIT: Hoare logic is a tool for formal verification, indeed. DbC is not, though.

We're talking around each other. What is your definition of formal verification?

Proving that a program meets its specification.

Is Hoare logic a tool in that process?

Yes. Hoare logic's inference rules define which Hoare triples can be “legally” derived. The programmer's task isn't only to provide a Hoare triple (which by itself is just an assertion that a program meets a specification), but also to provide a derivation of that triple (the actual proof of the assertion). Design by contract is akin to giving a Hoare triple, but never giving its derivation.

Design by contract, is it based or not based on Hoare logic?

It's not. In DbC, you have preconditions and postconditions, but no means whatsoever to actually prove that, whenever the procedure's initial state meets the precondition, its final state will meet the postcondition.

Well, I've found the point disagreement.

So design by contract, based on Hoare logic, applied in languages like SPARK Ada and Eiffel, produces statements that are unverifiable.

But Hoare logic, a thing without an executable implementation, produces statements which are verifiable.

> In DbC, you have preconditions and postconditions, but no means whatsoever to actually prove that, whenever the procedure's initial state meets the precondition, its final state will meet the postcondition.

Except many implementations of design by contract execute the postcondition check and raise an exception if it's not satisfied, so I don't think your statement is correct.

The very reason why you need to raise the exception is because the postcondition doesn't hold. The point to verification is to make sure the postcondition holds. So I stand by my original assertion: DbC isn't verification.

If I were to categorize it, I'd call DbC formal specification that, combined with Eiffel or SPARK tools, can be used to verify that interfaces or code maintain those specific properties. It's a partial form of formal specification and verification that's still useful.

It doesn't have to be fully specified or proven to count as formal verification. Partial verification is a thriving field.

Yep, that's perfectly reasonable.

SPARK combines those intended specs with language-level details that it feeds to a prover to show conditions hold or errors are absent. How is such Design-by-Contract not formal verification of specific properties of software?

I didn't say anything about SPARK, because I know nothing about it. But, if SPARK actually checks that the specs are met, it's doing more than just DbC.

My last statement, since you've edited several of your comments without marking them as edited which makes this conversation, well, not an accurate account of our dialogue. Thanks for that.

You state that design by contract has nothing to do with formal verification. You also later said that Hoare logic is a tool for formal verification. Design by contract is an implementation/application of Hoare logic. Ergo, it has something to do with formal verification.

I've never said it is formal verification, I've only said that it is part of it. It requires tooling and proper application for it to be useful/correct/effective. But that's true of everything in formal verification.

Design by contact is more or less a prerequisite to formal verification.

If you don't have a well-defined contact, you won't be able to verify that context is adhered to.

Exactly. The way this works in practice is that functions have ENTRY and EXIT conditions. When verifying the function in isolation, the ENTRY conditions are assumed true, and the verification process attempts to verify that the EXIT conditions will then hold.

When verifying a caller, the verification system must verify at each call that the ENTRY conditions hold, and can then assume, after the call, that the EXIT conditions are true.

You can extend this to objects. Objects have invariants, which must be true whenever control is outside the function. So an object invariant is both an ENTRY and and an EXIT invariant for all exported functions.

(This is the source of the idea that objects should have "getters" and "setters", rather than exporting fields for external access. You need some place to check the object invariant.)

(When is control inside an object? It's complicated. A strict language on this would have public and private functions, and you wouldn't be allowed to call public functions from private ones, because that's a re-entry. There's also the problem of calling "out the bottom" of an object and eventually re-entering the object. Classic source of bugs in GUIs, which are collections of objects that call each other up, down, and sideways. And if you block inside an object, is it unlocked? Spec# addressed all this, with difficultly.)

Well, there's a great aside in this thread as to whether or no DbC applies here in a discussion of formal verification and that's good stuff.

But I figured it was relevant to mention that there are both an RFC [1] on adding DbC as a language feature and a library [2].

[1] https://github.com/rust-lang/rfcs/issues/1077

[2] https://github.com/nrc/libhoare

> Giving the pre and post-conditions for a function is much more reasonable than dropping down to a verification tool like Coq or TLA+

Reasonable for what? The design hypothesis behind a high-level specification/verification tool like TLA+ is that no language is currently capable of being reasoned-about in such a way that large, complex applications can be verified affordably. So far, this hypothesis holds. Language-level verification is therefore valuable when you either need to verify very local properties (pre/post conditions of a single subroutine, that is very important and/or tricky) or you need to do full end-to-end verification, in which case you will be able to verify only relatively small and simplified programs (like seL4 or CompCert) and at a very high cost (reasonable for high-assurance software only). So language-level verification and high-level specification and verification are currently useful for very different things.

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

Also the Rust compiler had Typestate analysis at one point of its development. [1]

[1] http://marijnhaverbeke.nl/talks/rustfest_2016/#4

Typestate is basically all subsumed by the uniqueness system. The two systems are equivalent, so in a sense Rust still has typestate.

Rustbelt targets unsafe and safe code. In addition, it will also deal with concurrency (incl. weak memory).

Disclaimer: I am affiliated with the project.

There's a forthcoming paper at PLAS (co-located with ACM CCS, in late October) that applies formal reasoning to a Rust-like type system.

The contribution here is a formalization of borrowing and ownership semantics very close to Rust's, plus a sketch of how one would prove that these semantics give memory safety. The techniques can probably be adapted to an analysis of Rust itself.

Benitez, S. "Rusty Types for Solid Safety." ACM PLAS 2016. https://sergio.bz/docs/rusty-types-2016.pdf

(Full disclosure: Sergio and I are colleagues.)

This is a pretty good general introduction to Hoare Logic.

Tony Hoare meets Graydon Hoare :^)

I always wondered if they are related.

They are not.

Heh, just realized my https://github.com/Ericson2314/a-stateful-mir-for-rust is a lot more like separation logic than I knew.

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.

Adblock Pro did that for me, disabling it on the website fixes things

Reply on news.ycombinator.com