GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

[Remote API] `ValueError` Exception on `check`, then Hang #1628

Open WeeknightMVP opened 9 months ago

WeeknightMVP commented 9 months ago

Encountered this odd behavior when trying to check pkEncodeDecodeCorrect in cryptol-specs Primitive/Asymmetric/Signature/Dilithium/Final_Draft/Dilithium2.cry:

~/workspace/cryptol/cryptol-remote-api/python$ poetry shell
Spawning shell within ~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11
. ~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/bin/activate
(cryptol-py3.11) ~/workspace/cryptol/cryptol-remote-api/python$ pushd ../..
(cryptol-py3.11) ~/workspace/cryptol$ export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-remote-api)
(cryptol-py3.11) ~/workspace/cryptol$ popd
(cryptol-py3.11) ~/workspace/cryptol/cryptol-remote-api/python$ python
Python 3.11.7 (...)
>>> from os import environ
>>> from cryptol import connect
>>> HOME = environ['HOME']
>>> cryptol_specs=f"{HOME}/workspace/cryptol-specs"
>>> CRYPTOLPATH=f"{cryptol_specs}:{cryptol_specs}/Primitive/Asymmetric/Signature/Dilithium/Final_Draft"
>>> c = connect(cryptol_path=CRYPTOLPATH, reset_server=True)
>>> c.load_module("Dilithium2").result()
[]
>>> # the first `check` of "pkEncodeDecodeCorrect" throws a `ValueError`
>>> c.check("pkEncodeDecodeCorrect", num_tests=-1).result()
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/interaction.py", line 178, in result
    return self.process_result(self._result_and_state_and_out_err()[0])
                               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/interaction.py", line 155, in _result_and_state_and_out_err
    res = self.raw_result()
          ^^^^^^^^^^^^^^^^^
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/interaction.py", line 82, in raw_result
    wait_for_reply_to(self.request_id)
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/connection.py", line 487, in wait_for_reply_to
    self._process_replies()
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/connection.py", line 438, in _process_replies
    the_reply = json.loads(reply_bytes)
                ^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/lib/python3.11/json/__init__.py", line 346, in loads
    return _default_decoder.decode(s)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/lib/python3.11/json/decoder.py", line 337, in decode
    obj, end = self.raw_decode(s, idx=_w(s, 0).end())
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/lib/python3.11/json/decoder.py", line 353, in raw_decode
    obj, end = self.scan_once(s, idx)
               ^^^^^^^^^^^^^^^^^^^^^^
ValueError: Exceeds the limit (4300 digits) for integer string conversion: value has 7167 digits; use sys.set_int_max_str_digits() to increase the limit
>>> # ...and then the same `check` hangs...
>>> c.check("pkEncodeDecodeCorrect", num_tests=-1).result()
{Ctrl-C}
  C-c C-c^CTraceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "~/workspace/cryptol/cryptol-remote-api/python/cryptol/connection.py", line 316, in check
    self.most_recent_result = CryptolCheck(self, expr, num_tests, timeout)
                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/workspace/cryptol/cryptol-remote-api/python/cryptol/commands.py", line 183, in __init__
    super(CryptolCheckRaw, self).__init__(
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/interaction.py", line 62, in __init__
    self.init_state = connection.protocol_state()
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/workspace/cryptol/cryptol-remote-api/python/cryptol/connection.py", line 194, in protocol_state
    return self.most_recent_result.state()
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/interaction.py", line 146, in state
    res = self.raw_result()
          ^^^^^^^^^^^^^^^^^
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/interaction.py", line 82, in raw_result
    wait_for_reply_to(self.request_id)
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/connection.py", line 487, in wait_for_reply_to
    self._process_replies()
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/connection.py", line 436, in _process_replies
    reply_bytes = self.process.get_one_reply()
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/connection.py", line 181, in get_one_reply
    (msg, rest) = netstring.decode(self.buf)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/.cache/pypoetry/virtualenvs/cryptol-WSsLqK6b-py3.11/lib/python3.11/site-packages/argo_client/netstring.py", line 16, in decode
    def decode(netstring : bytes) -> Tuple[str, bytes]:

KeyboardInterrupt

As of Python 3.10.7, the ValueError is thrown when trying to convert a very large integer to a string, to mitigate a vulnerability. But this seems to throw off the Remote API server, which hangs on future requests (check or otherwise).