Support TLS in cryptol-remote-api (#1203)

Add support for TLS connections in both the rpc server
and client. Allow the client to disable certificate validation
via the `verify` keyword argument, i.e.,
`cryptol.connect(verify=False)`. The docker container
for `cryptol-remote-api` also contains a self-signed
cert for testing purposes.

Co-authored-by: Andrew Kent <andrew@galois.com>

.github/workflows/ci.yml

@@ -349,7 +349,11 @@ jobs:
 
       - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
         name: Test cryptol-remote-api
-        run: ./cryptol-remote-api/test_docker.sh ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }}
+        run: ./cryptol-remote-api/test_docker.sh http ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }}
+
+      - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
+        name: Test cryptol-remote-api (TLS)
+        run: ./cryptol-remote-api/test_docker.sh https ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }}
 
       - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
         uses: docker/build-push-action@v2

.gitpod.Dockerfile

@@ -0,0 +1,30 @@
+
+FROM gitpod/workspace-full
+
+# Install docker buildx plugin
+RUN mkdir -p ~/.docker/cli-plugins && \
+    wget \
+      https://github.com/docker/buildx/releases/download/v0.5.1/buildx-v0.5.1.linux-amd64 \
+      -O ~/.docker/cli-plugins/docker-buildx && \
+    chmod a+x ~/.docker/cli-plugins/docker-buildx
+
+USER root
+
+# Install Dropbear SSH server
+RUN apt-get update && DEBIAN_FRONTEND=noninteractive apt-get install -yq \
+        dropbear \
+    && apt-get clean && rm -rf /var/lib/apt/lists/* /tmp/*
+
+# Install Chisel
+RUN curl https://i.jpillora.com/chisel! | bash
+
+# Install GHC
+ARG GHCVER="8.10.3"
+ENV GHCUP_INSTALL_BASE_PREFIX=/opt \
+    PATH=/opt/.ghcup/bin:$PATH
+RUN curl -o /usr/local/bin/ghcup "https://downloads.haskell.org/~ghcup/0.1.14/x86_64-linux-ghcup-0.1.14" && \
+    chmod +x /usr/local/bin/ghcup
+RUN ghcup install cabal --set
+ENV PATH=/root/.cabal/bin:$PATH
+RUN ghcup install ghc ${GHCVER} && \
+    ghcup set ghc ${GHCVER}

.gitpod.yml

@@ -0,0 +1,39 @@
+image:
+  file: .gitpod.Dockerfile
+vscode:
+  extensions:
+    - haskell.haskell
+    - justusadam.language-haskell
+tasks:
+  - name: TCP Tunnel
+    command: chisel server --socks5
+  - name: SSH Server
+    command: |
+      [ -f /workspace/dropbear.hostkey ] || dropbearkey -t rsa -f /workspace/dropbear.hostkey
+      dropbear -r /workspace/dropbear.hostkey -F -E -s -p 2222 -P ~/dropbear.pid
+  - command: |
+      cabal v2-update
+      test -e cabal.project.freeze && exit 0
+      FREEZE=cabal.GHC-$(ghc --numeric-version).config
+      test -e $FREEZE && ln -s $FREEZE cabal.project.freeze
+  - command: |
+      mkdir -p ~/.ssh
+      if test -z "$SSH_KEY"; then
+          echo "Warning: SSH_KEY not set, skipping SSH setup"
+      else
+          echo "$SSH_KEY" >> ~/.ssh/authorized_keys
+          echo "1. Install Chisel on your local machine, e.g. curl https://i.jpillora.com/chisel! | bash"
+          echo "   see https://github.com/jpillora/chisel"
+          echo ""
+          echo "2. Connect via SSH from your local machine:"
+          echo "   ssh -o ProxyCommand='chisel client $(gp url 8080) stdio:%h:%p' gitpod@localhost -p 2222"
+          echo ""
+      fi
+ports:
+  - port: 8080
+  - port: 2222
+    onOpen: ignore
+  - port: 2375
+    onOpen: ignore
+  - port: 43022
+    onOpen: ignore

Dockerfile

@@ -1,4 +1,4 @@
-FROM debian:buster AS solvers
+FROM debian:buster-20210511 AS solvers
 
 # Install needed packages for building
 RUN apt-get update \
@@ -73,7 +73,7 @@ RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
 USER root
 RUN chown -R root:root /cryptol/rootfs
 
-FROM debian:buster-slim
+FROM debian:buster-20210511-slim
 RUN apt-get update \
     && apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 \
     && apt-get clean && rm -rf /var/lib/apt/lists/*

README.md

@@ -1,4 +1,6 @@
 [![Cryptol](https://github.com/GaloisInc/cryptol/workflows/Cryptol/badge.svg)](https://github.com/GaloisInc/cryptol/actions?query=workflow%3ACryptol)
+[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/GaloisInc/cryptol)
+
 
 # Cryptol, version 2
 

cryptol-remote-api/CHANGELOG.md

@@ -1,5 +1,11 @@
-# Revision history for cryptol-server
+# Revision history for `cryptol-remote-api` and `cryptol-eval-server`
 
-## 0.1.0.0 -- YYYY-mm-dd
+## 2.11.1 -- 2021-06-23
 
-* First version. Released on an unsuspecting world.
+* HTTPS/TLS support added. Enable by running server in `http` mode with `--tls`
+  flag or by setting an environment variable (command line `--help` contains details).
+
+
+## 2.11.0
+
+* First "released" version of `cryptol-remote-api`.

cryptol-remote-api/Dockerfile

@@ -1,6 +1,6 @@
 ARG GHCVER="8.10.3"
 ARG GHCVER_BOOTSTRAP="8.10.2"
-FROM debian:buster AS solvers
+FROM debian:buster-20210511 AS solvers
 
 # Install needed packages for building
 RUN apt-get update \
@@ -44,7 +44,7 @@ RUN latest="$(curl -sSL 'http://cvc4.cs.stanford.edu/downloads/builds/x86_64-lin
 # Set executable and run tests
 RUN chmod +x rootfs/usr/local/bin/*
 
-FROM debian:buster AS toolchain
+FROM debian:buster-20210511 AS toolchain
 ARG PORTABILITY=false
 RUN apt-get update && apt-get install -y libncurses-dev libz-dev \
     build-essential curl libffi-dev libffi6 libgmp-dev libgmp10 libncurses-dev libncurses5 libtinfo5 libnuma-dev \
@@ -81,7 +81,7 @@ RUN if ${PORTABILITY}; then \
 
 FROM toolchain AS build
 
-RUN useradd -m cryptol
+RUN useradd -u 1000 -m cryptol
 COPY --chown=cryptol:cryptol . /cryptol
 USER cryptol
 WORKDIR /cryptol
@@ -91,10 +91,9 @@ ENV LANG=C.UTF-8 \
     LC_ALL=C.UTF-8
 COPY cabal.GHC-${GHCVER}.config cabal.project.freeze
 
-RUN mkdir -p rootfs/usr/local/bin
-
 RUN cabal v2-update && \
     cabal v2-build -j cryptol-remote-api:exe:cryptol-remote-api cryptol-remote-api:exe:cryptol-eval-server && \
+    mkdir -p rootfs/usr/local/bin && \
     cp $(cabal v2-exec which cryptol-remote-api) rootfs/usr/local/bin && \
     cp $(cabal v2-exec which cryptol-eval-server) rootfs/usr/local/bin
 ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
@@ -103,9 +102,9 @@ RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
 USER root
 RUN chown -R root:root /cryptol/rootfs
 
-FROM debian:buster-slim
+FROM debian:buster-20210511-slim
 RUN apt-get update \
-    && apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 libnuma-dev \
+    && apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 libnuma-dev openssl \
     && apt-get clean && rm -rf /var/lib/apt/lists/*
 RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol
 COPY --from=build /cryptol/rootfs /
@@ -115,5 +114,11 @@ ENV LANG=C.UTF-8 \
     LC_ALL=C.UTF-8
 ENTRYPOINT ["/usr/local/bin/cryptol-remote-api"]
 WORKDIR /home/cryptol
+# Create self-signed certificates for HTTPS testing purposes - N.B.,
+# clients must opt in to accepting these by passing `verify=False` to
+# the `cryptol.connect` method (otherwise a security error is raised).
+RUN openssl req -nodes -newkey rsa:2048 -keyout server.key -out server.csr \
+      -subj "/C=GB/ST=London/L=London/O=Acme Widgets/OU=IT Department/CN=localhost"
+RUN openssl x509 -req -days 365 -in server.csr -signkey server.key -out server.crt
 CMD ["http", "--host", "0.0.0.0", "--port", "8080", "/"]
 EXPOSE 8080

cryptol-remote-api/docs/Cryptol.rst

@@ -13,39 +13,37 @@ The server supports three transport methods:
 
 
 ``stdio``
-  in which the server communicates over ``stdin`` and ``stdout``
+  in which the server communicates over ``stdin`` and ``stdout`` using `netstrings. <http://cr.yp.to/proto/netstrings.txt>`_
   
   
 
-Socket
-  in which the server communicates over ``stdin`` and ``stdout``
+``socket``
+  in which the server communicates over a socket using `netstrings. <http://cr.yp.to/proto/netstrings.txt>`_
   
   
 
-HTTP
-  in which the server communicates over HTTP
+``http``
+  in which the server communicates over a socket using HTTP.
   
   
-In both ``stdio`` and socket mode, messages are delimited using `netstrings. <http://cr.yp.to/proto/netstrings.txt>`_
-
 
 Application State
 ~~~~~~~~~~~~~~~~~
 
 According to the JSON-RPC specification, the ``params`` field in a message object must be an array or object. In this protocol, it is always an object. While each message may specify its own arguments, every message has a parameter field named ``state``.
 
-When the first message is sent from the client to the server, the ``state`` parameter should be initialized to the JSON null value ``null``. Replies from the server may contain a new state that should be used in subsequent requests, so that state changes executed by the request are visible. Prior versions of this protocol represented the initial state as the empty array ``[]``, but this is now deprecated and will be removed.
+When the first message is sent from the client to the server, the ``state`` parameter should be initialized to the JSON null value ``null``. Replies from the server may contain a new state that should be used in subsequent requests, so that state changes executed by the request are visible.
 
 In particular, per JSON-RPC, non-error replies are always a JSON object that contains a ``result`` field. The result field always contains an ``answer`` field and a ``state`` field, as well as ``stdout`` and ``stderr``.
 
 
 ``answer``
-  The value returned as a response to the request (the precise contents depend on which request was sent)
+  The value returned as a response to the request (the precise contents depend on which request was sent).
   
   
 
 ``state``
-  The state, to be sent in subsequent requests. If the server did not modify its state in response to the command, then this state may be the same as the one sent by the client.
+  The state, to be sent in subsequent requests. If the server did not modify its state in response to the command, then this state may be the same as the one sent by the client. When a new state is in a server response, the previous state may no longer be available for requests.
   
   
 

cryptol-remote-api/python/CHANGELOG.md

@@ -0,0 +1,6 @@
+# Revision history for `cryptol` Python package
+
+## 2.11.2 -- 2021-06-23
+
+* Ability to leverage HTTPS/TLS while _disabling_ verification of SSL certificates.
+  See the `verify` keyword argument on `cryptol.connection.connect(...)`.

cryptol-remote-api/python/cryptol/connection.py

@@ -17,7 +17,8 @@ def connect(command : Optional[str]=None,
             *,
             cryptol_path : Optional[str] = None,
             url : Optional[str] = None,
-            reset_server : bool = False) -> CryptolConnection:
+            reset_server : bool = False,
+            verify : Union[bool, str] = True) -> CryptolConnection:
     """
     Connect to a (possibly new) Cryptol server process.
 
@@ -33,6 +34,11 @@ def connect(command : Optional[str]=None,
     reset. (This ensures any states from previous server usages have been
     cleared.)
 
+    :param verify: Determines whether a secure HTTP connection should verify the SSL certificates.
+                   Corresponds to the ``verify`` keyword parameter on ``requests.post``. N.B.,
+                   only has an affect when ``connect`` is called with a ``url`` parameter
+                   or when the ``CRYPTOL_SERVER_URL`` environment variable is set.
+
 
     If no ``command`` or ``url`` parameters are provided, the following are attempted in order:
 
@@ -53,7 +59,7 @@ def connect(command : Optional[str]=None,
         c = CryptolConnection(command, cryptol_path)
     # User-passed url?
     if c is None and url is not None:
-        c = CryptolConnection(ServerConnection(HttpProcess(url)), cryptol_path)
+        c = CryptolConnection(ServerConnection(HttpProcess(url, verify=verify)), cryptol_path)
     # Check `CRYPTOL_SERVER` env var if no connection identified yet
     if c is None:
         command = os.getenv('CRYPTOL_SERVER')
@@ -65,7 +71,7 @@ def connect(command : Optional[str]=None,
     if c is None:
         url = os.getenv('CRYPTOL_SERVER_URL')
         if url is not None:
-            c = CryptolConnection(ServerConnection(HttpProcess(url)), cryptol_path)
+            c = CryptolConnection(ServerConnection(HttpProcess(url,verify=verify)), cryptol_path)
     # Check if `cryptol-remote-api` is in the PATH if no connection identified yet
     if c is None:
         command = find_executable('cryptol-remote-api')

cryptol-remote-api/python/poetry.lock

@@ -1,6 +1,6 @@
 [[package]]
 name = "argo-client"
-version = "0.0.4"
+version = "0.0.5"
 description = "A JSON RPC client library."
 category = "main"
 optional = false
@@ -12,7 +12,7 @@ requests = "*"
 
 [[package]]
 name = "bitvector"
-version = "3.4.9"
+version = "3.5.0"
 description = "A memory-efficient packed representation for bit arrays in pure Python"
 category = "main"
 optional = false
@@ -20,7 +20,7 @@ python-versions = "*"
 
 [[package]]
 name = "certifi"
-version = "2020.12.5"
+version = "2021.5.30"
 description = "Python package for providing Mozilla's CA Bundle."
 category = "main"
 optional = false
@@ -115,19 +115,19 @@ socks = ["PySocks (>=1.5.6,!=1.5.7,<2.0)"]
 [metadata]
 lock-version = "1.1"
 python-versions = ">=3.7.0"
-content-hash = "41e923e3f418b73af25a9f5557564c8efe79b24ec779a875d706963648aa762d"
+content-hash = "4fec48a3684b15cd29af1c2f3db5a9033d34a1605ad11aec7babafd2f6bcb1b1"
 
 [metadata.files]
 argo-client = [
-    {file = "argo-client-0.0.4.tar.gz", hash = "sha256:1ce6af1cbc738d08348dcb62d573968da58e2382cb4ea753cc061aa16d45ff6a"},
-    {file = "argo_client-0.0.4-py2-none-any.whl", hash = "sha256:74c13e9f3bf5a48eeda847af343bdaf54a950c100496ed3c342a51f5406cf568"},
+    {file = "argo-client-0.0.5.tar.gz", hash = "sha256:9b2157f3ea953df812948c27eb762dbe8401bb9d0dc74f49310b6636320a0347"},
+    {file = "argo_client-0.0.5-py3-none-any.whl", hash = "sha256:745239a231a0d891088ca2aedebd7ec075faf0f19c2f6b0ceafd252e3eed616d"},
 ]
 bitvector = [
-    {file = "BitVector-3.4.9.tar.gz", hash = "sha256:a5e94cbb4804213b1f0c32d84517cd8f0bb8c689b5eb8055d351632e220a5edd"},
+    {file = "BitVector-3.5.0.tar.gz", hash = "sha256:cac2fbccf11e325115827ed7be03e5fd62615227b0bbf3fa5a18a842a221839c"},
 ]
 certifi = [
-    {file = "certifi-2020.12.5-py2.py3-none-any.whl", hash = "sha256:719a74fb9e33b9bd44cc7f3a8d94bc35e4049deebe19ba7d8e108280cfd59830"},
-    {file = "certifi-2020.12.5.tar.gz", hash = "sha256:1a4995114262bffbc2413b159f2a1a480c969de6e6eb13ee966d470af86af59c"},
+    {file = "certifi-2021.5.30-py2.py3-none-any.whl", hash = "sha256:50b1e4f8446b06f41be7dd6338db18e0990601dce795c2b1686458aa7e8fa7d8"},
+    {file = "certifi-2021.5.30.tar.gz", hash = "sha256:2bbf76fd432960138b3ef6dda3dde0544f27cbf8546c458e60baf371917ba9ee"},
 ]
 chardet = [
     {file = "chardet-4.0.0-py2.py3-none-any.whl", hash = "sha256:f864054d66fd9118f2e67044ac8981a54775ec5b67aed0441892edb553d21da5"},

cryptol-remote-api/python/pyproject.toml

@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "cryptol"
-version = "2.11.1"
+version = "2.11.2"
 readme = "README.md"
 keywords = ["cryptography", "verification"]
 description = "Cryptol client for the Cryptol 2.11 RPC server"
@@ -15,7 +15,7 @@ include = [
 python = ">=3.7.0"
 requests = "^2.25.1"
 BitVector = "^3.4.9"
-argo-client = "0.0.4"
+argo-client = "0.0.5"
 
 [tool.poetry.dev-dependencies]
 mypy = "^0.812"

cryptol-remote-api/python/tests/cryptol/test_AES.py

@@ -7,7 +7,7 @@ from cryptol.bitvector import BV
 
 class TestAES(unittest.TestCase):
     def test_AES(self):
-        c = cryptol.connect()
+        c = cryptol.connect(verify=False)
         c.load_file(str(Path('tests','cryptol','test-files', 'examples','AES.cry')))
 
         pt = BV(size=128, value=0x3243f6a8885a308d313198a2e0370734)

cryptol-remote-api/python/tests/cryptol/test_CplxQNewtype.py

@@ -7,7 +7,7 @@ from cryptol.bitvector import BV
 
 class TestCplxQ(unittest.TestCase):
     def test_CplxQ(self):
-        c = cryptol.connect(reset_server=True)
+        c = cryptol.connect(reset_server=True, verify=False)
         c.load_file(str(Path('tests','cryptol','test-files', 'CplxQNewtype.cry')))
 
         forty_two = c.eval("fortyTwo").result()

cryptol-remote-api/python/tests/cryptol/test_DES.py

@@ -8,7 +8,7 @@ from cryptol.bitvector import BV
 
 class TestDES(unittest.TestCase):
     def test_SHA256(self):
-        c = cryptol.connect()
+        c = cryptol.connect(verify=False)
         c.load_file(str(Path('tests','cryptol','test-files','examples','DEStest.cry')))
 
         # we can run the test suite as indended...
@@ -18,26 +18,26 @@ class TestDES(unittest.TestCase):
         # self.assertTrue(all(passed for (_,_,passed) in vtres))
         # kares = c.eval('katest DES').result()
         # self.assertTrue(all(passed for (_,_,passed) in kares))
-        
+
         # ...but we can also do it manually, using the python bindings more
         def test(key, pt0, ct0):
             ct1 = c.call('DES.encrypt', key, pt0).result()
             pt1 = c.call('DES.decrypt', key, ct0).result()
             self.assertEqual(ct0, ct1)
             self.assertEqual(pt0, pt1)
-        
+
         # vktest
         vk = c.eval('vk').result()
         pt0 = BV(size=64, value=0)
         for (key, ct0) in vk:
             test(key, pt0, ct0)
-        
+
         # vttest
         vt = c.eval('vt').result()
         key = BV(size=64, value=0x0101010101010101)
         for (pt0, ct0) in vt:
             test(key, pt0, ct0)
-        
+
         # katest
         ka = c.eval('ka').result()
         for (key, pt0, ct0) in ka:

cryptol-remote-api/python/tests/cryptol/test_EvenMansour.py

@@ -8,7 +8,7 @@ from cryptol.bitvector import BV
 
 class TestEvenMansour(unittest.TestCase):
     def test_EvenMansour(self):
-        c = cryptol.connect()
+        c = cryptol.connect(verify=False)
         c.load_file(str(Path('tests','cryptol','test-files','examples','contrib','EvenMansour.cry')))
 
         F_10_4 = c.eval('F:[10][4]').result()

cryptol-remote-api/python/tests/cryptol/test_SHA256.py

@@ -8,7 +8,7 @@ from cryptol.bitvector import BV
 
 class TestSHA256(unittest.TestCase):
     def test_SHA256(self):
-        c = cryptol.connect()
+        c = cryptol.connect(verify=False)
         c.load_file(str(Path('tests','cryptol','test-files','examples','param_modules','SHA.cry')))
 
         m1 = CryptolLiteral('"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"')

cryptol-remote-api/python/tests/cryptol/test_basics.py

@@ -24,7 +24,7 @@ class BasicServerTests(unittest.TestCase):
 
     @classmethod
     def setUpClass(self):
-        self.c = cryptol.connect()
+        self.c = cryptol.connect(verify=False)
 
     @classmethod
     def tearDownClass(self):

cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py

@@ -21,7 +21,7 @@ class CryptolTests(unittest.TestCase):
 
     @classmethod
     def setUpClass(self):
-        self.c = cryptol.connect()
+        self.c = cryptol.connect(verify=False)
         self.c.load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
 
     @classmethod
@@ -203,7 +203,7 @@ class HttpMultiConnectionTests(unittest.TestCase):
     def test_reset_with_many_usages_many_connections(self):
         for i in range(0,100):
             time.sleep(.05)
-            c = cryptol.connect(url=self.url)
+            c = cryptol.connect(url=self.url, verify=False)
             c.load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
             x_val1 = c.evaluate_expression("x").result()
             x_val2 = c.eval("Id::id x").result()
@@ -213,12 +213,66 @@ class HttpMultiConnectionTests(unittest.TestCase):
     def test_reset_server_with_many_usages_many_connections(self):
         for i in range(0,100):
             time.sleep(.05)
-            c = cryptol.connect(url=self.url, reset_server=True)
+            c = cryptol.connect(url=self.url, reset_server=True, verify=False)
             c.load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
             x_val1 = c.evaluate_expression("x").result()
             x_val2 = c.eval("Id::id x").result()
             self.assertEqual(x_val1, x_val2)
 
 
+class TLSConnectionTests(unittest.TestCase):
+    # Connection to server
+    c = None
+    # Python initiated process running the server (if any)
+    p = None
+    # url of HTTP server
+    url = None
+    run_tests = True
+
+    @classmethod
+    def setUpClass(self):
+        os.system('openssl req -nodes -newkey rsa:2048 -keyout server.key -out server.csr'\
+            + ' -subj "/C=GB/ST=London/L=London/O=Acme Widgets/OU=IT Department/CN=localhost"')
+        os.system('openssl x509 -req -days 365 -in server.csr -signkey server.key -out server.crt')
+        server = os.getenv('CRYPTOL_SERVER')
+        if server is not None:
+            server = find_executable(server)
+        if server is None:
+            server = find_executable('cryptol-remote-api')
+        if server is not None:
+            self.p = subprocess.Popen(
+                [server, "http", "/", "--port", "8081", "--tls"],
+                stdout=subprocess.PIPE,
+                stdin=subprocess.DEVNULL,
+                stderr=subprocess.PIPE,
+                start_new_session=True)
+            time.sleep(5)
+            assert(self.p is not None)
+            poll_result = self.p.poll()
+            if poll_result is not None:
+                print(poll_result)
+                print(self.p.stdout.read())
+                print(self.p.stderr.read())
+            assert(poll_result is None)
+            self.url = "https://localhost:8081/"
+        else:
+            print("WARNING: TLS tests not being run because no cryptol server executable was found")
+            print("         (Note that this is expected behavior, however, for some CI tests)")
+            self.run_tests = False
+
+    @classmethod
+    def tearDownClass(self):
+        if self.p is not None:
+            os.killpg(os.getpgid(self.p.pid), signal.SIGKILL)
+        super().tearDownClass()
+
+    def test_tls_connection(self):
+        if self.run_tests:
+            c = cryptol.connect(url=self.url, verify=False)
+            c.load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
+            x_val1 = c.evaluate_expression("x").result()
+            x_val2 = c.eval("Id::id x").result()
+            self.assertEqual(x_val1, x_val2)
+
 if __name__ == "__main__":
     unittest.main()

cryptol-remote-api/python/tests/cryptol/test_low_level_ops.py

@@ -47,7 +47,7 @@ class LowLevelCryptolApiTests(unittest.TestCase):
         else:
             server = os.getenv('CRYPTOL_SERVER_URL')
             if server:
-                self.c = argo.ServerConnection(argo.HttpProcess(server))
+                self.c = argo.ServerConnection(argo.HttpProcess(server, verify=False))
             else:
                 server = find_executable('cryptol-remote-api')
                 if server:

cryptol-remote-api/test-cryptol-remote-api.py

@@ -10,8 +10,10 @@ if connType == 'socket':
     c = cryptol.connect(argo.RemoteSocketProcess(host, port=port, ipv6=False))
 elif connType == 'http':
     c = cryptol.connect(url="http://%s:%d/" % (host,port))
+elif connType == 'https':
+    c = cryptol.connect(url="https://%s:%d/" % (host,port))
 else:
-    raise Exception('specify socket or http for connection type')
+    raise Exception('specify socket, http, or https for connection type')
 
 c.load_module('Cryptol')
 assert c.evaluate_expression("1+1").result() == 2

cryptol-remote-api/test_docker.sh

@@ -2,17 +2,19 @@
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 
-TAG=${1:-cryptol-remote-api}
+PROTO=${1:-"http"}
+TAG=${2:-cryptol-remote-api}
 
 pushd $DIR
 
-rm $PWD/python/tests/cryptol/test-files/examples
-mv $PWD/../examples $PWD/python/tests/cryptol/test-files/
+rm -fr $DIR/python/tests/cryptol/test-files/examples
+cp -r $DIR/../examples $DIR/python/tests/cryptol/test-files/
 
-docker run --name=cryptol-remote-api -d \
-  -v $PWD/python/tests/cryptol/test-files:/home/cryptol/tests/cryptol/test-files \
+CONTAINER=$(docker run -d \
+  -v $DIR/python/tests/cryptol/test-files:/home/cryptol/tests/cryptol/test-files \
   -p 8080:8080 \
-  $TAG
+  $([[ "$PROTO" == "https" ]] && echo "-e TLS_ENABLE=1") \
+  $TAG)
 
 popd
 
@@ -25,7 +27,7 @@ NUM_FAILS=0
 echo "Setting up python environment for remote server clients..."
 poetry install
 
-export CRYPTOL_SERVER_URL="http://localhost:8080/"
+export CRYPTOL_SERVER_URL="$PROTO://localhost:8080/"
 poetry run python -m unittest discover tests/cryptol
 if [ $? -ne 0 ]; then
     NUM_FAILS=$(($NUM_FAILS+1))
@@ -35,7 +37,7 @@ popd
 
 echo "killing docker container"
 
-docker container kill cryptol-remote-api
+docker container kill $CONTAINER
 
 
 if [ $NUM_FAILS -eq 0 ]

deps/argo

@@ -1 +1 @@
-Subproject commit c733718138c10c70c6e690d4a2de83a7b07e6cc9
+Subproject commit 2481c42506c46be8b6562ab9dcef99fe85a54e5f