SMT checks of spec validity

[MrChico]

Even after a simple type checking, there are a number of ways in which specs can be malformed, possibly leading to crashes in different prover back ends.

There are a few checks that I think can be implemented quite straightforwardly with the assistance of an SMT checker, for example using the sbv library:

• Bound checking of expressions
  Can the expression assigned to a particular type fall out of the bounds of that type? Throw warning to suggest that the expression be further constrained to be bound.

• Case exhaustiveness / redundancy
  Throw warning if cases are not exhaustive, or if a case is redundant

• Array / mapping collisions
  In the classic token example:

     balanceOf[CALLER] => balanceOf[CALLER] - value
     balanceOf[to]     => balanceOf[to] + value

if CALLER == to, the same expression has been assigned to distinct values, and the spec doesn't make any sense. Specs like this should not be accepted.

[MrChico]

Some inspiration: https://github.com/LeventErkok/sbv/blob/master/Documentation/SBV/Examples/Transformers/SymbolicEval.hs

[franck44]

@MrChico I am not sure that using a direct encoding into SMTLIB syntax (this the example state_machine.{act,smt2}) is the best way to go.
SMT-solvers are used as back end solvers in many verification tools.
Let’s not re-invent the wheel: solidity may be translated into some language that has support for verification, and the translation may be proved “correct” or preserving some properties) which is easier than a direct encoding into SMTLIB syntax.

There are lots of techniques that are mature in the software verification community and it could be good to leverage them to build real trustworthy distributed systems.

Regarding the specs that are malformed, this is a valid point. But bear in mind that

1. Verification is about making sure (checking) that the implementation is doing the right thing (comparing the implementation with the spec). This can sometimes be automated or mechanised (model-checking, theorem proving)
2. Validation is about checking that the spec captures the “customers’ requirements”. This cannot usually be automated. The purpose of validation is to go from an possibly ambiguous and informal spec (say in plain English) to a formal one (in a logical language or temporal logic of some sort).

[leonardoalt]

@franck44 I'm not sure I get the first part of your comment. We're not reinventing the wheel: There are several tools out there that translate Solidity to some language which already has verification tooling. That's not the goal here. Act has nothing to do with Solidity (besides copying its storage layout).
In the example that you mentioned, state_machine.sol is there just for illustration purposes (to show where that Act came from). The smt2 query comes from reasoning about the specification itself, without any implementation. This is part of the modularity we're trying to achieve here.

[franck44]

thanks @leonardoalt

I'm not sure I get the first part of your comment. We're not reinventing the wheel: There are several tools out there that translate Solidity to some language which already has verification tooling.

I'd be interested to know what kind of tooling, and which target language is used.

That's not the goal here. Act has nothing to do with Solidity (besides copying its storage layout).
In the example that you mentioned, state_machine.sol is there just for illustration purposes (to show where that Act came from). The smt2 query comes from reasoning about the specification itself, without any implementation. This is part of the modularity we're trying to achieve here.

On the one hand, I think writing a spec in SMTLIB2 syntax may not be the most readable way to convey the intent. SMTLIB2 is a standard for the input syntax of SMT-solvers.
On the second hand, a specification is supposed to be independent of the implementation.
When I wrote re-inventing the wheel, I think there is more than a decade of work on program verification that''s been completely ignored and that may help to have a look at it.

Specification/implementation and verification that an implementation satisfies a spec dates back to the 60's (Hoare). I don't really understand what kind of modularity is achieved here and Hoare triples or pre/post-conditions are probably an established way of writing specification.

Some starting points (a few examples of what technology is currently available):

• Automated software verification, international competition on automated software verification (9th edition)

• Verify this conference 9th edition.

[leonardoalt]

I'd be interested to know what kind of tooling, and which target language is used.

Please check https://github.com/leonardoalt/ethereum_formal_verification_overview for a list of projects doing +- that. Note that many of these projects do employ state of the art formal verification techniques.

On the one hand, I think writing a spec in SMTLIB2 syntax may not be the most readable way to convey the intent. SMTLIB2 is a standard for the input syntax of SMT-solvers.

It looks like there might be some misunderstandings here: we're not writing specs in smtlib2. We are writing Act, and exporting proof obligations generated from analyzing the Act specification.

On the second hand, a specification is supposed to be independent of the implementation.

The specification is independent of the implementation, that's exactly the point of exporting proof obligations from the spec alone.

Specification/implementation and verification that an implementation satisfies a spec dates back to the 60's (Hoare). I don't really understand what kind of modularity is achieved here and Hoare triples or pre/post-conditions are probably an established way of writing specification.

Again, looks like a misunderstanding. One of the things Act allows you to do is exactly write pre and post conditions, so I don't know why you think we're not using that. I agree with you that it is probably an established way of writing specs, and we are doing that, but I disagree that other options should be disregarded just because of that. The modularity that I mean is for example, proving the post conditions written in the spec from the specs of storage update, and proving contract invariants as a separate step.

When I wrote re-inventing the wheel, I think there is more than a decade of work on program verification that''s been completely ignored and that may help to have a look at it.
Some starting points (a few examples of what technology is currently available):

Everyone working on Act has a background in formal methods, so I am very puzzled why you assume we are not aware of program verification and the decades of work on it, or why you think we're ignoring it.

[franck44]

Thanks for the link

I am happy to see that there is a lot of activity in the space of verifying smart contracts.

The modularity that I mean is for example, proving the post conditions written in the spec from the specs of storage update, and proving contract invariants as a separate step.

I think this is how some program verification tools (e.g. Dafny) operates, as well as other verification tools. Building summaries with pre and post-conditions (the spec) for each function and using/combining summaries enables modular verification. I am not sure there is anything new here.

Everyone working on Act has a background in formal methods, so I am very puzzled why you assume we are not aware of program verification and the decades of work on it, or why you think we're ignoring it.

I am not assuming anything here, and certainly nothing about anyone's background, but from the terminology used in the previous comments, it was not clear to me that we were on the same page.
At the end of the day, a smart contract is a program, and so program verification techniques can be used to detect defects and vulnerabilities in smart contracts. [the link you kindly provided contains some items that seem to follow this path].

If I understand well, the objective here is to provide better guarantees (absence of outOfbounds and so on) for the (Solidity) code.
So techniques like symbolic (concolic) execution, bounded model-checking, software model checking, static analysis are natural candidates.
And SMT-solvers can provide support for automated reasoning but may not provide a complete solution to the verification problem.

And to make it clear, I strongly support all the work on using formal methods :-) particularly on critical infrastructure like blockchains.

[leonardoalt]

it was not clear to me that we were on the same page.
If I understand well, the objective here is to provide better guarantees (absence of outOfbounds and so on) for the (Solidity) code.

@franck44 I think we're still not on the same page haha. We only recently updated our README, so I'm not sure you've had a chance to look into it (or maybe it's just badly written), but it could help to clarify some apparent misunderstandings.
Act has nothing to do with Solidity.
The primary goal is to be a specification language for Ethereum smart contracts, regardless which language the actual contract is written in, and not a program verification tool. Our goal is that existing and new smart contract verification tools will support Act specifications, and they will do the program verification part.
The second goal is to provide analysis on the specification itself as a standalone document. This is of course unrelated to the implementation (verified by whichever other tool), but can hopefully provide insights about post conditions and contract invariants. This is done by exporting proof obligations from Act (again, without any contract code) to different theorem provers, such as Coq, K, and SMT solvers. These are not at all supposed to represent or verify the whole program, but simple particular statements, that's why we use the theorem provers directly.

So techniques like symbolic (concolic) execution, bounded model-checking, software model checking, static analysis are natural candidates.
And SMT-solvers can provide support for automated reasoning but may not provide a complete solution to the verification problem.

Completely agree, but Act doesn't do program verification, so we're not doing any of the techniques from the first sentence. SMT solvers are used as one of the proof backends to prove particular statements, but are not expected at all to be the full solution.

I think this is how some program verification tools (e.g. Dafny) operates, as well as other verification tools. Building summaries with pre and post-conditions (the spec) for each function and using/combining summaries enables modular verification. I am not sure there is anything new here.

Yes, I agree with you. I didn't claim there is anything new in terms of verification techniques, that's exactly the point: To apply already existing concepts/ideas to the context of an Ethereum smart contract specification language, a feature we feel is missing in the ecosystem. Note that even Act itself isn't new, it is an extension of the previous Act specification format, which has been used to specify and verify important mainnet contracts.

And to make it clear, I strongly support all the work on using formal methods :-) particularly on critical infrastructure like blockchains.

Of course, I didn't think otherwise :)

[d-xo]

I have created seperate issues for the consistency checks suggested here to allow for easier tracking: #111 #110 #109.