fsainas / contracts-verification-benchmark Goto Github PK

Reference property by key rather than by position.

Files

Extend the toolchain to support skeletons of the following form:

{
    "name": "Example",
    "specification": "Description.",
    "properties": {
        "foo": "Foo property.",
        "bar": "Bar property."
    }
}

The toolchain should look for specification files and ground truth identified by the property key

solcmc
|---foo.sol
|---bar.sol
certora
|---foo.spec
|---bar.spec

property,version,truth,footnote-md
foo,v1,1,
foo,v2,0,
bar,v1,1,
bar,v2,0,

and should generate the README file accordingly.

# README
...

## Properties
- **foo**: Foo property.
- **bar**: Bar property.

Constraints

ID must be:

• [a-zA-Z0-9_-]+

Hi,

I saw your paper, nice! I think it's missing hevm and Halmos as a comparison, even though I think they are interesting?

https://github.com/a16z/halmos/
https://github.com/ethereum/hevm

Also, we have a benchmark set here:

https://github.com/eth-sc-comp/benchmarks

Maybe it'd be possible to merge/integrate the two?

Mate

The script run_solcmc.py generates command lines with two timeouts, like e.g.:

timeout 600 solc build/contracts/Htlc_reveal-auth-owner_v4.sol --model-checker-engine chc --model-checker-timeout 600 --model-checker-targets assert --model-checker-show-unproved

The problem is that the first timeout is expressed in seconds, while the second one is in milliseconds, so if the Z3 timeout works, the actual timeout is 600ms, which is too short for many experiments.

Fix the script to generate a default command line of the form:

timeout 10m solc build/contracts/Htlc_reveal-auth-owner_v4.sol --model-checker-engine chc --model-checker-timeout 0 --model-checker-targets assert --model-checker-show-unproved

In this way, solc/Z3 run without time constraints, and the actual timeout is that given by the Unix timeout command.

Currently, every result given by Certora is marked as strong:

    if no_errors_found(log.stdout):
        print(contract_path + ", " + spec_path + ": " + utils.STRONG_POSITIVE)
        return (utils.STRONG_POSITIVE, log.stdout+"\n"+log.stderr)
    else:
        print(contract_path + ", " + spec_path + ": " + utils.STRONG_NEGATIVE)
        return (utils.STRONG_NEGATIVE, log.stdout+"\n"+log.stderr)

When running the tool on a Certora specification file, its result should adhere to the following:

• When using assert and the property results green -> P!
• When using assert and the property results red -> F
• When using satisfy and the property results green -> P
• When using satisfy and the property results red -> F!

The --model-checker-timeout option of solc does not work consistently. For instance:

solc solcmc/build/contracts/VestingWallet_p2_v2.sol --model-checker-engine chc --model-checker-timeout 10000 --model-checker-targets assert --model-checker-show-unproved

does not terminate. This issue seems caused by a related issue of Z3, upon which solc relies.

Instead of using the --model-checker-timeout option of solc, use the Unix timeout command:

timeout <duration> solc solcmc/build/contracts/VestingWallet_p2_v2.sol --model-checker-engine chc --model-checker-targets assert --model-checker-show-unproved

Extend the toolchain to allow the inversion of the results provided by the tools.
This is needed to be able to express all the properties in skeleton.json as the actual properties expected by the contracts.

Allow specification files (of both Certora and SolCMC) to have the preamble

/// @custom:negate

indicating that the specified property is the negation of the property described in the skeleton. Results should be converted as follows:

• P -> N
• P! -> N!
• N -> P
• N! -> P!