s2n-tls icon indicating copy to clipboard operation
s2n-tls copied to clipboard

Add Docker image to be able to test cryptol

Open NLMalloy opened this issue 6 years ago • 1 comments

Problem:

Currently, the easiest way to run cryptol by itself is to run it with a docker image provided by galois. It requires code changes to your local branch. If we agree to own this image, we could both prevent the rabbit hunt to find how to get it working and stop devs constantly add/deleting the same 3 pieces.

Proposed Solution:

https://github.com/GaloisInc/s2n/tree/saw-docker This branch is out of date but you need 3 things from it to copy pasta into your repo

  1. create s2n/.devcontainer in your branch and copy the contents of the corresponding folder into it. It’s only one file https://github.com/GaloisInc/s2n/blob/saw-docker/.devcontainer/devcontainer.json Note: Mac users will have to change slashes to other direction //

  2. copy pasta this file and place it in the same location https://github.com/GaloisInc/s2n/blob/saw-docker/tests/saw/Dockerfile

  3. replace current .travis/install_z3_yices.sh with this https://github.com/GaloisInc/s2n/blob/saw-docker/.travis/install_z3_yices.sh

NLMalloy avatar Apr 06 '20 18:04 NLMalloy

We can provide an alternate for those who wish to develop on an EC2 instance.

export TESTS=tls SAW=true GCC_VERSION=NONE
codebuild/bin/s2n_codebuild.sh
export PATH=$PWD/test-deps/saw/bin/:$PWD/test-deps/z3/bin:$PATH

A brief example of how to load and run a Cryptol test:

ubuntu:s2n/ $ cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.8.1 (67fc367)
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :l tests/saw/spec/handshake/rfc_handshake_tls13.cry
Loading module Cryptol
Loading module s2n_handshake_io
Loading module rfc_handshake_tls13
rfc_handshake_tls13> :prove tls13rfcSimulatesS2N `{16}
Q.E.D.
(Total Elapsed Time: 15.602s, using Z3)

rday avatar Apr 06 '20 18:04 rday