dataesr/scientific-paragraphs-categorization huggingface dataset:
In this paper, the topology consists of N TCP sources, with the same propagation delay connected to a destination node through a router (see Figure  4 ). This simple topology is due to : 1. The high complexity behavior of a fleet of UAVs in which each UAV can be sender, receiver and router; 2. The difficulty for such systems to derive a reliable and representative network modeling from scratch. To implement an Intrusion Detection System (IDS) according to the network topology presented previously, the estimation module inserts itself between the other modules as follows: the estimation system receives noisy measurements (e. g. probability of packet, queue of the router buffer) as inputs from the sensors, then merges this data using the TCP model of the network to compute a solution to the estimation problem.
UAV ad hoc network hybrid platform In order to validate our new traffic estimator in real traffic conditions, we use a hybrid experimental system to take advantage of the low cost of a simulation while still obtaining the accuracy of a real protocol stack. We have been using virtual machine implementations to deal with the entire complexity of the Linux operating system. The traces used to generate UAV mobility patterns were extracted from real traces so that physical related factors could be as realistic as possible. The system we have been using to evaluate protocols is divided into several parts. It includes a set of tools that can deal with several scenarios: a hypervisor to run the virtual machines, measurement tools and a framework to allow virtual machines to communicate through a virtual wireless medium.
We chose to use VirtualBox as a visualization tool because it is an easy-to-use and efficient hypervisor. The virtualized system is a 12. 04 version Ubuntu, working with the It is a framework that interfaces a Linux-based system with an OM-NeT++ simulation. OMNeT++ is a powerful network simulator which simulates several systems and normalized protocols. An illustration of this system is shown in Figure  6. In  [45] , more details about this hybrid tool can be found. The main advantage of using such a hybrid simulator is to extract any characteristics from the simulation and to inject them into the Simulink design directly. The theoretical model is then used under real traffic conditions and not only theoretical stimulus. The advantage of such an evaluation is to take into account the huge variability and complexity of real traffic.
Discussion on traffic reconstruction performances These results look promising given that the estimator simulated with Matlab Simulink is able to detect the different intrusions rapidly and with an accurate threshold. The delay in the detection is negligible and the estimator can make an accurate distinction between legitimate traffic and traffic with intrusions. Consequently, this is a first promising result for intrusion detection system design applied to drone fleet network. In the next section, we will consider a more complex environment. Indeed, we will deploy our IDS in a real drone system and analyze if the first promising results we got with both our hybrid simulation / emulation platform and the Matlab Simulink estimator are confirmed.
Intrusion Detection System Implementation In this section, we describe how we have implemented in a real environment the IDS methodology described in Section 3 and validated in Section 4. This real environment is built on real communications between a drone (Parrot ARDrone) and a dedicated Ground Control Station (GCS). The GCS is performed with Paparazzi software. A malicious data will be generated to stress the communications between the GCS and the drone and we will be able to perform a real validation of our IDS methodology.
Onboard and ground systems cannot be mixed, consequently, there are two types of control system. Moreover, the first available systems were proprietary closed. Today they are challenged by the open source community that proposed opened hardware and source code solutions (cf. Paparazzi project at: https://wiki. paparazziuav. org/). Open source autopilots are mainly used by universities, laboratories for research and development activities such as our IDS system proposed by ENAC. These systems are constantly improved by its community members.
IDS method implementation into Paparazzi Paparazzi software is developed in a modular fashion, such that it allows easy development of individual function blocks. To be specific, the communication between GCS and test UAV node is done by a Linker module. Our IDS software is designed to first intercept / sniff packets between the Linker module and the UAV, then apply WLM analysis, in real-time, on collected packets and compare resulted signature with a bank of signatures to determine the nature of the traffic. Then, according to the attack information, the corresponding model is chosen from a bank of models to perform signature characterization of the attack. The aforementioned WLM analysis Matlab toolbox has been then implemented in C++ environment for the best performance and easiest implementation into different platforms.
This first implementation of the WLM analysis tool is an independent program running in Windows/Linux environment and it is to demonstrate the functionality and performance of this algorithm. Besides the calculation of signatures, the program also visualizes the results by calling open-source libraries: MathGL 2  and FLTK  3  and plotting the result in a new window. This allows us to have a global perspective of how the results will differ when malicious traffic is injected into the communication, before the actual acquisition of the bank of signatures. Once we verified the steady performance of our WLM analysis module, the bank of signatures can be acquired by feeding the tool with collected packets from known normal or malicious traffics and recording the resulted signatures. To have a more general understanding of different traffics, we consider an extra degree of freedom: acquisition period, in addition to moments of analysis and time scales (sampling frequencies).
The CompCert compiler is programmed (mostly) and verified (fully) using the Coq proof assistant  [Inria 2019 ]. The compiler itself is written as a sequence of 20 compiler passes, from the CompCertC source language down to assembly, going through eight intermediate languages (see Figure  11 ). Among them are standard optimization passes performing mainly instruction selection, dataflow analysis (used for constant propagation, common subexpression elimination and redundancy elimination), register allocation and function inlining. Compiler passes are either programmed and verified in Coq, or programmed in OCaml and verified in Coq, using translation validation. The correctness theorem states that the compilation is semantics-preserving, i. e. , does not introduce bugs in compiled programs. This main theorem decomposes into correctness theorems for each of the 20 compilation passes.
Again, each pass decomposes into elementary passes that are proved correct. A general theorem states the correctness of the sequential composition of two passes from the correctness of both passes. CompCert evolved significantly over the last 15 years, starting as an academic project and now being used in commercial settings. For example, CompCert was recently used in the certification of a highly safety-critical application  [Kästner et al. 2018]. With 100,000 lines of Coq and 6 person-years of effort, the CompCert proof is among the largest ever performed with a proof assistant. To make the question łDoes the CompCert compiler preserve security?ž precise, we must fix the notion of security we want to address. We focus on the specific setting of side-channel protection. More specifically, we consider łcryptographic constant-timež, a popular software-based countermeasure against timing-based and cache-based attacks.
This notion can be used to prove preservation of constanttime for a broad range of optimizations, and has been used to formally verify preservation of constant-time for a core language and compiler. This work raises the general question whether a realistic compiler like CompCert preserves cryptographic constant-time. All results presented in this paper have been mechanically verified using the Coq proof assistant. The complete Coq development is available as a supplementary material. The main contribution of this paper is a machine-checked proof that a mildly modified version of the CompCert compiler preserves cryptographic constant-time. To our best knowledge, our proof is the first of this kind, making CompCert the first formally verified secure compiler for a realistic programming language.
BACKGROUND ON THE COMPCERT VERIFIED C COMPILER CompCert  [Leroy 2009a ] is the first commercially available optimizing compiler that is formally verified. The CompCert compiler comes with a machine-checked correctness theorem, conducted using the Coq proof assistant [Inria 2019]; it states that the compilation does not introduce bugs in compiled programs. This section introduces the ingredients of the correctness proof of CompCert passes; they are further detailed in  [Leroy 2009b ]. First, the section describes the generic semantic framework used to define the formal semantics of the 10 languages of the compiler. Then, it details the proof techniques underlying the correctness lemmas. Last, it introduces memory injections that formalize how memory is transformed by compiler passes.
A trace is a list of events; this list may be finite or infinite. Small-step semantics of the CompCert languages are specified using a generic notion of a one-step transition relation → between a global environment G which does not change during execution, an initial program state S, a final program state S ′ and a trace t of input/output actions  [Leroy 2009b ]. Given an environment G, the transition from S to S ′ generates external events that are recorded in trace t. The definitions of the global environment and of the state differ from one language to another. They at least involve a local environment and a memory state M (shared by all the languages of the compiler). For example, in the RTL language 1  , the local environment is a  A diverging program execution observes infinite or finite traces (e.
g. , an infinite loop that does not observe external input/output events). Moreover, a generic notion of transition semantics is defined in CompCert. In addition to the type of program states, the type of global environments and the transition relation, the semantics defines two predicates representing the initial states of a program and the final states of a terminating program execution. The first predicate checks that the memory and global environment are initialized, and that there is a main function in P with a correct signature. In the remainder of this paper, for the sake of brevity, we omit the global environment G in the transition relations. G ⊢ S t - → S ′ (step transition) G ⊢ S t - → * S ′ (star transition) G ⊢ S t - → + S ′ (plus transition) G ⊢ S t - → n S ′ (counted transitions) G ⊢ S T -→ ∞ (infinite transitions).
Simulation Relations Between Program Executions In C and in CompCertC, the source language of CompCert, evaluation orders are not fully specified (meaning that the compiler is allowed to choose one of the possible evaluation orders). An example is an expression made of calls to several functions: the expression is safe and the calls can be evaluated in any order that the compiler may choose. CompCertC is the only non-deterministic language of CompCert in that respect. For this reason, the correctness theorem of CompCert is stated as follows: if the compiler produces code C from source S, without reporting a compile-time error, then every observable behavior of C is a possible behavior of S. The standard proof technique to conduct this proof is a backward simulation (i. e. , every behavior of C is also a behavior of S).
g. , an assignment including a division by zero that is detected as dead code by an optimization). Thus, in compiler verification, the correctness theorem only applies to safe programs (see Section 2. 1). For this reason, our new proof techniques only consider safe programs as well. Last, the most general forward-simulation diagram is defined in CompCert as follows. The correctness proof of a compiler pass from language L 1 to language L 2 relies on a forward simulation diagram shown in Figure  2  and expressed in the following theorem. Given a program P 1 and its transformed program P 2 , each transition step in P 1 with trace t must correspond to transitions in P 2 with the same trace t and preserve as an invariant a relation ≈ between states of P 1 and P 2. In order to handle diverging execution steps and rule out the infinite stuttering problem (that may hapen when infinitely many consecutive steps in P 1 are simulated by no step at all in P 2 ), the theorem uses a measure over the states of language L 1 that strictly decreases in cases where stuttering could occur.
Memory Injections The memory model of CompCert is shared by the semantics of all the languages. Memory states are collections of blocks, each block being an array of abstract bytes. A block represents a C variable or an invocation of malloc. Pointers are represented by pairs (b,i) of a block identifier and a byte offset i within this block. Pointer arithmetic modifies the offset part of a pointer value, keeping its block identifier part unchanged. Values stored in memory are the disjoint union of 64-bit integers, 64-bit floating-point numbers, pointers, and the special value vundef representing the contents of uninitialized memory  [Leroy et al. 2014 ]. The memory layout evolves during compilation of a program. Some memory blocks are added, while others are merged. To relate memories before and after these modifications, the memory model of CompCert comes with a central notion of memory injection that formalizes the effect of merging memory blocks together.
We model the leakages of P as a list of atomic leakages, where an atomic leakage results from a single step of the program execution  [Barthe et al. 2018 ]. An atomic leakage is either the truth value of a condition, or a pointer representing the address of either a memory access (i. e. , a load or a store) or a called function. This leakage model is compliant with our constant-time policy. Moreover, to observe leakages in all languages of CompCert, we instrument all their semantics, and enrich the traces of input/output events defined in CompCert by leakages (i. e. , we add leakages as a new kind of event). We thus benefit from all the existing definitions and lemmas about traces, that we directly reuse in our proofs. More precisely, we distinguish 3 semantics: the CompCert semantics with traces enriched by leakages, represented by the full step relation t -→ , and two semantics where some events are filtered out from traces.
We call them leak-only semantics (represented by the t -→ l step relation) and compileonly semantics (represented by the t -→ Comp step relation). A leak-only execution is based on the former relation, while a compile-only execution is based on the latter. We omit the arrow subscripts when the context makes clear which is considered. In leak-only semantics, the input/output events of the full semantics are filtered out to produce only leakages. In compile-only semantics, the leakages of the full semantics are filtered out to produce only input/output events. It corresponds hence to the original semantics of CompCert. As explained in the remainder of this paper, in our formalization, we either reuse directly standard simulation diagrams (and semantics) of CompCert or define new simulation diagrams involving one of our instrumented semantics.
These proof techniques range from simple proofs (see Section 5. 2) to tricky proofs requiring sophisticated simulation diagrams and peculiar instrumentations in the semantics (see Section 5. 5). Last, we write |t | the size of trace t (i. e. , the number of its observed events). Furthermore, we assume that the languages are deterministic. This assumption is appropriate for our intended application as cryptographic implementations are deterministic. Moreover, it does not seem straightforward what it would mean for a non-deterministic C program to be constant-time. The main cryptographic constant-time policy for CompCert is thus stated as follows. a , a ′ initial states of P =⇒ a ≡ a ′ (1) a final state of P a ≡ a ′ =⇒ a ′ final state of P (2) a t - → b a ′ t - → b ′ a ≡ a ′ =⇒ b ≡ b ′ (3) a t - → b a ′ t ′ -→ b ′ a ≡ a ′ =⇒ |t | = |t ′ | (4) Definition 3.
In the special case where t is empty, this property ensures that t ′ is empty too. This property is useful in our methodology and easily satisfied by all CompCert semantics. Another remark is that this property subsumes the non-cancelling assumption made by  [Barthe et al. 2018] , i. e. , that the equality of the leakages of two executions implies the pairwise equality of the leakages of each of their steps. This is a direct consequence of our property. When such same-point relations exist, they are all consequences of the most informative relation (written ≡ strongest ): two states are related if and only if they are reachable from two initial states within the same number of steps and producing the same trace. Although the relation ≡ strongest is convenient to prove general properties of ≡-related states, it is generally helpful to define a same-point relation for each language in terms of the control-flow components of the execution states.
We show that if a program P satisfies CTS n , then it also satisfies CTS. This proof is similar to the standard simulation proofs of CompCert. Let's first assume that the execution of P from s i terminates with leakage t in n steps, i. e. , s i t -→ n s f and s f is a final state. We can assume without loss of generality that s ′ i has a longer execution, whether terminating or infinite. We can split this execution in two parts, so that the first part takes also n steps and matches the execution starting from s i , i. e. , s ′ i t ′ -→ n s ′ n. By using CTS n , we have that t = t ′. Therefore, s f ≡ s ′ n by Lemma 3. 2. As s f is a final state, s ′ n is also necessarily a final state by Property 2. The execution starting from s ′ i is thus also terminating with leakage t ′ such that t = t ′.
To this end, we would like to strengthen the semantics of assembly programs to make the call-stack explicit and dynamically check that the targets of return instructions is consistent with this stack. However, assembly being the target language of the CompCert compiler, it is part of its trusted computing base (TCB) and should not be changed lightly. Therefore, we introduce an intermediate instrumented semantics with a ghost call-stack and assertions about its consistency. We then prove a simulation which justifies that the instrumentation can be removed (preserving traces, hence behaviors as well as the constant-time property). This implies that this instrumentation is only a proof intermediate and does not belong to the TCB. Finally, we prove the correctness of the compilation from the last intermediate language Mach to assembly using the instrumented semantics, embedding in the behaviors of assembly programs the knowledge that they come from the usual compilation process.
Non-preservation of our Policy by the Instruction Selection Pass Instruction selection is the first pass of the backend compiler. It optimizes Cminor expressions to take advantage of combined expressions and addressing modes of the target processor and of processor's capabilities  [Leroy 2009b ]. Cminor expressions are optimized into CminorSel expressions, that use machine-specific operators and addressing modes. These optimizations are defined using rewrite rules for each operator. The Cminor language supports all logical and arithmetic operators of C. Moreover, conversions between floats and integers are made explicit, using Cminor conversion operators. In Cminor, there are 5 kinds of constants, 33 unary operators and 40 binary operators. All the following intermediate languages, from CminorSel to Mach, share the same definition of operators, which are architecture dependent.
Thanks to the ty annotation, we benefit from these typing passes and did not need to change or to add special typing rules to ensure that Eop (select c ty) is typed in a safe way. The new selection operation is compiled down to the cmov instruction on x86 architecture. We chose to add our selection operation to the generic backend operations because it induces minimal changes in CompCert and does not require modifying directly the syntax of the languages of the backend. In a similar way, thanks to smart constructors, the changes in the compiler passes were minimal and so were the associated correctness proofs. The selection operation is compiled to the cmov instruction, during the last compiler pass, from Mach to assembly language. At Mach level, res <-Eop (select c ty) [r1;r2] operates over two registers r1 and r2, and stores the result in a register res.
In order to generate efficient code and to apply CompCert optimizations (e. g. , register allocation) on the selection operation as well, select is a two-address operation (i. e. , its first argument r1 and its result res lie in the same location). For an integer selection operation (when ty = int), this is done directly using one cmov instruction and the negation of the condition Moreover, the syntax of the cmov instruction requires c to be a testable condition (usable for a conditional jump), which in our case requires to transform c because of the way comparisons proceed on x86 architecture. More precisely, the x86 hardware provides a way to handle most comparisons of the source language; we call them testable conditions. Two comparisons (namely equality and inequality between floating point numbers) cannot be handled by the hardware, and require a software workaround.
PROVING THE PRESERVATION OF OUR CONSTANT-TIME POLICY Cryptographic constant-time preservation is a property about the leak-only semantics -→ l (see Section 3. 1) of a source and a target programs. Existing CompCert simulation diagrams deal with the compile-only semantics -→ Comp. Our proof engineering strategy is to benefit as much as possible from the proof scripts of these diagrams. First, this section details the main theorem of constant-time preservation. Then, it presents the four proof techniques we use to prove this theorem; except the last one, these are relaxations of the classical diagram that we prove on the full step relation -→. Then we derive, on one hand the standard compiler correct forward simulation diagram for the compile-only relation, and on the other hand a proof of constant-time preservation for the leak-only semantics.
Preservation of Constant-Time Security in CompCert Our modified version of CompCert preserves our cryptographic constant-time policy, as stated by the following main theorem, which considers a source Clight program. Clight is a determinized large subset of C. As explained in Section 3, we only consider deterministic languages, which C and CompCertC are not. We thus chose to start our compilation pipeline from the first determinate intermediate language, which is Clight. Wary programmers can directly write programs in this subset in order to make sure that the determinization pass from CompCertC to Clight did not modify their programs and are covered by our theorem. Theorem 5. 1 (Constant-Time security preservation). Let S be a safe Clight source program that is compiled into an x86 assembly program T.