Raphaël Monat

Abdelraouf Ouadjaout

Antoine Miné

A Multilanguage Static Analysis of Python Programs with Native C Extensions *

Keywords: Formal Methods, Static Analysis, Abstract Interpretation, Dynamic Programming Language, Multilanguage Analysis

Modern programs are increasingly multilanguage, to benefit from each programming language's advantages and to reuse libraries. For example, developers may want to combine high-level Python code with low-level, performance-oriented C code. In fact, one in five of the 200 most downloaded Python libraries available on GitHub contains C code. Static analyzers tend to focus on a single language and may use stubs to model the behavior of foreign function calls. However, stubs are costly to implement and undermine the soundness of analyzers. In this work, we design a static analyzer by abstract interpretation that can handle Python programs calling C extensions. It analyses directly and fully automatically both the Python and the C source codes. It reports runtime errors that may happen in Python, in C, and at the interface. We implemented our analysis in a modular fashion: it reuses off-the-shelf C and Python analyses written in the same analyzer. This approach allows sharing between abstract domains of different languages. Our analyzer can tackle tests of real-world libraries a few thousand lines of C and Python long in a few minutes.

Introduction

Modern programs are increasingly multilanguage. This allows developers to combine the strengths of different languages and reuse libraries written in other languages. A host language may call a guest language through an interface; this interface is also called a boundary. The guest language is frequently C and is usually referred to as native code or native C. In this paper, the host language is Python, and the guest language is C. This work supports the Python API [START_REF] Van Rossum | the Python development team: Python/C API Reference Manual[END_REF] as the interoperability mechanism between Python and C. 1 Using native C modules in Python is frequent as it allows writing high-level Python code, itself calling efficient C code. As a matter of fact, one in five of the 200 most downloaded Python libraries available on GitHub contains C code. Although useful, multilanguage programs generate additional sources of bugs. Indeed, developers need to take into account different safety mechanisms and memory representations. Python is safe to the extent that runtime errors in pure Python programs are encapsulated into exceptions, which can be caught later on. This safety property breaks when C modules are used since a runtime error in C may irremediably terminate the program or create an inconsistent state. Python and C also have different representations. For example, Python integer objects use at least 24 bytes of memory and have unlimited precision, while C integers have fixed lengths (generally ranging from 8 to 64 bits) and can suffer from overflows.

Static analysis aims at inferring program properties (e.g., the absence of runtime errors) by analyzing programs without executing them. Static analyzers tend to focus on analyzing one language at a time. They may use stubs to model the behavior of calls to other languages. These stubs may be time-consuming to implement if written by hand. They can undermine the soundness of the analyses since the actual code is not analyzed, and the stubs may be imprecise or wrong. For example, our previous work developing a type analysis for Python [START_REF] Monat | Static type analysis by abstract interpretation of Python programs[END_REF] uses official Python type annotations (defined by PEP 484 [START_REF] Van Rossum | Python Enhancement Proposal 484[END_REF]) as stubs. While this analysis tracks uncaught Python exceptions, these type annotations do not declare which exceptions may be raised, thus adding an unchecked assumption to the soundness property [START_REF] Monat | Static type analysis by abstract interpretation of Python programs[END_REF]Section 6.2].

We aim at analyzing both the native C code and the Python code (including callbacks to Python code from the native side) within the same analyzer, called Mopsa [START_REF] Journault | Combinations of reusable abstract domains for a multilingual static analyzer[END_REF]. We perform a precise, flow, and context-sensitive value analysis by abstract interpretation. Our analyzer works by induction on the syntax and switches from one language to the other just as the concrete program execution does. We present a multilanguage static analysis built upon pre-existing value static analyses by abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] of C [START_REF] Ouadjaout | A library modeling language for the static analysis of C programs[END_REF] and Python [START_REF] Monat | Static type analysis by abstract interpretation of Python programs[END_REF][START_REF] Monat | Value and allocation sensitivity in static Python analyses[END_REF]. It detects runtime errors in the native C code (invalid pointer operations, invalid memory accesses, integer overflows), in the Python code (raised exceptions), and at the boundary between the languages. The underlying address allocation and numeric abstractions are shared. A few multilanguage static analyses exist, and focus mostly on analyzing Java and C ( [START_REF] Tan | Ilea: inter-language analysis across Java and C[END_REF][START_REF] Furr | Checking type safety of foreign function calls[END_REF][START_REF] Furr | Polymorphic type inference for the JNI[END_REF][START_REF] Furr | Checking type safety of foreign function calls[END_REF][START_REF] Wei | JN-SAF: precise and efficient NDK/JNI-aware inter-language static analysis framework for security vetting of Android applications with native code[END_REF][START_REF] Lee | Broadening horizons of multilingual static analysis: Semantic summary extraction from C code for JNI program analysis[END_REF], cf. Section 6). They compute summaries of the effects of native code on the chosen abstract property in a bottom-up fashion. Those effects are then translated into the host language, where a standard analyzer for the host language can then be used. The use of summaries to convey the abstract meaning of functions makes it easier to rely on independent analyzers for each langage. However, the language and properties we target require precise context-sensitive value analyses that are difficult to perform bottom-up. Since Python is a dynamic programming language with a flexible semantics, it is not possible to analyze programs precisely in a contextinsensitive fashion. Additionally, a precise description of the Python heap at a native call is mandatory to analyze the called C code, check for pointer errors, and infer effects. We believe the approach described in this paper is general and could be extended to other multilanguage settings, such as the analysis of Java and C through the JNI.

Contributions.

-We define a multilanguage semantics for Python programs with native C modules using the Python C API. -We show how to lift analyses of Python and C into the multilanguage setting. The underlying address allocation and numeric abstractions are shared, paving the way for relational invariants between Python and C variables. -We built an implementation on top of an existing static analysis platform called Mopsa that was previously used to design independent analyses for C and for Python. We added support for multilanguage C/Python programs by only adding domains modeling the boundary. We reuse the previous domains analyzing C and Python off-the-shelf. Thanks to this construction, we can detect runtime errors at the boundary, but also in the Python code and in the native C code. -We evaluate our approach on six real-world libraries found on GitHub. We show that we can scale to libraries of 5,800 combined lines of Python and C code within five minutes.

Artifact. An artifact [START_REF] Monat | A Multi-Language Static Analysis of Python Programs with Native C Extensions[END_REF] is available alongside this article. The artifact makes Table 2 and the claim about the percentage of Python packages containing C code on Github (made in Section 1) reproducible. The example codes displayed in Figure 1 and Figure 12 are provided in the artifact, along with instructions to run our analyzer on them. The source code of the modified version of Mopsa is also included. We plan on merging our changes into the public version of Mopsa [START_REF] Journault | MOPSA: Modular Open Platform for Static Analysis[END_REF].

Limitations. Our concrete semantics is high-level and makes the assumption that builtin Python objects are only manipulated through the API in C (this assumption is verified by our analyzer). The garbage collection based on reference counting is not supported by our semantics. Thus, we cannot detect deallocations that are performed too soon or that are not performed at all. There is no formal soundness proof that our concrete semantics effectively models the behavior of the Python interpreter. Potential runtime errors in the API implementation modeled by our concrete semantics as builtins cannot be detected. 2Our implementation supports relational analyses, but those do not scale to realworld examples (thus, we use intervals for the numeric abstraction by default). These limitations could be removed in future work.

Outline. We start by showing a self-contained motivating example in Section 2, giving insights on how native C modules are defined and how they work with Python. We define the concrete semantics of these multilanguage programs in Section 3, and explain the abstractions performed in Section 4. Section 5 presents our implementation and the analysis results. We discuss related work in Section 6 and conclude in Section 7.

An Extension Module Example

This section provides an in-depth motivating example. We show how to define a native C extension module, and how it can be used by a Python client code. We end the section by discussing which errors may happen. When developers want to run native C code in Python, they define native C extension modules using the Python API. These modules may contain attributes, methods, and classes, just as any other Python module. However, these methods and classes are now written in C. API functions are denoted by the Py prefix (and written in magenta in the listings). The semantics of some of these functions are described formally in Section 3.

Counter module, viewed from Python. Our example is a C module defining a Counter class, alongside some client code in Python. This example is selfcontained and shown in Figure 1. From a high-level point of view, the counter module defines a Counter class. Instances of Counter can be created (count.py, line 4); their internal counter can be incremented using the incr method, which takes an optional integer argument being the increment (lines 6-7); they also have a read-only attribute counter returning their current value (line 8).

Counter, viewed from C. In C, instances of Counter will be stored using the CounterO struct. This struct starts with a PyObject ob_base field. All Python objects are represented as PyObjects in C. Putting the PyObject as the first field in the Counter structure allows casting to and from Python objects. 3The PyObject definition is part of the API and shown in Figure 2. Its fields are a reference counter for the garbage collector and a pointer to the class to The Counter class' specification is defined lines 52-59. It has three methods stored in the Py_tp_new, Py_tp_init, and Py_tp_methods fields. It also defines a special attribute member counter lines 41-42. The PyTypeObject structure is synthesized from the specification by PyType_FromSpec (line 72). These methods and members are lifted to become Python attributes and methods when the class is initialized (in PyType_FromSpec). Other fields are defined in the PyTypeObject structure. tp_basicsize, tp_itemsize define the size (in bytes) of instances. tp_flags is used to perform fast instance checks for builtin classes. tp_base points to the parent of the class. tp_dict is the class' dictionary used by Python to resolve attribute accesses (created during class initialization).

Module import. When executing the import counter statement, the C function PyInit_counter is called. This function starts by creating a module whose name (line 62) is counter with no methods attached to it (line 63). Then, the CounterT class is created (lines 71-72), and the class is bound to the module (lines 73-74). Python uses a reference-counting-based garbage collector, which has to be manually handled using the Py_INCREF and Py_DECREF macros in C. If no errors have been encountered, the module object is returned at the end of the function, and counter will now point to this module in Python.

Class initialization.

The call to PyType_FromSpec creates the Counter class from its specification. The function PyType_FromSpec starts by creating the PyTypeObject and fills its fields according to the specification. This structure is then passed to PyType_Ready which populates the tp_dict field of the class. This field is the class' dictionary used by Python to resolve attribute accesses. Before this call, the attribute counter and the methods __new__, __init__, and incr do not exist on the Python side. We explain how these C functions are encapsulated into Python objects by PyType_Ready. The prototype of C functions for Python is PyCFunction (Figure 2, line 6). Some signature adaptations may be needed for specific kinds of functions. For example, initialization methods (such as CounterInit) return a C int by convention. Thus, CounterInit will be wrapped into a function called wrap_init, which behaves as a PyCFunction. It is then encapsulated into a builtin Python descriptor object. Upon a call to this object, this descriptor performs pre-and post-call checks (described in Section 3). Continuing our example, wrap_init will be stored into an instance of the builtin wrapper_descriptor object. These descriptors are then added to the class dictionary. Table 1 describes the three other fields.

Counter creation.

When a new instance of Counter is created (line 4), Python starts by allocating it by calling Counter.__new__. This call will eventually be resolved into PyType_GenericNew (from tp_new), allocating the object and 2). Its first argument is the object instance (here, the instance stored in variable c), and the second argument is a tuple of the arguments passed to the function (for the call at line 6 it is a tuple of length one containing 2**p-1, and an empty one for the second call at line 7). PyArg_ParseTuple is a helper C function from the Python API converting the Python arguments wrapped in the tuple into C values. 4It uses a format string to describe the conversion. The | character separates mandatory arguments from the optional ones, while i signals a conversion from a Python integer to a C int. Internally, the conversion is done from a Python integer to a long (which may fail with an exception since Python integers are unbounded), which is then cast to an int if size permits (otherwise, another exception is set). In the first call to CounterIncr, i will be assigned 2**p-1 if the conversion is successful. In the second call, i will keep its default value, 1.

The internal value of the counter is then incremented by i, and then Python's None value is returned.

Counter access. Thanks to the complex semantics of Python, attribute accesses can actually hide calls to custom getter and setter functions through the descriptor protocol [START_REF] Monat | Static type analysis by abstract interpretation of Python programs[END_REF]Figure 6]. In our case, PyType_Ready takes the member declaration lines 40-43, and creates those custom getters and setters through a member_descriptor builtin object. The access to attribute counter at line 8 calls the getter of this member_descriptor object. This getter accesses the count field of the CounterO struct and converts the C integer into a Python integer. The READONLY flag in the declaration ensures that any call to the setter function raises an exception. These member descriptors are supported by our analysis.

What can go wrong? Depending on the chosen value of p the result r will range from (i) the expected value (r = 2 p when 0 ≤ p ≤ 30), (ii) conversion errors raised as OverflowError exceptions (with messages depending on wheter p ≤ 62), (iii) a silent integer overflow on the C side, causing a wrap-around which is an unexpected behavior for Python developers (r = -2 31 for p = 31).

All these errors are due to different representations between the builtin values of the language. The C integer overflow does not interrupt the execution. This motivates the creation of our analysis targeting all kinds of runtime errors in both host and guest languages as well as at the boundary. Our analysis infers all reachable C and Python values, as well as raised exceptions in order to detect these runtime errors. In this example, our analyzer is able to detect all these cases. Our analyzer is also able to prove that the program is safe when p ranges between 0 and 30.

Common bugs at the boundary. We refer the reader to the work of Hu and Zhang [START_REF] Hu | The Python/C API: evolution, usage statistics, and bug patterns[END_REF] for an empirical evaluation of bugs at the boundary between Python and C. The most frequent bugs happening at the boundary are:

mismatches between a returned NULL and the exception being set in C (NULL should be returned by Python C functions if and only if an exception has been set -cf. Figure 8 in the next section), mismatches between the C and Python datatypes during conversion (in calls to PyArg_ParseTuple, PyLong_FromLong), integer overflows during conversions from arbitrary-precision Python integers to C, reference-counting errors (not supported by our analyzer).

Concrete Semantics

This section defines the semantics of the interface between Python and C. It is built upon the semantics of each language. Our goal is to delegate most of the work to the semantics of each language, each used in a black-box fashion. This delegation will also simplify our implementation as we will reuse the analyses of Python and C in a similar black-box fashion.

A key assumption of our semantics is that builtin Python objects (such as integers and dictionaries) can only be accessed from C through the API provided by the interpreter. As such, any access to the builtins through the C API can be encoded as a call back to the Python language. Thus, each language will have complementary representations of Python objects. Each language has a view of any Python object. Accesses to the other view are done by switching language. To illustrate this representation on our running example, the int count field from a Counter instance is only exposed from the C. It is possible to read the counter's value from Python. This can only be done by calling a C function performing the conversion of the C integer into a Python integer. This object is new and independent from the C integer. Hence, only C code directly dereferences the field value from the object memory. Conversely, an attribute that is dynamically added to a Python object is stored in the instance's dictionary. This dictionary is opaque from C. Accessing it through the C language using the API will ultimately be evaluated as a Python attribute access in our semantics. As illustrated in these examples, mutable parts of the objects are not directly available through both languages. There is thus no need to perform systematic state reductions when switching from one language to the other.

Our concrete semantics defines the operators working at the boundary. These operators allow switching from one language to another or converting the value of one language to the other. We define how Python may call C functions, and how C may perform callbacks to Python objects. We also define conversions between Python integers and C longs. API functions working on other builtin datatypes (such as floats, strings, lists, ...) exist and are supported by our analysis. They are similar to the integer case and are not described in this article. The definitions of these operators rely on calls to boundary functions between the two languages. These boundaries ensure that objects have the correct shape in the other language state. The boundary from C to Python also checks that only valid Python objects are passed back.

We define the state on which each semantics operates. In the following, Python-related states and expressions will be written in green. C-related states and expressions will be in orange. We reuse the states defined in the work of Monat et al. [START_REF] Monat | Static type analysis by abstract interpretation of Python programs[END_REF] for Python and Ouadjaout and Miné [START_REF] Ouadjaout | A library modeling language for the static analysis of C programs[END_REF] for C. A set of heap addresses Addr (potentially infinite) is common to the states. Previous works [START_REF] Fromherz | Static value analysis of Python programs by abstract interpretation[END_REF][START_REF] Monat | Static type analysis by abstract interpretation of Python programs[END_REF][START_REF] Ouadjaout | A library modeling language for the static analysis of C programs[END_REF] define the semantics of Python and C. Python state (Figure 3). Python objects are split into a nominal part and a structural part. The nominal part ObjN can be a builtin object such as an integer (we omit other builtins for the sake of concision), a function, a class, or an instance (defined by the address of the class from which it is instantiated). The structural part ObjS maps attribute names to their contents' addresses. A state Σ p consists of an environment and a heap. The environment E p maps variable identifiers Id p to addresses (or LocalUndef for local variables with an undefined value). The heap H p maps addresses to objects. Given a state σ p ∈ Σ p , we write as σ. p its environment and σ.η p its heap. Following Fromherz et al. [START_REF] Fromherz | Static value analysis of Python programs by abstract interpretation[END_REF], the state is additionally tagged by a flow token to handle non-local control-flow: cur represents the current flow on which all instructions that do not disrupt the control flow operate (e.g., assignments, but not raise); exn collects the states given by a raised exception. exn is indexed by the address of the exception object, so each exception will be kept separate. These continuation-tagged states are standard in abstract interpreters working by induction on the syntax to model non-local control-flow. Evaluating an expression e through E p e in a given state yields a Python value in a new state. This value may be ⊥ if the evaluation fails. We use letb v, σ = f (e) in body as syntactic sugar for let r, σ = f (e) in if r = ⊥ then body else ⊥, σ. The heap H c maps addresses to the type of allocated resource and their size. The type of allocated resource is Malloc when the standard C library malloc is used 5 . The Python allocator (called by PyType_GenericNew) will create resources of type PyAlloc, ensuring that: (i) Python objects are well constructed by the correct allocator (ii) the C code cannot access these "opaque" objects and needs to use the API.

Σ = Σp × Σc p →c : Valuep × Σ → Valuec × Σ c →p : Valuec × Σ → Valuep ⊥ × Σ E p×c exprp : Σ → Valuep ⊥ × Σ E p×c exprc : Σ → Valuec ⊥ × Σ
Combined state (Figure 5). Two new kinds of nominal objects are added to Python: CFun f for Python functions defined in C, CClass c for Python classes defined in C (where f and c denote the name of the underlying C function or class declaration). The combined state used for the multilanguage semantics is the product of the Python and C states, written Σ. Note that each state may reference addresses originally allocated by the other language (in the running example, the Python variable c points to the address of the Counter instance, which has been allocated on the C side by PyType_GenericNew). In the following, we define two boundary functions converting a Python value into a C value and conversely (written p → c and c → p ). The multilanguage semantics E p×c • is defined over Python and C expressions. It operates over the whole state Σ and its return value matches the language of the input expression. We define the semantics of some builtins working at the boundary between Python and C, which require the whole state. For expressions not working at the boundary, the multilanguage semantics defaults to the usual Python or C semantics:

E p×c expr p (σ p , σ c ) = E p expr p (σ p ), σ c E p×c expr c (σ p , σ c ) = σ p , E c expr c (σ c )
Boundary functions. Boundary functions ensure that Python objects are correctly represented in the heap of each language. The C to Python boundary also ensures that only Python objects are passed back to Python. These functions do not convert values from one language to another. This kind of conversion is handled by builtin conversion functions such as PyLong_AsLong, PyLong_FromLong for Python integer to C long conversion. These boundary functions are lazy and shallow: (i) only objects switching languages are passed through those boundaries, (ii) an object that has already been converted does not need to be converted again (i.e., when its address is already in the other language's heap).

The boundary from Python to C is described in Figure 6. The boundary is first applied recursively to the class of the object (using the type operator of Python). Then, the ob_type field of the object is initialized to point to its class. The last step performed is to update the heap: the object has been allocated by Python, and has the size of PyObject (if the object is a class, it has the size of PyTypeObject, and we call the class initializer afterward).

The converse boundary (Figure 7) starts by checking that the value is a heap allocated Python object, allocated with resource type PyAlloc. It calls itself recursively on the class of the object (using the ob_type field in C). The Python heap is updated with the converted object.

C call from Python (Figure 8). The semantics of C function calls from Python is shown in Figure 8. The function in_check enforces that e 1 should be an instance of the class to which f is bound. Otherwise, a TypeError exception is raised. C functions callable from Python can only have two arguments (cf. the type of PyCFunction, Figure 2, line 6). Thus, the Python arguments are split into the first one e 1 and the other ones, bundled in a tuple. The boundary from Python to C is applied to e 1 , and to the tuple containing the other arguments. Then, the C function is evaluated using the standard C semantics. Afterward, out_check ensures that the function returned NULL if and only if an exception has been set in the interpreter state. Otherwise, a SystemError exception is raised. Finally, the C value is passed through the boundary function.

Python call from C (Figure 9). Calls back to Python from the C code are possible using the PyObject_CallObject function. The first argument is the object being called. The second argument is a tuple containing all the parameters. These two arguments are first passed through the C to Python boundary. Then, we use the Python semantics to evaluate the call (the * operator in Python unpacks the tuple into the arguments of the variadic function). If the call is successful (i.e., the execution is normal, shown by flow token cur ), the converse boundary function is applied. If an exception has been raised during the evalu- ation of the Python call, we revert to the cur flow token and pass the exception object e through the boundary. The result of the call will be NULL, and the exception will be set on the C side by calling PyErr_SetNone.

Python exceptions in C. Python exceptions may be raised from the C code using the PyErr_SetNone builtin. In the Python interpreter, this sets a flag in a structure describing the interpreter's state. We model this by setting a global variable exc with the Python object passed as an argument. Additional functions such as PyErr_Occurred checking if an exception has been raised and PyErr_Clear removing raised exceptions are modeled by accessing and setting this same global variable.

Conversion builtins of the API. We show conversion functions from C long to Python integers and back in Figure 10. Converting a C long of value v c to a Python integer is done by calling the integer constructor in the Python semantics, and applying the boundary afterwars. To perform the other conversion, we apply the boundary function to the C value. Then, we check if the corresponding Python value v p is an integer by looking into the Python heap. If that is the case, we check that this integer fits in a C long (Python integers are unbounded). Otherwise we raise an OverflowError and the function returns -1. A TypeError exception is raised and the function returns -1 if the object is not an integer.

Thanks to the definition of builtins such as PyLong_AsLong, other builtins calling this function can be analyzed directly using their source code from the Python interpreter's implementation. For example, when PyArg_ParseTuple encounters an 'i' char in its conversion string, it executes the code shown in Figure 11. 6 As explained in our example from Section 2, it first calls PyLong_AsLong and converts the long to int checking for additional overflows. Our analyzer is able to analyze this piece of code directly. In our implementation, about half of 6 PyArg_ParseTuple is defined as stub (just as PyLong_AsLong is), but the case of integers is delegated to the interpreter's implementation shown in Figure 11.

E p×c PyLong_FromLong(vc) (σp, σc) = p →c (Ep int(vc) (σp), σc) E p×c PyLong_AsLong(vc) (σp, σc) = let vp, σp, σc = c →p(vc, σp, σc) in if σ.ηp = int(i) then if i ∈ [-2 63 , 2 63 -1] then i, σp, σc else -1, σp, Sc PyErr_SetNone(PyExc_OverflowError) σc else -1, σp, Sc PyErr_SetNone(PyExc_TypeError) σc

Threats to validity. Our goal is to analyze Python programs with native C

modules and detect all runtime errors that may happen. Assuming that those C modules use Python's API rather than directly modify the internal representation of builtins seems reasonable when analyzing third-party modules. This is the recommended approach for developers, as it eases maintenance of the codebase since API changes are not frequent and documented. Our analysis is able to detect if a program does not use the Python API and tries to modify a builtin Python object directly. This concrete semantics is already high-level. A lower-level semantics where implementation details of builtins are exposed would be much more complex. It would not benefit our analysis, which aims at detecting runtime errors in the user's codebase. We have established this semantics by reading the code of the reference Python interpreter. Proving that our semantics is a sound abstraction of such lower-level semantics is left as future work.

Abstract Semantics

Concrete states use numeric values in different places (e.g, the C state has machine numbers, pointer offsets and resource sizes). All these values will be centralized in a common numeric domain in the abstract state. This centralization allows expressing invariants between all those numeric variables, possibly improving the precision. We show a generic construction of the abstract multilanguage state. We assume the abstract semantics of Python and C are provided through E # p • , E # c • . These can be instantiated practice using previous works [START_REF] Ouadjaout | A library modeling language for the static analysis of C programs[END_REF][START_REF] Monat | Value and allocation sensitivity in static Python analyses[END_REF]. We assume that each language's abstract state relies on an address allocation abstraction (such as the callsite abstraction or the recency abstraction [START_REF] Balakrishnan | Recency-abstraction for heap-allocated storage[END_REF]) and a numeric abstraction (such as intervals, octagons, …). We write Σ u the cartesian product of these two abstractions. The abstract Python (resp. C) state can then be decomposed as a product

Σ p = Σ p × Σ u (resp. Σ c = Σ c × Σ u ).
The multilanguage abstract state consists in the cartesian product of the Python and C abstract states, where the address allocation and numeric states are shared:

Σ p×c = Σ p × Σ c × Σ u .
Just as the concrete semantics builds upon the underlying C and Python semantics, so does our abstract semantics. The abstract semantics of the boundary operators is structurally similar to the concrete ones (each concrete operator is replaced with its abstract counterpart). We show this transformation on the abstract semantics of PyLong_FromLong (to be compared with Figure 10).

E # p×c PyLong_FromLong(v c ) (σ p , σ c ) = p → c E # p int(v c ) (σ p ), σ c
Sharing the address allocation and numeric abstractions allows expressing relational invariants between the languages. In the example in Figure 12, a nonrelational analysis would be able to infer that 0 ≤ i ≤ 99, but it cannot infer that the number of calls to incr is finite. It would thus infer that -2 31 ≤ r < 2 31 , report an overflow error and be unable to prove the assertion at the end. Note that the value of r originates from the C value of the count field in the instance defined in c. With a relational analysis where C and Python variables are shared in the numeric domains, it is possible to infer that num(@ int ) + 1 = num( @ Counter , 16, s32 ). num(@ int ) is the numeric value of the integer bound to i. num( @ Counter , 16, s32 ) is the numeric value of the Counter instance (i.e., the value of count in the Counter struct, here represented as the cell [START_REF] Miné | Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics[END_REF] referenced by the Counter instance, at offset 16 being a 32-bit integer). Our analyzer is able to prove that the assertion holds using the octagon abstract domain [START_REF] Miné | The octagon abstract domain[END_REF].

Soundness. Assuming the underlying abstract semantics of Python and C are sound, the only cases left in the soundness proof are those of the operators working at the boundary. Since the abstract semantics of those operators is in point-to-point correspondence with the concrete semantics, the soundness proof is straightforward.

Experimental Evaluation

Implementation. We have implemented our multilanguage analysis within the open-source, publicly-available static analysis framework called Mopsa [START_REF] Journault | Combinations of reusable abstract domains for a multilingual static analyzer[END_REF][START_REF] Journault | MOPSA: Modular Open Platform for Static Analysis[END_REF]. A specific feature of Mopsa is to provide loosely-coupled abstract domains that the user combines through a configuration file to define the analysis. We were able to reuse off-the-shelf value analyses of C programs [START_REF] Ouadjaout | A library modeling language for the static analysis of C programs[END_REF] and Python programs [START_REF] Monat | Value and allocation sensitivity in static Python analyses[END_REF] already implemented into Mopsa. The only modification needed was to add a multilanguage domain, implementing the semantics of the operators at the boundary, just as our semantics (both concrete and abstract) do.

The configuration for the multilanguage analysis is shown in Figure 13. A configuration is a directed acyclic graph, where nodes are either domains or domain combinators. Domains can have their own local abstract state. The global abstract state is the product of these local states. Domains can also be iterators over language constructions. Each analyzed expression (or statement) flows from the top domain of the configuration to the bottom until one domain handles it. The multilanguage domain is at the top. It dispatches statements not operating at the boundary to the underlying Python or C analysis. The Python and C analyses are in a cartesian product, ensuring that when a statement goes through them, it will be handled by only one of the two sub-configurations. An example of stateful domain is "C.pointers", which keeps points-to information. "Py.exceptions" is an example of iterator domain. It handles the raise and try operators of Python. Both Python and C analyses share an underlying "universal" analysis, to which they can delegate some statements. This "universal" part provides iterators for intra-and inter-procedural statements, as well as the address allocation and numeric abstractions. The numeric abstraction displayed here only uses intervals, but it can be changed to a reduced product between a relational domain and intervals, for example.

This multilanguage domain consists in 2,500 lines of OCaml code (measured using the cloc tool), implementing 64 builtin functions such as the ones presented in the concrete semantics. This is small compared to the 11,700 lines of OCaml for the C analysis and 12,600 lines of OCaml for the Python analysis. These domains rely on "universal" domains representing 5,600 lines of OCaml and a common framework of 13,200 lines of OCaml. We also reuse the C implementation of 60 CPython functions as-is.

Corpus selection. In order to perform our experimental evaluation, we selected six popular Python libraries from GitHub (having in average 412 stars). These libraries are written in C and Python and do not have external dependencies. The noise library [START_REF] Duncan | Native-code and shader implementations of perlin noise for Python[END_REF] aims at generating Perlin noise. Libraries compared to the total number of runtime error checks, the latter being also displayed in parentheses -performed by the analyzer for C (resp. Python). The selectivity is computed by Mopsa during the analysis. The C analysis checks for runtime errors including integer overflows, divisions by zero, invalid memory accesses and invalid pointer operations. The Python analysis checks also for runtime errors, which include the AttributeError, TypeError, ValueError exceptions. Runtime errors happening at the boundary are considered as Python errors since they will be raised as Python SystemError exceptions. The second to last column shows the number of functional properties (expressed as assertions) defined by the tests that our analyzer is able to prove correct automatically. The last column shows the number of transitions between the analyzed Python code and the C code, averaged per test.

We observe that Mopsa is able to analyze these libraries in a few minutes with high selectivity for the detection of Python and C runtime errors. Our analysis is able to detect some bugs that were previously known. For example, the ahocorasick module forgets to initialize some of its iterator classes, and some functions of the bitarray module do not set an exception when they return an erroneous flag, raising a SystemError exception. We have not manually checked if unknown bugs were detected by our analysis. We have instrumented Mopsa to display the number of crossings (from Python to C, or C to Python). The average number of crossings per test is shown in the last column of Table 2. The minimal number of crossings is one per test. Thus these tests seem correct to benchmark our approach since they all alternate calls to native C code and Python code.

The multilanguage analysis is limited by the current precision level of the underlying C and Python analyses but would naturally benefit immediately from any improvements in these. However, we focused on the multilanguage domains only in this study. We leave as future work the improvements required independently on the C and Python analyses for our benchmarks. We now describe a few areas where the analysis could benefit from improvements. Mopsa is unable to support some tests for now, either because they use unsupported Python libraries or because the C analysis is too imprecise to resolve some pointers. The unsupported tests of the ahocorasick analysis are due to imprecisions in the C analysis, which is not able to handle a complex trie data structure being stored in a dynamic array and reallocated over and over again. In llist, some tests use the getrefcount method of the sys which is unsupported (and related to CPython's reference-based garbage collector, which we do not support). In addition, some tests make pure-Python classes inherit from C classes: this is currently not supported in our implementation, but it is an implementation detail that will be fixed. For the bitarray tests, tests are unsupported because they use the unsupported pickle module performing object serialization, or they use the unsupported sys.getsizeof method, or they perform some unsupported input-output operations in Python. In addition, the C analysis is too imprecise to resolve some pointers in 18 tests.

The selectivity is lower in the C analysis of levenshtein, where dynamic arrays of structures are accessed in loops: the first access at tab[i].x may raise an alarm and continue the analysis assuming that i is now a valid index access. However, subsequent accesses to tab[i].y, tab[i].z will also raise alarms as the non-relational numeric domain is unable to express that i is a valid index access. Proving the functional properties is more challenging, and not the main goal of our analysis, which aims detecting runtime errors. For example, the assertions of the noise library check that the result of complex, iterative non-linear arithmetic lies in the interval [-1, 1]. Some assertions in the llist or bitarray library aim at checking that converting their custom container class to a list preserves the elements. Due to the smashing abstraction [START_REF] Blanchet | Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software[END_REF] of the Python lists, we cannot prove these assertions.

Related Work

Native code analysis. Some works focus on analyzing native C code in the context of language interoperability, without analyzing the host language. Tan and Croft [START_REF] Tan | An empirical security study of the native code in the JDK[END_REF] perform an empirical study of native code use in Java and provide a classification by bug patterns; a similar study has been performed by Hu and Zhang [START_REF] Hu | The Python/C API: evolution, usage statistics, and bug patterns[END_REF] for the Python/C API. Kondoh and Onodera [START_REF] Kondoh | Finding bugs in Java native interface programs[END_REF] check that native calls to Java methods should handle raised exceptions using a typestate analysis. Li and Tan [START_REF] Li | Finding bugs in exceptional situations of JNI programs[END_REF] ensure that the native control-flow is correctly interrupted when a Java exception is raised. The work of Li and Tan [START_REF] Li | JET: exception checking in the Java native interface[END_REF][START_REF] Li | Exception analysis in the Java Native Interface[END_REF] infers which Java exceptions may be raised by JNI code, allowing the exception type-safety property of Java programs to be extended to the JNI. CpyChecker [START_REF] Malcolm | A static analysis tool for CPython extension code[END_REF] is a GCC plugin searching for common erroneous patterns in C code using the CPython API. Two works [START_REF] Li | Finding reference-counting errors in Python/C programs with affine analysis[END_REF][START_REF] Mao | RID: finding reference count bugs with inconsistent path pair checking[END_REF] aim at detecting reference counting errors in C code using the CPython API. Brown et al. [START_REF] Brown | Finding and preventing bugs in JavaScript bindings[END_REF] define specialized analyses for specific patterns of C++ interoperability that may jeopardize type or memory safety of JavaScript. Contrary to these works, we analyze both host and guest languages. [START_REF] Matthews | Operational semantics for multi-language programs[END_REF] defines the first semantics of multilanguage systems, using the notion of boundaries to model conversion between languages. Buro and Mastroeni [START_REF] Buro | On the multi-language construction[END_REF] generalize this construction using an algebraic framework. We use a similar notion of boundary in our concrete semantics.

Multilanguage semantics. The seminal work of Matthews and Findler

Multilanguage analyses. Buro et al. [START_REF] Buro | On multi-language abstraction -towards a static analysis of multi-language programs[END_REF] define a theory based on abstract interpretation to combine analyses of different languages, and show how to lift the soundness property to the multilanguage setting. They provide an example of multilanguage setting where they combine a toy imperative language with a bit-level arithmetic language. The notion of boundary functions used in their work performs a full translation from the state of one language to the other. Our semantics works on the product of the states, although it can be seen as an abstraction of the semantics of C and Python, where the boundary performs a full state conversion (but the boundary from Python to C would be a concretization). From an implementation standpoint, our approach avoids costly state conversions at the boundary and allows sharing some abstract domains.

Chipounov et al. [START_REF] Chipounov | S2E: a platform for in-vivo multi-path analysis of software systems[END_REF] perform symbolic execution of binaries, thus avoiding language considerations. Their approach is extended by the work of Bucur et al. [START_REF] Bucur | Prototyping symbolic execution engines for interpreted languages[END_REF], which supports any interpreted language by performing symbolic execution over the interpreter. Our approach is more costly to implement since we do not automatically lift the interpreter's code to obtain our analyzer. Thanks to its higher-level, we think our approach should be more precise and efficient.

The next works perform multilanguage analyses by translating specific effects of what native functions do (they usually generate a summary using a bottomup analysis) to the host language. This allows removing the native code and use existing analyses of the host language. Tan and Morrisett [START_REF] Tan | Ilea: inter-language analysis across Java and C[END_REF] compile C code into an extended JVML syntax form, allowing the use of the bug-finding tool Jlint afterwards. Furr and Foster [START_REF] Furr | Checking type safety of foreign function calls[END_REF][START_REF] Furr | Polymorphic type inference for the JNI[END_REF][START_REF] Furr | Checking type safety of foreign function calls[END_REF] perform inference of OCaml and Java types in C FFI code, which they crosscheck with the types used in the client OCaml/Java code. They assume there are no out-of-bounds accesses and no type casting in the C code. An inter-language, bottom-up taint analysis for Java and native binary code in the setting of Android applications is proposed by Wei et al. [START_REF] Wei | JN-SAF: precise and efficient NDK/JNI-aware inter-language static analysis framework for security vetting of Android applications with native code[END_REF]. Lee et al. [START_REF] Lee | Broadening horizons of multilingual static analysis: Semantic summary extraction from C code for JNI program analysis[END_REF] aim at detecting wrong forein function calls and mishandling of Java exceptions in Java/JNI code. They extract summaries of the Java callbacks and field accesses from the JNI code using Infer, transform these summaries into Java code, and call the FlowDroid analyzer on the whole. Contrary to these works, our analyzer supports both languages, and it switches between languages just as the real code does. The properties we target require precise context-sensitive value analyses that are diffcult to perform bottom-up.

Library analyses. Previous work aim at analyzing libraries with no access to their client code [START_REF] Allen | Combining type-analysis with pointsto analysis for analyzing Java library source-code[END_REF][START_REF] Rinetzky | Modular shape analysis for dynamically encapsulated programs[END_REF] using a "most-general client". The work of Kristensen and Møller [START_REF] Kristensen | Reasonably-most-general clients for JavaScript library analysis[END_REF] refines the notion of most-general client in the setting of dynamic programming languages. However, it focuses on libraries where functions are typed. Python libraries are not explicitly typed. Extending their work to our untyped, multilanguage setting is left as future work.

Conclusion

This article presents a multilanguage analysis able to infer runtime errors in Python code using native C extensions. Our analyzer is able to reuse value analyses of Python and C off-the-shelf. It shares the address allocation and numeric abstractions between the Python and C abstract domains. We are able to analyze within a few minutes real-world Python libraries written in C and having up to 5,800 lines of code. To the best of our knowledge, we have implemented the first static analyzer able to soundly detect runtime errors in multilanguage programs.

Future work includes extending our implementation to analyze the standard Python library and large Python applications. This will require handling more dependencies, having a relational analysis that scales, and addressing the precision limitations of the underlying C and Python analyses. We plan to instrument our implementation to verify (or infer) type annotations of the standard library provided in the typeshed [START_REF]Typeshed[END_REF] project. It would also be interesting to target multilanguage-specific safety properties (such as correct garbage collection counts). Another future work is to try our approach in other multilanguage settings (such as Java/C).

==Fig. 3 .=Fig. 4 .

 34 Fig. 3. Concrete Python State

Fig. 5 .

 5 Fig. 5. Combined State

p

  →c(vp, σp, σc) = if vp ∈ σ.ηc then (vp, 0), σp, σc else letb typ, σp = Ep type(vp) σp in letb (tyc, 0), σp, σc = p →c(typ, σp, σc) in let σc = Sc vp->ob_type = tyc σc in let σp, σc = if σp(vp) = Class(c) then let σc = σ. c, σ.ηc[vp → PyAlloc, sizeof(PyTypeObject)] in E p×c PyType_Ready(vp) (σp, σc) else σp, (σ. c, σ.ηc[vp → PyAlloc, sizeof(PyObject)]) in (vp, 0), σp, σc

Fig. 6 .

 6 Fig. 6. Python to C value boundary

Fig. 7 .Fig. 8 .Fig. 9 .

 789 Fig. 7. C to Python value boundary

Fig. 10 . 5 PyErr_SetString(PyExc_OverflowError, 6 " 8 } 11 PyErr_SetString(PyExc_OverflowError, 12 "Fig. 11 .

 10568111211 Fig. 10. Conversion from Python builtin integers to C long 1 long ival = PyLong_AsLong(obj); 2 if(ival == -1 && PyErr_Occurred()) { 3 return 0; 4 } else if (ival > INT_MAX) { 5 PyErr_SetString(PyExc_OverflowError,

Fig. 12 .

 12 Fig. 12. Example code where relationality between C and Python improves precision

*self, PyObject *args) 19 { 20 int i = 1; 21 if(!PyArg_ParseTuple(args, "|i", &i)) 22 return NULL; 23 self->count += i; 24 Py_RETURN_NONE; 25 } 26 27 static int 28 CounterInit(CounterO *self, PyObject *args, 29 PyObject *kwds) 30 { 31 self->count = 0; 32 return 0; 33 } 34 35 static PyMethodDef CounterMethods[] = { 36 {"incr", (PyCFunction) CounterIncr,

		count.py		counter.c
	1	import counter	40 static PyMemberDef CounterMembers[] = {
	2	import random	41	{"counter", T_INT, offsetof(CounterO,
	3		42	count), READONLY, ""},
	4	c = counter.Counter()
	5	p = random.randrange(128)
	6	c.incr(2**p-1)
	7	c.incr()
	8	r = c.counter
		counter.c
	9 #include <Python.h>
	10 #include "structmember.h"
	11
	12 typedef struct {
	13	PyObject ob_base;
	14	int count;
	15 } CounterO;
	16
	17 static PyObject*
	18 CounterIncr(CounterO 37 METH_VARARGS, ""}, {NULL}
	38 };

{NULL} 43 }; 44 45 static PyType_Slot CounterTSlots[] = { 46 {Py_tp_new, PyType_GenericNew}, 47 {Py_tp_init, CounterInit}, 48 {Py_tp_methods, CounterMethods}, 49 {Py_tp_members, CounterMembers}, {0, 0} 50 }; 51 52 static PyType_Spec CounterTSpec = { 53 .name = "counter.Counter", 54 .basicsize = sizeof(CounterO), 55 .itemsize = 0, 56 .flags = Py_TPFLAGS_DEFAULT 57 | Py_TPFLAGS_BASETYPE, 58 .slots = CounterTSlots 59 }; 60 61 static struct PyModuleDef countermod = { 62 PyModuleDef_HEAD_INIT, .m_name = "counter", 63 .m_methods = NULL, .m_size = -1 64 };

	65
	66 PyMODINIT_FUNC
	67 PyInit_counter(void)
	68 {
	69	PyObject *m = PyModule_Create(&countermod);
	70	if(m == NULL) return NULL;
	71	PyObject* CounterT =
	72	PyType_FromSpec(&CounterTSpec);

73 if(CounterT == NULL || PyModule_AddObject(

	74	m, "Counter", CounterT) < 0) {
	75	Py_DECREF(m);
	76	return NULL;
	77	}
	78	return m;
	79 }

Fig. 1. Example of a Python client program alongside a C counter module 1 typedef struct PyObject { 2 Py_ssize_t ob_refcnt; 3 struct PyTypeObject *ob_type; 4 } PyObject; 5 6 typedef PyObject *(*PyCFunction) 7 (PyObject *, PyObject *); 8 typedef int (*initproc) 9 (PyObject *, PyObject *, PyObject *); 10 11 typedef struct PyMethodDef { 12 const char *ml_name; PyCFunction ml_meth; 13 int ml_flags; const char *ml_doc; 14 } PyMethodDef; 15 16 typedef struct PyMemberDef { 17 const char *name; int type; 18 Py_ssize_t offset; int flags; 19 const char *doc; 20 } PyMemberDef; 21 22 typedef struct PyTypeObject { 23 PyObject ob_base; 24 const char *tp_name; 25 Py_ssize_t tp_basicsize; 26 Py_ssize_t tp_itemsize; 27 unsigned long tp_flags; 28 struct PyMethodDef *tp_methods; 29 struct PyMemberDef *tp_members; 30 struct PyTypeObject *tp_base; 31 PyObject *tp_dict;

  PyTypeObject is Python's type object, from which all classes derive. The second field of CounterO is the instance's data: an integer count, not directly exposed to Python.

	which it belongs.
	32	initproc tp_init;
	33	newfunc tp_new;
	34 } PyTypeObject;
	Fig. 2. Extract of Python's API header files

Table 1 .

 1 Python Counter structure summary initializing the necessary fields (such as ob_refcnt and ob_type of PyObject). Then, Counter.__init__ is called and the C function CounterInit ends up being called. It initializes the count field of the CounterO struct to 0.

	Attribute Encapsulating Object Underlying Wrapper Underlying C definition
	__new__ builtin_function	tp_new_wrapper	PyType_GenericNew
	__init__ wrapper_descriptor wrap_init	CounterInit
	incr	method_descriptor ∅	CounterIncr
	counter member_descriptor ∅	CounterMembers[0]

Counter increment. When the incr function is called, it is resolved through Python's attribute accesses into CounterIncr. CounterIncr uses the standard Python function prototype, corresponding to PyCFunction (Figure

Table 2 .

 2 Analysis results of libraries using their unit tests

	Library	|C| |Py| Tests	CLOCK	Check-Cic	Check-Cip	Assert. Py C
	noise	722 675 15 /15 19s 99.6% (4952) 100.0% (1738)	0 /21	6.6
	ahocorasick 3541 1336 46 /92 59s 93.1% (1785) 98.0% (4937)	30 /88	5.4
	levenshtein 5441 357 17 /17 1.6m 79.9% (3106) 93.2% (1719)	0 /38	2.7
	cdistance	1433 912 28 /28 1.9m 95.3% (1832) 98.3% (11884) 88 /207	8.6
	llist	2829 1686 167 /194 4.3m 99.0% (5311) 98.8% (30944) 235 /691	51.7
	bitarray	3244 2597 159 /216 4.6m 96.3% (4496) 94.6% (21070) 97 /374	14.9

Other interoperability mechanisms such as the ctypes from the standard library, the cffi library, the cython project, or the swig project all use code using this API or generate code targetting this API. We could thus analyze this generated code.

However, half of the API supported by our implementation uses the original C implementation, which is analyzed and where runtime errors would be detected.

According to the ISO C reference, "a pointer to a structure object, suitably converted, points to its initial member, and vice versa".

Py_BuildValue is the converse function translating C values to Python ones.

Other resources (such as file descriptors) can also be defined[START_REF] Ouadjaout | A library modeling language for the static analysis of C programs[END_REF].

* This work is partially supported by the European Research Council under Consolidator Grant Agreement 681393 -MOPSA.

levenshtein, ahocorasick, cdistance [START_REF] Haapala | Levenshtein Python C extension module[END_REF][START_REF] Muła | Pyahocorasick library[END_REF][START_REF] Meyer | Distance library[END_REF] implement various stringrelated algorithms. llist [START_REF] Jakubek | Linked lists for CPython[END_REF] defines linked-list objects (both single and double ones). bitarray [START_REF] Schnell | Bitarray library[END_REF] provides an implementation for efficient arrays of bits. Our analysis is context-sensitive in order to perform a precise value analysis. Thus, we needed some client code to analyze those libraries. We decided to analyze the tests defined by those libraries: they should cover most usecases of the library, and ensure that the transition between Python and C are frequent, which is ideal to stress-test our analysis. Some libraries (noise, bitarray, and llist) come with example programs with less than 50 lines of code that we analyze within 15 seconds. We have not been able to find applications with a well-defined entry point using those libraries (or they had big dependencies such as numpy). Our experimental evaluation thus focuses on the analysis of the libraries' tests.

Analysis results. We show the results of our analysis in


Patrick Eugster
email: peugster@cs.purdue.edu

Pascal Felber
email: pascal.felber@unine.ch

Fabrice Le Fessant
email: fabrice.lefessant@inria.fr

The "Art" of Programming Gossip-based Systems *

) what kind of applications would in the end be built on top of such protocols. We address the first question by arguing that gossip-based protocols are all built following one and the same pattern, and describing three building blocks which we claim are used to support this recurrent pattern-most notably a source of randomness. We validate these claims by devising simplified versions of well-known protocols, in a layered fashion, on top of a conceptual interface describing these basic services. The second question is addressed by arguing that gossip-based protocols exhibit some probabilistic or imperfect flavor (e.g., probabilistic or partial completion), and by proposing to take such probabilistic behavior into account when devising interfaces for applications building on top of gossip-based protocols. We argue for inherent support for these probabilities in the programming model.

INTRODUCTION

Although gossip-based (or epidemics-style) approaches have been already employed in many early distributed algorithms, it is recently through the advent of large-scale and peer-topeer systems that gossip-based programming has become popular.

An emblematic example of the use of gossip-based algorithms is the robust and scalable propagation of information in distributed systems [START_REF] Birman | Bimodal Multicast[END_REF]. A process that wishes to disseminate a new piece of information to the system does not send it to a server, or a cluster of servers, in charge of forwarding it, but rather to a set of other peer processes, chosen at random. In turn, each of these processes does * While the authors claim that gossip-based programming may be equated to an "art", they by no means pretend mastery of that art. the same, and also forwards the information to randomly selected processes, and so forth.

The principle underlying this information dissemination technique mimics the spread of a rumour among humans via gossiping or the spread of infectious diseases as epidemics; hence the names gossip-based and epidemic dissemination algorithms.

Once started, epidemics are hard to eradicate: a few people infected by a contagious disease are able to spread it, directly or indirectly, to a large population. Epidemics are resilient to failures in the infection process. That is, even if many infected people die before being able to transmit the disease, or are immunised, the epidemic is still reliably propagated over populations.

Gossip-based dissemination algorithms are simple and easy to deploy. In addition to their attractive scalability promises, they exhibit a very stable behaviour even in the presence of a high rate of link and/or process failures. There is no single point of failure and the reliability degrades gracefully with the number of failures. A large amount of research has been devoted to observing, analysing, and devising mathematical theories for epidemics. This are at the disposition of designers of gossip-based algorithms Applying the epidemic idea to disseminate information among a large number of processes with a dynamic connection topology is thus very appealing [START_REF] Karp | Randomized Rumor Spreading[END_REF]. Not surprisingly, the use of gossip-based algorithms has been explored in various other potentially large-scale applications such as database replication [START_REF] Demers | Epidemic Algorithms for Replicated Database Maintenance[END_REF], failure detection [START_REF] Van Renesse | A Gossip-Style Failure Detection Service[END_REF], data aggregation [START_REF] Gupta | Scalable Fault-Tolerant Aggregation in Large Process Groups[END_REF], resource discovery and monitoring [START_REF] Van Renesse | Astrolabe: A Robust and Scalable Technology for Distributed System Monitoring, Management, and Data Mining[END_REF], or publish/subscribe [START_REF] Costa | Epidemic Algorithms for Reliable Content-Based Publish-Subscribe: An Evaluation[END_REF].

But how does one best go about building actual gossip-based protocols? Trying to answer this question has brought us to address two preliminary questions, namely [START_REF] Ancona | A Core Calculus for Java Exceptions[END_REF] what the intrinsics of such systems or protocols are, and ( 2) what kind of applications would in the end be built on top of such protocols. We attempt to provide answers to these questions in the following, before proposing corresponding support for gossip-based programming and outlining first steps that could be used for corresponding research agendas.

DEVELOPING GOSSIP-BASED PROTOCOLS

In order to propose better support for gossip-based protocols, we first present a characterization of these protocols, based (1) on a recurrent pattern underlying these protocols, and (2) on basic services they require.

A recurrent pattern of gossip-based interaction

Based on our observation of existing gossip-based protocols found in the literature and deployed, we conjecture that all gossip-based protocols follow the same general interaction pattern. Locally, an application performs the following steps:

Upon the reception of an event (which can be a message or the expiration of a timer), the process can:

1. query and/or modify its local neighborhood, 2. modify the event and/or generate a new event, and 3. select the neighbor(s) to send the event to.

One can argue that this pattern is generic enough to describe the behavior of any distributed protocol, gossip-based or not, or that, inversely, any distributed protocol can be refactored to abide to this pattern. We believe that the intrinsics of gossip-based protocols are manifest in the above pattern in that, at least at this point, the local neighborhood is neither assumed nor necessarily intended to be "complete", not even eventually. In addition, many gossip-based protocols are characterized by their non-determinism (notably in neighbors selection when communication) and, often, by their periodic operation.

Core services for gossip-based protocols

The crucial distinction to other distributed protocols crystalizes in combination with the following three building blocks, which we claim to be underlying any gossip-based protocol:

(a) a source of randomness, (b) a set of neighboring processes, and (c) communication channels to these neighbors.

So far, the model is intentionally generic, in order to accommodate different protocols and underlying services and infrastructures with varying semantics. For instance, the precise semantics of communication channels are not detailed at this point, as they may vary according to the underlying network etc. The most salient of these three building blocks is the source of randomness. While not all protocols that are referred to in the literature as gossip-based ones do indeed make explicit use of randomization, there are definitely many typical examples of gossip-based protocols which do involve explicit randomization. As a matter of fact, randomness is key to the robustness and scalability of many gossip-based protocols (e.g., [START_REF] Birman | Bimodal Multicast[END_REF][START_REF] Gupta | Efficient Epidemic-Style Protocols for Reliable and Scalable Multicast[END_REF]). Non-determinism may also "emerge" as a consequence of the impossibility of tracking all actions and reactions of a large set of nodes. In contrast to many deterministic protocols, gossip-based ones do not attempt to bring perfect order and structure into the system, not even evetually.

An API for gossip-based protocols

We have validated this model by defining a minimal Application Programming Interface (API) for these building blocks and implementing higher level services in a layered manner. We have also implemented several gossip-based protocols, notably: automatic neighbour management, gossipbased broadcast following the Renyi-Erdös graph model [START_REF] Erdös | On the evolution of random graphs[END_REF][START_REF] Kermarrec | Probabilistic Reliable Dissemination in Large-Scale Systems[END_REF], random walk [START_REF] King | Choosing a Random Peer[END_REF], Gnutella search protocol [START_REF] Gnutella | [END_REF], and CY-CLON [START_REF] Voulgaris | Cyclon: Inexpensive membership management for unstructured P2P overlays[END_REF].

All our examples are presented as informal pseudo-code with various simplifications to clarify the presentation. Actual implementations are likely to be more involved. Yet, the general principle will remain unchanged.

Remove neighbor

The second part of the API deals with peer neighborhood. The neighborhood of a peer p is a list of other peers with whom p is interested to work. It can be seen as a weak version of a group-membership system, where the local view only contains a subset of the system's processes. To simplify presentation, we assume that we can ask for a random subset of a peer's neighbors by calling getNeighbors with an integer parameter specifying the size of the expected subset. The final part of the API deals of course with communications. A peer can send (non-atomically) a message to a set of peers, receive a message from another peer, and call a function after a given delay. All these operations are obviously non-deterministic, as no guarantee is given on the reliability of communication channels nor timers.

Illustration

We now convey our claims by illustrating how our minial API can be used to construct well-known gossip-based protocols. Note that the examples shown below have been chosen to be representative of different types of gossip-based protocols that use various services provided by the underlying API, but they do not exhaustively cover the full spectrum of gossip-based protocols.

Figure 1 provides an overview of the illustrated building blocks, and how they can (the top-most components need not be built on top of the third layer) be layered on top of each other. The first protocol that we consider implements automatic neighbor management by replacing failed neighbors (see Algorithm 4). We use timers to periodically send heartbeat messages to our neighbors. When we detect that a neighbor failed to send a heartbeat, we replace that neighbor by another one discovered using a random walk (to be described shortly). This protocol would typically be used in unstructured overlays to maintain a constant number of neighbors per node.

22:

until n ∈ GetNeighbors()

23:

addNeighbor(n)

24: end function

Our second example is a gossip-based broadcast that follows the Renyi-Erdös graph model [START_REF] Erdös | On the evolution of random graphs[END_REF][START_REF] Kermarrec | Probabilistic Reliable Dissemination in Large-Scale Systems[END_REF], in which each peer that receives a message for the first time forwards it to a number of neighbors logarithmic in the network size (see Algorithm 5). Note that there exist several approaches for estimating the size of a dynamic network (e.g., [START_REF] Horowitz | Estimating network size from local information[END_REF][START_REF] Kostoulas | Decentralized schemes for size estimation in large and dynamic groups[END_REF][START_REF] Merrer | Peer to peer size estimation in large and dynamic networks: A comparative study[END_REF]).

Algorithm 6 illustrates a random walk with a bounded distance. A counter in the message is decreased at each hop before the message is forwarded to a random neighbor. When the counter becomes null, i.e., the walk ends, the originator receives a notification from the final peer and replaces a random neighbor by the peer discovered by the random walk. Such a protocoal can be used to continuously reshuffle the network. send(RENYI-ERDOS, msg) to GetNeighbors(log(N ))

7:

Received ← Received ∪ {msg} 8:

end if

9: end function

A simplified version of the Gnutella protocol [START_REF] Gnutella | [END_REF] is shown in Algorithm 7. A search is initiated by flooding a region of the network (using a degree and a diameter of 7). A peer that receives the query for the first time searches its local database and returns local matches, if any, to the neighbor that sent the query. Hence, replies follow the reverse path of queries.

The originator of the search collects and prints replies. This example illustrates how exceedingly gossip-based protocols can provide powerful and sophisticated funtionality when executed by a large number of nodes.

27:

removeNeighbor(GetNeighbors(1))

28:

addNeighbor(n)

29:

end if

30: end function

Finally, Algorithm 8 illustrates the CYCLON protocol [START_REF] Voulgaris | Cyclon: Inexpensive membership management for unstructured P2P overlays[END_REF] that periodically reshuffles the neighborhood of the peers. Each peer p repeatedly initiates a neighbor exchange operation by (1) selecting a random subset of neighbors and a random peer q from that subset; (2) replacing q by p in the subset; (3) sending the subset to q; (4) receiving a subset of q's neighbors from q; and (5) updating p's neighbors using the subset received from q. Again, we observe that complex functionality (when considerred from a global perspective) can be implemented by remarkably simple gossip-based protocols.

Although the set of gossip-based protocols used for illustration is far from exhaustive, it covers a wide range of epidemic behaviors and interaction patterns. This tends to indicate that the core services identified could easily support other gossip-based protocols. One can easily construct higher-level building blocks useful for a wide range of applications, such as a peer sampling service [START_REF] Jelasity | The peer sampling service: experimental evaluation of unstructured gossip-based implementations[END_REF]. It is important to consider that all the algorithms discussed here use a source of randomness, which we believe is a distinguishing feature of gossip-based algorithms.

DEVELOPING GOSSIP-BASED APPLICATIONS

No matter the precise reason for which gossip-based solutions are employed-scalability, efficiency, reliability-their non-deterministic nature ends up reflecting through probabilistic guarantees and behavior. We advocate for making this probabilistic nature explicit, rather than employing gossip-based building blocks as if they provided deterministic guarantees.

Employing probabilistic protocols

We view deterministic protocols as special cases of probabilistic protocols. They just succeed with probability P = 1 or fail. We envision a system where probabilities are reflected in the interface, i.e., primitives for distributed interactions are parametrized with some probabilistic measures. We distinguish two places in which these measures can appear, namely as (a) input values, and/or (b) output values.

32: end function

More precisely, any primitive or operation triggering a gossipbased protocol can benefit from input values, which can be used to characterize the expected or required quality of the protocol result. Such values can help the protocol adjust certain of its own parameters in an attempt to satisfy the demand. Output values are the dual of input values; they reflect the imperfect nature of gossip-based protocols by conveying feedback on the outcome of a gossip-based primitive, e.g., an estimation of the outcome, or a lower bound on the partial completion.

Take the example of a gossip based broadcast, where an input probability specifies a lower bound on the desired coverage ratio (say 50 + %) or, alternatively, the probability that all processes receive the message (cf. [START_REF] Eugster | ∆-Reliable Broadcast: A Probabilistic Measure of Broadcast Reliability[END_REF]). An example of output "probability" in this case could consist in returning information at a given point about the fraction of processes known to have been reached by then in the former case, or an estimation of the probability that all processes indeed received the message in the latter case. As an alternative, one could even imagine being continuously updated about the quality of such "partial" results, and automatically triggering some action as soon as a desired or required threshold is reached.

We conjecture that making probabilities explicit in the application could also help developers embrace gossip-based protocols. Classical probabilistic protocols behave well most of the times, but there is always a chance that things turn bad; we believe that such considerations are a hindrance to a wider adoption of gossipping. Many applications can deal with "imperfect" behavior given that the degree of imperfection is known or a lower bound can be guaranteed. For instance, a distributed system may need to disseminate infor- mation such that a majority of the peers must be reached to preserve consistency, but liveness is increased if more peers receive the information.

Reasoning about probabilities

Several authors have described protocols with probabilistic guarantees, and composed these. For instance, Eugster has proposed in [START_REF] Eugster | Handbook on Theoretical and Algorithmic Aspects of Sensor, Ad Hoc Wireless and Peer-to-Peer Networks, chapter Reliable Computing in Ad-hoc Networks[END_REF] a system built by successive layering of probabilistic components akin to the ones in Figure 1-communication channels with probabilistic transmission guarantees, probabilistic broadcast, and probabilistic quorum replication (see Figure 2). An end application of this stack is a distributed certification authority. Probabilistic specifications for each layer have been provided, illustrating how a probabilistic property in a core component leads to probabilistic properties of any component build on top.

Composing probabilistic components

Can one develop inherent programming language support to promote probabilistic input as well as output values? In the context of program proving, several authors have proposed foundations for reasoning also about probabilistic components. McIver and Morgan [START_REF] Mciver | Abstraction, refinement and proof for probabilistic systems[END_REF] for instance introduce probabilistic guarded commands and probabilistic loops as fundamental building blocks. Probabilities defy the traditional way of reasoning about programs and proving their correctness. In axiomatic semantics for instance, it is common to work with Hoare-triples 1 of the form {A}f {B}, where a function or operation f may execute if its precondition A holds, guaranteeing its postcondition B subsequently. If one can prove that B implies C, where C is the precondition for some second operation g, reasoning can be performed stepwise in a scenario as the following:

{A}f {B}g{D}... Suppose now f is part of a probabilistic protocol. In this case, B will be satisfied with a probability only, or, if f provides feedback on its success rate, B can be integrating that rate, and a simple conditional branch can be used to guard g.

Introducing inherent support for such branching for instance only seems to make sense if all probabilistic components do 1 Axiomatic semantics are sometimes also referred to as Hoare-logic [START_REF] Hoare | An Axiomatic Basis for Computer Programming[END_REF].

manifest input and output probabilities with the same semantics. Given the wide variety of different (probabilistic) properties of existing protocols, we don't think this path can be straightforwardly pursued. In particular, only few protocols provide output values, i.e., feedback on their completion.

Dealing with multiple outputs

The possibility of a probabilistic component yielding different outcomes in response to its invocation leads to the issue of dealing with these multiple outputs. This situation is reminiscent of exception handling mechanisms in programming languages, in particular object-oriented ones. In earlier languages without support for such exceptions, as in C, different outcomes of a function, including outcomes reflecting errorenous states or failures, would simply be achieved by returning specific values representing such states, for instance simple integer values (e.g., -1 for an aborted operation). Inherent (static) support for exceptions in programming languages such as Java have improved both readability and safety of code with respect to such "design pattern"-like approaches [START_REF] Ancona | A Core Calculus for Java Exceptions[END_REF].

Programmers could strongly benefit from similar support for programming with probabilistic components, when providing information representing probabilistic output. Rather than signallng a potential set of exceptions that a function can return, we foresee a set of probabilities that are provided as part of the outcome of such a primitive. Such probabilities can be returned alongside with a "classic" return value, or only in absence thereof; several of them can be returned as outcome of the invocation of the probabilistic component. We advocate for try... catch-like constructs to support safe branching based on different outcome scenarios. The conditions for such branching are then application-defined criteria based on the potentially multiple output values (probabilities), for example representing thresholds triggering different subsequent behavior.

Encapsulating probabilistic behavior

In functional programming languages such as Haskell, monads [START_REF] Wadler | The Essence of Functional Programming[END_REF] have been proposed as programming language constructs to separate the handling of exceptional outcomes from the "common" execution (evaluation) path, and to avoid "partial" computations if at some point along such a path an exceptional state arises. Such computations are considered to be side-effects in this context. Monads have been used to explicitly deal with such side-effects by deferring any computation until a "safe point". I/O have been in this sense modeled as desired side-effects, which are however also to become effective only at precise points in time.

In the same sense, a monadic type system could allow for a cleaner separation of pure logical functionality of a program from its probabilistic, imperfect, nature. How such support would exactly look, and how probabilistic behavior could be expressed in it, requires however further investigation.

CONCLUSION

Gossip-based protocols are now important building stones in large-scale decentralized systems, such as peer-to-peer networks. In this paper, we presented two important aspects in programming such gossip-based protocols.

First, we proposed a very simple low-level interface, suffisant enough to write gossip-based protocols. Although this interface might appear standard in distributed systems, one of its key features is the inheritent randomness and nondeterminism of its primitives: indeed, more than other protocols, gossip-based protocols must deal with a very small knowledge of the system and very weak assumptions on the reliability of its components (communication channels and hosts), requiring to use a large amount of probabilistic operations. Through multiple examples, we showed that this interface can express well-known gossip-based protocols, from the simplest ones to more complicated ones.

Finally, we claimed at a higher-level that functionalities implemented over gossip-based protocols should be able to provide either the user or the system with probabilities of success. This favors the design of a language with "probabilistic primitives", where programs with underlying probabilities would be easy to develop and reason about. Such programs would be good candidates to manage and use gossip-based protocols and functionalities.

Interface 3 1 : 2 :Call back upon message 3 :

 3123 Communication fun send(msg) to dest Send message fun addMsgHandler(msg, handler) fun addTimer(delay, handler) Call back at given time

Figure 1 :

 1 Figure 1: Illustration of core services and APIs

Algorithm 5 Receive msg from n 5 :

 55 Renyi-Erdös 1: addMsgHandler(RENYI-ERDOS, Renyi-Erdos) 2: Received ← ∅ 3: N ← ApproximateSystemSize() 4: function Renyi-Erdos(n, msg) if msg ∈ Received then 6:

Figure 2 :

 2 Figure 2: Combining probabilistic components

  The first part of the API deals with randomness. It allows algorithms to access a random number generator and "flip a coin", as often required by algorithms with probabilistic properties like the Ben-Or consensus algorithm[START_REF] Ben-Or | Another advantage of free choice: Completely asynchronous agreement prototols[END_REF].

	Interface 1 Randomness
	1: fun random(range) : int	Returns a random number
	Interface

2 Neighborhood 1: fun getNeighbors(nb) : peer list Returns list of neighbors 2: fun addNeighbor(peer) Add new neighbor 3: fun removeNeighbor(peer)