key: cord-0045072-tsuoo7p2 authors: Bartolo Burlò, Christian; Francalanza, Adrian; Scalas, Alceste title: Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper) date: 2020-05-13 journal: Formal Techniques for Distributed Objects, Components, and Systems DOI: 10.1007/978-3-030-50086-3_13 sha: cea1b700bf1442da7d8b2582b702120dfc16b464 doc_id: 45072 cord_uid: tsuoo7p2 We present our preliminary work towards a comprehensive solution for the hybrid (static + dynamic) verification of open distributed systems, using session types. We automate a solution for binary sessions where one endpoint is statically checked, and the other endpoint is dynamically checked by a monitor acting as an intermediary between typed and untyped components. We outline our theory, and illustrate a tool that automatically synthesises type-checked session monitors, based on the Scala language and its session programming library (lchannels). Session Types [12, 13, 27] have emerged as a central formalism for the verification of concurrent and distributed programs. Session-types-based analysis ensures that a program correctly implements some predetermined communication protocol, stipulating the desired exchange of messages [4, 16] . The analysis is typically performed statically, via type checking, before the programs are deployed. However, full static analysis is not always possible (e.g., when the source code of third-party programs and components is unavailable); in such cases, session types are checked at runtime via monitors [6, 10, 17, 19] . We view these approaches as two extremes on a continuum: our aim is to develop practical hybrid (static and dynamic) verification methodologies and tools for distributed programs in open settings. In particular, our aim is to verify distributed systems where: The research was partly supported by the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant agreement No. 778233. (i) we make no assumptions on how messages are delivered between components; (ii) the components available prior-deployment are checked statically; and (iii) the components that are unavailable for checking prior-deployment are verified at runtime, by deploying autogenerated, type-checked monitors. To achieve this aim, we present a methodology with three key features, presented as contributions in this paper: F1. Open systems are prone to malicious attacks and data corruption. Thus, we describe protocols via augmented session types including runtime data assertions (reminiscent of interaction refinements [18] ), and synthesise monitors that automate such data checks. Unlike [6, 18] , our monitors are independent, type-checked processes, that can be deployed over any network. F2. We develop a tool that, given a session type S, can synthesise the Scala code of (1) a type-checked monitor that verifies at run-time whether an interaction abides by S (aim (iii)), and (2) the signatures usable to implement a process that interacts according to S, in a correct-by-construction manner (aim (ii)). F3. Our monitor synthesis can abstract over low-level communication protocols, bridging across a variety of message transports (e.g., TCP/IP, REST, etc.): this is key to facilitate the interaction with third-party (untyped) components in open systems (aim (i)); this is also unlike previous work on session monitoring (theoretical [6] or practical [19] ) that focus on a specific technology and runtime system, or assume a centralised message routing medium. A session type defines the intended behaviour of a participant that communicates with another over a channel. Our work is based on session types with assertions: Session types R, S :: We assume a set of base types B, and introduce payload identifiers V (with their types) and assertions A (i.e., predicates on payload values). Branching (or ) . A process implementing a session type S can correctly interact with a process implementing the dual type of S, denoted S-where each selection (resp. branching) of S is a branching (resp. selection), with the same choices: The type S login below describes the protocol of a server handling authorised logins. Notice that the type uses two assertion predicates: -validAuth() checks if an OAuth2-style token [20] authorises a given user; -validId() checks whether an authentication id is correct for a given user. The server waits to receive Login(uname:Str, pwd :Str, tok :Str), where tok is a token obtained by the client from an authorisation service. Once received, the values of uname and tok are passed to the predicate validAuth() which checks whether tok contains a desired cryptographically-signed authorisation for uname: if it evaluates to true, the server can either send Success including an id , or Retry. If the server chooses the former, then id and uname must be validated by validId (): if it succeeds, the message is sent and the server continues along session type R. If the server chooses to send Retry, the session loops. We now give an overview (Sect. 3.2) and an example-driven tour (Sect. 3.3) of our methodology; but first, we summarise the toolkit underlying its implementation (Sect. 3.1). lchannels [21, 24, 25] is a library implementation of session types in the Scala programming language. Its API is inspired by the continuation-passing encoding of session types into the linear π-calculus [9] . lchannels allows to implement a program that communicates according to a session type S by (1) (2) the library provides run-time linearity enforcement: e.g., if a "one-shot" channel object is used twice to send messages, then the program is not advancing along S, hence lchannels discards the message and raises an error. Srv C We now illustrate how our methodology is implemented, as a tool [7] targeting the Scala programming language. Consider the scenario on the right: a client C exchanges messages with a server Srv over a network. Srv implements the session type S login outlined in Example 1, and expects each client C to follow the dual, S login . However, in an open system, we cannot guarantee that C abides by S login . The messages sent from Srv to C (and vice versa) must pass through the monitor Mon. As Srv and Mon use lchannels to interact, they are statically typed according to S login and S login ; instead, there is no assumption on the interaction between Mon and C: it is handled by a user-supplied connection manager (CM), which acts as a translator and gatekeeper by transforming messages from the transport protocol supported by C to the Mon's CPSP classes, and vice versa. Hence, CM provides a message transport abstraction for Mon and Srv: to support new clients and message transports, only CM needs extending. When the monitor is initialised, it invokes CM to set up the communication channel with client C, through a suitable message transport: e.g., in the case of TCP/IP, CM creates a socket and initialises the I/O buffers. Each message sent from Srv to Mon via lchannels is analysed by Mon, and if it conforms to S login and its assertions, it is translated by CM and forwarded to C. Dually, each message sent from C to Mon is translated by CM and analysed by Mon, and if it conforms to S login and its assertions, it is forwarded to Srv. Mon's assertion checks provide additional verification against incorrect values from Srv or C. To illustrate our approach and implementation, we now follow the message exchanges prescribed by S login , showing how they engage with the elements of our design. Roughly, Mon acts as a state machine: it transitions by receiving and forwarding messages between Srv and CM, abiding by the type S login and its dual. CM, in turn, provides a send/receive interface to Mon, and delivers messages to/from client C. The monitor also maintains a mapping, called payloads, that associates the payload identifiers of S login to their current values. We begin with the login request sent from a client over TCP/IP. The client's message is initially handled by the connection manager CM, which provides a receive method like the one shown above: it is invoked by Mon to retrieve messages. When invoked, receive checks the socket input buffer inBuf: if a new supported message is found (line 3, where the message matches the regex loginR), the corresponding CPSP class is returned to the monitor; otherwise, the unaltered message is returned (line 4). On the left is the synthesised code for Mon that handles the beginning of S login . The monitor invokes CM's method receive (shown above) to retrieve the latest message (line 2). Depending on the type of message, the monitor will perform a series of actions. By default, a catch-all case (line 9) handles any messages violating the protocol. If Login is received, the monitor initially invokes the function validateAuth() with the values of uname and tok; i.e., the assertion predicate in S login corresponds to a Scala function (imported from a user-supplied library). If the function returns true, the message is forwarded to the server Srv (line 5), otherwise the monitor logs the violation and halts. The function used to forward the message (!!), which is part of lchannels, returns a continuation channel that is stored in cont. The value of uname is stored in a mapping (line 6) since it is used later on in S login . Finally, the monitor moves to the next state, by calling the synthesised method sendChoice1, passing cont to continue the protocol. On the left is the synthesised code of Mon that handles the server's response to the client. According to S login , the server can choose to send either Success or Retry; correspondingly, the monitor waits to receive either of the options from Srv, using the function ? from lchannels (line 2). -If the server sends Success, including the value id as specified in S login , the first case is selected (line 3). The monitor evaluates the assertion on id and uname (stored in receiveLogin above, and now retrieved from the payloads mapping): if it is satisfied, the message is sent to the client (line 5) via CM's send method (explained below), and the monitor continues according to session type R. Otherwise, the monitor logs a violation and halts (line 8). -Instead, if the server sends Retry (line 10), the message is forwarded directly to the client using the method send of the CM (see below); notice that there are no dynamic checks at this point, as there is no assertion after Retry in S login . The monitor then goes back to the previous state receiveLogin. Notably, unlike the synthesised code of receiveLogin (that handles the previous external choice), there is no catch-all case for unexpected messages from Srv. In fact, here we assume that Srv is written in Scala and lchannels, hence statically checked, and conforming to S login ; hence, it can only send one of the expected messages (as per Sect. 3.1). The monitor only checks the assertions on Srv's messages. Finally, we review the send method of CM: it translates messages from a CPSP class instance to the format accepted by the client's transport protocol. In this case, the format is a textual representation of the session type. The catch-all case (lines 4-5) is for debugging purposes. We presented our preliminary work on the hybrid verification of open distributed systems, based on session types with assertions and automatically syntehsised monitors-with a supporting tool [7] based on the Scala programming language. Future Work. Our approach adheres to the "fail-fast" design methodology: if an assertion fails, the monitor logs the violation and halts. In the practice of distributed systems, "fail-fast" is advocated as an alternative to defensive programming [8] ; it is also in line with existing literature on runtime verification [5] . Our further rationale for this design choice is that we intend to investigate monitorability properties of session types, along the lines of recent work [1, 2, 11] , and identify any limits, in terms of what can be verified at runtime. We plan to extend our approach to multiparty sessions [14, 15] , in connection to existing work [22, 23] based on lchannels and Scribble [26, 28] . Finally, we plan to investigate how to handle assertion violations by adding compensations to our session types, formalising how the protocol should proceed whenever an assertion fails. Related Work. The work in [6] formalises a theory of monitored (multiparty) session types, based on a global, centralised router providing a safe transport network that dispatches messages between participant processes. The main commonality with our work is that session types are used to synthesise monitors. The main differences (besides our focus on a tool implementation) are that (1) we do not assume a centralised message routing system, and consider the network adversarial (as per contribution F1) and use monitors to also protect typed participants; (2) our monitors can enforce data constraints, through assertions; and (3) in our setting, if a participant sends an invalid message, the monitor will flag violations (and stop computation) whereas [6] drops the invalid message, but will continue forwarding the rest, akin to runtime enforcement via suppressions [3] . Our protocol assertions are reminiscent of interaction refinements in [18] , that are also statically generated (by an F# type provider), and dynamically enforced when messages are sent/received. However, we enforce our assertions by synthesising well-typed monitoring processes that can be deployed over a network, whereas [18] injects dynamic checks in the local executable of a process. Adventures in monitorability: from branching to linear time and back again. PACMPL 3(POPL) An operational guide to monitorability On runtime enforcement via suppressions Behavioral types in programming languages Introduction to runtime verification Monitoring networks through multiparty session types FMOODS/FORTE -2013 STMonitor implementation Session types revisited Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python Monitorability for the Hennessy-Milner logic with recursion Types for dyadic interaction Language primitives and type discipline for structured communication-based programming Multiparty asynchronous session types Multiparty asynchronous session types Foundations of session types and behavioural contracts Monitors and blame assignment for higherorder session types A session type provider: Compiletime API generation of distributed protocols with refinements in f# Let it recover: multiparty protocol-induced recovery OAuth Working Group: RFC 6749: OAuth 2.0 framework A linear decomposition of multiparty sessions for safe distributed programming A linear decomposition of multiparty sessions for safe distributed programming (artifact) Lightweight session programming in scala Lightweight session programming in scala (artifact) An interaction-based language and its typing system The scribble protocol language