Can't run saw-remote-api using Docker image

[michaelabernardo]

Hi there!

I've been trying to set up the Salsa20 example you have for saw-remote-api using the galoisinc/saw-remote-api Docker image, and I keep running into some issues. Would you be able to give me some guidance?

I tried changing connect("cabal -v0 v2-run exe:saw-remote-api") to connect(argo.connection.HttpProcess(url=sys.argv[1])) in the salsa20.py script.

The errors I get include:

Dashboard error: can't connect to server: HTTPConnectionPool(host='localhost', port=1123): Max retries exceeded with url: /test/salsa20.py?title=salsa20.py (Caused by NewConnectionError('<urllib3.connection.HTTPConnection object at 0x7f2a57808390>: Failed to establish a new connection: [Errno 111] Connection refused'))

and

AttributeError: 'HttpProcess' object has no attribute 'send_command'

I get similar errors changing the connection to a RemoteSocketProcess.

Also, even though it doesn't successfully connect, I get ✅ All verified! at the end.

Thanks for the help!

[pnwamk]

Can you say a little more about your setup? Specifically I'm curious about the following at the moment:

• how was the server run?
• which version of the server are you working with? (I think galoisinc/saw-remote-api will default to latest with digest 355f47997cb5 at the moment -- if you type docker inspect IMAGE_ID (where IMAGE_ID corresponds to the saw-remote-api instance your running, i.e. see the output of docker images) there should be a RepoDigests entry with a sha256 hash which can confirm specifically which version of the server you've got)
• which salsa20.py script were you trying to run against the server? (which file, which repo commit if applicable, etc)
• what commands were you using to run the script and from which directory?

Perusing around the repositories and Docker hub with what you posted above in mind, I think you may have (reasonably) expected some of the scripts in the argo/examples directory to work, but unfortunately those are likely out of date and need to be removed (the examples we're actively developing/testing against/etc are in saw-script/saw-remote-api/test-scripts).

[pnwamk]

(As an aside: apologies for there not yet being a README or similar for setting up and running saw-remote-api on some simple examples. It's now on our todo list #1052.)

[michaelabernardo]

Sure! You're definitely right, though -- I was looking at an old version of the salsa20.py. Using the newer version, what would be the appropriate command to use to run the script?

• I'm running the server as a service in a CI pipeline. The setup looks something like this:

    - name: galoisinc/saw-remote-api:latest
      alias: saw-remote-api-http
      entrypoint: ["/usr/local/bin/saw-remote-api", "http", "--host", "0.0.0.0", \
"--port", "8080"]

• I am using the latest with that digest
• I was using the salsa20.py from argo/examples -- you're right, I was definitely using an old version
• To run, I used the command python3.7 test/salsa20.py "http://saw-remote-api-http:8080"

[michaelabernardo]

(As an aside: apologies for there not yet being a README or similar for setting up and running saw-remote-api on some simple examples. It's now on our todo list #1052.)

Thanks! That will definitely be helpful!

[pnwamk]

Below are some steps that worked locally for me with the galoisinc/saw-remote-api:latest container on Docker Hub. It's not super pretty... but it seems to work. It might be nice to get some examples and scripts that make this less painfull... Anyway, let me know if this doesn't work for you or if you still have issues running it in your particular setup and I'd be happy to dig further.

Steps

If needed, identify the docker image of interest and give it a cute name (SAW) for readability.

$ docker image ls
$ export SAW=<REPLACE WITH galoisinc/saw-remote-api IMAGE ID>

Clone the saw-script repo, checkout the state of the repo that corresponds to the v0.7 release (i.e., the state of affairs that matches the container galoisinc/saw-script:latest at Docker Hub)

$ git clone [email protected]:GaloisInc/saw-script.git
$ cd saw-script
$ git checkout tags/v0.7
$ git submodule update --init

Apply a small patch to change some of the test files to use the HTTP server and refer to file locations in the docker image.

$ git apply < <(curl -sSL "https://gist.githubusercontent.com/pnwamk/888542c10e32cfcae79cd5f605d2f68e/raw/d936fbb88777480e2523db206edbfe3d64cca046/http_salsa20.diff")

Let python know where to look for argo and saw modules and install any missing python dependencies.

$ export PYTHONPATH=$PWD/deps/argo/python:$PYTHONPATH
$ python3 -m pip install -r $PWD/deps/argo/python/requirements.txt

Go to the test directory, launch the server, and copy the salsa20 files into the docker container so the server can load them.

$ cd saw-remote-api/test-scripts
$ export SAWC="$(docker run -d -p 8080:8080 $SAW)"
$ docker cp salsa20.bc $SAWC:/home/saw
$ docker cp Salsa20.cry $SAWC:/home/saw

Run the script to interact with the SAW server.

$ python3 salsa20.py

If everything worked out, you should see:

Starting server
Connecting to SAW server at http://localhost:8080
Loading Cryptol spec
Loading LLVM module
Verifying rotl
Verifying s20_quarterround
Verifying s20_rowround
Verifying s20_columnround
Verifying s20_doubleround
Verifying s20_hash
Verifying s20_expand32
Verifying s20_crypt32
Done

[michaelabernardo]

Thanks so much! I was able to get it working locally following your instructions, and I'm going to keep playing around with it.

One other question - is there something I have to do in order to run the verification again? I tried to change a <<< to a >>> in the salsa20.py script so I could see what would happen if the proof fails, and I got this error:
saw.exceptions.CryptolError: error: Attempted to register the following name twice: cryptol:/Salsa20/quarterround
And now even if I change the script back to the original, I still get that error.

[pnwamk]

I believe that error is complaining that you’re reloading files which are already loaded on the server when you run the script again. I can look into it more in a bit... it seems like either there should be a graceful way to avoid that on the server’s end (I.e., just don’t load the file again if it’s already loaded) or if not for some reason, the reported error should be more helpful at a minimum. Anyway, you could try commenting out the load statements as a workaround and see if that works.

…

On Mon, Feb 1, 2021 at 6:52 AM michaelabernardo ***@***.***> wrote: Thanks so much! I was able to get it working locally following your instructions, and I'm going to keep playing around with it. One other question - is there something I have to do in order to run the verification again? I tried to change a <<< to a >>> in the salsa20.py script so I could see what would happen if the proof fails, and I got this error: saw.exceptions.CryptolError: error: Attempted to register the following name twice: cryptol:/Salsa20/quarterround And now even if I change the script back to the original, I still get that error. — You are receiving this because you were assigned. Reply to this email directly, view it on GitHub <#1051 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA36B2UOKAI5WOJVU53I6ILS425ZPANCNFSM4WZDZJLQ> .

[pnwamk]

The aforementioned possible workaround does not work around the issue =\

I'll have to prod more here and report back.

[pnwamk]

I think this issue is resolved. Please don't hesitate to re-open or open a new issue if I'm mistaken.

Also FYI, we've moved the development of the python clients for cryptol and saw here (at least for the time being): https://github.com/GaloisInc/galois-py-toolkit

[pnwamk]

As an update to this resolution, the experiment of having the python client live in a separate repository (galois-py-toolkit) ended up convincing us it should instead live here.

The SAW Python client is now located here: https://github.com/GaloisInc/saw-script/tree/master/saw-remote-api/python I tried to add enough to the README in that directory to explain how to get things up and running, but please reach out and/or file issues if things are not clear or seem broken.

In case it is useful, note this bash script we are using to run several verification scripts in sequence against a single running Docker container instance in CI.

[michaelabernardo]

The README looks awesome and is super helpful! I think there may have been a typo in the docker command:

$ docker run --name=saw-remote-api -d \
  -v $PWD/tests/saw/test-files:/home/saw/tests/saw/test-files \
  -p 8080:8080 \
  galoisinc/saw-remote-api:nightly

Currently the -v is $PWD/tests/saw/test-files:/home/saw/tests/test-files

[pnwamk]

Indeed - thanks for pointing it out! Just created a fix PR.