Fateh Boudardara
email: fatehboudardara@railenium.eu

Abderraouf Boussif
email: abderraoufboussif@railenium.eu

Pierre-Jean Meyer
email: pierre-jean.meyer@univ-eifel.fr

Mohamed Ghazel
email: mohamed.ghazel@univ-eifel.fr

A review of abstraction methods towards verifying neural networks

Keywords: CCS Concepts:, Theory of computation → Abstraction, Logic and veriication, • Computing methodologies → Neural networks Formal veriication, neural network veriication, Abstraction, Abstract interpretation

Neural networks as a machine learning technique are increasingly deployed in various domains. Despite their performances and their continuous improvement, the deployment of neural networks in safety-critical systems, in particular for autonomous mobility, remains restricted. This is mainly due to the lack of (formal) speciications and veriication methods and tools that allow for getting suicient conidence in the behavior of the neural network-based functions. Recent years have seen neural network veriication getting more attention; and many veriication methods were proposed, yet the practical applicability of these methods to real-world neural network models remains limited. The main challenge of neural network veriication methods is related to the computational complexity and the large size of neural networks pertaining to complex functions. As a consequence, applying abstraction methods for neural network veriication purposes is seen as a promising mean to cope with such issues. The aim of abstraction is to build an abstract model by omitting some irrelevant details or some details that are not highly impacting w.r.t some considered features. Thus, the veriication process is made faster and easier while preserving, to some extent, the relevant behavior regarding the properties to be examined on the original model. In this paper, we review both the abstraction techniques for activation functions and model size reduction approaches, with a particular focus on the latter. The review primarily discusses the application of abstraction techniques on feed-forward neural networks, and explores the potential for applying abstraction to other types of neural networks. Throughout the paper, we present the main idea of each approach, and then discuss their respective advantages and limitations in details. Finally, we provide some insights and guidelines to improve the discussed methods.

INTRODUCTION

Neural Network (NN) is one of the most popular machine learning techniques [START_REF] Goodfellow | Deep learning[END_REF][START_REF] Lecun | Deep learning[END_REF]. The use of such an approach has shown fast progress during the last decade, giving rise to a noticeable enhancement of the technique, as witnessed by its successful achievements in various domains [START_REF] Liu | A survey of deep neural network architectures and their applications[END_REF]. Nowadays, applications of NNs can be encountered in a wide range of domains, such as in inancial transactions, trading, forecasting and fraud detection [START_REF] Liu | A survey of deep neural network architectures and their applications[END_REF][START_REF] Ajeet | Application of deep learning for object detection[END_REF]. In recent years, with the advances in terms of computational performances, NNs have been widely adopted in image recognition and object detection systems [START_REF] Ajeet | Application of deep learning for object detection[END_REF]. Namely, they are increasingly investigated to be deployed for safety-critical applications, in particular for the design of environment monitoring and decision-making functions in autonomous vehicles and trains [START_REF] Trentesaux | The autonomous train[END_REF]. A software module of a safety-critical system needs to be certiied before its deployment. Thus, it is required to develop methods to verify safety speciications and certify such NN-based software [START_REF] Ivanov | Verifying the safety of autonomous systems with neural network controllers[END_REF][START_REF] Ivanov | Compositional Learning and Veriication of Neural Network Controllers[END_REF].

The earliest works that deal with the veriication of NN models are based encoding the model at hand as a system of linear equations, which can then be solved using of-the-shelf veriication tools, namely SAT/SMT solvers [START_REF] Ehlers | Formal veriication of piece-wise linear feed-forward neural networks[END_REF][START_REF] Katz | Reluplex: An eicient SMT solver for verifying deep neural networks[END_REF][START_REF] Pulina | An abstraction-reinement approach to veriication of artiicial neural networks[END_REF] and MILP solvers [START_REF] Cheng | Maximum resilience of artiicial neural networks[END_REF][START_REF] Dutta | Output range analysis for deep neural networks[END_REF][START_REF] Lomuscio | An approach to reachability analysis for feed-forward relu neural networks[END_REF][START_REF] Tjeng | Evaluating Robustness of Neural Networks with Mixed Integer Programming[END_REF]. Although these methods are theoretically sound 1 and complete 2 , they are limited to small-size neural networks due to the non-linearity of NN models. Indeed, the number of linear constraints grows exponentially with the number of neurons for which the activation functions need to be linearized, which may give rise to a state-space explosion problem. Therefore, veriication methods based on over-approximation have been proposed to help mitigate this problem while preserving the soundness but not the completeness [15, 23, 33, 39, 52, 65ś67, 70] (see [START_REF] Urban | A Review of Formal Methods applied to Machine Learning[END_REF] for more details). Among these techniques, abstraction methods try to ease the veriication problem by abstracting the activation function using linear bounds [START_REF] Ehlers | Formal veriication of piece-wise linear feed-forward neural networks[END_REF] or abstract domains [START_REF] Gehr | Ai2: Safety and robustness certiication of neural networks with abstract interpretation[END_REF][START_REF] Singh | Fast and efective robustness certiication[END_REF][START_REF] Singh | An abstract domain for certifying neural networks[END_REF], or by reducing the size of the network to improve the scalability of NN veriication engines. In the latter case, an abstract (or reduced) model, which is smaller and easier to verify, is generated from the original network [START_REF] Yisrael Elboher | An abstraction-based framework for neural network veriication[END_REF][START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF]; thus, instead of applying the veriication method directly on the original model, the veriication process can be enhanced by applying it on the reduced model.

Regarding the substantial interest in NN veriication and the amount of existing methods for certifying NNs, many surveys and reviews on NN veriication methods have been proposed in the literature. For instance, Leofante et al. [START_REF] Leofante | Automated veriication of neural networks: Advances, challenges and perspectives[END_REF] established three types of NN veriication properties: equivalence, invertibility and invariance. They also provided a review of NN veriication techniques based on constraints solving. Liu et al. [START_REF] Liu | Algorithms for verifying deep neural networks[END_REF] classiied the existing veriication methods into three basic categories: optimization, reachability and search-based veriication techniques. Huang et al. [START_REF] Huang | A survey of safety and trustworthiness of deep neural networks: Veriication, testing, adversarial attack and defence, and interpretability[END_REF] conducted a review about deep NN safety and trustworthiness. For NN veriication, the authors distinguished between global and local properties. Regarding the guarantees of the veriication technique, the survey classiies NN veriication techniques into deterministic, approximative and statistical. According to [START_REF] Tran | Veriication approaches for learning-enabled autonomous cyber-physical systems[END_REF], veriication methods can be classiied as geometric-based methods, MILP, SAT/SMT and optimization-based methods, even though MILP and SAT/SMT based veriication methods can also be considered as particular cases of optimization techniques. Recently, Urban et al. [START_REF] Urban | A Review of Formal Methods applied to Machine Learning[END_REF] discussed the veriication methods applied to machine learning. For NN veriication, the authors proposed a classiication of the existing methods into complete or incomplete methods with respect to the output of the veriication process. Moreover, the review [START_REF] Urban | A Review of Formal Methods applied to Machine Learning[END_REF] summarizes formal veriication approaches for diferent machine learning techniques such as support vector machine and decision trees. Another research area that is surveyed in [START_REF] Bollig | A Survey of Model Learning Techniques for Recurrent Neural Networks. A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday[END_REF] involves exploiting the sequential behavior of Recurrent Neural Networks (RNNs) to convert RNN models into automata and verify certain properties on the resulting automaton model. Although such techniques can also be seen as a form of NN abstraction into automata, their focus on recurrent neural networks places them out of the scope of the present survey where we primarily consider feed-forward neural networks.

Among all the surveys and reviews discussed above, and to the best of our knowledge, no existing work ofers an overview on the abstraction methods for feed-forward NNs veriication purposes. The aim of this work is to present a review on the existing activation function abstraction and model reduction methods in the literature for NN veriication, and derive a critical discussion regarding these techniques. Concretely, for each presented approach we will sketch out the main idea, analyze its advantages and its drawbacks, and discuss the corresponding formal guarantees. For model reduction techniques, we will particularly highlight how each method can afect the veriication process, and we will discuss further research directions in terms of these techniques. Although this work focuses on feed-forward NNs, we also provide some perspectives on how these abstraction methods can be adjusted to support other types of NNs. It is worth noticing that in this paper, we only consider NN abstraction methods that are used for veriication purposes, i.e., we do not include neural networks' compression techniques such as quantization and edges pruning [START_REF] Han | Deep compression: Compressing deep neural networks with pruning, trained quantization and hufman coding[END_REF], since their goal is to build a compressed model to speed up the run-time execution [START_REF] Cai | Optimus: An Operator Fusion Framework for Deep Neural Networks[END_REF], while preserving the model's accuracy but not necessarily its behavior, neither providing formal guarantees on the compressed model. The remainder of the paper is structured as follows: In Section 2, preliminary concepts and notations pertaining to neural networks are introduced, the veriication problem of NNs is stated and an overview of the existing NN veriication methods is provided. Section 3 reviews existing NN abstraction approaches, with a deeper focus on model reduction methods. Besides discussing the main features of the evoked techniques, some pointers to possible enhancements of the discussed methods will be provided. Finally, in Section 4 we recall the main indings through our review and outline some challenges and perspectives regarding NN abstraction.

BACKGROUND 2.1 Neural networks

A feed-forward neural network (FFNN) is a sequence of interconnected layers { 1 , 2 , ..., }. When the number of layers is important, the term Deep Neural Networks is used. In an NN, each layer holds one or many nodes, called neurons. The irst layer 1 is called the input layer, the last one is the output layer and the remaining layers : 2 ≤ ≤ -1 are referred to as hidden layers. Likewise, the nodes in the hidden layers are called hidden nodes. Each hidden node is associated with a bias and an activation function. The nodes of a layer ∈ { 2 , 3 , ..., } are connected to the nodes of the previous layer via weighted edges. That is to say, a neuron of layer receives data from layer -1 , calculates the weighted sum of this data and adds a bias. An activation function is then applied, and the result is forwarded to interconnected neurons of the next layer +1 (more details are given below). The propagation of data from the input layer to the output layer, passing through multiple hidden layers, is called łfeed-forward propagationž. An NN is built upon a training phase that aims to recognize and encode the underlying input-output relationship (correlation) of a data set. To evaluate an NN model, the accuracy, which is the rate of correct predictions, is calculated. Fig. 1 shows a neural network of 4 layers: an input layer of 3 inputs, two hidden layers of 4 and 3 nodes, respectively, and a 2-node output layer.

An NN model can indeed be seen as a function N : → , where is the input domain and is the output domain of the model. For image classiication for example, is a matrix of pixel values representing an Fig. 2. An example showing the connection between a neuron of and -1 image, is the set of all possible classes of these images. As an NN model consists of a sequence of layers, N can be considered as a composition of a set of functions { 1 , 2 , ..., } where , 1 ≤ ≤ is the corresponding function of layer . This can be written, formally, as: N () = ( -1 (...( 1 ())...), where 1 is the identity function. In the following, we give some formal deinitions pertaining to NN concepts and properties that will be used later on in this paper.

Deinition 2.1. For a layer : ∈ {1 . . . }, we deine the set of neurons of by , with | | the number of neurons in the layer . And for a neuron ∈ , its value w.r.t to an input is (). For simplicity, when is not speciic, we use instead of ().

Let ∈ be a neuron of a hidden layer , its value is calculated in two steps:

(1) Aine transformation: calculates the sum of previous layer's outputs modulated by the weights assigned to the corresponding edges, plus the bias. This can be formulated as:

= =| -1 |  =1 -1 , × -1, +
where -1 , is the weight of the edge connecting the nodes -1, and , and is the bias of the node . Note that is also called the pre-activation value of .

(2) Activation function: the inal value , also called the value after activation, is determined by applying an activation function to , i.e. = ( ). The two steps are summarized in Equation [START_REF] Michael E Akintunde | Veriication of RNN-based neural agentenvironment systems[END_REF]. The obtained value is the output value of which will be forwarded to the next layer +1 . Fig. 2 illustrates these steps on an example.

= =| -1 |  =1 -1 , × -1, + (1)
The calculation of the NN output = N () for a given input , is done by successively applying these operations, layer by layer, from the input to the output layer.

Depending on the application, there exists several activation functions: Sigmoid, Tanh, Relu, etc. [START_REF] Zhu | PFLU and FPFLU: Two novel non-monotonic activation functions in convolutional neural networks[END_REF]. Relu (for Rectiied Linear Unit), as deined in Equation (2), is a piece-wise linear function that has linear behaviors in (-∞, 0] and in [0, +∞). The Relu activation function is widely used in NN, and due to its simple form and its piece-wise linear behaviour, the majority of the existing neural network veriication and abstraction approaches consider models with this activation function [START_REF] Huang | A survey of safety and trustworthiness of deep neural networks: Veriication, testing, adversarial attack and defence, and interpretability[END_REF][START_REF] Katz | Reluplex: An eicient SMT solver for verifying deep neural networks[END_REF][START_REF] Lomuscio | An approach to reachability analysis for feed-forward relu neural networks[END_REF].

() = max(, 0) = , if ≥ 0 0, otherwise (2)
Remark (Weights). In this paper, the weight of an edge connecting ∈ to a node +1, ∈ +1 is written as or ( , +1, ).

Verification of neural networks

Formal veriication is the domain of proving or disproving that a system meets certain formal speciications and properties. A veriication problem is deined as:

|= ? (3)
which is equivalent to answering the question: does the system model M satisfy the property P? Depending on the veriication technique, the system has to be modelled (e.g., state transition model) and the speciications need to be expressed respecting some speciic syntax (e.g., temporal logic). The aim of a veriication technique is to prove that P holds on M or generate a counterexample witnessing the violation of P. Many veriication techniques, such as model-checking, SAT/SMT, abstract interpretation, and theorem proving have been broadly and successfully applied to verify software-intensive systems [START_REF] Biere | Handbook of satisiability[END_REF][START_REF] Clarke | Handbook of model checking[END_REF]. Accordingly, formal veriication for NN can be deined as in Formula ( 3), where M is the NN model and P is the property to be checked, which is generally a mathematical formula constituted of a set of constraints on the inputs and the outputs of the network.

According to Leofante et al. [START_REF] Leofante | Automated veriication of neural networks: Advances, challenges and perspectives[END_REF], for a given NN represented by its corresponding function N : → , the NN veriication problem can be stated as follows:

• Deine () and () as a set of constraints on the input (preconditions) and the output (postconditions), respectively. Here, () and () are sorted irst order logic formulas. • For all satisfying the preconditions (), verify whether or not N () fulills the postconditions (N ()). This can be formulated as follows:

∀ ∈ , () =⇒ (N ()) (4)
Example 2.2. By taking = R 2 and = R as the input and output domains of some given NN, the veriication problem deined by Formula (4) can be instantiated as:

() : 1 ∈ [ 1 , 1 ] ∧ 2 ∈ [ 2 , 2 ], with = ( 1 2 ) (N ()) : N () ≥
where , , ∈ R, and ≤ . The veriication problem of this example thus aims to check that for all input in the 2-dimensional interval deined in the precondition, the corresponding output N () is lower-bounded by as in the postcondition.

Example 2.3. To verify the robustness property of a classiication network for an input image 0 , i.e., to check for a classiication problem that the network assigns the same label (class) to all inputs within a small region surrounding 0 , the veriication problem can be formulated using (4) as follows: where ∥.∥ is a given norm.

         () () ≥ 0 < 0 ≥ 0 () ≥ 0 < 0 < 0
It is worth mentioning that the paper [START_REF] Leofante | Automated veriication of neural networks: Advances, challenges and perspectives[END_REF] introduces other types of properties such as equivalence between two NNs. However, it should be noted that most of the existing veriication methods and all the abstraction methods reviewed in this paper concentrate on verifying a single network and rely on properties based on Formula 3.

Verifying properties of NNs is increasingly receiving more attention and many approaches have been proposed in recent years [START_REF] Huang | A survey of safety and trustworthiness of deep neural networks: Veriication, testing, adversarial attack and defence, and interpretability[END_REF][START_REF] Liu | Algorithms for verifying deep neural networks[END_REF]. The straightforward veriication way consists of encoding the NN behavior, as well as the property to be checked, as a system of linear equations, and then use an appropriate engine to perform the veriication process. For instance, SAT/SMT and MILP encoding are widely used to verify NNs properties [START_REF] Cheng | Maximum resilience of artiicial neural networks[END_REF][START_REF] Dutta | Output Range Analysis for Deep Feedforward Neural Networks[END_REF][START_REF] Huang | Safety veriication of deep neural networks[END_REF][START_REF] Katz | Reluplex: An eicient SMT solver for verifying deep neural networks[END_REF][START_REF] Katz | The marabou framework for veriication and analysis of deep neural networks[END_REF][START_REF] Lomuscio | An approach to reachability analysis for feed-forward relu neural networks[END_REF][START_REF] Tjeng | Evaluating Robustness of Neural Networks with Mixed Integer Programming[END_REF]]. These methods are also called complete because they encode the exact behavior of the network. However, since most of the common activation functions are nonlinear, this kind of veriication methods does not scale in the case of large neural networks, and sufers from state-space explosion. For example for the piece-wise linear activation function Relu, each Relu node has to be split into two linear constraints, i.e.: if = (), then = 0 when < 0 and = when is positive. Therefore, solving a veriication problem of a network of Relu nodes leads to solving 2 linear sub-problems as illustrated in Fig. 3. To address this issue, several approaches based on abstraction have been proposed. The next section provides more details about this category of techniques.

ABSTRACTION APPROACHES FOR NEURAL NETWORK VERIFICATION

In order to overcome the drawbacks of complete veriication methods for NN, some abstraction approaches are proposed. The main idea behind these approaches consists in generating an abstract model from the original network ensuring that whenever the property P holds on the abstract model N , it necessarily holds on the original one N , i.e.,:

|= =⇒ |= . ( 5
)
However, these approaches may fail to provide any conclusion on the original network when the property is violated on the abstract model. This is in fact due to spurious counterexamples. Namely, when the property does not hold, a counterexample (CE) on the abstract model is generated, but due to the over-approximation of the abstract model, this CE might not correspond to any real behavior in the original model (i.e., spurious counterexample).

Concretely, the abstraction of NN can be performed in two diferent manners: • Activation function abstraction (AF abstraction): to ease the veriication process, non-linear activation functions of the NN are over-approximated by a set of linear constraints. • NN model reduction: abstracting the network model by merging some nodes in order to reduce the size of the network, and thus improve the scalability of existing veriication tools. A detailed survey of these methods is given in Sections 3.1 and 3.2, respectively.

Remark (Reinement). Some works consider improving the incomplete veriication methods by ruling out as many spurious CE as possible by introducing a reinement phase. In other words, the veriication method reines the abstract model iteratively until we can prove either the property holds or the generated CE exhibits a real behavior on the original model [START_REF] Ehlers | Formal veriication of piece-wise linear feed-forward neural networks[END_REF][START_REF] Tran | Veriication of deep convolutional neural networks using imagestars[END_REF][START_REF] Tran | Star-based reachability analysis of deep neural networks[END_REF][START_REF] Wang | Eicient formal safety analysis of neural networks[END_REF][START_REF] Wang | Formal security analysis of neural networks using symbolic intervals[END_REF].

Abstraction of the activation function

The key challenge of NN veriication is pertaining to the non-linearity of activation functions. AF abstractionbased veriication approaches are applied to handle this issue by over-approximating the activation functions with linear constraints.

The earliest work dealing with NN veriication problem was introduced by Pulina et al. [START_REF] Pulina | An abstraction-reinement approach to veriication of artiicial neural networks[END_REF]. In this work, authors divided the function into small regions, then a linear over-approximation is computed for each region, as shown in Fig. 4.

With the same spirit, Ehlers [START_REF] Ehlers | Formal veriication of piece-wise linear feed-forward neural networks[END_REF] proposed a precise -abstraction technique where is replaced by a system of linear constraints (see Fig. 5a) and hence the veriication problem of NN is reformulated as a linear programming (LP) problem that can be solved using classic LP solvers. The approach in [START_REF] Ehlers | Formal veriication of piece-wise linear feed-forward neural networks[END_REF] was implemented in a tool called Planet and brings the LP toolkit GLPK into play along with the Minisat solver for veriication.

Gehr et al. [START_REF] Gehr | Ai2: Safety and robustness certiication of neural networks with abstract interpretation[END_REF] applied an abstract interpretation method [START_REF] Cousot | Abstract interpretation: a uniied lattice model for static analysis of programs by construction or approximation of ixpoints[END_REF] on NN for the irst time. They proposed a framework called 2 (Abstract Interpretation for Artiicial Intelligence) that soundly over-approximates NN operations by means of abstract domain 3 . The approach can be extended to support other abstract domains. 2 can handle feed-forward and convolutional neural networks (CNN) with andfunctions. The approach in [START_REF] Gehr | Ai2: Safety and robustness certiication of neural networks with abstract interpretation[END_REF] was extended by Singh et al. [START_REF] Singh | Fast and efective robustness certiication[END_REF] to support and ℎ activation functions. This is accomplished by means of abstract transformers based on zonotopes for each function. As an example, the abstraction of is given in Fig. 5b Furthermore, Singh et al. [START_REF] Singh | An abstract domain for certifying neural networks[END_REF] proposed a new method, called , based on Abstract Interpretation by introducing a new abstract domain. DeepPoly combines loating point polyhedra and intervals. Each neuron is represented by its concrete and symbolic upper and lower bounds. Moreover, Singh et al. [START_REF] Singh | An abstract domain for certifying neural networks[END_REF] introduced abstract transformers for popular NN operations: aine transformation, , , ℎ andto propagate the inputs successively through the layers of the network. For , two diferent abstractions are proposed as shown in Figs. 5c and5d. It is worthwhile to mention that the approach supports both feed-forward and convolutional NN.

While the previous works consider only a single neuron, some others try to deine sound approximations of a set of neurons, jointly. Singh et al. [START_REF] Singh | Beyond the Single Neuron Convex Barrier for Neural Network Certiication[END_REF] introduced a new method that provides an approximation of nodes (in the same layer) at a time in order to capture dependencies of the inputs. First, the nodes are selected and then the convex relaxation of the group of nodes is calculated. The framework has a parameter which represents the number of nodes to be considered together. A more general framework, based on [START_REF] Singh | Beyond the Single Neuron Convex Barrier for Neural Network Certiication[END_REF], was recently proposed by Müller et al. [START_REF] Niklas Müller | PRIMA: general and precise neural network certiication via scalable convex hull approximations[END_REF]. The framework, called (PRecIse Multi-neuron Abstraction), computes the convex over-approximation of a set of outputs of arbitrary activation function, including , and ℎ. The approach decomposes the activations into overlapping groups of size , then calculates the convex approximation of the octahedral over-approximation for each group . Finally, it takes the union of all the obtained output constraints. These constraints combined with the encoding of the whole NN are used for veriication.

Other techniques based on symbolic propagation are proposed in [START_REF] Li | Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster veriication[END_REF][START_REF] Yang | Enhancing robustness veriication for deep neural networks via symbolic propagation[END_REF] to enhance the precision of abstract interpretation-based approaches. In symbolic propagation every neuron is associated with a formula expressed using the activations of neurons in its previous layers. In [START_REF] Singh | Boosting robustness certiication of neural networks[END_REF], a combination of over-approximation techniques with linear relaxation methods is proposed so as to gain more precision of over-approximation techniques and the scalability of complete methods.

These techniques can be adapted to support further types of NNs. One way to deal with Recurrent Neural Networks is to generate an equivalent feed-forward neural network and then apply the abstraction method [START_REF] Michael E Akintunde | Veriication of RNN-based neural agentenvironment systems[END_REF][START_REF] Jacoby | Verifying recurrent neural networks using invariant inference[END_REF]. For Convolutional Neural Networks, most of the techniques are applicable and the only restriction is that the activation function of the convolution layer has to be Relu or other supported functions such as Sigmoid and Tanh [START_REF] Singh | An abstract domain for certifying neural networks[END_REF].

NN model reduction

The main objective of NN model reduction is to reduce the size of the NN model while guaranteeing some behavioral relation: the desired property P holds on the original model N whenever it holds on the reduced model N as deined in [START_REF] Bollig | A Survey of Model Learning Techniques for Recurrent Neural Networks. A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday[END_REF]. Fig. 6 provides an illustrative example of the main idea behind model reduction applied on a small neural network.

Such a behavioral relation is obtained by ensuring that is an over-approximation of (i.e. all behaviors of can be reproduced in ). Therefore, the reduction process must carefully select the set of neurons to be merged (or removed), and determine how to calculate the weights of the new edges.

Prabhakar and Afzal [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF] proposed a method based on Interval Neural Networks (INN) for output range analysis. In this method, the nodes of the same layer are merged while replacing the weights of their input edges by the interval hull of the incoming edges. In other words, the weights of incoming edges are replaced by [min( ), max( )], where are the values of the incoming weights to the nodes to be merged. The weights of the outgoing edges from these nodes are replaced by the interval hull multiplied by the number of merged nodes : × [min( ), max( )].

For the veriication part, Prabhakar and Afzal [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF] adapted INN to MILP big-M encoding [START_REF] Cheng | Maximum resilience of artiicial neural networks[END_REF] and used the Gurobi MILP solver for veriication. The performance of this method is tested on the airborne collision avoidance ACAS Xu benchmark [START_REF] Kyle D Julian | Policy compression for aircraft collision avoidance systems[END_REF][START_REF] Katz | Reluplex: An eicient SMT solver for verifying deep neural networks[END_REF]. The authors claim that the abstraction enhances the veriication process. Namely, Gurobi was not able to verify a number of properties on the original model (no return), while the same properties have been successfully checked when Gurobi was applied on the abstract model.

Recently, Boudardara et al. [START_REF] Boudardara | Interval Weight-Based Abstraction for Neural Network Veriication[END_REF] proposed an interval-weight based model reduction method. The elaborated method supports Relu and Tanh neural networks. While an outgoing weight of a set of merged nodes is the sum of absolute values of their corresponding outgoing weights, an abstract incoming weight is an interval deined as: the min and the max of the sign of the corresponding outgoing weights of the merged nodes multiplied by the the original incoming weights. The sign function deined in this work returns 1 if the value is at least equal to 0, and -1 otherwise. The method is applied to the ACAS Xu Relu-NN benchmark [START_REF] Katz | Reluplex: An eicient SMT solver for verifying deep neural networks[END_REF], where the Interval Bound Propagation (IBP) algorithm [START_REF] Xiang | Reachable set estimation for neural network control systems: A simulation-guided approach[END_REF] is used to calculate the output range on the original and abstract networks. Moreover, the authors of [START_REF] Boudardara | Interval Weight-Based Abstraction for Neural Network Veriication[END_REF] have varied the number of merged nodes to assess the output range and the IBP computation time for abstract networks. It has been shown, in particular, that merging more nodes accelerates the IBP algorithm while generating larger output ranges. The authors observe that the wide output range is due to the IBP algorithm which is not an exact veriication method. However, this work does not discuss possible adaptation to support other veriication tools. More recently, Boudardara et al. [START_REF] Boudardara | A sound abstraction method towards eicient neural networks veriication[END_REF] introduced a variant of the approach designed to accommodate all non-negative activation functions, such as Relu and Sigmoid functions. This new method has been also evaluated on the ACAS Xu Relu-NNs, wherein it demonstrated an interesting competitive performance in comparison to the two methods proposed in [START_REF] Boudardara | Interval Weight-Based Abstraction for Neural Network Veriication[END_REF][START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF].

In [START_REF] Sotoudeh | Abstract Neural Networks[END_REF], Sotoudeh and Thakur, by introducing the notion of Abstract Neural Network (ANN), provided a formalization of a general abstraction approach. In ANN, the weights are represented using abstract domains. Accordingly, the approach proposed by Prabhakar and Afzal [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF] can be considered as a particular instantiation of this approach using the interval abstract domain. Notice that the proposed approach supports a wide range of activation functions. Moreover, it can be instantiated using other convex abstract domains and it is not restricted to intervals as used in INNs [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF]. The approach provides a generic formula to calculate the weight merging matrix from the original weight matrix and the partitions and of two successive abstract layers and +1 , respectively. A partition is a rearrangement of a set of neurons, i.e., if = { 1 , 2 , 3 }, a possible partition of would be = {{ 1 , 2 }, { 3 }}, which means that 1 and 2 will be merged in the abstract network. is the convex combination (calculated by a function ) of the partitioning combination matrix of and , denoted by and , respectively, and the weight matrix , i.e., = (, , ). Next, the abstract weight matrix, denoted by , is built by applying a convex abstract domain on the obtained : = ( ). The reduced model is obtained by applying the same procedure to every layer, iteratively. Therefore, the obtained reduced model is an over-approximation for any non-negative activation function that satisies the Weakened Intermediate Value Property (WIVP). Although some activation functions can have negative values and others are not continuous (thus not WIVP), the authors of [START_REF] Sotoudeh | Abstract Neural Networks[END_REF] claim that there is always a way to overcome these problems, as they showed for Leaky and the ℎℎ activation functions.

In [START_REF] Ashok | Deepabstract: Neural network abstraction for accelerating veriication[END_REF], Ashok et al. apply K-means clustering algorithms to partition each hidden layer into subgroups, such that ≤ | |, then replace each subgroup with its representative neuron. The abstraction method, called DeepAbstract, has three parameters: the original network , a inite set of input-points and a vector which contains the number of nodes on each abstract layer. For each hidden layer , the following steps are performed: Note that the representative neuron of a cluster is the nearest neuron to the centroid of , thus; the incoming weights of remain the same as the corresponding neuron before abstraction. All the other neurons from cluster are omitted with their incoming edges.

In addition, Ashok et al. [START_REF] Ashok | Deepabstract: Neural network abstraction for accelerating veriication[END_REF] provide a method to lift the veriication results from the abstract model to the original one. The idea is to calculate the accumulated error induced by replacing a cluster of neurons by its representative for each image in , and then propagate this error through the successive layers using the DeepPoly veriication Algorithm4 . A set of experiments were conducted to check the performance of DeepAbstract. Local robustness of some MNIST images was checked and the authors claim that the veriication time was reduced by 25% when DeepPoly is combined with DeepAbstract.

Elboher et al. [START_REF] Yisrael Elboher | An abstraction-based framework for neural network veriication[END_REF] proposed an abstraction approach based on merging neurons of the same category (see hereafter) to build a smaller model so as to enhance the scalability of the existing veriication tools. Regarding the veriication property, which has the form: : ∀ ∈ () =⇒ ≤ , the aim of this approach is to build a reduced model (its corresponding function is N ), s.t ∀ ∈ , N () ≥ N (). Therefore, |= whenever |= (i.e., N () ≤ ). First, each neuron is labelled according to the sign of its outgoing weights. A neuron is split if it has both positive and negative outgoing weights. Next, to guarantee that is an over-approximation of , the proposed method tries to increase the output of the abstract model by classifying each neuron as or . The class means the output will increase by increasing the value of this neuron, while a neuron is marked as when decreasing its value leads to increasing the output's value.Finally, the nodes of the same layer and the same category can be merged by summing up the weights of their outgoing edges and taking the min value of the the weights of their incoming edges if they are marked as , or the max value for any group of nodes. Moreover, some heuristics are proposed in [START_REF] Yisrael Elboher | An abstraction-based framework for neural network veriication[END_REF] to enhance the abstraction process. The proposed method is applied on ACAS Xu networks while Marabou [START_REF] Katz | The marabou framework for veriication and analysis of deep neural networks[END_REF] is used as back-end veriication tool. A comparison study between the abstraction method combined with Marabou and the vanilla version of Marabou was conducted, and the results showed that the abstraction method allows Marabou to verify more properties in less execution time.

A novel approach based on bisimulation [START_REF] Kim | Bisimulation through probabilistic testing[END_REF] is proposed by Prabhakar [START_REF] Prabhakar | Bisimulations for neural network reduction[END_REF]. The generated abstract neural network is equivalent, or bisimilar, to the original one. To guarantee the equivalence between and , two neurons and to be merged must have the same activation function, the same bias value ( = ) and the same weights for each incoming edge respectively, i.e., ∀ ′ ∈ -1 , ( ′ , ) = ( ′ , ). Due to the strict conditions that, generally, do not hold in most of real networks, Prabhakar [START_REF] Prabhakar | Bisimulations for neural network reduction[END_REF] extends the NN bisimulation to a more feasible relaxed method, called NN -bisimulation. Using NN -bisimulation ( ∈ R + ), two nodes and in can be merged if the following conditions are satisied: (1) and have the same activation function

(2) | -| ≤ (3) ∀ ′ ∈ -1 , | ( ′ , ) -( ′ , )| ≤
where ≥ 0. So the obtained network is -bisimilar to network .

Taking advantages of code refactoring [START_REF] Fowler | Refactoring: improving the design of existing code[END_REF], Shriver et al. [START_REF] Shriver | Refactoring neural networks for veriication[END_REF] introduced the concept of refactoring neural networks to restructure the initial model and preserve its accuracy to enhance further operations on it, for instance veriication. Concretely, NN refactoring consists of two steps: architecture transformation and distillation. The former applies some changes on the network's architecture by dropping or changing some layers and/or their types that are not supported by veriication tools (e.g. residual blocks and convolutional layers). The latter updates the model's parameters: weights and biases, while preserving the original model's behavior, which is captured by its accuracy and test error according to Shriver et al. [START_REF] Shriver | Refactoring neural networks for veriication[END_REF]. A tool called R4V was developed from this approach. R4V was tested on DAVE-2 [START_REF] Bojarski | End to end learning for self-driving cars[END_REF] and DroNet [START_REF] Loquercio | Dronet: Learning to ly by driving[END_REF] networks. The used veriication tools are presented in Table 1.

Table 1. A list of NN model reduction methods used for verification. The underscore symbol "-" is used to denote that no information is provided in the corresponding original paper.

Method

Pub The results showed that applying the veriication tools on the refactored model improves their scalability. For example, Planet [START_REF] Ehlers | Formal veriication of piece-wise linear feed-forward neural networks[END_REF] fails to check any property on DroNet within 24 hours. However, after refactoring the network, Planet was able to verify three out of the ten properties.

The main features of the above discussed neural networks reduction techniques are summarized in Table 1. The last two columns of the table contain veriication methods and the data sets used during the evaluation of the abstraction method. Veriication methods are those used during the evaluation of the abstraction in the original paper; notice that other methods can be used to verify the obtained abstract model.

An example is provided in Figure 7 to demonstrate the application of some of the methods mentioned in this section [START_REF] Boudardara | Interval Weight-Based Abstraction for Neural Network Veriication[END_REF][START_REF] Yisrael Elboher | An abstraction-based framework for neural network veriication[END_REF][START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF][START_REF] Sotoudeh | Abstract Neural Networks[END_REF] 7 . Notice that the abstract network using the ANN method [START_REF] Sotoudeh | Abstract Neural Networks[END_REF] with the box (or interval) abstract domain is the same as the abstract network obtained using the method of INN [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF] (see Figure 7b). The example presents a segment of a Relu-NN, i.e, 1 is an arbitrary neuron of a hidden layer and not the input of the network, and all nodes are assigned a Relu activation function. We apply abstraction (using the selected methods) to merge the two nodes 3 and 4 , while assuming that ( 1 ) = 1, and we calculate the value of 5 , ( 5 ) and ( 5 ) on the original and the abstract networks, respectively. While model reduction methods [START_REF] Boudardara | Interval Weight-Based Abstraction for Neural Network Veriication[END_REF][START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF][START_REF] Sotoudeh | Abstract Neural Networks[END_REF] (Figures 7c and7b) ensure that the output of the original network is within the ranges of the output of the abstract network, i.e.: ( 5 ) ∈ ( 5), the method introduced in [START_REF] Yisrael Elboher | An abstraction-based framework for neural network veriication[END_REF] (Figure 7e) guarantees that the output of the obtained abstract network is always greater than the output's value of the original network, i.e.: ( 5 ) ≤ ( 5)

It is worth noting here that these techniques can be adjusted to support other types of NNs. For instance, RNN can be transformed into an equivalent FFNN [START_REF] Michael E Akintunde | Veriication of RNN-based neural agentenvironment systems[END_REF][START_REF] Jacoby | Verifying recurrent neural networks using invariant inference[END_REF], and then model reduction approaches can be applied to generate the abstract network. On the other hand, model reduction can be applied on the fully connected part of CNNs [START_REF] Ostrovsky | An abstraction-reinement approach to verifying convolutional neural networks[END_REF][START_REF] Xu | Conv-Reluplex: a veriication framework for convolution neural networks[END_REF]. Regarding Binarized Neural Networks (BNN), due to their binary behaviour and their small size (a) A toy NN example before applying model reduction (the original network). For ( 1 ) = 1, we have ( 5 ) = 2 (b) The abstract network using INN method [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF] and ANN [START_REF] Sotoudeh | Abstract Neural Networks[END_REF]. For ( 1 ) = 1, ( 5 ) = [0, 17], and we have ( 5 ) ∈ ( 5) (c) The abstract network using the method presented in [START_REF] Boudardara | Interval Weight-Based Abstraction for Neural Network Veriication[END_REF]. For ( 1 ) = 1, ( 5 ) = [0, 12], and we have ( 5 ) ∈ ( 5) (d) The network ater neurons' classification (positive /negative and increasing /decreasing) [START_REF] Yisrael Elboher | An abstraction-based framework for neural network veriication[END_REF] (e) The abstract network using the method of Elboger et al. [START_REF] Yisrael Elboher | An abstraction-based framework for neural network veriication[END_REF]. For ( 1 ) = 1, ( 5 ) = 12, and we have ( 5 ) ≤ ( 5) Fig. 7. The application of diferent model reduction methods on a toy example of NN comparing to other types of NNs, their veriication does not require abstracting their behavior and, generally, exact methods such as SAT and MILP can be applied directly [START_REF] Jia | Eicient exact veriication of binarized neural networks[END_REF][START_REF] Lazarus | A mixed integer programming approach for verifying properties of binarized neural networks[END_REF][START_REF] Narodytska | Verifying properties of binarized deep neural networks[END_REF].

It is worth mentioning that another family of techniques based on merging neurons and removing some edges without afecting the accuracy of the model exists in the literature. These techniques are called NN compression and acceleration, and their objective is to build a smaller network with low computational complexity, so that it can be embedded on devices with limited resources and used in real-time applications, while keeping the accuracy as high as possible [START_REF] Cheng | A survey of model compression and acceleration for deep neural networks[END_REF][START_REF] Han | Deep compression: Compressing deep neural networks with pruning, trained quantization and hufman coding[END_REF][START_REF] Liang | Pruning and quantization for deep neural network acceleration: A survey[END_REF]. Although both NN model reduction and NN compression strive to reduce the number of neurons, NN compression techniques cannot be used for veriication, since the generated models do not fulil the abstraction condition presented in Formula [START_REF] Bollig | A Survey of Model Learning Techniques for Recurrent Neural Networks. A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday[END_REF]. In other words, verifying a property on the compressed network obtained by any compression method does not imply that the property does hold in the original network.

Discussion

This section discusses the aforementioned model reduction methods, while highlighting their limitations and proposing some possible area of improvements. In order to fairly compare the eiciency of the discussed approaches, we analyze them according to three main criteria (with respect to the available information in the original papers): (i) the precision of the over-approximation, (ii) the minimal number of neurons that can be obtained when the reduction method is applied until saturation, and (iii) the eiciency regarding the veriication time and the number of the veriied properties on the reduced model versus the original one.

The abstraction method based on INNs, proposed by Prabhakar et al. [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF] seems to be very useful when the problem of output range analysis is considered. An exhaustive application of this method leads to merge all neurons of each hidden layer and replace them by one abstract neuron. The results of their paper show that the precision depends highly on the number and the selection of the nodes to be merged. The method needs some improvements to be more precise, since no study has been provided for neuron selection. In addition, operations on intervals may impact the precision of this method. MILP encoding is proposed to solve the veriication problem on INNs, and to the best of our knowledge, no other veriication method is proposed to verify INNs. Moreover, this method is restricted to abstract NNs with non-negative activation functions [START_REF] Sotoudeh | Abstract Neural Networks[END_REF]. Consequently, Sotoudeh et al. [START_REF] Sotoudeh | Abstract Neural Networks[END_REF] proposed some fundamentals to abstract any NNs with diferent activation functions using any convex abstract domain and which is not limited to intervals. In [START_REF] Sotoudeh | Abstract Neural Networks[END_REF], the authors provide an example of abstraction based on octagons, but no explanation was given of the meaning of using such abstract domain to represent the merged neurons. Moreover, the work would have been more relevant if it had included an evaluation study to concretely show how the ANN can be extended to deal with other abstract domains. In [START_REF] Boudardara | Interval Weight-Based Abstraction for Neural Network Veriication[END_REF], Boudardara et al. proposed a method that is similar to INNs [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF], where the incoming weights are encoded as intervals, while the outgoing weights are scalars. However, unlike INNs, the proposed method is not limited to non-negative activation functions and can support the use of Tanh activation function. Moreover, the authors claim that the method can be adjusted to support other activation functions as well.

DeepAbstract, proposed by Ashok et al. [START_REF] Ashok | Deepabstract: Neural network abstraction for accelerating veriication[END_REF], is parametrized by the number of clusters on each layer; if there are few clusters, the model will be more abstract and less precise. In addition, this method relies on the discrete input set that is used during clustering phase and can only verify the robustness of the model on points within this set . Ashok et al. [START_REF] Ashok | Deepabstract: Neural network abstraction for accelerating veriication[END_REF] claim that the veriication time was reduced by 25% when DeepAbstract is used along with DeepPoly, however, only 195 out of 200 images could be veriied to be robust against 197/200 when DeepPoly is used without abstraction.

The abstraction-reinement proposed by Elboher et al. [START_REF] Yisrael Elboher | An abstraction-based framework for neural network veriication[END_REF] boosted the Marabou veriier to check more properties (58 out of 90 property versus 35/90). Moreover, the abstraction method reduces the total query median runtime from 63671 seconds to 1045 seconds. As a consequence of the classiication of neurons, this method can abstract a layer to four neurons at most. This is one of the main drawbacks of this method since only neurons belonging to the same category can be merged. It should also be mentioned that only properties in the form: ≤ are considered, although authors claim that the approach is adaptable to cope with various types of properties by adjusting the output layer. In addition, this method cannot be applied if some neurons have negative values. For instance, this method cannot be applied in hidden layers if the used activation function returns negative values such as sigmoid and Leaky Relu. For the same reason, the irst hidden layer cannot be abstracted if the inputs are negative. An example demonstrating this case is given in Fig. 8, where is an input, is the output.

The NN in Fig. 8.b is generated using Elboher et al. 's method [START_REF] Yisrael Elboher | An abstraction-based framework for neural network veriication[END_REF], which is supposed to be an abstraction of the original model of Fig. 8.a. Both and use the activation function on the hidden layer. Although for negative inputs the output of is always zero: ∀ ≤ 0, = 0, the output of is always positive, for instance, for = -1, = 3, thus the condition of the over-approximation ∀ ∈ : N () ≥ N () does not hold.

The NN bisimulation method proposed in [START_REF] Prabhakar | Bisimulations for neural network reduction[END_REF] guarantees the equivalence between abstract and original models, thus ofers an exact abstraction. However, the set of conditions are hard to satisfy on real neural network, especially the condition on weights. On the other hand, the relaxed version, NN--bisimulation, looks more feasible but needs further improvements to keep trace of the veriied property on the abstract model and lift it to provide guarantees on the original network.

In [START_REF] Shriver | Refactoring neural networks for veriication[END_REF], Shriver et al. propose an eicient approach with a dedicated tool, called R4V, to simplify and compress NN models. The wide experimental study they performed with diferent veriication tools and data sets shows that R4V ofers actual beneits to overcome the limitations of some NN veriication techniques. However, this method enables to verify properties on the refactored model and does not propose a way to lift these guarantees to the original model. In other words, it does not provide any guarantee of whether the property holds on the original model.

Regarding the challenges of neural network veriication, developing a new general approach that overcomes the issues related to the existing abstraction methods mentioned above is necessary. The works [START_REF] Ashok | Deepabstract: Neural network abstraction for accelerating veriication[END_REF][START_REF] Prabhakar | Bisimulations for neural network reduction[END_REF][START_REF] Shriver | Refactoring neural networks for veriication[END_REF] could be adopted and combined with some heuristics to select candidate neurons to be merged. For instance, the -bisimulation method [START_REF] Prabhakar | Bisimulations for neural network reduction[END_REF] can be used to select similar nodes by analyzing their incoming weights. The approach in [START_REF] Ashok | Deepabstract: Neural network abstraction for accelerating veriication[END_REF] can be adapted using discretization of the input region, so that the nodes that are close to each other (in the same cluster) are good candidates for abstraction.

While the technique in [START_REF] Yisrael Elboher | An abstraction-based framework for neural network veriication[END_REF] ensures that N () ≤ N (), the three methods presented in [START_REF] Boudardara | Interval Weight-Based Abstraction for Neural Network Veriication[END_REF][START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF][START_REF] Sotoudeh | Abstract Neural Networks[END_REF] go further by guaranteeing that the output of the original network is always included within the output range of the obtained abstract network, i.e., N () ∈ N (). However, it is necessary to conduct a comparative study to assess the performance of these methods. On the other hand, an abstract network obtained using DeepAbstract [START_REF] Ashok | Deepabstract: Neural network abstraction for accelerating veriication[END_REF] can be used only to verify the robustness of the model on inputs within the set of images that is used during the clustering phase. The last column of Table 1 summarizes the relation between the original and the abstract networks using diferent methods.

CONCLUSION

In this work, we discussed the problem of neural network veriication and we presented diferent existing techniques used to solve this problem. We showed that the abstraction of neural networks can be used to help tackle the non-linearity and the complexity of the generated models. Abstraction of neural networks can be applied in two levels: abstracting the activation function and reducing the network's size (model reduction). While the abstraction of activation functions aims to over-approximate the non-linear activation functions with linear constraints, model reduction is used to reduce the number of neurons of the network. Both categories are applied to improve the veriication process as a whole. The abstraction has to be sound, meaning that the desired behavior of the original model must be maintained. In this paper we focused more on model reduction methods since, to the best of our knowledge, no survey about neural networks reduction for veriication purposes has been introduced.

While the main focus of this work is on the application of abstraction methods to feed-forward neural networks, discussing their advantages, limitations, and the formal guarantees provided by each model reduction method, we also addressed the perspectives and potential applicability of these methods to other types of NNs, including convolutional neural networks (CNNs) and recurrent neural networks (RNNs).

Fig. 1 .

 1 Fig. 1. Example of a neural network

Fig. 3 .

 3 Fig.3. An example of state-space explosion. For two Relu nodes, case spliting leads to four linear subproblems.

Fig. 4 .

 4 Fig. 4. The activation function Sigmoid () and its abstraction in ∈ [-2, 2]. The solid line represents = () and each small region (yellow rectangles) is an over-approximation of [51].

Fig. 5 .Fig. 6 .

 56 Fig. 5. Relu activation function abstractions using diferent abstract domains. The ( = ()) is represented by the green line and its over-approximation on the range ∈ [, ] by the blue filled area.

( 1 )

 1 For every ∈ , calculate the value () of each neuron in , (2) Apply K-means to split each layer into clusters. Let denote the set of clusters of , (3) For each cluster ∈ : (a) Determine the representative neuron , (b) Calculate the corresponding outgoing weights of :

Fig. 8 .

 8 Fig. 8. Counterexample of Elboher et al. [17] abstraction method

  . Year Supported AFs Veriication methods

						Evaluation on Guarantees of the
							reduced model
	R4V [53]		2019	Relu	Relupex[31],	DAVE-2[4],	None
					ERAN[55],	DroNet[44]
					Neurify[65],
					Planet[16]
	INN [50]		2019	Relu	MILP [43]	ACAS Xu [31] N () ∈ N ()
	ANN [58]		2020	Relu,	-	-	N () ∈ N ()
				Leaky Relu 5
	DeepAbstract [2] 2020	Relu	ERAN	MNIST[36]	Depends on the
							data set
	Elboher et al. [17] 2020	Relu	Marabou[32] ACAS Xu [31] N () ≤ N ()
	Bisimulation [49] 2021	Relu	-	-	N ≡ N 6
	Boudardara	et	2022	Relu, Tanh	IBP[68]	ACAS Xu [31] N () ∈ N ()
	al. [7]

Whenever the method returns that the property holds, it indeed holds on the system.

The veriication method never returns "Unknown".

ACM Trans. Embedd. Comput. Syst.

∈ : N ( 0 ) = () : ∥ -0 ∥ ≤ (N ()) : N () = ACM Trans. Embedd. Comput. Syst.

An abstract domain is a set of logical constraints that deine a geometric shape. The most popular abstract domains are: box (or Interval), zonotope and polyhedra. For example, a zonotope abstract domain[START_REF] Khalil Ghorbal | The zonotope abstract domain taylor1+[END_REF] is deined by a set of constraints , s.t: = + =1 , where ∈ [ , ] is an error term and , are constants.

Available at https://github.com/eth-sri/ERAN.

The authors claim that the method can be adjusted to support other activation function

The abstract network is equivalent to the original one when bisimulation is used which is not the case for -bisimulation

Supplementary details are needed to apply the other methods. For example DeepAbstract[START_REF] Ashok | Deepabstract: Neural network abstraction for accelerating veriication[END_REF] needs a data set for the clustering algorithm. ACM Trans. Embedd. Comput. Syst.

ACKNOWLEDGMENTS

This research work is funded by the French program žInvestissements d'Avenirž and is part of the French collaborative project TASV (Train Autonome Service Voyageurs), with SNCF, Alstom Crespin, Thales, Bosch, and Spirops


Amélie Gonzalez
email: amelie.gonzalez@inria.fr

Djob Mvondo

David Bromberg
email: david.bromberg@inria.fr

Takeaways of Implementing a Native Rust UDP Tunneling Network Driver in the Linux Kernel

C is the primary programming language used in the Linux kernel. Recently, the Linux developer community oversaw the experimental addition of Rust into the kernel's build system. Networking is one of the areas often mentioned when discussing the adoption of Rust. In networking, both perfect memory management and performance are critical.

In this paper, we present a Rust UDP tunneling driver for Linux, which provides UDP encapsulation between two peers. We use this driver to discuss design considerations of writing Rust networking code for Linux. We then compare the performance of our driver against a similar driver written in C. We find that our Rust driver performs slightly worse on a gigabit link for both latency (+0.1906%, p-value = 1.464e-15) and throughput (-0.00090%, p-value = 6.004e-5). We then discuss potential causes for that loss.

Introduction

Since its creation by Denies Ritchie in 1972, C has remained the standard programming language for the development of operating systems. It was created with the goal of reducing the amount of assembly used for programming UNIX. C gives developers access to low-level functionality, like bitwise operators, pointers management, manual memory management, and inline assembly. However, improper usage of C is known to lead to unwanted memory issues.

The most representative example of using C for an operating system is the Linux kernel, which also features some assembly language code. It also showcases the issues around writing C source code: dangling pointers, pointers used after free, leaked memory, are all issues that have been found in Linux in particular [START_REF] Chou | An Empirical Study of Operating Systems Errors[END_REF][START_REF] Palix | Faults in Linux: Ten Years Later[END_REF] for decades. Linux is not alone in that respect, but despite its rigorous peer-review process for patch submission, errors still end up into the code base.

Other languages have emerged since C such as Rust, which provides access to similar, low-level operations while also imposing strict verification of its memory safety model at compile-time, and handling as much memory management as possible for its developer. It benefits from being a compiled language, while restricting the potential damage stemming from improper memory management.

Rust is a contender in the realm of programming system languages. Operating systems have already been written with it (Redox [START_REF] Redox | The Redox Operating System[END_REF], Tock [START_REF] Levy | Multiprogramming a 64kB Computer Safely and Efficiently[END_REF], RedLeaf [START_REF] Vikram Narayanan | RedLeaf: Isolation and Communication in a Safe Operating System[END_REF], Theseus [START_REF] Boos | Theseus: an Experiment in Operating System Structure and State Management[END_REF]), and it can be used in Linux for driver development since version 6.1-rc1. Rust has been used to explore the development of Linux drivers for storage devices [START_REF] Hindborg | Linux Rust NVMe Driver Status Update[END_REF], or direct rendering media [START_REF] Lina | Tales of the M1 GPU[END_REF]. Another area of interest for Rust usage is networking; network drivers allocate and deallocate chunks of memory according to inbound and outbound packets that fly between the kernel and network cards at extremely high speeds. Maintaining performance, all the while avoiding memory handling errors, is critical, and encourages using a language like Rust. These kinds of errors may have catastrophic consequences: they may either freeze portions of the kernel, or kill it entirely [START_REF] Gu | Characterization of linux kernel behavior under errors[END_REF].

In this paper, we evaluate the use of Rust against that of C for networking drivers in Linux, notably in terms of performance impact. We focus our study on the development of a UDP tunneling driver. Developing such a driver has the advantage of requiring no hardware considerations. At the same time, UDP tunneling is a key building block of technologies such as virtual private networks. UDP is preferred for tunneling over TCP to avoid TCP-over-TCP retransmissions snowballing, or "TCP meltdown". UDP is also simpler of a transmission protocol, as it performs its task with "best effort" guarantees.

We implemented a native Rust UDP tunneling driver in Linux, by extending proposals for code providing access to networking features in Rust for Linux 1 . We then evaluated this driver against another version, written in C. We evaluated both throughput and latency for both drivers over a gigabit duplex link. Our results suggest that Rust suffers from a very slight performance penalty when compared to C, while remaining very close from its level of performance. The Rust driver transfers an average of 914.78 Mbps with an average latency of 127.1 𝜇𝑠, while the C driver transfers 915.79 Mbps for an average latency of 126.8 𝜇𝑠.

Background

We will first discuss the use of Rust as a systems programming language, followed by a presentation of the experimental project which brought support for it in Linux, and, finally, the features we targeted for our driver, in the original Linux kernel C code. For the sake of remaining legible, we will not delve too deeply into the behavior of Rust. Readers already familiar with the language can focus on its integration in Linux, while others will benefit from our explanation of the core memory safety rules of Rust.

Rust for Systems Programming

Rust [START_REF]The Rust Programming Language[END_REF][START_REF] Hoare | Project Servo. Mozilla Annual Summit[END_REF] promises to address the memory safety problems of previous programming languages by combining two concepts baked into its type system: ownership and borrowing. The owner of a memory allocation (a structure, enumeration, scope of code, . . . ) oversees its initialization, destruction (as soon as the compiler deems it possible), and may move the ownership to another owner. It can also provide references to the owned allocation, which may allow modifications or not. The enforcement of memory safety relies on tracking the lifetime of all allocations at compile-time, and checking that at no time there exists a mutable reference alongside any other reference, mutable or not, to the same allocation.

Rust also provides traits: sets of properties a type can implement, which guarantee to the compiler, that said type behaves a certain way. For example, the Copy trait guarantees that a byte-per-byte copy of a memory allocation of a type that implements it will results in an identical copy of the previous allocation being created. Traits can be combined with generics to provide these features in combination with other types that can, themselves, verify certain constraints. If you implement Add<T: Foo> over a type Bar, you provide an implementation of addition between your type and any type that implements the trait Foo.

There is however a caveat to Rust's safety when programming operating systems and drivers. Since an operating system performs operations such a Direct Memory Access or context switching, there must remain within the code base of a Rust operating system a fraction of source code that cannot comply with compiler checks [START_REF] Levy | The Case for Writing a Kernel in Rust[END_REF]. Another example is memory-mapped I/O operations: an operating system will have to write at arbitrary addresses in the memory to interact with hardware. In order for developers to perform such operations, Rust has an unsafe keyword. Programmers mark functions or blocks of code with unsafe to tell the compiler to forego compile-time memory safety checks. In these situations, as long as unsafe code is guaranteed to be sound by the developer, all other safety guarantees of the language are preserved. This is one of the challenges that comes with programming using unsafe in Rust: only unsafe code is known to be able to cause memory problems, but those could manifest somewhere else, including safe code [START_REF] Qin | Understanding Memory and Thread Safety Practices and Issues in Real-World Rust Programs[END_REF].

Rust for Linux

The Rust API provided in Linux combines core Rust language code for primitive types and standard types implemented by Rust for Linux developers, as well as abstractions built around regular C kernel code called through FFI. Bindings to that C code are mechanically generated using bindgen [START_REF]rust-bingen -Automatically generates Rust FFI bindings to C (and some C++) libraries[END_REF]. These bindings are then called through unsafe Rust code encapsulated in abstractions that provide features for the Rust side of the kernel. In Figure 1, which summarizes this mechanism, we can see a divide between the Rust and C sides of Linux kernel code. Features need to be exposed as bindings, and we have to manually add code in the abstraction layer before Rust drivers can use them. Otherwise, driver developers would need to interact directly with unsafe code, which could negate the safety benefits of Rust.

In Rust, the conventional way to hide unsafe from endusers of your code is through abstractions. Abstractions wrap your unsafe code and perform conversions and checks [START_REF]FFI -The Rustonomicon[END_REF]. This is especially useful for unsafe code performing foreign function interface (FFI) calls.

Linux C code cannot be verified by the Rust compiler. Rust drivers which use the safe interface provided by abstractions have to trust that the underlying C code and the abstractions are not faulty. As long as the C code is safe, and unsafe Rust in the abstractions sound, all other Rust code should be safe [START_REF] Qin | Understanding Memory and Thread Safety Practices and Issues in Real-World Rust Programs[END_REF]. If abstractions are unsound, they might cause memory errors in the Rust drivers. If the C code mishandles memory, it needs to be fixed for the sake of the whole kernel. Fixing errors in C then returns both the C and Rust code to stability. In Linux, Rust developers are forced by style conventions to write a comment, above every unsafe block, about why their unsafe blocks are sound. Type invariants and unsafe function safety prerequisites must also be documented with comments.

Currently, the Rust for Linux (RFL) community focuses on abstractions for core kernel features such as file-system access [START_REF] Miculas | [END_REF], media peripherals [1], data structures [START_REF] Lina | [END_REF], etc.

At the time our work began, none of the few networking abstractions available provided features we required. The available abstractions only allowed to write simple network filters and create TCP sessions.

Linux and its Network Stack

Memory safety is critical in the net subsystem. Network drivers and the network stack have to manipulate packets as memory on the NIC, and later as memory in the kernel in the form of socket buffers. Improper handling could lead to out of bounds access, use-after-free errors, etc. These errors have catastrophic consequences in Linux, usually leading to kernel bugs (an entire subsystem going offline) at best, or kernel panics (entire and sudden crash of the operating system) at worse [START_REF] Gu | Characterization of linux kernel behavior under errors[END_REF].

Network tunnels are a key building block to create more complex network topology, such as virtual private networks (VPNs), so that computers which do not share a common network can still communicate over a shared, virtual, private network. Currently, the wireguard Linux kernel module provides VPN functionality using the WireGuard protocol [START_REF] Donenfeld | WireGuard: Next Generation Kernel Network Tunnel[END_REF].

Our Driver and Its Abstractions

As a first step in the exploration of the performance of Rust for native network drivers in Linux, we implemented a UDP tunneling driver written in Rust. Abstractions were necessary to provide these features in Rust. Since we wanted to write a UDP tunneling driver that is efficient, we decided to base our structure on WireGuard's kernel module. Wire-Guard is a state-of-the-art VPN protocol [START_REF] Donenfeld | WireGuard: Next Generation Kernel Network Tunnel[END_REF], and its kernel implementation has been thoroughly tested and checked.

Abstractions

In order to write the drivers, abstractions had to be incorporated on top of the source code made available by the RFL community. We based our work on the October 2022 pull request by Tomonori Fujita [START_REF] Fujita | rust: add initial netdevice support[END_REF]. who added a few methods to the wrapper around Linux's network device structure, and a stub for the network device operation factory. We only used and expanded said stub. Approximately 2500 more lines of Rust code were needed, for a total of under 4000 lines added in the rust sub-directory. We wrote 45 new wrapper structures, traits and enumerations in order to write our UDP tunneling network driver.

While we could consider upstreaming this work to the Linux kernel, the current policy is to merge code only if it has a user (i.e. a driver). For a driver to be accepted, it needs to provide features not already present in the kernel. We consider that this proof of concept driver does not fit the requirements to be upstreamed, and therefore the abstractions made alongside it cannot be either.

Initialization

When a C module is loaded, the kernel executes a callback provided in the module declaration that performs all initialization tasks. In Rust, this is represented as a method to be declared for the implementation of the trait Module over a type. That type is understood to represent your module, and is instantiated once when your module is loaded by the kernel, and dropped when the module is unloaded. The Here, we give examples of how we adapted this philosophy while designing our driver and abstractions.

Our driver declares a type in its top-level file that represents the module itself, which will simply hold the declaration of a Router NetLink type: an interface family you can define in a driver with custom implementation of operations such as interface creation, deletion, queue number gathering, and so on. These operations are useful for drivers that want to provide features not backed immediately by hardware, such as virtual private networks, TUN, TAP, etc.

To provide the set of functions that define a RTNL type for our driver, we use the concept of traits in Rust, by creating a trait called LinkOperations which is implemented for one of our types. The trait handles fully abstracting away all bindings from Rust users, only exposing data types that are abstractions around the argument types used in the C version of these callbacks. The implementer type is then passed to a factory type, which will perform the work of creating a descriptor in memory, and register it with the C kernel API. We hold an instance of the factory specialized over our RTNL implementer type to show that the registration is effective.

Before an interface can be shown to users of the system, it has to register itself to the kernel. We use one of the RTNL callback functions we just declared to perform that operation, through a wrapping around Linux's register_netdevice. We name that wrapper method Device::register_locked (indicating that an environment lock for RTNL data is locked before the method is called). Device configuration methods can be created by wrapping around C bindings, and simply extracting arguments, as shown in Listing 1. Methods like to_result are made available by the foundation work of RFL developers. Here, it helps transform errno error numbers to a Rust Result enumeration. We aimed to remain idiomatic in our driver to comply with the RFL project coding style.

Network Interface Private Data

Every network interface in Linux can have an area of memory allocated when it is initially created, for the purpose of storing its own information. That area of memory lies at the first 32-byte aligned address beyond the net_device 1 l e t wrap = unsafe { dev . g e t _ p r i v _ d a t a : : < Data > ( ) ? } ; 2 l e t p r e f = wrap . i n i t i a l i z e _ w i t h ( Data : : new ( dev ) ) ? ; 3 / / Or , i f s u r e t h a t i n i t i a l i z a t i o n h a p p e n e d 4 l e t p r e f = unsafe { wrap . a s s u m e _ i n i t i a l i z e d ( ) } ;

Listing 2. Access to the Private Data Area in Rust structure, and takes the size declared in the RTNL descriptor registered for our type. It can be accessed in C with netdev_priv(), which returns a pointer.

In our Rust driver, we use that memory area to store various information about the peer at the other end of our tunnel, as well as a buffer of socket buffers received and waiting to be processed. Accessing that memory area comes with challenges in Rust. We need to return a mutable reference to a memory area of an unconstrained size at an arbitrary address, that may or may not have been initialized. Our RTNL Rust trait declares an associated type constrained to implement the Sized trait (indicating a size known at compile time), which is used to determine the size of private area allocation. We then use a structure called NetPrivateData which can be generic over any Sized type, and wraps around the pointer returned by netdev_priv. In the driver, we then decide whether or not to initialize the area with an instance of the private data type, or assume initialization. Because we cannot ensure that the area is already initialized, or that a zeroed memory area (since the entire area is zero-allocated by the kernel) makes sense for the Rust private data type, both of these operations are unsafe. They require that the driver programmer make an informed and conscious decision to use a potentially uninitialized area, as well as what type they provide. An example is given in Listing 2.

In our driver, we know that our access and usage of the device's private data area is safe because the kernel guarantees the order in which RTNL, and other callbacks are called, and we can guarantee that initialization of the memory area happens (and does not fail) before it is used in the next callbacks. This is also true in for network drivers written in C.

Processing Socket Buffers

Linux's network system manipulates packets through a structure called socket buffers, which contains metadata parsed from packet data, and various pointers to a memory area that contain the actual contents of the packet. Manipulation of said pointers allow drivers to rewrite and cut parts of a packet, such as headers.

The networking API grants network drivers access to socket buffer through pointers. The Rust pendant is a mutable reference to a socket buffer abstraction structure created from a pointer at the abstraction border. Said structure reference is passed in the data path of our driver, and wrapper methods help us manipulate the data buffer pointers to remove encapsulation headers at reception. The current implementation of that abstraction in the kernel::net module means we cannot drop socket buffers (as happens upon errors detected in the data path) as easily as we would in C. Rust's type system prevents us from dropping a instance of an object through a reference to it, which is all that is available to drivers in the data path.

In order to compromise on that restriction, we implemented manual drop methods that would free the structure on the kernel side through a mutable reference. This violates the invariant placed on our socket buffer abstraction: "during the lifetime of an instance, the underlying kernel structure must exist and contain a valid socket buffer". The driver tested at the time of submission had no safeguard against a reuse of the abstraction's reference after a drop call, we return from the data path in our driver to avoid reuse. This leaves the type invariant still violated, as the abstraction instance remains valid and potentially usable by other parts of the program.

An actual solution to that issue would involve passing the socket buffer abstraction as an owned instance to functions in the data path. This is possible in one way, if we define the wrapper to contain a pointer to the C socket buffer, instead of being a Rust representation of the C socket buffer structure. Functions in the data path therefore have access to an owner instance (which contains the C pointer), which they are free to drop. For functions branching out from the main chain of function calls, the instance ownership can be moved to these functions, which would then return the instance back if it has not been dropped. Another option for auxiliary functions is to obtain a mutable reference, and return a code signaling to the instance owner (i.e. the main data path caller function) that the socket buffer must be dropped. An improved version of our driver will test this design approach.

Socket buffers show how Rust's type system forces developers of safe wrappers to carefully consider the way data is handled, and how difficult that design step can be.

Evaluation

We will present the final rounds of evaluation against the current version of the driver, our setup, results, and interpretation. The evaluation will cover performance in terms of network latency and throughput for our Rust driver, a C implementation, and the link they use for tunneling.

Evaluation Setup

We used two Intel NUCs, model NUC7i7BNH, connected to a Cisco Catalyst 2960-S switch with category 5.E RJ45 cables. They each have 4 Intel Core i7-7567U CPUs, paced at 3.50 GHz. Their NIC is an Intel Corp. Ethernet Connection I219-V, revision 21. The link is negotiated as 1000 Base-T full duplex. We used a build of Linux 6.3.0, based on the configuration of Linux 4. Ubuntu 18.04.6. The configuration was updated with default values and we enabled Rust and our modules. Our tree is based on RFL's rust branch (commit bc22545f).

Performance tests consist of a latency test and a throughput test. Latency is measured with the netperf [START_REF] Jones | Care and Feeding of Netperf 2[END_REF] utility's TCP_RR test over 100 runs consisting of 5 seconds of warmup with the ping command from the iputils suite (version iputils-s20161105), 60 seconds of measurement, and 5 seconds of cooldown. The mean latency, 50%, 90% and 99% percentiles are taken each run. Throughput is measured with netperf's TCP_STREAM test, with the same number of runs, structured the same way. Average throughput is measured each run. For latency, netperf reports percentiles with three significant figures, but keeps five to compute the mean. We round that mean to only keep three significant figures. Throughput means are kept at five significant figures as given by netperf, considering that it gives a precision to the tens of kilobits per second. We do not run download tests in both directions because our setup is symmetric.

As for our drivers, we argue that our C and Rust drivers are comparable for the following reasons: the Rust driver makes use of the same C Linux networking API provided by Linux, but wrapped in safe abstractions. When writing the C driver, we simply called the same methods wrapped for the Rust side, in the same order, for the same processing steps.

Benchmark Results

In out experiments, the baseline represents performance of the link used to connect both test devices.

Latency. Summarized results for the latency tests are provided in Table 1. These values are computed over the output mean for each individual test run. For latency, lower is better. Overall, the C and Rust drivers are very close to one another in terms of latency, with only a slight gap of under half a microsecond between their means. A t-test shows that this difference is significant over our n = 4000 points, with p-value = 1.464e-15. Our Rust driver has slightly worse minimal and maximal observed latency as well. The standard derivation 𝜎 is slightly higher for C by about 0.03 ns, but we cannot reject the hypothesis of a statistical error (p = 0.9449). We can therefore assume the latency distributions of both drivers share the same standard derivation. Both drivers are slower than the baseline. These results concord with Figure 2, which shows that the trend for latency in Rust is slightly higher than C, not only in terms of means, but also medians, as well as 90 th and 99 th percentile. These results, in particular the significant statistical difference observed for latency means, suggests a slightly higher processing time taken in the data path of our driver. That difference could be attributed to poor programming on our part, as well as the presence of some performance concerns observed by the RFL community, which we discuss in subsection 4.3.

Throughput. Throughput measurements statistics presented in Table 2 show very close performance between the Rust and C drivers. The last column of that table shows the number of points in each category outside of the 95% confidence interval.

The baseline interface has throughput values measured between 930.95 Mbps and 934.39 Mbps. With abnormal values removed, the C driver transfers around 915.79 Mbps, while the Rust driver is a bit behind, with only 915.78 Mbps on average. The bitrate variation between both drivers is around ten kilobits per second on average. Statistical testing show that this difference is still significant (p = 6.004e-5). We interpret this to mean that our Rust driver reaches the same level of performance as the C one, but with a small overhead of about 0.00090%. However, Rust usage in our driver, whether from the language or our use of it, slows down traffic ever so slightly.

Overall, our Rust driver, as a whole, is slower in both latency and throughput.

Missing Bits & Limitations

One limitation identified in our tests is that a one gigabit per second of throughput is not enough to put devices involved in the test under stress. This was the best bare-metal hardware available to us at the time. It is very clear to us that further experiments must take place with better hardware.

Regarding our driver and its integration within Rust for Linux, we discern problems existing with our current implementation (missing features, or shortcuts taken to counter strict Rust typing), as well as known limitations of RFL as it exists today.

Missing Features. It is currently impossible to delete an interface created with our Rust driver. Reference counting is improperly handled, as we do not delete all resources in the private data area, including a counted reference to the device itself. Any attempt will result in the kernel's entire network subsystem freezing while waiting for references to be freed. We currently rely on shortcuts taken in the Rust driver code because of time constraints. One of them is a cast from a socket buffer reference to a pointer, which is converted back through unsafe code later on. This shortcut was taken to get around lifetimes of socket buffers and quickly put together a working driver. While this stems from our trying to push problems to later, it illustrates the fact that Rust's strict security model may feel like an obstacle to programmers, who may be tempted to use and abuse unsafe to bypass it.

Current limits of RFL. A limitation we can attribute to using Rust in Linux is the use of unsafe in our driver for a direct call to the binding of udp_tunnel_xmit_skb (a method of the udp_tunnel kernel module). It is currently impossible to write abstractions for udp_tunnel in the kernel crate of the rust subsystem. Said crate is linked into the standalone vmlinux kernel binary, while udp_tunnel and its method stay alone in their own module binary file. The linker cannot resolve the call to a binding to udp_tunnel_xmit_skb. The only solutions appear to be either writing a kernel module that uses bindings to provide abstractions to the C UDP tunneling module in Rust, or otherwise rewriting udp_tunnel using Rust networking abstractions which do not exist at the moment.

Furthermore, we can only empirically verify that our Rust code is valid and provides the wanted features. While there is existing work trying to create verification tools for unsafe Rust [START_REF] Qin | Understanding Memory and Thread Safety Practices and Issues in Real-World Rust Programs[END_REF], it is not known whether they can handle constraints specific to methods calls via FFI. None of the abstractions written for Rust for Linux are mechanically and rigorously proven sound.

Finally, the problem of inlining through FFI is Rust is still under investigation [2]. Inlining by LLVM is automatically done within Rust code. However, the current Rust build infrastructure of the kernel makes it such that inlining is not available between C code compiled with a C front-end of LLVM (eg. clang), and a Rust front-end of LLVM (eg. rustc). Link Time Optimization (LTO) would need to be enabled in the build system. Developers of RFL have already discussed supporting that feature [2].

Other Driver proposals and Related Work

Usage of Rust in systems programming is not new, even in terms of networking. However, we contribute a first look into using Rust for developing networking drivers in Linux.

Other Abstraction and Driver Proposals

Others have undertaken the task of making network drivers for Linux in Rust, albeit with different goals.

In July 2021, Finn Behrens opened a request to inspect and merge his RTNL and network device manipulation abstractions [3]. It proposed changes that now require rewrites of code later merged in Rust for Linux's experimental tree.

Tomonori Fujita developed his own e1000 out-of-tree Rust driver [START_REF] Fujita | fujita/rust-e1000[END_REF]. It uses direct calls to bindings, and relies on his original October 2022 RFL proposal [START_REF] Fujita | rust: add initial netdevice support[END_REF]. He posted a first draft of his more complete networking abstraction patch set in May 2023. The patch set covers basic representation of network devices, network namespaces, handling of socket buffers, network device operations and Ethernet operations. While there is an intersection with our own abstractions, it is slim. Tomonori Fujita focuses on writing hardware drivers, while we wanted to focus on tunneling. His proposal is currently being reviewed by the netdev community [START_REF] Fujita | [END_REF]. We chose not to rewrite our code until the Linux community decides on what set of abstractions to adopt into mainline.

Related Work

Emmerich et al. have previously made network drivers for Linux in higher level languages [START_REF] Emmerich | The Case for Writing Network Drivers in High-Level Programming Languages[END_REF]. Rust was included in that list. Their drivers all resided in userland, and used kernel bypass with DPDK alongside custom-made wrappers. They also showed that Rust reaches performance close to, but ever so slightly under C. They also address the cost of safety in Rust to explain that performance gap.

Redox [START_REF] Redox | The Redox Operating System[END_REF] is a general purpose UNIX-like operating system developed in Rust. It is still actively developed, and can provide a functional desktop environment. Its developers have chosen a micro-kernel approach, and run their drivers in userspace. Redox is network-capable. The work of Emmerich et al. also evaluated Redox's networking. They noted, at the time, that these drivers were not optimized and a poor performance compared to their C userspace driver. It could be interesting to study the current performance of Redox's network stack [START_REF]redox-os/netstack[END_REF], which is based on smolTCP [START_REF]smoltcp-rs/smoltcp: a smol tcp/ip stack[END_REF].

Tock [START_REF] Levy | Multiprogramming a 64kB Computer Safely and Efficiently[END_REF] is an operating system for embedded hardware. It is the fruit of research around the benefits of writing kernels in Rust [START_REF] Levy | The Case for Writing a Kernel in Rust[END_REF]. In their design, however, Levy et al. focused on devices such as security keys, operations such as USB access or DMA, and did not discuss design considerations or examples of networking in Tock.

Isolation of trusted and verified code has been explored, including in Rust [START_REF] Burtsev | Isolation in Rust: What is Missing?[END_REF][START_REF] Vikram Narayanan | RedLeaf: Isolation and Communication in a Safe Operating System[END_REF]. Kirth et al. developed PKRU-Safe [START_REF] Kirth | PKRU-Safe: Automatically Locking down the Heap between Safe and Unsafe Languages[END_REF], a combination of a compiler plugin and allocator for the Rust toolchain that leveraged Intel Memory Protection Keys (MPK) to protect safe memory from potential errors or exploits stemming from the unsafe code. With their design, developers annotate frontiers between unsafe and safe code. Combined with profiling, PKRU-Safe can determine which allocations are used in the unsafe region, and which are not. These mechanisms could be applicable in our situation, with heavy modification of the Linux build system. Sandcrust [START_REF] Lamowski | Sandcrust: Automatic Sandboxing of Unsafe Components in Rust[END_REF] is a sandboxing system built around process isolation and accessible in Rust with a macro crate. The approach involves serialization and transmission of data through pipes, which incurs high overhead. Sandcrust relies on process isolation, meaning it can only exist above the kernel.

Conclusion & Further Work

In this paper, we present our work on a UDP tunneling driver written in Rust in Linux. Rust is especially useful for network drivers, as they need to manage memory perfectly while also remaining extremely efficient.

Overall, once abstractions are available to use the kernel's networking API, writing a network driver in Rust in Linux is possible. Yet, we note that Rust's type system and safety checks make that process complex, and requires a lot of careful planning to safely wrap C API. Handling pointer structures, such as with socket buffers, is especially complicated. We show that our Rust driver performs only very slightly worse in terms of performance than a C equivalent. The Rust driver exhibits a statistically significant difference of means across samples for both latency (+0.1892% compared to the C driver) and throughput (-0.0011%) on our gigabit link.

We envision exploring our driver scalability, notably on better hardware and bigger links. These bigger links (10, 25 or even 100 gigabit per second) will likely create higher CPU stress and allow us to get a clearer picture of current processing bottlenecks of Rust networking in Linux.

At the same time, we will address shortcuts and missing features discussed above, with the goal of closing the performance gap with C while providing as safe a driver as possible.

Figure 1 .

 1 Figure 1. Schematic View of Interactions Between Rust Drivers, Rust Abstractions, and Original Linux C Code

1Listing 1 .

 1 pub fn r e g i s t e r _ l o c k e d (&mut s e l f ) -> Result { 2 t o _ r e s u l t ( unsafe { 3 b i n d i n g s : : r e g i s t e r _ n e t d e v i c e ( s e l f . 0 . g e t ( Device Registration Method implementation of the Drop trait is the idiomatic Rust equivalent to a C module exit callback. The RFL community has already provided foundations for module declaration that implement basic Linux API in Rust in an idiomatic fashion.

Figure 2 .

 2 Figure 2. Latency Metrics for the C and Rust Drivers

Table 1 .

 1 15.0-197-generic available for Latency Measurements in Microseconds

	Interface Mean Min Max 𝜎	Points outside
		95% interval
	Baseline 122.2 117 127 1.10	176
	C 126.8 120 132 1.37	273
	Rust 127.1 121 134 1.34	176
	Values computed over n = 4000 latency mean
	measurements.

Table 2 .

 2 Throughput Statistics in Mbps

Code available at https://gitlab.inria.fr/WIDE/linux-rust-tunnel-driver, tag