For solc-verify, Docker file needs an update?

[thomas-genet]

Description

I tried to build solc-verify from the Docker file docker/Dockerfile-solcverify.src and the command line:

docker build -t solc-verify -f docker/Dockerfile-solcverify-local.src .

But it fails on my computer.

Steps to Reproduce

docker build -t solc-verify -f docker/Dockerfile-solcverify-local.src . 
[+] Building 1.8s (8/11)                                                        
 => [internal] load build definition from file-solcverify.src              0.0s
 => => transferring dockerfile: 1.56kB                                     0.0s
 => [internal] load .dockerignore                                          0.0s
 => => transferring context: 2B                                            0.0s
 => [internal] load metadata for docker.io/library/ubuntu:focal            1.1s
 => [1/8] FROM docker.io/library/ubuntu:focal@sha256:669e010b58baf5beb283  0.0s
 => CACHED [2/8] RUN apt update && DEBIAN_FRONTEND="noninteractive" apt i  0.0s
 => CACHED [3/8] RUN pip3 install psutil                                   0.0s
 => CACHED [4/8] RUN curl --silent "https://api.github.com/repos/CVC4/CVC  0.0s
 => ERROR [5/8] RUN curl --silent "https://api.github.com/repos/Z3Prover/  0.7s
------
 > [5/8] RUN curl --silent "https://api.github.com/repos/Z3Prover/z3/releases/latest" | grep browser_download_url | grep -E 'ubuntu' | cut -d '"' -f 4 | wget -qi - -O z3.zip   && unzip -p z3.zip '*bin/z3' > /usr/local/bin/z3   && chmod a+x /usr/local/bin/z3:
#8 0.636 [z3.zip]
#8 0.636   End-of-central-directory signature not found.  Either this file is not
#8 0.636   a zipfile, or it constitutes one disk of a multi-part archive.  In the
#8 0.636   latter case the central directory and zipfile comment will be found on
#8 0.636   the last disk(s) of this archive.
------
executor failed running [/bin/sh -c curl --silent "https://api.github.com/repos/Z3Prover/z3/releases/latest" | grep browser_download_url | grep -E 'ubuntu' | cut -d '"' -f 4 | wget -qi - -O z3.zip   && unzip -p z3.zip '*bin/z3' > /usr/local/bin/z3   && chmod a+x /usr/local/bin/z3]: exit code: 9

I am wondering wether this Docker file has been updated recently? However, since I am new to Docker, I may do something wrong but I manage to build and run the default focal image.

Thanks in advance,

Thomas

[hajduakos]

Thanks for reporting. We haven't checked the docker file for a while, seems like there is an issue with Z3. I will take a look soon.

[thomas-genet]

Thank you very much!

[hajduakos]

Seems like latest releases do not have an Ubuntu binary. We'd have to investigate, but as a quick solution, can you try replacing latest with 36678822 in the following line of docker/Dockerfile-solcverify.src?

https://github.com/SRI-CSL/solidity/blob/0106cfb19b1c30f394ae0e3ed27ac36727502475/docker/Dockerfile-solcverify-local.src#L25

In other words, that line should be

RUN curl --silent "https://api.github.com/repos/Z3Prover/z3/releases/36678822" | grep browser_download_url | grep -E 'ubuntu' | cut -d '"' -f 4 | wget -qi - -O z3.zip \ 

This would use an older release with an Ubuntu binary.

[thomas-genet]

This is better. However it fails on Boogie this time :-)

[...]
=> [6/8] RUN wget https://packages.microsoft.com/config/ubuntu/20.04/pa  17.4s
 => ERROR [7/8] RUN dotnet tool install --global boogie                    3.1s
------                                                                          
 > [7/8] RUN dotnet tool install --global boogie:                               
#10 0.452                                                                       
#10 0.458 Welcome to .NET Core 3.1!                                             
#10 0.458 ---------------------                                                 
#10 0.458 SDK Version: 3.1.416                                                  
#10 0.458 
#10 0.458 Telemetry
#10 0.458 ---------
#10 0.458 The .NET Core tools collect usage data in order to help us improve your experience. It is collected by Microsoft and shared with the community. You can opt-out of telemetry by setting the DOTNET_CLI_TELEMETRY_OPTOUT environment variable to '1' or 'true' using your favorite shell.
#10 0.458 
#10 0.458 Read more about .NET Core CLI Tools telemetry: https://aka.ms/dotnet-cli-telemetry
#10 0.458 
#10 0.458 ----------------
#10 0.458 Explore documentation: https://aka.ms/dotnet-docs
#10 0.458 Report issues and find source on GitHub: https://github.com/dotnet/core
#10 0.458 Find out what's new: https://aka.ms/dotnet-whats-new
#10 0.458 Learn about the installed HTTPS developer cert: https://aka.ms/aspnet-core-https
#10 0.458 Use 'dotnet --help' to see available commands or visit: https://aka.ms/dotnet-cli-docs
#10 0.458 Write your first app: https://aka.ms/first-net-core-app
#10 0.458 --------------------------------------------------------------------------------------
#10 2.969 error NU1202: Package Boogie 2.12.1 is not compatible with netcoreapp3.1 (.NETCoreApp,Version=v3.1) / any. Package Boogie 2.12.1 supports: net6.0 (.NETCoreApp,Version=v6.0) / any
#10 3.060 The tool package could not be restored.
#10 3.060 Tool 'boogie' failed to install. This failure may have been caused by:
#10 3.060 
#10 3.060 * You are attempting to install a preview release and did not use the --version option to specify the version.
#10 3.060 * A package by this name was found, but it was not a .NET Core tool.
#10 3.060 * The required NuGet feed cannot be accessed, perhaps because of an Internet connection problem.
#10 3.060 * You mistyped the name of the tool.
#10 3.060 
#10 3.060 For more reasons, including package naming enforcement, visit https://aka.ms/failure-installing-tool
------
executor failed running [/bin/sh -c dotnet tool install --global boogie]: exit code: 1

[thomas-genet]

If this is too complex to repair, I would be happy to download a docker image already built to play a bit with solc-verify. Is it available somewhere?

Best,

Thomas

[jcrreis]

Hello, I have the same problem as @thomas-genet , can't run Dockerfile it fails when installing Boogie. Did you find any workaround or is the project dead?

Thank you

[hajduakos]

Hi @thomas-genet and @jcrreis !

Sorry, as of now, we are not really working on this project actively. Seems like the issue is that the latest versions of Boogie are not compatible anymore with .NET core 3.1. Also, they seem to not support CVC4 anymore (but support CVC5, which we didn't experiment with). Probably, this line could be modified:

https://github.com/SRI-CSL/solidity/blob/0106cfb19b1c30f394ae0e3ed27ac36727502475/docker/Dockerfile-solcverify-local.src#L38

to use an older Boogie version:

RUN dotnet tool install --global boogie --version 2.8.18

I am looking into this now.

[hajduakos]

Seems like my above comment solves the issue with Boogie. However, the CVC4 repo now redirects to the CVC5 repo, so instead CVC4-archived should be used. I'm testing that fix. If it works, I'll make a commit.

[hajduakos]

@thomas-genet @jcrreis can you please try my latest commit 8ea107c?

To me it works:

From root dir, execute

docker build -t solc-verify -f docker/Dockerfile-solcverify-local.src .
cd docker
./runsv.sh ../test/solc-verify/examples/Annotations.sol

Outputs something like:

C::add: OK
C::[implicit_constructor]: OK
C::[receive_ether_selfdestruct]: OK
Use --show-warnings to see 1 warning.
No errors found.

[jcrreis]

Hello @hajduakos , I can confirm that your commit is indeed working. Thank you for the support.

[jcrreis]

Hello again @hajduakos ,

I think I found a bug using this tool for solc 0.8.0

I tried to verify this contract:

//SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.0;

/// @notice __verifier_sum_uint(balances) <= address(this).balance
contract Reentrancy {

    mapping(address =>  uint) balances;

    function deposit() public payable {
        balances[msg.sender] += msg.value;
    }

    function withdraw(uint amount) public {
        require(balances[msg.sender] >= amount, "Insuficient Funds");
        (bool ok, ) = msg.sender.call{value: amount}("");
        if (!ok) revert("");
        balances[msg.sender] -= amount;
    }
}

And got the following output:

Reentrancy::deposit: OK
Reentrancy::withdraw: OK
Reentrancy::[implicit_constructor]: OK
No errors found.

Shouldn't the tool return an invariant might not hold, since this contract is vulnerable to a reentrant attack?

I see that you committed to 0.7 branch, but I would like to run this in more recent solidity versions that doesn't have to deal with overflow/underflow checking, is 0.8 version not stable yet?

Thank you.

[hajduakos]

@jcrreis Hey! Yes, unfortunately the 0.8 branch is not stable yet, we started experimenting with it but stopped actively working on it. Sometimes I do some small patches to 0.7 but as of now, we do not have plans for 0.8.

Closing this issue, but feel free to open new ones should there be further issues.

[thomas-genet]

@hajduakos thank you for the update! Best.