1. 5
  1. 3

    I found the code of the verifyer-in-the-middle! It’s here, in a codebase of the Ocean Observatories Initiative’s cyber infrastructure:


    It took me some work to find this, the artefact link in the paper’s References section went to a Conflunce page that is both dead and not in Wayback. Thanks be to SciHub; without them I wouldn’t have been able to access the paper with a better link.

    Side note 1: dr. Neykova and prof. Yoshida both have super interesting publication lists.

    Side note 2: there is a recent (2018) talk The Do’s and Don’ts of Error Handling, by Joe Armstrong, that also mentions MITM protocol verifyers/enforcers. (Link goes directly to that bit, it runs for about 2 minutes). His argument runs ‘protocols are contracts; contracts assign blame, which encourages both parties to fulfil the contract. What is sent on the wire is rarely observed; a contract checker in the middle lets you know which component is out of spec’. The paper “How to Verify Your Python Conversations” is an (earlier!) practical instance of such a contract checker.

    1. 1

      Further notes: this is not, in fact, a verifyer-in-the-middle, but something even cooler: local verifyers that are guaranteed to enforce global correctness.

      The authors (Rumyana Neykova did the implementing in the OOI codebase; Nobuko Yoshida is a Very Important Researcher in the field of Multi-Party Session Types, calculus, and verification):