Camille Sivelle

Lorys Debbah

Maxime Puys
email: maxime.puys@cea.fr

Pascal Lafourcade
email: pascal.lafourcade@uca.fr

Thibault -4459-511x]

Franco-Rondisson

Automatic Implementations Synthesis of Secure Protocols and Attacks from Abstract Models

Attack generation from an abstract model of a protocol is not an easy task. We present BIFROST (Bifrost Implements Formally Reliable prOtocols for Security and Trust), a tool that takes an abstract model of a cryptographic protocol and outputs an implementation in C of the protocol and either a proof in ProVerif that the protocol is safe or an implementation of the attack found. We use FS2PV, KaRaMeL, ProVerif and a dedicated parser to analyze the attack traces produced by ProVerif. If an attack is found then BIFROST automatically produces C code for each honest participant and for the intruder in order to mount the attack.

Introduction

The security of a communication protocol involves two different aspects: (i) the security of the protocol itself and (ii) the security of the cryptographic schemes involved. Several tools are now available to formally prove the intrinsic security of both protocols (like ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF], Scyther [START_REF] Cremers | The scyther tool: Verification, falsification, and analysis of security protocols[END_REF] or Tamarin [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF]) and primitives (like CryptoVerif [START_REF] Blanchet | A computationally sound mechanized prover for security protocols[END_REF] or Easycrypt [START_REF] Barthe | Computer-aided security proofs for the working cryptographer[END_REF]) see [START_REF] Barbosa | Sok: Computer-aided cryptography[END_REF] for a survey. However, another issue comes into play. Security flaws often appear when implementing code for a given protocol, even for a proven secure one. In this case, the attack does not rely on an intrinsic flaw of the protocol, but involves vulnerabilities related to the code design or even from the programming language. It also happens too often that the implementation is a slightly different protocol than the one proven (for instance the order of the content of an encrypted message is changed) and thus have the formal proof becoming meaningless. In 2014, the Heartbleed [START_REF] Durumeric | The matter of heartbleed[END_REF] attack over SSL/TLSv1.0 whose feasibility had been formally proven in [START_REF] Bhargavan | Cryptographically verified implementations for tls[END_REF] is an example of an attack targeting the implementation. We can also mention a famous attack of the SSH protocol in Debian Linux distributions where the generation of a fresh nonce was wrongly implemented [5]. Hence implementing a secure protocol is a sensitive task and every detail is important.

Contributions:

We propose an automatic tool-chain named BIFROST (Bifrost Implements Formally Reliable prOtocols for Security and Trust), that takes as input a cryptographic protocol modeled in F*, we call this input a protocol model in the rest of the paper, and combines the following existing tools: FS2PV [START_REF] Bhargavan | Verified interoperable implementations of security protocols[END_REF], KaRaMeL [START_REF] Protzenko | Verified low-level programming embedded in f[END_REF] (formerly known as KreMLin) and ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF]. BIFROST produces:

1. An implementation in C from a protocol modeled in F*. 2. If the protocol is safe then a proof in ProVerif is produced. 3. If ProVerif finds a flaw then an implementation in C of the attack is given.

BIFROST supports several standard cryptographic primitives that correspond to those supported by ProVerif. We are able to use several symmetric encryption schemes, public key encryption schemes, signatures schemes and hash functions. All these primitives are wrapped around widely-known cryptographic primitive libraries such as MbedTLS. BIFROST unifies their APIs and make them directly compatible with verification tools such ProVerif. BIFROST has been successfully tested on the famous Needham-Schroeder [START_REF] Needham | Using encryption for authentication in large networks of computers[END_REF] and Otway-Rees [START_REF] Otway | Efficient and timely mutual authentication[END_REF] protocols, alongside a MAC based password protocol taken from [START_REF] Bhargavan | Verified interoperable implementations of security protocols[END_REF].

Formal verification tools need to over-approximate an attacker's capabilities in order to be sure that a protocol is secure in regards to a given property. Therefore, the attacks generated by such tools can sometimes not be feasible in practice. If the protocol was not found secure, the attack implementation generated by BIFROST can be played along with the protocol implementation previously generated. If the execution of the attack found by formal verification succeeds, it proves its feasibility in a practical context. This can give an automatic confirmation that the protocol is not secure, rather than manually implementing the attack.

Related Work: Several tools can be related to BIFROST. We classify them in three categories: (i) generic code verification tools, (ii) cryptographic protocol verification tools, (iii) tools specifically designed to generate code from verifiable protocol models. Generic code verification and cryptographic protocol verification tools are not directly related works to BIFROST, but they are related to the basic blocks used in the approach. Thus, we will mainly mention the one used within BIFROST and their main competitors.

Generic code verification tools: They have been developed for several tens of years. Among many other reference tools we can list:

-The B method [START_REF] Abrial | The B-book: assigning programs to meanings[END_REF] -F* [START_REF] Swamy | Verifying higherorder programs with the Dijkstra monad[END_REF] is a general-purpose functional programming language designed by Swamy et al. in 2013 which allows to specify properties alongside code. Then, various analyses can be performed on the code such as dependent types, monadic effects, refinement types, and a weakest precondition calculus.

We use F* models in BIFROST, due to their compatibility with the other bricks used in our toolchain.

Cryptographic protocol verification tools: They have been developed since 1995, when G. Lowe found an attack on the formerly proven Needham-Schroeder protocol [START_REF] Lowe | Breaking and fixing the needham-schroeder public-key protocol using fdr[END_REF]. Such tools often implement the Dolev-Yao [START_REF] Dolev | On the security of public key protocols[END_REF] intruder model and check all possible actions for an attacker interacting with multiple sessions of a given protocol in parallel to verify security properties such as secrecy or authentication. Multiple tools have been introduced since 1995 [START_REF] Barbosa | Sok: Computer-aided cryptography[END_REF] and benchmarked [START_REF] Lafourcade | Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties[END_REF][START_REF] Barbosa | Sok: Computer-aided cryptography[END_REF]. Among them we can list:

-Tamarin [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF] is a security protocol prover designed by Meier et al. since 2013.

Tamarin is able to handle an unbounded number of sessions. Protocols are specified as multi-set rewriting systems with respect to temporal first-order properties. It relies on Maude [START_REF] Escobar | Maude-npa: Cryptographic protocol analysis modulo equational properties[END_REF] and supports equational theories such as Diffie-Hellman. -DY* [START_REF] Bhargavan | Dy*: a modular symbolic verification framework for executable cryptographic protocol code[END_REF] We chose ProVerif in our tool chain, since it is stable and that several bricks of our approach are compatible with this well established tool.

Cryptographic protocol code generation tools:

There exist some tools allowing to generate code from verifiable protocol models, such as BIFROST.

-Spi2Java [START_REF] Pozza | Spi2Java: Automatic cryptographic protocol java code generation from spi calculus[END_REF] is a framework proposed in 2004 that automatizes the generation of Java implementations from protocols described in spi calculus, an extension of pi-calculus. This method allows for formal verification of security properties through translation of the spi-calculus specifications to a format that can be verified by ProVerif prior to code generation. -In 1993 and in 2009, Bieber et al. [START_REF] Bieber | Abstract machines for communication security[END_REF] and Benaissa et al. [START_REF] Benaissa | Cryptographic protocols analysis in event b[END_REF] respectively proposed an approach to analyze the security of cryptographic protocols using the Event-B framework. To the best of our knowledge, they partly implement the Dolev-Yao model as a library for the internal verifier of Event-B, allowing them to specify lemmas describing security properties to be proven such as secrecy and authentication. It is however unclear if their approach is able to find an attack trace. As their framework relies on Event-B, specifications can be refined into C-like code.

-In 2009, Bhargavan et al. [START_REF] Bhargavan | Cryptographic protocol synthesis and verification for multiparty sessions[END_REF] proposed a compiler allowing to translate protocols modeled in some ad-hoc language into ML-like implementations. They provide various security verifications through a custom type-checker [START_REF] Bengtson | Refinement types for secure implementations[END_REF] which performs security verifications similar to ProVerif and Tamarin. -AnBx [START_REF] Modesti | AnBx: Automatic generation and verification of security protocols implementations[END_REF] Finally, several previous works mention that they perform protocol synthesis. However, if their works share resemblance with ours, this terminology should not be confused with protocol implementation synthesis which aims at automatically generating executable protocol implementations. For instance, Bellare et al. [START_REF] Bellare | A modular approach to the design and analysis of authentication and key exchange protocols[END_REF] and Katz et al. [START_REF] Katz | Scalable protocols for authenticated group key exchange[END_REF] synthesize protocol models resistant to active intruders from protocol models resistant to passive intruders in the context of authenticated group key exchange. Cortier et al. [START_REF] Cortier | Synthesizing secure protocols[END_REF] translate a single-session protocol into a multi-session protocol secure against a Dolev-Yao intruder. Sprenger [START_REF] Sprenger | Developing security protocols by refinement[END_REF] et al. rely on Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: a proof assistant for higher-order logic[END_REF] to write secure-by-design protocol models. In 2008, Bhargavan et al. [START_REF] Bhargavan | Verified interoperable implementations of security protocols[END_REF] synthesize ProVerif models from F# protocol implementations in a tool called FS2PV. We are using FS2PV in BIFROST because it is compatible with ProVerif and it will help us in our goal to generate attack implementations in C.

Overall, only cryptographic protocol code generation tools are direct competitors to BIFROST. All other presented works are related to internal tools used within BIFROST (e.g., cryptographic protocols verification tools). Moreover, to the best of our knowledge, if all tools mentioned above are able to faithfully translate a protocol from a provable model into a programming language (with their own limitations), none of them are dealing with attacks found by the verification tools.

Outline: In Section 2, we introduce the BIFROST framework. In Section 3, we delve into the technical challenges regarding automatic code generation from protocol models and explaining the inner-workings of BIFROST. In Sections 4 and 5, we respectively present the cryptographic primitives supported and how we automatically generate code for attacks found. In Section 6 we give a detailed example of the approach on the Needham-Schroeder protocol which will be part of technical report of this paper and in the manual of BIFROST. Finally, we conclude in Section 7.

Overview of BIFROST

Our aim is, with the same input file, to be able to generate C code with KaRaMeL and a π-calculus file for ProVerif. For this, we use a subset of F* that is compatible both with the subset of F# that is used by FS2PV, and also with low* (the subset of F* that can be compiled into C) in order to be able to use KaRaMeL. In the rest of the paper, we denote this subset F $ . When it is clear from the context we also use F*. In Figure 1, we describe the BIFROST approach. From a cryptographic protocol model (1) the user needs to write an F $ file. In step (2), we generate a π-calculus model using FS2PV, which can then be verified by ProVerif in step (3) with respect to the security properties described in a .query file. If the protocol is safe and ProVerif proves the security of the requested properties in step (4), we apply KaRaMeL in step (5) to the initial model in F $ to generate C code corresponding to the implementation of the roles of each participant in the protocol [START_REF] Abrial | The B-book: assigning programs to meanings[END_REF], thus bridging the gap between the formal verification of the protocol and its implementation. If the protocol is not safe it means that ProVerif found an attack in step ( 7), then we parse the ProVerif attack trace using a tool we have developed [START_REF] Barbosa | Sok: Computer-aided cryptography[END_REF] to generate the corresponding F $ code. We apply KaRaMeL to the obtained F $ files to automatically generate the C code implementing the role of the attacker in the protocol. In the following, we describe in Section 3 some of the challenges for transforming abstract models into a practical implementation. We then present, in Section 4, the different cryptographic primitives that are available in BIFROST and how we integrate them to allow crypto-agility. Finally, we show, in Section 5, how we manage to generate attack implementations from ProVerif traces.

From Abstract Model to Implementation

The translation from an abstract model to a concrete implementation brings several challenges. The F $ model which serves as an input for our toolchain relies on a set of functions for cryptographic primitives, network operations and data manipulation, which are all currently imposed by FS2PV. One important point is that FS2PV only uses an abstract definition of these function to translate the input F $ protocol description into a ProVerif model. However, when generating the C implementation of the protocol, all these functions must also be defined with their proper implementation. Moreover, their implementation must fit their purpose in the real world. For instance, if the Net.send function is internal to FS2PV for its analysis at the abstract model phase, it must actually be sending packets on a network when called by real code. Some abstract functions can have multiple implementations depending on user choices. For instance, a Crypto.symenc function can be translated into AES or ChaCha encryption while Net.send can translate to a TCP/IP send or a LoraWan send depending on context. On the other hand, some functions defined and called within the abstract model do not serve any purpose in the implementation (such as π-calculus' f ork).

BIFROST libraries. To this end, we propose a series of C libraries Crypto, Net, Data and Pi, implementing all the necessary functions to link and run the C code produced by KaRaMeL from our model. Figure 2 describes the translation of the different libraries of abstract functions into their implementations.

-Data contains several functions necessary for data types manipulation. In FS2PV representation, the principal data type is the Byte, which can represent variables of various size and nature, as it could be a nonce as well as a key, or even a concatenation of different Bytes. This is problematic in C, as those can hardly be represented by the same data structures and might introduce some type flaw attacks, as the one existing on the fixed version of Needham-Schroeder by G. Lowe, where a confusion between identity and nonces allows an intruder to mount an attack [START_REF] Ceelen | Chosen-name attacks: An overlooked class of type-flaw attacks[END_REF]. The solution we proposed in our Data library is to define the Byte as a C structure, composed of an integer representing the subtype of the object, an integer representing the size of the object and an union of the C structures corresponding to each possible subtype (nonce for example).

-Crypto gathers all the functions relative to the cryptographic operations in the protocol. Most of its functions are meant to be crypto-agile and thus are algorithm agnostic wrappers to specific primitives such as RSA or AES. -The Net library of BIFROST includes basic network operations. As of now, they are implemented on either TCP/IP sockets or low level UART connections. However, supporting various protocols is possible with BIFROST but it is important to ensure the compatibility with the network model of ProVerif. -Finally, the Pi library relates to internal π-calculus functions used by ProVerif for its analysis (mainly for process scheduling) and does not have any real purpose in real life. Thus, this module does not need to be translated into C. Keys management. Another difference between the protocol model and the role implementation is the way that keys are managed. When verifying a protocol with ProVerif, private keys are often modeled as terms freshly generated at the beginning of the protocol, public keys being derived from these terms and published on a public channel. This is sufficient to consider that each participant knows a given public key in the formal model. However, this traditional setup for verification, consisting in broadcasting keys or supposing that participants already know each other's public keys beforehand is more complicated to pull off on real hosts. Within BIFROST, we use the following key management to reconcile both formal verification and implementation usability (it can also apply to any supposedly pre-shared keys): two distinct main functions are defined for the formal verification and the implementation generation. One is required by FS2PV in which each participant role is called with keys created by abstract methods from FS2PV. This file is then translated as the main process clause used by ProVerif to setup roles instances. On the other hand, KaRaMeL produces C code for every participant, plausibly running on different systems, and each of them requires its main function. Thus, the role of each participant is described in a F $ file containing a role function, which takes in argument the keys, and a main function, in which the keys are loaded from a .pem file. This choice presupposes that the keys are generated and stored on each system executing a participant's role beforehand, which is common for embedded devices.

Cryptographic Primitives

To allow crypto-agility by letting the user choose a cryptographic algorithm among different options, we decided to handle all the following schemes and to implement several algorithms for each of them.

-Symmetric encryption uses a key shared by both participants to encrypt and decrypt data. Symmetric keys are often smaller than asymmetric keys which allows communication to be fast. We support three algorithms for symmetric encryption: AES-128/192/256 in CBC mode, Blowfish in CBC mode and Chacha20. -Message Authentication Code uses symmetric keys to check the integrity and authenticity of data. We support the following four algorithms: AES with CMAC, Poly1305-AES, Chacha20-Poly1305 and HMAC. -Hashing has a lot of applications in cryptography. It can be used to compute fingerprints for example. We support two hashing algorithms: SHA2 and RIPEMD160.

-Asymmetric encryption uses a public key, private key pair to encrypt and decrypt. It is often used to transfer symmetric keys. We support two algorithms for asymmetric encryption: RSA-OAEP and RSA-PKCS1-v1.5. -Asymmetric signature uses a public key, private key pair to check for the integrity and the authenticity of data. We support three algorithms for asymmetric signature: RSA-PKCS1-v1.5, RSA-PSS and ECDSA.

Cryptographic primitives management in BIFROST relies on MbedTLS [1], a C library developed by ARMmbed. It implements the TLS [START_REF] Dierks | The transport layer security (TLS) protocol version 1.2[END_REF] protocol and required cryptographic primitives. MbedTLS is designed to fit on small embedded systems. However, one of the key concerns of BIFROST is to allow for cryptoagility, which would in our case translate as the possibility for the toolchain to handle both different algorithms and different cryptographic libraries, such as OpenSSL [3] or OpenQuantumSafe [2], in order to fit as easily to existing code base. In practice, any cryptographic operation requires different MbedTLS function calls (e.g., to set the seed or initialize the context before encrypting). As all these atomic function calls are not defined within FS2PV and ProVerif, granularity differs with MbedTLS. Thus, we created a C library composed of functions that would act as wrappers above MbedTLS's functions. More precisely, we wanted those wrappers to encompass every intermediate function of MbedTLS (or another library) to provide a more generic function to the user, which would also fit the granularity of protocol models. The use of this library also allows the user to choose the primitives to use for a given protocol.

Different options allow us to choose which primitive to use. The choice of which primitive should be used is currently left to the user of BIFROST (which is the protocol modeler and not the final user). This choice is partly motivated by the context of embedded systems where not all primitives are supported by chip vendors and some freedom in the choice can be important. Yet, letting any user choose their cryptographic primitives will often lead to vulnerable systems. While leaving room for freedom of choice, we intend to support cryptographic suites3 which will automatically include a combination of validated cryptographic primitives with their proper configuration (e.g., ECDHE_PSK_WITH_AES_128_ GCM_SHA256). By defining the right macros, preprocessor will comment out code for unused primitives. In a similar way, the user can choose the size of its keys with preprocessor directives, the idea being to give the user maximum control over the parameters for each primitive. This control is the one that MbedTLS provides so we did not restrict the options provided by the library but we eased the way to select them. This allows a user to custom the protocol by choosing the cryptographic primitives' parameters he wishes to use.

Attack Generation

The generation of the attack implementation is based on the output printed by ProVerif in case an attack is found. This output corresponds to an attack trace in applied π-calculus which describes the steps performed by the intruder to violate the specified security property. As already presented in Figure 1, the approach we chose for this part was to first parse the attack trace from ProVerif's output in order to obtain an abstract syntax tree [START_REF] Barbosa | Sok: Computer-aided cryptography[END_REF], and to use that tree to generate the F $ file implementing the actions described in the trace. We then apply KaRaMeL [START_REF] Barthe | Computer-aided security proofs for the working cryptographer[END_REF] to that F $ file to generate the C implementation of the attacker's role [START_REF] Basin | An on-the-fly model-checker for security protocol analysis[END_REF]. We motivate the choice of generating F $ code and using KaRaMeL rather than generating C code directly from the syntax tree for the coherency it guarantees with the C code generated from the protocol model with KaRaMeL. To our knowledge, there is no tool or framework allowing to generate executable code for an attack found by a protocol verification tool. The generated C code can then be compiled and executed alongside a normal protocol session (or more if needed) in order to play the attack.

ProVerif Attack Trace Parsing: To parse the attack traces from the ProVerif outputs, we have chosen to proceed in Python, using the Lark module [START_REF]Python Lark parser[END_REF]. Lark is a parsing library able to parse any context-free grammar, using an advanced grammar language based on EBNF, a metalanguage that allows to describe the syntactic rules of programming languages. The first step is therefore to determine the grammar of ProVerif outputs and to describe it in EBNF language. Globally, an attack trace is made up of a succession of lines that can be considered as instructions. We consider four different types of instructions in ProVerif's language: in, out, new and event.

The in and out instructions aim to send and receive messages from a channel and have the same grammar. The elements that we want to retrieve in our syntax tree are:

1. their two arguments (for example c and M _6 for the out of Listing 1.1), 2. the equality given after the with keyword (for instance M _1 = pk(skB_1)

for the in), 3. the line number in the process (5 or 12).

In Listing 1.1, c, M _6, and M _1 are variable or channel names, pk(skB_1) or aenc(n_3, pk(skB_1)) are functions applied these variables. As terms can be functions applied multiple times to another term, we define values as either ground terms or function results and line numbers correspond to natural numbers. Then, we can define the in and out instructions as in Listing 1.2.

1 o u t : " o u t " " ( " v a l " , " v a l " ) " " w i t h " v a l "=" v a l " a t " "{" l i n e "}" 2 i n : " i n " " ( " v a l " , " v a l " ) " " w i t h " v a l "=" v a l " a t " "{" l i n e "}" Listing 1.2: Grammar for in/out instructions.

We also define similar rules for new and event keywords. The new instruction allows a participant or the intruder to generate a fresh term. On the other hand, event does not have any effect on the protocol but allows to place markers in the trace which can be used for reachability properties. Their form is shown in Listing 1.3.

1 new n_1 c r e a t i n g n_3 a t {21} 2 e v e n t endB (A, pk ( skA_1 ) , Bob , pk ( skB_1 ) , n_2) a t {25} Listing 1.3: Example of new/event instructions.

Similarly, these instructions are translated in EBNF as shown in Listing 1.4.

1 new : "new" v a l " c r e a t i n g " v a l " a t " "{" l i n e "}" 2 e v e n t : " e v e n t " v a l " a t " "{" l i n e "}" " ( g o a l ) "? Listing 1.4: Grammar for new/event instructions.

Generating F $ Code: From the syntax tree obtained, we write a program that generates a code in F $ . Processing will differ according to the type of instruction. An out corresponds for example to a sending by one of the hosts defined in the protocol. As the code generated at this step corresponds to the behavior of the intruder, a call to F $ N et_recv function is performed on the channel indicated by the variable stored in the AST. Similarly, an in means that the intruder must send the given message on the channel, leading to a call to N et_send. When the declaration in the with statement involves functions, for example M _6 = aenc(n_3, pk(skB_1)), we translate these into the corresponding functions in our libraries. The events could be ignored since they do not bring anything to the attack in itself. We therefore simply use a logging system when an event is raised. The case of the new requires a little more work because ProVerif does not distinguish the generation of nonces from the generation of encryption keys.

However, the functions that are assimilated in F $ are not the same. To remedy this problem, we use a preprocessing function that goes through the tree a first time to determine on one hand if the generation of each variable is done by the intruder, and on the other hand, the type of this variable. The latter is given by the functions that are applied to it after creation. The algorithm used for the generation of the code can therefore be summarized as shown in Listing 1.5. 6 An Example: the Needham-Schroeder Protocol

We show how BIFROST can be applied on the well-known Needham-Schroeder protocol. We first describe this protocol in Section 6.1, then we show in Section 6.2 how this protocol is modeled in F $ and it is translated into C code using BIFROST. Finally, we detail in Section 6.3 the generation of the implementation of an attack on this protocol from the attack trace found by ProVerif.

The Needham-Schroeder Protocol

The Needham-Schroeder [START_REF] Needham | Using encryption for authentication in large networks of computers[END_REF] protocol is a mutual authentication protocol involving two parties A and B. They wish to agree on a shared value that they will use to secure further communications. In this protocol, messages are sent on an insecure channel. N A , N B are nonces, pk A , pk B are public keys and (m) pk B symbolizes the public encryption of the message m. The first message (A, N A ) pk B is used to initiate a new session between A and B. The second message is used by A to authenticate B and the third one is used by B to authenticate A. Nonces are also used to prevent replay attacks.

A -→ B :(A, N A ) pk B B -→ A :(N A , N B ) pkA A -→ B :(N B ) pk B
In 1996 G. Lowe [START_REF] Lowe | Breaking and fixing the needham-schroeder public-key protocol using fdr[END_REF] found a famous attack on this protocol. This attack assumes that a dishonest agent I impersonates the honest agent B in the previous protocol, leading to a man-in-the-middle attack.

A -→ I :(A, N A ) pk I I -→ B :(A, N A ) pkB B -→ I :(N A , N B ) pk A I -→ A :(N A , N B ) pk A A -→ I :(N B ) pk I I -→ B :(N B ) pk B
With this attack, the intruder obtains both N A and N B which allows him to derive any secret based on those two nonces. He also impersonates A when speaking to B. This vulnerability was fixed by Gavin Lowe [START_REF] Lowe | Breaking and fixing the needham-schroeder public-key protocol using fdr[END_REF] by modifying only one message in the Needham-Schroeder-Lowe (NSL) protocol:

A -→ B :(A, N A ) pk B B -→ A :(N A , N B , B) pkA A -→ B :(N B ) pk B
One can see that with this variant, the intruder is not able to get the nonce N B . Indeed, as the intruder tries to perform the attack, A will cipher with pk I as she is willingly talking with the intruder. However, upon reception of the second message containing the identity of B, A will realize she is not talking to I as she was willing to initially and will not send the last message, thus preventing I from getting the last nonce.

From Protocol Model to Implementation

The code 1.6 is the role of A in the Needham-Schroeder protocol in F $ , and the code 1.7 is the protocol implementation in C generated by KaRaMeL are given in Figure 3. The code for B is similar. We can see that in F $ code 1.6, we start by establishing the communication channel 10.0.0.2, port 80 (which we will use for the IP address of B). Then a pair of keys is generated and public keys are published on the network. A listens for the public key of B4 . After this initialization phase, the protocol can start and A generates a nonce and sends it and her name encrypted with the public key of B according to the first step of the protocol. Then A waits for the answer of B. Once B's response is received, A checks the correspondence between the nonce sent in the first message and the one received from B. If the nonces match them A confirms to B that she has received N B by sending it back to B encrypted by B's public key.

The C code produced by BIFROST is given in the code 1.7. It follows exactly the same steps and use all libraries proposed by the tool. Moreover, we argue that even for an automatically generated code. It stays fairly understandable and possible to analyze with C static analyzers such as Frama-C or CPPcheck.

Attacker Implementation Generation

The F $ code of the role of A displayed in Listing 1.6 is translated into pi-calculus by FS2PV and can be analyzed by ProVerif5 . To do so, we need to provide a query (i.e., a security property) for ProVerif to verify. In this example, this query is shown in Listing 1.8 and requires the last message received by B from A to actually be sent by A for B earlier, ensuring authentication of A to B on N B . Listing 1.9: Attack trace found by ProVerif.

The attack found by using ProVerif is actually the same as the one discovered by Lowe and presented in Section 6.1. It can be read as the following (with lines 1-5 prior the roles of A and B): Line 1 : creation of sk A ; Line 2 : creation of sk B ; Line 3 : creation of sk I ; Line 4 : share sk I for the intruder; Line 5 : share pk B for the intruder; Line 6-7 : start event from B and A Line 8 : creation of nonce N A ; Line 9 : A sends (A, N A ) pk I ; Line 10 : B receives (A, N A ) pkB . This message is built by the intruder using the message from A. Line 11 : creation of nonce N B ; Line 12 : B sends (N A , N B ) pk A ; Line 13 : A receives (N A , N B ) pk A ; Line 14 : A sends (N B ) pk I ; Line 15 : B receives (N B ) pk B . This message is built by the intruder using the message from A.

The F $ representation of the role of the intruder generated by the Python parser can be found in Listing 1.10. The reader may take note that it follows the steps of the attack described above. The C implementation is generated by KaRaMeL, similarly to the roles of A and B, and after compilation it can be executed along with the two roles in order to play the attack. Finally, when we add Lowe's correction to the protocol model (described in Section 6.1), we can indeed see that ProVerif declares the protocol safe for the given properties.

Conclusion

We present BIFROST, a toolchain allowing to automatically generate C code from an abstract model of cryptographic protocols. BIFROST takes as inputs a protocol modeled in F $ and output C files. To generate these files BIFROST uses KaRaMeL to obtain an implementation of the protocol that corresponds to the model. Moreover, BIFROST transforms the F $ specifications into a π-calculus file using FS2PV and this file is sent to ProVerif to verify if the protocol is safe or not. If ProVerif finds a flaw, then we produce the additional C files that allow us to mount the attack on the protocol implementation. For this we have designed a parser of ProVerif's output, able to generate F $ model describing the attack trace. This F $ file can be translated into C code using KaRaMeL in the same way as other roles. Moreover, BIFROST can deal with several cryptographic primitives and network parameters. The choice of using ARM mBedTLS as a backend relies on its common use within industry products, especially within embedded systems. However, support with HACL* 6 which is a formally verified cryptographic library would be possible and make sense to have a completely verified toolchain. On a similar note, gcc/clang could be switched to CompCert 7 , a formally verified compiler. As a future work, we intend to switch FS2PV for an F* compatible translator that will allow us to support multiple verification tools alongside ProVerif. This will allow us to not rely on F# anymore and have a protocol representation only requiring to be compatible with F*. We also aim to extend BIFROST to be able to consider equational theories and advanced trace-based security properties like forward secrecy and post-compromise security. Security against side-channel and fault attacks could also be studied.

  is a tool developed by Bhargavan et al. in 2021. It is an implementation of the Dolev-Yao intruder model in F* and allows security properties verification on a protocol taking advantage of the internal F* prover. It is however currently unable to produce attack traces. -ProVerif [19] is developed by Blanchet et al. since 2001 and relies on Horn clause analysis to check an unbounded number of sessions.

Fig. 1 :

 1 Fig. 1: The BIFROST toolchain.

Fig. 2 :

 2 Fig. 2: Abstract functions libraries translated into C code.

  22 do n o t h i n g ( a l r e a d y p r o c e s s e d d u r i n g t h e p r e p r o c e s s i n g ) 23 r e t u r n output Listing 1.5: F $ code generation.

Fig. 3 :

 3 Fig. 3: Input code of A's role in F $ and generated C code.

1

  query ev : Ev ( BMessageB ( a , b , nb ) ) ==> ev : Ev ( AMessageA ( a , b , nb ) ) .Listing 1.8: Query used by ProVerif Using this query, ProVerif is able to find an attack. The trace is also quite long and we chose to narrow down the output to what is shown in Listing 1.9.

1

  new T55 c r e a t i n g T55_1 a t {90} 2 new T53 c r e a t i n g T53_1 a t {92} 3 new T51 c r e a t i n g T51_1 a t {94} 4 out ( NethttpChan , CryptoAsymPrivKey ( DataFresh (M) ) ) with M = T51_1 a t {96} 5 out ( NethttpChan , CryptoAsymPubKey ( DataBin (M_1) ) ) with M_1 = DataPK ( DataFresh ( T53_1 ) ) a t {97} 6 e v e n t Ev ( BStart ( DataUtf8 ( SBobS ( ) ) , DataUtf8 ( S A l i c e S ( ) ) ) ) a t {128} 7 e v e n t Ev ( AStart ( DataUtf8 ( S A l i c e S ( ) ) , DataUtf8 ( S I n t r u d e r S ( ) ) ) ) a t {100} 8 new T49 c r e a t i n g T49_1 a t {102} 9 out ( NethttpChan , DataBin (M_2) ) with M_2 = DataAsymEncrypt ( DataBin ( DataPK ( DataFresh ( T51_1 ) ) ) , DataConcat ( DataUtf8 ( S A l i c e S ( ) ) , DataFresh ( T49_1 ) ) ) a t {104} 10 i n ( NethttpChan , [ . . . ] ) = DataAsymEncrypt ( DataBin ( DataPK ( DataFresh ( T53_1 ) ) ) , DataConcat ( DataUtf8 ( S A l i c e S ( ) ) , DataFresh ( T49_1 ) ) ) a t {130} 11 new T29 c r e a t i n g T29_1 a t {135} 12 out ( NethttpChan , DataBin (M_3) ) with M_3 = DataAsymEncrypt ( DataBin ( DataPK ( DataFresh ( T55_1 ) ) ) , DataConcat ( DataFresh ( T49_1 ) , DataFresh ( T29_1 ) ) ) a t {137} 13 i n ( NethttpChan , DataBin (M_3) ) with M_3 = DataAsymEncrypt ( DataBin ( DataPK ( DataFresh ( T55_1 ) ) ) , DataConcat ( DataFresh ( T49_1 ) , DataFresh ( T29_1 ) ) ) a t {105} 14 out ( NethttpChan , DataBin (M_4) ) with M_4 = DataAsymEncrypt ( DataBin ( DataPK ( DataFresh ( T51_1 ) ) ) , DataFresh ( T29_1 ) ) a t {111} 15 i n ( NethttpChan , [ . . . ] ) = DataAsymEncrypt ( DataBin ( DataPK ( DataFresh ( T53_1 ) ) ) , DataFresh ( T29_1 ) ) a t {138}

1

  let roleI skI pkB adr1 adr2 : Int32 . t = 2 let c2 = connect adr2 in 3 let c1 = listen adr1 in 4 let m_04 = skI in 5 let m_05 = pkB in 6 let m_09 = Net . recv ( c1 ) in 7 let m_13 = utf8 ( " Alice " ) in 8 let m_15 = rsa_decrypt m_04 m_09 in 9 let ( m_16 , m_17 ) = iconcat m_15 in 10 let m_14 = m_17 in 11 let m_12 = concat m_13 m_14 in 12 let m_10 = rsa_encrypt m_05 m_12 in 13 let m_11 = Net . send c2 m_10 in 14 let m_20 = Net . recv ( c2 ) in 15 let m_21 = Net . send c1 m_20 in 16 let m_22 = Net . recv ( c1 ) in 17 let m_25 = rsa_decrypt m_04 m_22 in 15 let m_23 = rsa_encrypt m_05 m_25 in 19 let m_24 = Net . send c2 m_23 in 20 let z = Net . close c2 in 0 l Listing 1.10: Role of the intruder in F $

  is a formal method software development framework proposed by Abrial et al. in 1996 based on set theory and first order logic in order to write and check code specifications. The goal is to both check consistency of specifications and code. -Frama-C [24] is a tool developed in 2012 by Cuoq et al. that performs static analysis on C programs. Various analyses are supported such as dead code deletion, value analysis or weakest-precondition calculus.

i n ( c , ( Bob ,M_1) ) with M_1 = pk ( skB_1 ) a t {5}

out ( c ,M_6) with M_6 = aenc ( n_3 , pk ( skB_1 ) ) a t {12} Listing 1.1: Example of in/out instructions.

https://ciphersuite.info/cs/

This is a common modeling practice in protocol verification, allowing the intruder to choose who A is going to talk to.

As this code is really long, we will not show it in this article.


Olivier Bethoux
email: olivier.bethoux@centralesupelec.fr

Linear Controllers: PID controller design

Keywords: Feedback control, time-domain specifications, linear controller, stability margins, PID control, zero-pole compensation, frequency-response design, performances robustness

In this paper, the issue of designing and tuning a standard three-term PID controller is addressed.

To achieve this goal, both the basics of linear controllers and the key principles of the PID controller are described. Subsequently, two popular design approaches are studied and then illustrated in a specific use case. The paper ends with a global conclusion including guidelines on extra material to address implementation issues.

INTRODUCTION

Many plants require automatic control in order to enforce specific system variables to meet the related reference values in real time. To achieve this goal, engineers need to design feedback controls of dynamic systems. It contributes to stabilize an intrinsically unstable system and enables an effective reference tracking by rejecting, at any time, system and environment uncertainties [START_REF] Bolton | Instrumentation and Control Systems[END_REF].

Energetic Macroscopic Representation, which is a graphic formalism developed for multi physics system [START_REF] Bouscayrol | Graphic Formalism for the Control of Energetic Multiphysics Systems[END_REF], is one very efficient tool to define a relevant control structure to any plant. Based on the plant model, it permits first to define the maximal control structure of the studied system and then, considering the sensors constraints, deduce the practical control structure [EEEPE 40011] [START_REF] Bouscayrol | Control structures for multi-machine multi-converter systems with upstream coupling[END_REF][START_REF] Pera | Maximal and Practical Control Structure of a PEM fuel cell system based on Energetic Macroscopic Representation[END_REF].

Designing each identified control loops comes into the realm of control systems design. This scientific field offers numerous feedback control laws. One of these solutions is the Proportional-Integral-Derivative (PID) controller which benefits from a high cost/performance ratio [START_REF] Bolton | Instrumentation and Control Systems[END_REF]. As this classic three-term controller proves to be used in most industrial applications, it is crucial for electrical engineers to master its basic principles.

The present article aims at providing the basics of PID control so that the reader could successfully tune the 3-term controller parameters in any specific use case. The suggested tuning methods are explained by way of a practical example.

The paper is organized as follows. Section 2 explains the frequency loop-shaping requirements that the selected analog controller has to meet so as to ensure high stability margin, high damping ratio (close to 1), low tracking errors and small sensitivity regarding noises and system model uncertainties. It then gives the PID controller structure and outlines the main role of each terms.

Section 3 briefly describes the studied case and defines the related control design specifications.

Section 4 addresses the control tuning using the dominant poles cancellation method. Section 5 presents an alternative approach based on the frequency-response design method. Finally, section 6 draws conclusions and perspectives of the suggested approaches, mentioning practical implementation issues such as sensitivity assessment, computer aided design, integrative antiwindup strategy, feedforward terms and digital control law enabling using microcontrollers.

CONTROLLER DESIGN OUTLINES AND PID CONTROL BASICS

As shown in figure 1, an elementary feedback control is composed of 3 blocks:

1. A plant (also called system), consisting of an actuator, a process and a sensor.

2.

A comparator computing the error 𝜀𝜀(𝑡𝑡) between the reference signal 𝑦𝑦 𝑟𝑟𝑟𝑟𝑟𝑟 (𝑡𝑡) and the controlled one 𝑦𝑦(𝑡𝑡).

3.

A controller aiming at providing in real time the control variable 𝑢𝑢(𝑡𝑡) so that the measured variable 𝑦𝑦(𝑡𝑡) accurately follows its reference value 𝑦𝑦 𝑟𝑟𝑟𝑟𝑟𝑟 (𝑡𝑡). Note that the variable being tracked is the sensor output and not the physical quantity at stake. In some cases, such as temperature or pressure controls, the slow dynamics of the sensor requires the use of a larger phase margin specification to prevent the real variable to face unexpected transient overshoot.

To analytically define the controller structure and adjust its settings, the designer needs a dynamic model of the plant. In the case where the plant mathematical description is a linear differential equation, Laplace transform is used and both the studied system and the controller are described by transfer functions: 𝐻𝐻 𝑃𝑃 (𝑠𝑠) and 𝐶𝐶(𝑠𝑠), respectively.

Fig. 1: block diagram of a feedback control.

Loop-shaping

The controller is designed to meet the

𝐻𝐻 𝐶𝐶𝑂𝑂 (𝑠𝑠) = 𝑌𝑌(𝑠𝑠) 𝑌𝑌 𝑟𝑟𝑟𝑟𝑟𝑟 (𝑠𝑠) = 𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑠𝑠) 1 + 𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑠𝑠) (1)
Hence, it derives that:

|𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑗𝑗𝑗𝑗)| ≫ 1 → 𝐻𝐻 𝐶𝐶𝑂𝑂 (𝑗𝑗𝑗𝑗) ≅ 𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑗𝑗𝑗𝑗) 𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑗𝑗𝑗𝑗) = 1 |𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑗𝑗𝑗𝑗)| ≪ 1 → 𝐻𝐻 𝐶𝐶𝑂𝑂 (𝑗𝑗𝑗𝑗) ≅ 𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑗𝑗𝑗𝑗) 1 = 𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑗𝑗𝑗𝑗) (2)
Consequently, to comply with the feedback specification, the key ideas of the loop-shaping are: • In practice, a phase margin value more than 60° combined with a gain margin value above a 10 to 15 dB threshold usually enables to limit step overshoot below 10% and ensure attractive robustness with respect to plant parameter uncertainties.

• Moreover, based on a pure integrator behavior (𝑗𝑗 0 𝑠𝑠 ⁄ ), a rough estimate of the 5% settling time tST,5% versus the cross-frequency is provided by: Next sub-section shows that the PID controller is a simple and usually efficient option to address these 3 feedback control challenges.

𝑡𝑡 𝑆𝑆𝑆𝑆,5% ≅ 3 𝑗𝑗 𝑋𝑋 (3) 3.
Fig. 2: Open-loop frequency requirements for efficient feedback control.

PID controller basics

The PID controller is defined by the time-domain equation:

𝑢𝑢(𝑡𝑡) = 𝐾𝐾 𝑃𝑃 �𝜀𝜀(𝑡𝑡) + 1 𝑇𝑇 𝐼𝐼 � 𝜀𝜀(𝜏𝜏). 𝑑𝑑𝜏𝜏 𝑡𝑡 0 + 𝑇𝑇 𝐷𝐷 𝑑𝑑𝜀𝜀 𝑑𝑑𝑡𝑡 (𝑡𝑡)� (4)
which, in Laplace transform, is:

𝐶𝐶 𝑃𝑃𝐼𝐼𝐷𝐷 (𝑠𝑠) = 𝑈𝑈(𝑠𝑠) 𝜀𝜀(𝑠𝑠) = 𝐾𝐾 𝑃𝑃 �1 + 1 𝑇𝑇 𝐼𝐼 𝑠𝑠 + 𝑇𝑇 𝐷𝐷 𝑠𝑠� = 𝐾𝐾 𝑃𝑃 � 1 + 𝑇𝑇 𝐼𝐼 𝑠𝑠 + 𝑇𝑇 𝐼𝐼 𝑇𝑇 𝐷𝐷 𝑠𝑠 2 𝑇𝑇 𝐼𝐼 𝑠𝑠 � (5)
The PID transfer function combines 3 independent additional terms:

1. The proportional term (𝐾𝐾 𝑃𝑃 ) which acts at any frequency and hence permits to adjust the cross frequency 𝑗𝑗 𝑋𝑋 and consequently the settling time 𝑡𝑡 𝑆𝑆𝑆𝑆,5% , 2. The integral term (𝐾𝐾 𝑃𝑃 𝑇𝑇 𝐼𝐼 𝑠𝑠 ⁄ ) which mainly acts at low frequency (𝑗𝑗 < 1 𝑇𝑇 𝐼𝐼 ⁄ ) providing a high gain and hence a high LF accuracy combined with an attractive rejection of model uncertainties. This term also introduces a possibly destabilizing 90°phase delay. Note that the derivative term is a non-causal element and most importantly provides high gain at HF which may amplify sensor noise. Therefore, the derivative term may be filtered in the high frequency domain as shown by the following adapted transfer function:

𝐶𝐶 𝑃𝑃𝐼𝐼𝐷𝐷,𝑟𝑟 (𝑠𝑠) = 𝑈𝑈(𝑠𝑠) 𝜀𝜀(𝑠𝑠) = 𝐾𝐾 𝑃𝑃 �1 + 1 𝑇𝑇 𝐼𝐼 𝑠𝑠 + 𝑇𝑇 𝐷𝐷 𝑠𝑠 1 + (𝑇𝑇 𝐷𝐷 𝑅𝑅 ⁄ )𝑠𝑠 � ( 6
)
where 𝑅𝑅 is usually selected in the

USE CASE

Many approaches permit tuning the 3 parameters of the PID controller to fulfill the feedback control requirements [START_REF] Rames | PID tuning rules for SOPDT systems: Review and some new results[END_REF]. The present article focuses on two main ways of addressing this issue and implements them on a practical use case to validate the suggested strategies.

Adopted use case

The mathematical description of the process at stake is a third order linear differential equation. Its related transfer function can be described by:

𝐻𝐻 𝑃𝑃 (s) = 𝐻𝐻 𝑃𝑃,0 (1 + 2𝑚𝑚 𝑎𝑎 𝜏𝜏 𝑎𝑎 𝑠𝑠 + 𝜏𝜏 𝑎𝑎 2 𝑠𝑠 2 ) • (1 + 𝜏𝜏 𝑏𝑏 𝑠𝑠) (7)
Where the dynamic model settings are given in Tab. 1.

Tab

1ST APPROACH: ZERO-POLE CANCELLATION COMBINED WITH KP TUNING

1 st Strategy outlines

The first adopted strategy is to simplify the open-loop transfer function. For this purpose, 𝑇𝑇 𝐼𝐼 and 𝑇𝑇 𝐷𝐷 are adjusted so that the 2 polynomial roots of the PID transfer function could cancel the plant dominant poles (i.e. LF poles). Then, the third parameter 𝐾𝐾 𝑃𝑃 is tuned to fulfill the feedback specification as best as possible.

1 st strategy implementation

In the present case, the plant function has 3 poles divided into a complex conjugate pair such as 2 � and a distinct HF real pole, namely 𝑝𝑝 3 = -1 𝜏𝜏 𝑏𝑏 ⁄ . Hence, setting 𝑇𝑇 𝐼𝐼 = 2𝑚𝑚 𝑎𝑎 𝜏𝜏 𝑎𝑎 and 𝑇𝑇 𝐷𝐷 = 𝜏𝜏 𝑎𝑎 2𝑚𝑚 𝑎𝑎 ⁄ permits to achieve the zero-pole cancellation approach.

𝑝𝑝 1,2 = -1 𝜏𝜏 𝑎𝑎 ⁄ �𝑚𝑚 𝑎𝑎 ± 𝑗𝑗�1 -𝑚𝑚 𝑎𝑎
Therefore, it derives the following open-loop transfer function:

𝐻𝐻 𝑂𝑂𝑂𝑂,1 (s) = 𝐾𝐾 𝑃𝑃 • 𝐻𝐻 𝑃𝑃,0 𝑇𝑇 𝐼𝐼 𝑠𝑠 • (1 + 𝜏𝜏 𝑏𝑏 𝑠𝑠) (8)
Where the only tuning parameter is the proportional gain 𝐾𝐾 𝑃𝑃 .

Subsequently, the closed-loop transfer function is expressed as a unit static gain second-order system.

𝐻𝐻 𝐶𝐶𝑂𝑂,1 (s) = 1 1 + 𝑇𝑇 𝐼𝐼 𝐾𝐾 𝑃𝑃 𝐻𝐻 𝑃𝑃,0 𝑠𝑠 + 𝑇𝑇 𝐼𝐼 𝜏𝜏 𝑏𝑏 𝐾𝐾 𝑃𝑃 𝐻𝐻 𝑃𝑃,0 𝑠𝑠 2 (9)
Its natural frequency and damping ratio are both defined using the 𝐾𝐾 𝑃𝑃 gain. Based on second-order characteristics or using a software tool, an adequate value is computed enabling to fulfil the settling time and overshoot requirements.

In sum, Tab 3 shows the settings defined by this first approach while figure 4

2ND APPROACH: FREQUENCY COMPENSATION

Essential features of the 2 nd strategy

The second suggested strategy consists in compensating the plant frequency response to achieve a global open-loop transfer function suitable with the feedback specification. For this purpose, 𝑇𝑇 𝐷𝐷 is adjusted to enhance the phase margin while 𝐾𝐾 𝑃𝑃 setting enables to get the open-loop cross frequency 𝑗𝑗 𝑋𝑋 consistent with the settling time demand. 𝑇𝑇 𝐼𝐼 parameter is set to achieve the specification without impacting the stability margins.

2 nd strategy implementation

Refering to eq. 3, a rough estimate of the desired cross frequency is:

𝑗𝑗 𝑋𝑋 ≅ 3 𝑡𝑡 𝑆𝑆𝑆𝑆,5% = 30 𝑟𝑟𝑑𝑑𝑑𝑑. 𝑠𝑠 -1 .
At this specific frequency, the plant phase is only: 𝜑𝜑 𝑃𝑃 (𝑗𝑗 𝑋𝑋 ) = -187°. With a view to attaining the 8 4

Closed-loop (b)

Open-loop (a) OS% ≈ 0.7% stability and overshoot objectives, a phase margin of no less than 60°is required. Also, a 67° phase compensation is needed. Additionally, the global gain should be 0 𝑑𝑑𝑑𝑑 at the selected cross frequency. Adopting the standard ratio 𝑇𝑇 𝐼𝐼 𝑇𝑇 𝐷𝐷 ⁄ = 4 (suggested by Ziegler and Nichols [START_REF] Ziegler | Optimum settings for automatic controllers[END_REF] or Åström et Hägglund [START_REF] Åström | Revisiting the Ziegler-Nichols step response method for PID control[END_REF] in their heuristic methods) and referring to the PID controller frequency response plotted in Figure 3, lead to adopt the parameter pair (𝐾𝐾 𝑃𝑃 , 𝑇𝑇 𝐷𝐷 ) as: (11.2 , 0.1). The choice of 𝑇𝑇 𝐼𝐼 = 4𝑇𝑇 𝐷𝐷 = 0.4 𝑠𝑠 enables keeping attractive transient behavior while achieving zero steady state error.

Tab 4 sums up the settings defined by this second method while figure 5 shows the feedback time response regarding a step reference. Note that the actual settling time is around the desired value but slightly higher than it. This is caused by the approximate relationship between the desired settling time and the tuned cross frequency (Eq. 3). If needed, and based on this first settings, the PID parameters can be adjusted.

CONCLUSION AND PERSPECTIVES

This paper aims at providing the key elements to design and tune the PID controller which remains the most commonly used control technique. Firstly, it explains the crucial concepts enabling to develop this controller in any use case. Second, it describes two of the standard approaches used to tune the 3-term controller. To make the document easier to understand and reuse, each approach is developed using the same specific example.

This basic material should facilitate the extensive understanding of PID control, which is a broad scientific and technologic area addressed in numerous scientific books. In addition, on certain matters progress is still being made by research labs over the world. To go further, partial remaining issues are:

1. The robustness of the feedback control performance. For instance, in case where the effective natural frequency is 20% lower than expected, the first approach is more impacted than the second since the optimal zero-pole cancellation is not effective anymore. Figure 6 illustrates the current step response of each method in this peculiar case. 4. When the model characteristics are well known, it is effective to add feedforward terms which would limit the action of the PID controller and hence reduce its deviation. For instance, the steady state control value deduced both from the plant model and the reference value is an appropriate feed-forward term [START_REF] Visioli | Practical PID Control[END_REF]. Indeed, it may induce a larger overshoot than expected using the selected phase margin and damping ratio. Hence, in alternative PID structures, the integrator term still acts on the error variable 𝜀𝜀 while the proportional and derivative terms only acts on the output variable 𝑦𝑦.

1 .

 1 At Low Frequency (LF), a high open-loop gain |𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑗𝑗𝑗𝑗)|, above LF boundary, implies a closed-loop gain value close to unity and hence a high steady state accuracy and an efficient tracking of LF reference signal even considering model uncertainties.

2 .

 2 At medium frequency (MF), i.e. in the transition band [𝑗𝑗 𝑋𝑋 3 ⁄ , 3𝑗𝑗 𝑋𝑋 ] around the crossfrequency 𝑗𝑗 𝑋𝑋 where |𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑗𝑗𝑗𝑗 𝑋𝑋 )| = 1, it is crucial that the MF slope is as close to -20 𝑑𝑑𝑑𝑑 𝑑𝑑𝑑𝑑𝑑𝑑𝑑𝑑𝑑𝑑𝑑𝑑 ⁄ as possible to ensure large stability margins.

  At High Frequency (HF), a low open-loop gain |𝐻𝐻 𝑂𝑂𝑂𝑂 (𝑗𝑗𝑗𝑗)|, below HF boundary, implies a low closed-loop gain value and hence a proper filtering of sensor noise as well as a suitable mitigation of the unmodelled fast dynamics of the plant.

Fig. 3 :

 3 Fig. 3: PID controller frequency response 𝑪𝑪(𝒋𝒋𝒋𝒋) based on 𝑲𝑲 𝑷𝑷 = 𝟏𝟏

Tab. 3 :Fig. 4 :

 34 Fig. 4: Step response of the plant in (a) open-loop (dashed line) and (b) in closed-loop tuned

Tab. 4 :Tab. 4 :Fig. 5 :

 445 Fig. 5: Step response of the plant in

5 .

 5 Keeping the closed-loop characteristic equation (and hence the same closed-loop poles), alternative PID structures may be introduced to modify the zeros of the closed loop transfer function. Consequently, it impacts the transient response. The key idea is to avoid the initial pulse in the control signal 𝑢𝑢 induced by the step change in the reference variable 𝑦𝑦 𝑟𝑟𝑟𝑟𝑟𝑟 .

6 .

 6 Discrete PID. Modern PID controller are usually implemented in a digital system such as a microcontroller or a FPGA device[EEEPE 40029]. Digital control requires some specific techniques to at least adapt the continuous control law. In case of specific requirements, defining the correct algebraic equation is an extensive issue based on a deep theory[START_REF] Franklin | Digital Control of Dynamic Systems[END_REF][START_REF] Godoy | RST-controller design: a rational teaching method based on two diophantine equations[END_REF].

Fig. 6 :

 6 Fig. 6: Sensitivity of the closed-loop step response

  The derivative term (𝐾𝐾 𝑃𝑃 𝑇𝑇 𝐷𝐷 𝑠𝑠) which mainly acts at high frequency 𝑗𝑗 > 1 𝑇𝑇 𝐷𝐷 ⁄ providing a stabilizing 90° phase lead which enables to adjust a cross frequency combined with large phase and gain margins.

	3.
	Low frequency boundary		-Measurement noise attenuation -Fast neglected dynamics rejection
	-Model uncertainties rejection -Steady state error mitigation	x	High frequency boundary
	Transition band ≥ 1 decade
	Pass band		Stop band
	0°-
	90°-		-Ensuring large stability margins -Fulfilling the desired settling time
	180°ω

Tab. 2: the desired feedback specification.

		.1: Dynamic model settings
	𝐻𝐻 𝑃𝑃,0	𝜏𝜏 𝑎𝑎	𝑚𝑚 𝑎𝑎	𝜏𝜏 𝑏𝑏
	0.70	159.2 ms	0.55	15.9 ms
	Tab. 1: dynamic model settings.
	3.2. Feedback control specification
	The feedback control goal is threefold (Tab 2).
	Tab.2: Feedback control specification
	𝜀𝜀 ∞	𝑡𝑡 𝑆𝑆𝑆𝑆,5%	OS%
	0.0	100.0 ms	10.0 %

1. First, obtaining a zero steady state error 𝜀𝜀 ∞ , 2. Second, achieving a settling time 𝑡𝑡 𝑆𝑆𝑆𝑆,5% of the step response on 100 𝑚𝑚𝑠𝑠 time scale, 3. Third, having an overshoot (OS%) in step response lower than 10%.

  2. The extensive use of computer-aided control systems design software tools. Once the PID control guidelines are fully understood and assimilated, these tools can provide optimized settings [EEEPE 40006]. For instance, Linear Quadratic Regulator (LQR) theory can be successfully used to design optimal PID controllers which is an attractive way to address the feedback control sensitivity with respect to noise and parameter uncertainties[START_REF] Das | LQR based improved discrete PID controller design via optimum selection of weighting matrices using fractional order integral performance index[END_REF][START_REF] Tamizi | An easy to implement and robust design control method dedicated to multi-cell converters using inter cell transformers[END_REF].

3. The practical saturation of the control variable due to actuator limitation. Whenever the control value reaches its threshold, the plant is in open-loop while the integrator keeps integrating, gradually providing a huge value. It results in large overshoots and possibly unstable response. This phenomenon is known as integrator windup. Many strategies, called anti-windup techniques, can mitigate this problem

[START_REF] Da Silva | Analysis of Anti-windup Techniques in PID Control of Processes with Measurement Noise[END_REF]

.