Karthikeyan Bhargavan
email: karthikeyan.bhargavan@inria.fr

Franziskus Kiefer

Pierre-Yves Strub
email: pierre-yves@strub.nu

hacspec: towards verifiable crypto standards

Keywords:

come   L'archive ouverte pluridisciplinaire

Introduction

Cryptographic algorithms such as those standardized by organizations like the NIST, IETF, and the ISO, are written with a focus on clarity, ease of implementation, and interoperability. To this end, standards authors employ a combination of carefully edited text, precise mathematical formulas, and pseudocode. Many standards include test vectors and some even include reference code written in popular languages like C or python. Each standard is looked over by dozens of experts before publication and then closely vetted by the developer community during implementation and deployment. Standards vs. Implemenations. Despite this care, implementing cryptographic standards remains challenging and error-prone for a variety of reasons.

First, the mathematical structure used in a cryptographic algorithm may be easy to specify but hard to implement correctly and efficiently. For example, most elliptic curve standards such as [START_REF]Elliptic Curves for Security[END_REF], require modular arithmetic over large prime fields, but implementing bignum arithmetic efficiently and correctly is hard, leading to numerous subtle bugs that are hard to find simply by testing. 1 Second, the specification of an algorithm in a standard may not account for side-channel attacks that require specific countermeasures to be implemented. For example, the natural way to implement the AES standard [START_REF] Dworkin | Advanced Encryption Standard (AES)[END_REF] leads to cachetiming attacks [START_REF] Bernstein | Cache-timing attacks on aes[END_REF] that are hard to protect against without significantly changing the main routines of the algorithm [START_REF] Käsper | Faster and timing-attack resistant aes-gcm[END_REF].

Third, standards typically do not specify the interface (API) through which applications may use the cryptographic algorithm in practice. For example, the SHA-2 specification [START_REF]Federal Information Processing Standards Publication[END_REF] specifies how a message can be hashed in one pass, but does not describe the incremental hashing interface that is commonly used, and which can be quite error-prone to implement [START_REF] Mouha | Finding bugs in cryptographic hash function implementations[END_REF].

Fourth, the security guarantees and assumptions of a cryptographic algorithm are often subtle and easy to misunderstand, leading to dangerous vulnerabilities. For example, the GCM [START_REF] Dworkin | Recommendation for Block Cipher Modes of Operation: Galois/-Counter Mode (GCM) and GMAC[END_REF] and ECDSA [START_REF] Institute | Public Key Cryptography for the Financial Services Industry: The Elliptic Curve Digital Signature Algorithm[END_REF] specifications both require unique nonces but the use of bad randomness and incorrect configuration has led to realworld implementations that repeat nonces, leading to practical attacks [START_REF] Böck | Nonce-disrespecting adversaries: Practical forgery attacks on GCM in TLS[END_REF][START_REF] Courtois | Private key recovery combination attacks: On extreme fragility of popular bitcoin key management, wallet and cold storage solutions in presence of poor rng events[END_REF].

These are just a few of the reasons why there is often a substantial gap between a cryptographic standard and its implementations. It is hard to close this gap just with testing since cryptographic algorithms often have corner cases that are reached only with low probability and some properties like side-channel resistance and cryptographic security are particularly hard to test. Instead, we advocate the use of formal methods to mathematically prove that an implementation meets the standard and protects against side channels as well as programmatically check expected cryptographic security guarantees of the spec. Formal Verification of Cryptography. A wide range of verification frameworks have been proposed for the analysis of cryptographic algorithms and their implementations. The Software Analysis Workbench (SAW) can verify C and Java implementations for input-output equivalence with specifications written in Cryptol, a domain-specific language for specifying cryptographic primitives [START_REF] Tomb | Automated verification of real-world cryptographic implementations[END_REF]. The Verified Software Toolchain can be used to verify C implementations against specifications written in Coq [START_REF] Appel | Verified software toolchain[END_REF]. HACL is a library of modern cryptographic algorithms that are written in F , verified against specifications written in F , and then compiled to C [START_REF] Zinzindohoué | HACL*: A verified modern cryptographic library[END_REF]. Fiat-Crypto generates efficient verified C code for field arithmetic from high-level specifications embedded in Coq [START_REF] Erbsen | Simple high-level code for cryptographic arithmetic -with proofs, without compromises[END_REF]. Vale can be used to verify assembly implemenations of cryptography against specifications written in Dafny or F [START_REF] Bond | Vale: Verifying high-performance cryptographic assembly code[END_REF]. Jasmin is another crypto-oriented assembly language verification tool with a verified compiler written in Coq [START_REF] Almeida | Jasmin: High-assurance and high-speed cryptography[END_REF]. EasyCrypt can be used to build cryptographic game-based security proofs for constructions and protocols written in a simple imperative language [START_REF] Barthe | Easy-Crypt: A Tutorial[END_REF]. The Foundational Cryptography Framework (FCF) mechanizes proofs of cryptographic schemes in Coq [START_REF] Petcher | The foundational cryptography framework[END_REF]. CryptoVerif can be used to develop machine-checked proofs of cryptographic protocols written in the applied pi calculus [START_REF] Blanchet | A computationally sound mechanized prover for security protocols[END_REF].

In order to benefit from any of these verification frameworks, the first step is to write a formal specification of the cryptographic algorithm. Since each framework uses its own specification language, this step can be tedious, timeconsuming, and error-prone. Furthermore, the resulting formal specification is often tailored to suit the strengths of a particular verification framework, making it difficult to check the conformance of the specification with the standard or to compare it with other formal specifications.

Ideally, the published standard would itself include a formal-enough reference specification from which these tool-specific specs could be derived. Indeed, standards bodies have considered incorporating formal languages in the past. Since 2001, the IETF has a guideline on the use of formal languages in standards, which sets out sensible requirements, such as "The specification needs to be verifiable". 2 Nevertheless, the use of formal languages in cryptographic standards has not caught on, probably because authors did not see a significant benefit in exchange for the time and effort required to write formal specifications.

In this paper we propose hacspec, a new domain-specific formal language for cryptographic algorithms that we believe is suitable for use in standards. The language comes equipped with syntax and type checkers, a testing framework, and several verification tools. Hence, standards authors can use it to formalize, test, and verify pseudocode written in hacspec before including it in the standard. Furthermore, the language provides a common front-end for various cryptographic verification frameworks, so that proofs in these frameworks can be precisely compared and composed.

The authors believe that it is vital for a cryptographic standard to not only specify the mathematical algorithm describing the standard but also to allow engineers to implement the specification securely. In order to securely implement a specification it is important to make sure that the implementation is correct, i.e. that the implementation is functionally equivalent to the specification. This is especially important for highly optimized implementations that are hard to verify manually. The mechanisms proposed in this paper allow to prove this correctness property. The proposed tools further allow to prove cryptographic properties of the specified algorithm as well as security properties of an implementation. While these additional proofs do not necessarily belong into a specification of an algorithm, it makes the specification the single document of reference when implementing the algorithm or examining its security.

hacspec is designed in order to keep the barriers of entry low by being very close to what some specification authors use already and most engineers, mathematicians, and researchers are familiar with. Because of the design and additional benefits hacspec offers the authors believe that hacspec has a good chance to get adopted by specification authors.

Contributions and Outline

The design of hacspec originates from discussions at the HACS workshop 3 held alongside the Real-World Crypto conference 2018. The workshop participants included crypto developers for many major crypto libraries as well as researchers behind many popular verification frameworks. Together, we sought to achieve a balance between developer usability and ease of formal verification. This paper is the realization and continuation of the discussions and outcomes of that group.

We present hacspec in Section 2, a new specification and verification architecture for cryptographic standards. We describe the syntax of the hacspec language and show how it can be used to write cryptographic specifications on some examples in Section 3. We present compilers from hacspec to F and EasyCrypt and show how the resulting specifications are used as verification targets in formal proofs in Section 5.1 and 5.2. Finally, we present our current status and ongoing work in Section 6. Everything described in this paper is implemented and available in the hacspec git repository. 42 Architecture and Design Goals Figure 1 depicts the proposed architecture of hacspec and design workflow. In the remainder of this section we describe each component and its design goals. In subsequent sections, we will describe in more detail how our current tool-set realizes these goals, and we will present preliminary results. A new specification language. hacspec is a new domain-specific language for cryptographic algorithms that aims to build a bridge between standards authors and formal verification tools. Consequently, the language needs to be familiar to spec writers, mathematicians, and crypto developers alike, but with precise semantics that can be easily translated to various formal specification languages.

We chose to design hacspec as a subset of python (version 3.6.4) since python syntax is already used as pseudocode in various standards, e.g. [START_REF] Langley | Elliptic Curves for Security[END_REF][START_REF] Josefsson | Edwards-Curve Digital Signature Algorithm (EdDSA)[END_REF], and hence is familiar to standards authors and crypto developers. Python is especially well suited for this task since it is an imperative language that supports native bignums (arbitrary-size integers) and has an expressive type annotation syntax. As we will see in Section 3 we restrict and enhance the python syntax in many ways to enable compilation to typed formal specifications. Scope and Limitations. Although hacspec may eventually be used as a starting point for specifying cryptographic protocols and APIs, we emphasize that capturing anything other than cryptographic algorithms is out of scope for hacspec at this point. By focusing only on cryptographic algorithms, we believe we obtain a simpler syntax and are able to design more usable tools. Also note that the language as defined in Section 3 currently does not allow to use more advanced concepts such as higher-order functions. Because it would increase the complexity of the compiler, more advanced features -while planned -are left for future work. Syntax and Type Checking. Since specifications written in hacspec are meant to be used as a basis for formal proofs, it is important that the specs themselves . hacspec specification and verification architecture. Authors of cryptographic standards write their alogrithm in hacspec, aided by the syntax and type checker. They can then test their specs by executing the spec in python (along with an implementation of the builtin library). They can also use spec compilers to generate formal specifications in languages like F , EasyCrypt, etc., that can in turn be used as the basis for verifying the correctness of various implementations, or for proving the cryptographic security guarantees of the algorithm.

are correct. We propose several static and run-time tools that can find common programming errors in hacspec specifications.

First, we provide a syntax checker written in python that can find simple errors and reject specifications that use python features or control structures that are not supported by our domain-specific language. Second, we use a runtime type checker plugin for python called TypeGuard to find type errors in hacspec specifications. Using these two tools, authors who only have python on their system can already author and check hacspec specifications.

As a third tool, we also provide a static type checker for hacspec written in OCaml which can find violations of the annotated types at compile time. In addition to finding type errors, this typechecker generates a typed abstract syntax tree (AST) that is then used as a basis for our spec compilers.

Running & Testing Specifications. A key goal of hacspec is that the specifications should be executable. hacspec specifications are already written in a subset of python but they use many domain-specific types and data structures. We provide a library written in python that implements these builtin types and data structures, so that the specification can be run by a standard python interpreter and tested against test vectors.

Hence, a hacspec can also be seen as a reference implementation of the standard that can be used to guide other implementations and test them for correctness. However, these specs should clearly not be used in real-world deployments as they are not intended to be side-channel free or performant. Verifying Implementations. The hacspec language is designed to support compilation to formal specifications for a variety of verification frameworks. We present a compiler from hacspec to F in Section 5.1 and show that specifications generated by this compiler can be used to verify implementations written in Low , a subset of F that can be compiled to C.

We also envision compilers from hacspec to Cryptol and Coq models that can serve as formal specifications for verifying code written in C, Java, and assembly, using the SAW, Fiat-Crypto, VST, and Jasmin verification frameworks. Verifying Cryptographic Security. Formal specifications compiled from hacspec can also be used as the basis for cryptographic proofs. We present a compiler from hacspec to EasyCrypt in Section 5.2 and show how such specifications can be used to prove that a construction meets its cryptographic security guarantees under precise assumptions on its underlying primitives. Hence, we intend for hacspec to provide a starting point for mechanized cryptographic proofs of standards. We also envision compilers that can generate specifications for other cryptographic verification frameworks like FCF [START_REF] Petcher | The foundational cryptography framework[END_REF].

The hacspec Language

In this section, we will describe the syntax of hacspec language. As we shall see in Section 3.2 this syntax is already adequate to write cryptographic algorithms. But for developer convenience we also provide a builtin library that contains a number of commonly-used types, constants, operators, and functions. This library is described in Section 3.3.

hacspec syntax

The full syntax of hacspec is depicted in Arrays can be accessed in two ways: a[i] reads the i'th element of an array a; a[i:j] copies a slice of the array a from index i (inclusive) to index j (exclusive) into a fresh array and returns the result.

A function call, written f(e1,...,en), calls the function f that may be userdefined or from the builtin library. A special case of builtin functions are unary and binary infix operators (e.g. arithmetic operators like +, bitwise operators like <<, and comparison operators like ==).

Functions in hacspec are call-by-value, the arguments to the function are first evaluated, then the resulting values are copied into the arguments of the function, and then the function is called with these arguments. The function itself may allocate and modify local state, as we will see below, but all this state is deallocated when the function returns; only the output of the function remains. Consequently, function calls are observationally pure, i.e. they have no side effects and hence can be treated as pure functions that return a fresh result.

Notably, all hacspec expressions produce a fresh value: even when an expression evaluates to an array, the resulting value is a fresh array value, not a pointer into or an alias to some other array. Types. The basic types in hacspec are integers (int), booleans (bool), and strings (str). Types can be parameterized, that is, they are defined as functions over both types and values; such parametric types can be instantiated by applying them to specific types and expressions x(t1,...,tn,e1,...,em). Two special cases of such parametric types are tuples and arrays. Each n-tuple has a type tuple_t(t1,...,tn), where the first component has type t1, the second has type t2, and so on. Arrays have type vlarray_t(t), where the contents of the array have type t. These are called variable-length arrays since their length is only known at run-time.

As we will see, the builtin library defines more types and type constructors for writing refinement types, which can be used to annotate and check specs for more advanced logical properties. Statements. A hacspec specification is a sequence of statements, each of which defines a global constant, a type, or a function. Such statement sequences are written one on each line (hence with a newline as a separator), with the indentation of each line indicating the block that the statement belongs to. This syntactic convention, taken from python, simplifies and unclutters the specification by removing the need for block and statement separators.

All variables must be declared before use; thus the statement x:t declares a new variable x that has type t, whereas the statement x:t = e declares and initializes x that has type t to the value obtained by evaluating e. New type abbreviations are defined by writing x:Type = t; by convention all user-defined type names are suffixed by _t (e.g. vlarray_t).

Local variables can be modified with an assignment x = e or an augmented assignment, e.g. x += e, which applies a binary operator before assignment. Note, however, that global variables in a specification are constant; they are assigned a value at initialization time and never change thereafter. Within a function body, we can read global variables and the function arguments, but we may only modify declared function-local variables.

Arrays held in local variables can be modified by the statement x[i] = e, which constructs a new array value by setting the i'th value in the current value of the array x to the result of evaluating e and writes this new array value into x. We may also modify a slice of an array by writing x[i:j] = e, which copies the array value resulting from evaluating e into the indicated slice of array x.

Conditional expressions and for-loops are standard, except that we allow the use of elif to combine an else with a subsequent if, and we allow the use of break to escape from a loop early. Each branch of a conditional, and each loop body is itself a sequence of statements, one on each line and indented appropriately.

Functions are defined with types annotating their arguments and results: def f(x1:t1,...,xn:tn)→t declares a new function called f with n arguments x1,...,xn with types t1,...,tn, and returns a result of type t. The body of the function is a sequence of statements; notably, the statement return e returns from the function with the evaluation of e as the result.

Each specification has a name (the name of the file in which it resides) and a sequence of statements that defines a cryptographic algorithm. Specifications can refer to other specifications by importing selected variables from the other specification into its own namespace by writing e.g. from otherspec import function1.

Example: Poly1305

Using the syntax defined above we can now write specifications like the Poly1305 MAC algorithm [START_REF]ChaCha20 and Poly1305 for IETF Protocols[END_REF]. An excerpt of this hacspec, showing the core polynomial computation, appears in Spec 1.

The first 5 lines define the field of integers modulo the prime p = 2 130 -5. Line 1 declares and initializes the global variable p. The functions fadd (Lines 2-3) and fmul (Lines 4-5) define addition and multiplication in the field (modulo p). Both functions take two arguments of type int and return an int.

The function poly evaluates a polynomial over the prime field at a particular field element and returns the result. A polynomial of degree n is represented by an array of integers, where the 0'th element of the array contains the n'th coefficient, the (n-1)'th element contains the first coefficient, and the coefficient with degree 0 is assumed to be 0.

In the Poly1305 MAC algorithm, this array of coefficients is an encoding of the plaintext (text), and the value at which it is being evaluated is the MAC key (key). The body of the poly function first declares the local variable result of type int and initializes it to 0. It then iterates over the length of text with a for-loop. The loop body (Line 10) updates the value of result by multiplying (fmul) the key with the sum (fadd) of the previous result and the i-th coefficient in text. Thus, for a text of size n, this function computes the field element:

key n • text[0] + key n-1 • text[1] + . . . + key • text[n -1] modulo p.

The Builtin Library

hacspec comes with a builtin library that implements many common functionalities needed by cryptographic algorithms. The full list of provided functions and types can be found in the hacspec documentation. 1 While it is possible to write specs entirely with the syntax defined in Table 1, the builtin library makes writing precise specs easier and simplifies compilation and formal proofs. The set of cryptographic primitives (specs) implemented while working on hacspec (see Section 6 for details on the currently implemented primitives) can be used as well but are not provided as a library right now. Modular Arithmetic. As we saw in Spec 1, cryptographic algorithms often rely on arithmetic modulo some (large, not necessarily prime) integer. The builtin library defines a type called natmod_t(n), representing natural numbers modulo n (the set {0, . . . , n -1}). It also defines modular arithmetic operations +, -, *, ** (addition, subtraction, multiplication, exponentiation) on values of this type.

Hence, using the natmod_t type, we can rewrite the Poly1305 specification as shown in Spec 2. We first define a type felem_t for the field elements (naturals modulo p). We can then directly use * and + for field operations, without needing to define fadd and fmul. Furthermore, the spec is now more precise: it requires that the arguments of poly are in the prime field and guarantees that the result of polynomial evaluation is a field element, and violations of this post-condition can and should be checked in the spec and its implementations.

The type refine_t(t,f) takes a type t and a predicate f from type t to bool, and returns a new type that represents values of type t that satisfy f. Elements of this new type can be implicitly converted to elements of type t but not vice-versa. Refinement types can be used to encode arbitrary logical invariants and are extensively used in verification frameworks like F and Coq. When a refinement type is used on a function argument, it becomes a precondition for calling the function; when it is used in the result type, it becomes a post-condition guaranteed by the function. Since refinement predicates can be arbitrarily complex, checking refinement types is not always easy. We show how these types can be checked at run-time, using the python plugin Typeguard, or can be verified statically with powerful verification tools like F .

Not all function specifications can be written using refinements. For example, refinements cannot specify how the result of a function relates to its arguments. We are experimenting with a general contract mechanism for hacspec, implemented as annotations, that can fill this gap.

Checking and Executing hacspec

We expect the hacspec language to be used at two levels. Standards authors and cryptographic researchers may write a hacspec for a new cryptographic algorithm and include it as pseudocode in a standard or in a research paper. They would like to easily check their spec for syntax and basic type errors and test it for correctness errors. For such users we provide tools written in python so that they do not need to install or learn any new tool to be able to achieve their goals.

More advanced users will want to check their hacspec for deeper properties, ranging from logical invariants to cryptographic security. They may also want to verify that an implementation of the algorithm, written in C or assembly, is correct with respect to the hacspec. For these users, we provide a syntax and static type checker, and compilers to various verification frameworks. To run these tools, one must install OCaml as well as the target verification tool. Note that verifying existing implementations requires a compilation target such as cryptol or VST that do not exist yet.

In this section, we describe our tool-set for checking and running hacspec and highlight the main challenges in implementing these tools.

Syntax and Static Type Checking

Since hacspec is a subset of python, specification authors used to python may be tempted to use python features that are not supported by our domain-specific language. To check that a hacspec is valid we have built a python tool called hacspec-check that is part of the hacspec python package. This checker enforces the syntax in Table 1; it finds and points out invalid expressions, types, and statements, and forbids the use of external values and functions that are not included in the builtin library.

The syntax checker only ensures that the type annotations in a hacspec have the right syntax, it does not check that the code is type-correct. We wrote an additional tool in OCaml that statically enforces the hacspec type system. It requires that all variables be declared before use, and that they are used in accordance with their declared type. This tool does not perform any inference, but still, it must account for basic types (like int), builtin types (like uint32_t), and parameterized types (like array_t(t,l)). The checker also knows and enforces the types for all the builtin operators and functions in the builtin library. In particular, the type-checker prevents aliasing of mutable data structures like arrays, by ensuring that two array variables never point to the same array value -when assigning an array variable, the assigned value must be a fresh copy of an array.

Executing hacspec with Run-time Checks

Because hacspec uses python syntax it can be directly executed using the python runtime. We provide a python implementation, called speclib.py, for the builtin library. To make hacspec easy to use for spec authors the library and the hacspec-check command line tool are bundled in the hacspec python package. 1After installing this package, the spec author can include the standard library: from hacspec.speclib import * and write and run specifications.

Our python library uses python classes to implement the various types and type constructors: natmod_t, uintn_t, array_t, etc. Each class defines the relevant unary and binary operators (e.g. +) for a type by overloading the corresponding python "magic" methods (e.g. __add__) in that class. We define each of these operator methods to first check that the left and right expressions are both of the expected type, before calculating the result and casting it to the expected return type. Python also allows us to define custom getters and setters for arrays using the standard syntax (e.g. a[1] += b [START_REF]ChaCha20 and Poly1305 for IETF Protocols[END_REF]), and we overload these methods to check that the array and the assigned values have a consistent type, and that all indexes are within bounds, before executing the expected array access operation. Vectors and matrices are sub-classes of arrays but are provided with point-wise binary operators that are subject to further checks.

Although python allows a rich type annotation syntax (allowing arbitrary expressions to compute types), it does not itself check these types. However, there are various tools and plugins that can check type annotations statically or at runtime. For example, mypy2 can perform basic static type checking, but unfortunately it does not not support everything needed by hacspec, e.g., generic types, custom types, or type aliases. Instead, we use run-time type checking with typeguard3 , which allows spec authors to quickly get feedback on the correctness of their used types without having to use an additional execution environment.

Typeguard checks functions that are annotated with the @typechecked decorator for conformance to their declared types. We annotate all the functions in our builtin library and hence require that they be used correctly. The same is required from all user-written hacspec functions. In addition to the checks built into Typeguard, our library functions themselves perform a variety of builtin semantic checks that can detect common coding errors in hacspec specifications. For example; Every array access is bound-checked to make sure that it is not over-or under-running the array; When modifying array elements type checks ensure that only compatible values are added; Arithmetic operations ensure that only operands of appropriate bit-lengths and moduli are used, e.g., rotate and shift functions ensure that the shift values are positive and not greater than the integers bit-length; Using refinement types ensures that the type is correct and within the refined value range.

For each specification we encourage authors to provide an extensive test-suite as a list of positive and negative test vectors. These should include all the testvectors provided in the standard but also other test-suites, such as those provided by NIST4 or open-source projects like Wycheproof5 . Running tests on the code with run-time type-checking can make the execution very slow but provides higher assurance in the spec. Our specs can also be tested in an optimized mode that disables these run-time type-checks.

Verifying hacspec

For advanced users, we describe two verification tools we are currently building for hacspec: one for verifying implementations using F and the other for building cryptographic proofs in EasyCrypt. Both tools are based on the typed AST, generated by the hacspec static type-checker.

F Compiler

F is a general-purpose programming language targeted at building verified software [START_REF] Swamy | Dependent types and multi-monadic effects in F*[END_REF]. In particular, it has been used to build a verified cryptographic library called HACL [START_REF] Zinzindohoué | HACL*: A verified modern cryptographic library[END_REF]. For each cryptographic algorithm HACL includes an optimized stateful implementation written in a subset of F called Low . Code written in this subset can be compiled to C code and hence used within cryptographic protocol implementations, such as TLS libraries.

The Low implementation of each algorithm is verified for functional correctness against a formal specification written in F . Unlike the implementation, the specification is pure and total; i.e. it cannot have any side-effects and must always terminate. In addition to correctness, Low code is also proved to be memory safe and have secret independent execution time, i.e. it does not branch on secret values or access memory at secret addresses.

HACL includes hand-written specifications for all the algorithms in the library. Our goal is to replace these specifications with those written in hacspec and to make it easier for new HACL specifications to be compiled from hacspec. To this end we develop a compiler from hacspec to F specifications.

First, we implement the hacspec builtin library as an F module (SpecLib.fst), so that the compiled F specifications can also have access to all the types and functions used in the source specification. This library module defines hacspec types like int, natmod_t, vlarray_t etc. in terms of the corresponding types in the F standard library. In particular, hacspec arrays (vlarray_t(t)) are implemented as immutable sequences (seq t) in F . We implement all unary and binary operators using function overloading in F .

Then, we implement a translation from hacspec specifications to F modules that syntactically transforms each value, expression, and statement to the corresponding syntax in F . For example, the Poly1305 specification in Spec 2 translates to the F specification in Spec 3. The main syntactic change in the F version is that all statements that modify local variables get translated to pure expressions (in a state-passing style) that redefine the local variables (using scoped let-expressions) instead of modifying them. For loops are translated to an application of the higher-order repeati combinator, which applies a function a given number of times to the input. In addition to the syntactic translation of the code, the F compiler translates hacspec refinement types to refinement types in F , so that the F typechecker can verify all of them statically using an SMT solver.

In a typical workflow the standard author writes a hacspec for a cryptographic algorithm, translates it to F , and typechecks the result with F to find progamming errors. The crypto developer then writes an optimized implementation of the algorithm in Low and verifies that it is memory-safe, secret independent, and that it conforms to the specification derived from the hacspec. For example, a Low implementation of Poly1305 would first need to implement the modular arithmetic in natmod_t with prime-specific optimized bignum arithemetic. The developer would then typically write a stateful version of poly that modified the result in-place. Proving that this implementation matches the specification is a challenging task, but one made easier by libraries of verified code in HACL .

EasyCrypt Compiler

EasyCrypt is a proof assistant for verifying the security of cryptographic constructions in the computational model. EasyCrypt adopts the code-based approach [START_REF] Barthe | Easycrypt: A tutorial[END_REF], in which security goals and hardness assumptions are modeled as probabilistic programs (called experiments or games) with unspecified adversarial code. EasyCrypt uses formal tools from program verification and programming language theory to rigorously justify cryptographic reasoning.

EasyCrypt is composed of several ingredients: i) a simply-typed, higherorder, pure functional language that forms the logical basis of the framework; ii) a probabilistic While language that allows the algorithmic description of the schemes under scrutiny; and iii) programming language logic. These logic include a probabilistic, relational Hoare logic, relating pairs of procedures; a probabilistic Hoare logic allowing one to carry out proofs about the probability of some event during the execution of a procedures; and an ordinary (possibilistic) Hoare logic.

The compiler from hacspec to EasyCrypt is composed of two phases. First, the types and procedures are translated from the hacspec syntax to the relevant EasyCrypt constructions. Since EasyCrypt enjoys a simply-typed language discipline, nearly all refinements have to be pruned during this phase. However, we have some special support for types that depend on fixed values: in that case, we define a generic theory that encloses the dependent type and use the Easy-Crypt theory cloning for generating instances of that type for some fixed values. This translation relies on a EasyCrypt library that mirrors speclib. When the translator detects that a procedure is pure, deterministic and terminates (w.r.t. the EasyCrypt termination checker), this one is translated directly as a logical operator. In all other cases, hacspec procedures are translated to While-based EasyCrypt ones. Some constructions ares not supported by the current compiler. For example, EasyCrypt does not allow the definition of recursive procedures and inner procedures and we currently simply reject them. We plan to modify the compiler so that it encodes these constructs as valid EasyCrypt programs.

In a second phase, top-level refinements (i.e. refinements that apply to the arguments or result types of a procedure) are translated into EasyCrypt statements using the probabilistic Hoare logic. We give, in Spec 4, the Poly1305 specification in Spec 2 translated to EasyCrypt. From that point, it is then possible to use EasyCrypt to prove these statements, hence verifying the soundness of the hacspec refinements directly in Easy-Crypt. However, we expect developers to follow a two-tier workflow. First, developers can use the F compiler of Section 5.1 and derive the correctness of the refinements using the F type-checker. Because both F and EasyCrypt work on the same specification by construction (they are obtained from the compilation of the same hacspec procedure), this step enforces that the refinements that are translated as Hoare statement into EasyCrypt are sound. In a second step, developers could take advantage of EasyCrypt to prove the security of the obtained primitives. Indeed, EasyCrypt comes with all the necessary materials (relational probabilistic logic, libraries of standard cryptographic games, experiments & arguments) for the study of cryptographic primitives in the computational model, using the now standard game-hopping technique. For example, in addition to Poly1305, one could also write in hacspec the Chacha20 encryption scheme, obtain their EasyCrypt counter-part, and prove in the same system that they provide a secure AEAD (Authenticated Encryption with Associated Data) scheme. This, along with the verified Low implementation of Chacha20-Poly1350, would lead to an efficient and formally proven secure AEAD scheme.

Note that by the different nature of the two involved languages (hacspec & EasyCrypt), the obtained EasyCrypt specification might not be in total adequacy with EasyCrypt idioms. However, using EasyCrypt relational logic, one can start by first proving that the hacspec specifications simulate a handwritten, more natural, EasyCrypt one. Although this requires more work to link the EasyCrypt proofs to the hacspec specifications, it gives a formal link between the two.

Evaluation, Conclusion, and Future Work

To evaluate hacspec we implemented several standardized cryptographic algorithms using only the builtin library. Table 2 summarizes the specifications we currently have written and tested in hacspec as well as their F version if available. Even more complex algorithms such as Kyber or the SHA2 and SHA3 function families (with all their variants including SHAKE), as well as combined algorithms like the AES-GCM and ChaCha20-Poly1305 AEAD can be written in less than 300 lines of hacspec. (The combined AEAD algorithms in Table 2 list the lines of code for the combination of cipher and MAC as well as the combined lines of code of cipher and MAC.) Modern algorithms that are designed to have rather straight-forward implementations like Poly1305 or Curve25519/Curve448 can be implemented in 50 to 70 lines of code. This shows that hacspec allows concise specifications of common cryptographic algorithms.

The last column in Table 2 lists the lines of F code that is produced when compiling the hacspec code. Not all specs can be compiled to F at this point because some hacspec constructs are not fully supported by the compiler yet. The hash algorithms SHA2, SHA3, and Blake2 for example use inner functions for like to see more compilers to other formal languages such as cryptol and Coq to allow formal proofs of specifications using hacspec in those frameworks.

Fig. 1

 1 Fig.1. hacspec specification and verification architecture. Authors of cryptographic standards write their alogrithm in hacspec, aided by the syntax and type checker. They can then test their specs by executing the spec in python (along with an implementation of the builtin library). They can also use spec compilers to generate formal specifications in languages like F , EasyCrypt, etc., that can in turn be used as the basis for verifying the correctness of various implementations, or for proving the cryptographic security guarantees of the algorithm.

Spec 1 .

 1 Poly1305 hacspec 1 p:int = 2 ** 130 -5 2 def fadd(x:int, y:int) -> int: 3 return (x + y) % p 4 def fmul(x:int, y:int) -> int: 5 return (x * y) % p 6 7 def poly(text:vlarray_t(int), key:int) -> int: 8 result: int = 0 9 for i in range(array.length(text)): 10 result = fmul(key,fadd(result, text[i])) 11 return result

Spec 3 .

 3 Poly1305 hacspec using the builtin library 1 let p : nat = (2 ** 130) -5 2 type felem_t = natmod_t(p) 3 let poly (text:vlybtes_t) (key:felem_t) : felem_t = 4 let result = natmod(0, p) in 5 repeati (length text) 6 (fun i result -> key * (result + text.[i])) 7 result

Spec 4 .

 4 Poly1305 hacspec using the builtin library 1 op p : int = 2 ^130 -5. 2 3 clone import NatMod as FElem_p with op size <-p. 4 5 module Spec = { 6 proc poly(text : byte array, key : felem_t) : felem_t = { 7 var result = FElem.zero, i; 8 i = 0; while (i < Array.length text) { 9 result = key * (result + FElem.mk (Byte.to_int (text.[i])

Table 1 ,

 1 divided in terms of values, expressions, types, statements, and specs. Values. Specifications in hacspec define computations over values. The simplest values are arbitrary-size integers, booleans, and strings. Integer constants can be written in decimal, binary, octal, or binary; booleans are True or False; string constants begin and end with quotes (" or '). The builtin library defines additional constants. The two main data structures used in hacspec are tuples and

	Values v ::=	n	integer constants
		| True | False	boolean constants
		| '...' | "..."	string constants
		| (v1,...,vn)	tuple constant
		| array([v1,...,vn])	array constant
	Expressions e ::= v	values
		| x | m.x	local and global variables
		| (e1,...,en)	tuple construction
		| array([e1,...,en])	array construction
		| array.length(e)	array length
		| e[e0]	array access
		| e[e0:e1]	array slice
		| e(e1,...,en)	function call
		| e1 binop e2	builtin binary operators
		| unaryop e	builtin unary operators
	Types t ::=	int, str, bool	basic types
		| tuple_t(t1,...,tn)	tuples
		| vlarray_t(t)	variable-length array
		| x	user-defined or builtin type
		| x(t1,...,tn,e1,...,em)	builtin type application
	Statements s ::= x: Type = t	type declaration
		| x: t	variable declaration
		| x = e	variable assignment
		| x binop= e	augmented variable assignment
		| (x1,..,xn) = e	tuple matching
		| x[i] = e	array update
		| x[i] binop= e	augmented array update
		| x[i:j] = e	array slice update
		| if e:	if-elif-else conditional
		s1...sn
		elif e:
		s1'...sn'
		else
		s1''...sn''
		| for i in range(e):	for loop
		s1...sn
		| break	break from loop
		| def x(x1:t1,...,xn:tn) → t: function declaration
		s1 ... sn
		| return e	return from function
		| from x import x1, x2,..., xn module import
	Specs σ ::=	s1...sn	sequence of statements

Table 1

 1 . Tuple constants are written (v1,...,vn), parentheses are optional, and array constants are written array([v1,...,vn]). Expressions. Expressions represent purely functional computations that yield values without any side-effects. Expressions include values as well as tuples and arrays constructed with a sequence of expressions (evaluated left to right). Variables (x) may be local or global; global variables may be qualified by a module name (e.g. array.empty). Global variables may only be assigned once when they are initialized; thereafter they are read-only.

. hacspec syntax: values, expressions, types, statements, and specifs. For types, constants, functions, and operators provided by the builtin library, see Section 3.3.

arrays

https://www.ietf.org/iesg/statement/pseudocode-guidelines.html

https://hacs-workshop.github.io/

https://github.com/hacs-workshop/hacspec/

https://hacs-workshop.github.io/hacspec/docs/

https://pypi.org/project/hacspec/

http://www.mypy-lang.org/

https://github.com/agronholm/typeguard/

https://csrc.nist.gov/Projects/Cryptographic-Algorithm-Validation-Program

[START_REF] Barthe | Easycrypt: A tutorial[END_REF] https://github.com/google/wycheproof

Acknowledgments. We would like to thank all participants of the HACS workshop that made this work possible. hacspec is an ongoing project with a number contributors in addition to the the authors. Online Materials. hacspec source code: https://github.com/hacs-workshop/hacspec/ hacspec builtin library documentation: https://hacs-workshop.github.io/ hacspec/docs/ hacspec mailing list: https://moderncrypto.org/mailman/listinfo/hacspec

Machine Integers. A special case of natmod_t(n) are integers of a certain bitlength, i.e. when n is of the form 2 l . In particular, many cryptographic algorithms are defined over machine integers like unsigned 32-bit integers, which correspond to natmod_t(2 ** 32). The builtin library defines types for commonly used machine integers like uint8_t, uint16_t, uint32_t, uint64_t, and uint128_t as well as an arbitrary-length unsigned integer type uintn_t(n). These integers provide the usual arithmetic operators like natmod_t but further provide bitwise operators ^, |, &, <<, >> (xor, or, and, left-shift, right-shift) and the unary operator ∼ (bitwise negation). In addition, the library defines functions for rotating machine integers, and converting between integers of different sizes.

Byte-arrays, Vectors, and Matrices. The library defines abbreviations for several commonly-used variants of arrays. For example, the type array_t(t,l) represents arrays of type t and length l, a special case of the vlarray_t(t) type.

The type vlbytes_t represents variable-length byte-arrays (vlarray_t(uint8_t)), which are commonly used as inputs and outputs of cryptographic algorithms. The corresponding fixed-length byte-array type is bytes_t(l). These byte-array types provide library functions that convert byte-arrays to and from arrays of machine integer values; for example, the functions bytes.from_uint32s_le and bytes.to_uint32s_le inter-convert byte-arrays and uint32_t arrays, interpreted in little-endian order. Another useful special case of arrays are vectors (vector_t(t,l)), which represent fixed-length arrays of numeric types. The content of a vector is either an integer (int), or natmod_t(n), or uintn_t(l), or another vector type. The advantage of using vectors is that they offer pointwise arithmetic operators (+,-,*,**), as well as standard functions like dot-products. We can build multi-dimensional vectors as vectors of vectors, but the builtin library provides a special type matrix_t(t,rows,cols) for two-dimensional vectors, for which it defines matrixvector and matrix-matrix multiplication functions.

Type Abbreviations, Refinements, and Contracts. For the most part, specification authors can use just the types in the standard library to write their specs and use local type abbreviations when needed, for clarity, like the felem_t type in Spec 2. However, in many cases we may want to define a more specific type that represents a subset or a refinement of an existing type. The builtin library already provides commonly used refinements, like nat_t (integers ≥ 0), pos_t (integers > 0) and range_t(s,e) (integers from s to e -1). In addition, it provides a construct for users to define their own refinement types. concise handling of multiple digest lengths, which can not be properly compiled to F at the moment. Conclusion. In this paper we described the goals and architecture of hacspec, a new specification language for cryptographic algorithms. We defined hacspec as a domain-specific language with minimal syntax that can be interpreted by the python runtime. We showed that together with a builtin library hacspec allows to write succinct specifications of cryptographic algorithms. To allow spec authors to use hacspec without much effort we provide an implementation of the builtin library in python and a tool to check the spec syntax. To verify specs written in hacspec we showed how to compile specs to F and EasyCrypt. This enables formal proofs of correctness of code with respect to the spec, proves of protection against side channels and memory issues, as well as cryptographic security proves.

Future Work. The compiler and builtin library are still in early stages and are likely to evolve over time. Additional library features such as function contracts are in development. The goal of this work is to describe the current state of hacspec and invite spec authors to use it and give feedback to guide future development of the hacspec language, the builtin library, and tooling. We would


Swann Marx
email: marx.swann@gmail.com.

Yacine Chitour
email: yacine.chitour@lss.supelec.fr.

Christophe Prieur
email: christophe.prieur@gipsa-lab.fr

Stability analysis of a 1D wave equation with a nonmonotone distributed damping

Keywords: 1D wave equation, nonlinear control, Lyapunov functionals

. The asymptotic behavior analysis is based on an attractivity result on a specific infinite-dimensional linear time-variant system.

INTRODUCTION

This paper is concerned with the asymptotic behavior of a one-dimensional wave equation subject to a nonmonotone nonlinear damping. For control systems, it is always crucial to consider nonlinear feedback laws. In particular, the definition of the nonlinearity under consideration in this paper includes the saturation, which models amplitude limitations on the actuator. Such a phenomenon appears in most of control systems, and it can lead to undesirable behavior in terms of stability. Moreover, considering that such a nonlinearity is nonmonotone is crucial for control systems, because the model of the nonlinearity might have some error.

However, as illustrated in many papers [START_REF] Alabau-Boussouira | On some recent advances on stabilization for hyperbolic equations[END_REF], [START_REF] Haraux | L p estimates of solutions to some nonlinear wave equations in one space dimension[END_REF], [START_REF] Marx | Stability analysis of dissipative systems subject to nonlinear damping via Lyapunov techniques[END_REF], [START_REF] Slemrod | Feedback stabilization of a linear control system in Hilbert space with an a priori bounded control[END_REF], [START_REF] Feireisl | Strong decay for wave equations with nonlinear nonmonotone damping[END_REF], etc.), the monotone property of the nonlinearity is crucial to first prove the asymptotic stability of the system under consideration and second characterize the trajectory of the latter system. In order to characterize the asymptotic behavior of the trajectory of the system under consideration, we consider the initial conditions in an another functional setting than the classical one, that is L p (0, 1), with p ∈ [2, ∞].

There exists a vast litterature about linear PDEs subject to monotone nonlinear dampings. For instance, in [START_REF] Slemrod | Feedback stabilization of a linear control system in Hilbert space with an a priori bounded control[END_REF], asymptotic stability of the origin of abstract con-⋆ This works has been partially supported by Advanced Grant DYCON (Dynamic Control) of the European Research Council Executive Agency.

trol systems subject to monotone nonlinear dampings is proved, using an infinite-dimensional version of LaSalle's invariance principle. These results have been then extended to more general infinite-dimensional systems in Marx et al. (2017a). More recently, in [START_REF] Marx | Stability analysis of dissipative systems subject to nonlinear damping via Lyapunov techniques[END_REF], trajectory of such systems have been characterized via Lyapunov techniques. Let us also mention [START_REF] Prieur | Wave equation with cone-bounded control laws[END_REF] and [START_REF] Marx | Global stabilization of a Korteweg-de Vries equation with a saturating distributed control[END_REF], where a wave equation and a nonlinear Korteweg-de Vries, respectively, subject to a nonlinear monotone damping are considered and where the global asymptotic stability is proved. Finally, in [START_REF] Kang | Boundary control of delayed ode-heat cascade under actuator saturation[END_REF], the local asymptotic stability of a heat equation coupled with an ODE, controlled from the boundary with a saturated feedback law, is proved.

The case of nonmonotone nonlinear damping have been considered in few papers. In [START_REF] Feireisl | Strong decay for wave equations with nonlinear nonmonotone damping[END_REF], the global asymptotic stability of a one-dimensional wave equation subject to a nonmonotone nonlinear damping is proved, thanks to some compensated compactness technique. The characterization of the trajectories is, however, not provided. In [START_REF] Martinez | Exponential stability for the wave equation with weak nonmonotone damping[END_REF], the trajectory of a wave equation in two dimensions suject to a nonmonotone damping is characterized, but for only a specific nonmonotone damping. In this paper, we rather focus on a more general nonlinear nonmonotone damping, but only for a one dimensional wave equation. We are able to characterize the trajectories of the system by studying the functional spaces L p (0, 1).

There exists also few papers dealing with the one dimensional wave equation in this functional setting. Let us mention [START_REF] Haraux | L p estimates of solutions to some nonlinear wave equations in one space dimension[END_REF], which derives a well-posedness analysis of a one dimensional wave equation in this functional setting. Moreover, an optimal decay rate is obtained for this equation. Recently, in [START_REF] Amadori | Decay of approximate solutions for the damped semilinear wave equation on a bounded 1d domain[END_REF], a similar result have been obtained, using techniques coming from conservation laws theory. Note that both of these results hold true only for monotone nonlinear damping, which is not the case of our paper.

In our paper, after introducing a general nonlinear nonmonotone damping, we propose a well-posedness analysis of a one-dimensional wave equation subject to such a damping. Futhermore, using Lyapunov techniques, we are able to characterize the trajectory of this system in the L p , p ∈ [2, ∞), provided that the initial conditions are in L ∞ . This proof is mainly based on a result about linear timevarying infinite-dimensional system, which is introduced and proved in Appendix A.

This paper is organized as follows. In Section 2, the main results of the paper are collected. We propose a wellposedness and an asymptotic stability theorems. The second result proposes futhermore a precise characterization of the trajectories of the system. Section 3 is devoted to the proof of the main results. Finally, Section 4 collects some concluding remarks, together with further research lines to be followed. Appendix A introduces a result of independant interest about exponential convergence of a specific time-varying infinite-dimensional linear systems, following a finite-dimensional strategy provided in [START_REF] Chitour | On the continuity and incremental-gain properties of certain saturated linear feedback loops[END_REF] and [START_REF] Liu | On finitegain stabilizability of linear systems subject to input saturation[END_REF], but which is instrumental for the proof of our asymptotic stability theorems.

Notation: For any p ∈ [2, ∞), the space L p (0, 1) denotes the space of functions f satisfying

1 0 |f (x)| p dx 1 p < +∞.
The space L ∞ (0, 1) denotes the space of functions satisfying ess sup x∈[0,1] |f (x)| ≤ +∞. For any p ∈ [2, ∞], the Sobolev space W 1,p (0, 1) (resp. W 2,p (0, 1)) is defined as follows W 1,p 0 (0, 1) :

= {f ∈ L p (0, 1) | f ′ ∈ L p (0, 1) and f (0) = f (1) = 0} (resp. W 2,p (0, 1) := {f ∈ L p (0, 1) | f ′ , f ′′ ∈ L p (0, 1)}).

MAIN RESULTS

The aim of this paper is to provide an asymptotic stability analysis of the following system:

   z tt (t, x) = z xx (t, x) -σ(a(x)z t (t, x)), (t, x) ∈ R + × [0, 1] z(t, 0) = z(t, 1) = 0, t ∈ R + z(0, x) = z 0 (x), z t (0, x) = z 1 (x), x ∈ [0, 1],
(1) where z denotes the state, a : [0, 1] → R + is measurable and bounded by some positive constant a ∞ and σ is a scalar nonlinear damping which satisfies the following properties: Definition 1. [Scalar nonlinear damping] A function σ : R → R is said to be a scalar damping function if 1. It is locally Lipschitz and odd; 2. One has σ(0) = 0; 3. For any s ∈ R, σ(s)s > 0; 4. The function σ is differentiable at s = 0 with σ ′ (0) = C 1 for some C 1 > 0.

Due to this definition (especially, item 2), the origin is an equilibrium point for (1). Note that this nonlinearity is not assumed to be monotone. The monotone property is in many cases really useful for either the well-posedness of the equation or the asymptotic stability of the origin. We refer the reader to [START_REF] Marx | Stability analysis of dissipative systems subject to nonlinear damping via Lyapunov techniques[END_REF] for a complete discussion on this topic.

Example 1. (Example of nonlinear dampings). Below are listed some examples of nonlinear dampings:

1. The classical saturation, defined as follows:

σ(s) = sat(s) :=    s if |s| ≤ 1, s |s| if |s| ≥ 1, (2)
satisfies all the properties of Definition 1. 2. The following nonlinearity

σ(s) = sat 1 4 s - 1 30 sin(10s) (3)
is also a nonlinear damping. Note moreover that it is not monotone, as illustrated by Figure 1. As illustrated in [START_REF] Marx | Stability analysis of dissipative systems subject to nonlinear damping via Lyapunov techniques[END_REF], some regularity is needed to obtain a characterization of the asymptotic stability of (1). To be more precise, we need the state z t to be bounded in L ∞ (0, 1). With a monotone nonlinearity σ, one would have this regularity result thanks to some nonlinear semigroup theorems. In the case of the system under consideration in this paper, we need to follow another strategy.

Our strategy relies on the introduction of these functional spaces:

H p (0, 1) := W 1,p 0 (0, 1) × L p (0, 1) D p (0, 1) := W 2,p (0, 1) ∩ W 1,p 0 (0, 1) × W 1,p 0 (0, 1), (4) with p ∈ [2, ∞].
The first functional space is equipped with the following norm:

(z, z t ) Hp(0,1) := 1 0 [z x (x)| p dx 1 p + 1 0 |z t (x)| p dx 1 p , ∀p ∈ [2, ∞), (z, z t ) H∞(0,1) := z x L ∞ (0,1) + z t L ∞ (0,1) , for p = ∞. (5)
The second one is equipped with the following norm (z, z t ) Dp(0,1) :=

1 0 |z xx (x)| p dx 1 p + 1 0 |z tx (x)| p dx 1 p , ∀p ∈ [2, ∞) (z, z t ) D∞(0,1) := z xx L ∞ (0,1) + z t,x L ∞ (0,1) , for p = ∞.
(6) Considering that (z 0 , z 1 ) ∈ H ∞ (0, 1), our aim is to prove an L ∞ regularity on the state z t so that we can obtain a characterization of the asymptotic behavior of the trajectory in H p (0, 1), with p ∈ [2, ∞). But before stating such a result, we need a suitable notion of solution for systems modeled with (1). Such a notion is provided by the following well-posedness theorem: Theorem 1. [Well-posedness] For any initial conditions (z 0 , z 1 ) ∈ H ∞ (0, 1), there exists a unique solution (z,

z t ) ∈ L ∞ (R + ; W 1,∞ (0, 1)) × W 1,∞ (R + ; L ∞ (0, 1)) to (1)
. Moreover, the following inequality is satisfied, for all t ≥ 0 (z, z t ) H∞(0,1) ≤ 2 max( z ′ 0 L ∞ (0,1) , z 1 L ∞ (0,1) ). 1 (7) Now that the functional setting is introduced, we are in position to state our asymptotic stability result Theorem 2. [Semi-global exponential stability] Consider initial conditions (z 0 , z 1 ) ∈ H ∞ (0, 1) satisfying:

(z 0 , z 1 ) H∞(0,1) ≤ R, (8) where R is a positive constant. Then, for any p ∈ [2, ∞), there exist two positive constants K := K(R) and β := β(R) such that (z, z t ) Hp(0,1) ≤ Ke -βt (z 0 , z 1 ) Hp(0,1) , ∀t ≥ 0. (9)

PROOF OF THE MAIN RESULTS

Proof of Theorem 1

The proof of Theorem 1 relies on the following wave equation with a source term

   z tt (t, x) = z xx (t, x) + h(t, x), (t, x) ∈ R + × [0, 1] z(t, 0) = z(t, 1) = 0, t ∈ R + z(0, x) = z 0 (x), z t (0, x) = z 1 (x), x ∈ [0, 1], (10)
where h denotes the source term. From (Haraux, 2018, Theorem 1.3.8), we know that, provided that z 0 , z 1 ∈ H 2 and that h ∈ L 2 (R + ; L 2 (0, 1)), there exists a unique solution z ∈ C(R + ; H 1 0 (0, 1)) ∩ C 1 (R + ; L 2 (0, 1)) to (10). In particular, since H ∞ (0, 1) ⊂ H 2 , this result holds true also for initial conditions (z 0 , z 1 ) ∈ H ∞ . The first step of our analysis in this section is to prove that picking initial conditions in H ∞ (0, 1) and the source term h ∈ L 2 (R + ; L ∞ (0, 1)) improves also the regularity of the solution z itself.

To do so, our aim is to give an explicit formula for the latter equation, using the reflection method surveyed in [START_REF] Strauss | Partial differential equations[END_REF]. Roughly speaking, this method consists in extending the explicit formulation of trajectory of the wave equation in an unbounded domain to a bounded domain.

To do so, we extend the initial datas to the whole line to be odd with respect to both x = 0 and x = 1, that is z 0 (-x) =z 0 (x) and z 0 (2x) =z 0 (x), ( 11)

1
The term z ′ 0 denotes the derivative of z 0 with respect to x.

where z 0 denotes the 2-periodic odd extension of z 0 . A way to do this is to define z 0 as follows:

z 0 (x) =    z 0 (x), 0 < x < 1 -z 0 (-x), -l < x < 0 extended to be of period 2 (12)
We can define similarly a 2-periodic odd extension of z 1 (resp. h), denoted by z 1 (resp. h). Thanks to [START_REF] Strauss | Partial differential equations[END_REF], Theorem 1, Page 69), we can therefore define the explicit trajectory z of (10) (known as the D'Alembert formula) as follows:

z(t, x) = 1 2 [ z 0 (x + t) + z 0 (x -t)] + 1 2 x+ct x-ct z 1 (s)ds + 1 2 t 0 x+(t-s)
x-(t-s)

h(w, s)dwds.

(

) 13
We can further define z t as follows

z t (t, x) = 1 2 ( z ′ 0 (x + t) -z ′ 0 (x -t)) + 1 2 ( z 1 (x + t) -z 1 (x -t)) + 1 2 t 0 h(s, x + (t -s)) -h(s, x -(t -s)) ds (14) It is clear from these two latter equations that, when picking (z 0 , z 1 ) ∈ H ∞ (0, 1) and h ∈ L 2 (R + ; L ∞ (0, 1)), then z ∈ C(R + ; W 1,∞ (0, 1)) ∩ C 1 (R + ; L ∞ (0, 1)).
We assume now that h is written as follows h(t, x) := -σ( a(x)y(t, x)), (15) where a is a 2-periodic extension of a, y ∈ L 2 (0, T ; L 2 (0, 1)) and σ is a scalar nonlinear damping (which is odd, due to Item 1 of Definition 1). In particular, it means that h ∈ L 2 (R + ; L 2 (0, 1)). The proof of Theorem 1 consists first in applying a fixed-point theorem, which will allow us to prove the well-posedness of (1) for a small time T > 0 and second in using a stability result in [START_REF] Haraux | L p estimates of solutions to some nonlinear wave equations in one space dimension[END_REF], stated as follows Proposition 1. Let us consider initial condition z 0 , z 1 ∈ H ∞ (0, 1). If there exists a solution to (1), then the time derivative of the following functional along the trajectories of (1)

φ(z, z t ) := 1 0 (F (z t + z x ) + F (z t -z x )) dx, ( 16
)
with F any even and convex function, satisfies

d dt φ(z, z t ) ≤ 0.
The latter proposition implies that φ(z, z t ) ≤ φ(z 0 , z 1 ), ∀t ≥ 0.

(17) In particular, following the discussion in the proof of Corollary 2.3. in [START_REF] Haraux | L p estimates of solutions to some nonlinear wave equations in one space dimension[END_REF]

, if one picks 2 F (s) = [Pos(|s|- 2 max( z 0 L ∞ (0,1) , z 1 L ∞ (0,1) ))] 2 , then one obtains that φ(z, z t ) = 0, ( 18
)
2 The function Pos : s ∈ R → Pos(s) ∈ R + is defined as follows:

Pos(s) = s if s > 0 0 if s ≤ 0.
which implies that, for all t ≥ 0 max(

z x (t, •) L ∞ (0,1) , z t (t, •) L ∞ (0,1) ) ≤ 2 max( z ′ 0 L ∞ (0,1) , z 1 L ∞ (0,1) ). ( 19
)
Noticing that (z, z t ) H∞(0,1) ≤ max( z x (t, •) L ∞ (0,1) , z t (t, •) L ∞ (0,1) ), it is clear then that, for all t ≥ 0 (z, z t ) H∞(0,1) ≤ 2 max( z ′ 0 L ∞ (0,1) , z 1 L ∞ (0,1) ) ( 20) This estimate implies that, once one is able to prove that there exists a solution (z, z t ) of (1) in

L ∞ ([0, T ]; W 1,∞ (0, 1)) ∩ W 1,∞ ([0, T ]; L ∞ (0, 1)),
for a small time T > 0, then the well-posedness of ( 1) is ensured in

L ∞ (R + ; W 1,∞ (0, 1)) ∩ W 1,∞ (R + ; L ∞ (0, 1)).
Now, we are in position to prove Theorem 1.

Proof. Let us define F T the space of measurable functions defined on [0, T ]×R which are bounded, odd and 2-periodic in space. We endow F T with the L ∞ -norm so that it becomes a Banach space. Hence, denoting by • T the norm of the latter functional space, we have, for every y ∈ F T y T := sup

(t,x)∈[0,T ]×R |y(t, x)|. ( 21
)
Let us consider B K (y) the closed ball in F T centered at y ∈ F T of radius K ≥ 0, where K remains to be defined.

We can now define the mapping with which we will apply a fixed-point

φ T : F T → F T y → φ T (y), (22)
where

φ T (y) = 1 2 ( z ′ 0 (x + t) -z ′ 0 (x -t)) + 1 2 ( z 1 (x + t) -z 1 (x -t)) - 1 2 t 0 a(x + t -s)σ( a(x + t -s)y(s, x -(t -s)) + a(-x + t -s)σ( a(-x + t -s)y(s, -x -(t -s)) ds (23)
Using the fact that σ is locally Lipschitz, note that, for every y 0 ∈ F T and K > 0, there exists a positive constant C(y 0 , K) such that, for every y, y

∈ B K (y 0 ) φ T (y) -φ T ( y) T ≤ C(y 0 , K)T y -y T . (24) Pick K such that K := 2 ( φ T (y 0 ) T + y 0 T ) (25
) and T sufficiently small such that C(y 0 , K)T ≤ 1.

(26) Consider a sequence (y n ) n∈N defined as

y n+1 = φ T (y n ).
If we prove that this sequence converges to y ⋆ , then we can deduce that y ⋆ = φ T (y ⋆ ). This means that there exists a fixed-point for the mapping φ T , which implies in particular that (1) is well-posed in the desired functional spaces. To prove the convergence of this sequence, we prove that it is a Cauchy sequence. Indeed, since B K (y 0 ) is complete, any Cauchy sequence converges in this set. By induction, one can prove that y n+1y n T ≤ (C(y 0 , K)T ) n y 0y 1 T (27) and y n ∈ B K (y 0 ). ( 28) Indeed, thanks to the choice of T in (26), these two properties are easily proved for n 0 and, moreover, we have with ( 24), for all n ≥ 1 y n+1 -

y n T = φ(y n ) -φ(y n-1 ) T ≤C(y 0 , K)T φ(y n-1 ) -φ(y n-2 ) T ≤(C(y 0 , K)T ) n y 0 -y 1 T . (29)
The inequality ( 27) can be deduced from the above inequality. The property (28) can be proved as follows:

y n+1 ≤ y n T + y 1 T + y 0 T ≤ y 0 T + φ T (y 0 ) T + φ T (y 0 ) T + y 0 T ≤K (30)
where in the first line we have used ( 27) and, in the second line, we have used the fact that y n ∈ B K (y 0 ).

The two properties ( 27) and ( 28) show that the sequence y n is a Cauchy sequence. Since B K (y 0 ) is a complete set, this sequence is therefore convergent. This means in particular that there exists a fixed-point to the mapping φ T (y 0 ), which implies that, for sufficiently small time T , there exists a unique solution z ∈ L ∞ (0, T ; W 1,∞ (0, 1)) and z t ∈ L ∞ (0, T ; L ∞ (0, 1)). Thanks to (20), we can deduce that there exists unique solution z ∈ L ∞ (R + ; W 1,∞ (0, 1)) and z t ∈ L ∞ (R + ; L ∞ (0, 1)). This concludes the proof of Theorem 1. •

Proof of Theorem 2

The proof of Theorem 2 is divided into two steps: first, we transform the system (1) into a system in the form (A.1), which is in particular a linear time-variant system, and apply Theorem 3 for the space H 2 , which is indeed the only Hilbert space among all the spaces H p (0, 1). Second, using the fact that the solutions are bounded in H ∞ (0, 1) thanks to Theorem 1, and invoking an interpolation theorem, which is the Riesz-Thorin theorem, we conclude.

Proof.

First step: semi-global exponential stability in H 2 . We first fix p = 2, but still consider the initial conditions (z 0 , z 1 ) ∈ H ∞ (0, 1). Moreover, we suppose that there exists a positive constant R such that the initial conditions satisfy (z 0 , z 1 ) H∞(0,1) ≤ R.

(31) In particular, due to Theorem 1, one has (z, z t ) H∞(0,1) ≤ 2R, ∀t ≥ 0.

(32)

The system (1) may be rewritten as follows

   z tt = z xx -d(t, x)a(x)z t , z(t, 0) = z(t, 1) = 0, z(0, x) = z 0 (x), z t (0, x) = z 1 (x), (33)
with

d(t, x) =      σ( a(x)z t ) a(x)z t , if a(x)z t = 0, C 1 , if a(x)z t = 0. ( 34
(A) ⊂ H → H [v 1 v 2 ] ⊤ → v 2 v ′′ 1 ⊤ (35)
and B = 0 a(x) ⊤ . It is well known that A generates a strongly continuous semigroup of contractions (see [START_REF] Haraux | Nonlinear vibrations and the wave equation[END_REF]). Now, let us check whether d(t, •) satisfies (A.2), for all t ≥ 0.

Since the initial conditions (z 0 , z 1 ) ∈ H ∞ (0, 1) and are bounded by R in the H ∞ (0, 1) norm, then invoking Theorem 1 we have, for all t ≥ 0 sup

x∈[0,1] |z t (t, x)| ≤ 2R. ( 36
)
Moreover, since a(x) ≤ √ a ∞ , for all x ∈ [0, 1], and because d is a continuous function, there exist two positive constants d 0 and d 1 , depending on R and a ∞ such that

d 0 := min ξ∈[-2 √ a∞R,2 √ a∞R] σ(ξ) ξ ≤ d(t, x) ≤ max ξ∈[-2 √ a∞R,2 √ a∞R] σ(ξ) ξ := d 1 .
(37) Note moreover that the origin of the following system   

z t = z xx -d 0 z t 0) = z(t, 1) = 0 z(0, x) = z 0 (x), z t (0, x) = z 1 (x). ( 38
)
is exponentially stable in H 2 for any initial conditions (z 0 , z 1 ) ∈ H 2 (see e.g. [START_REF] Prieur | Wave equation with cone-bounded control laws[END_REF]). The related operator of this system is Ad 0 BB ⋆ , with domain D(A d0 ) = D 2 . Therefore, all the properties required in Theorem 3 are satisfied. Hence, there exist two positive constants K := K(R) and β := β(R) such that (z, z t ) H2 ≤ Ke -βt (z 0 , z 1 ) H2 , ∀t ≥ 0.

(39)

Second step: Semi-global exponential stability in H p (0, 1). From Theorem 1, we know that, for every initial conditions (z 0 , z 1 ) ∈ H ∞ (0, 1) satisfying (z 0 , z 1 ) H∞(0,1) ≤ R, and noticing that the trajectory of (1) can be expressed with the evolution family W (t, 0) associated to (33) 3 , one has W (t, 0)(z 0 , z 1 ) H∞(0,1) ≤ 2R, ∀t ≥ 0. (40)

Now, fix t > 0. Note that W (t, 0) is a linear operator from (L 2 (0, 1)) 2 (resp. (L ∞ (0, 1)) 2 ) to (L 2 (0, 1)) 2 (resp. (L ∞ (0, 1)) 2 ), if it associates (z ′ 0 , z 1 ) ∈ L 2 (0, 1) 2 (resp. (z ′ 0 , z 1 ) ∈ L ∞ (0, 1) 2 ) to (z x , z t ) ∈ L 2 (0, 1) (resp. (z x , z t ) ∈ L ∞ (0, 1) 2 ). Hence, we can apply the so-called Riesz-Thorin theorem (Bergh and Löfström, 2012, Theorem 1.1.1, Page 2) and conclude that W (t, 0) Hp(0,1) ≤ 2 K 2

2 p e -2β p t , ∀t ≥ 0, (41)

3 Evolution families are extension of semigroups for time-variant linear infinite-dimensional systems.

where W (t, 0) corresponds exactly to the trajectory of (1) with the initial condition z 0 , z 1 ∈ H ∞ (0, 1). In particular, for every (z 0 , z 1 ) ∈ H ∞ (0, 1), one therefore has, for every t ≥ 0 W (t, 0)(z 0 , z 1 ) Hp(0,1) ≤ W (t, 0) Hp(0,1) (z 0 , z 1 ) Hp(0,1) ≤2 K 2

2 p e -2β p t (z 0 , z 1 ) Hp(0,1) .

This concludes the proof of Theorem 2. •

CONCLUSION

In this paper, we have provided a well-posedness analysis of a one-dimensional wave equation subject to a nonlinear nonmonotone damping. Futhermore, a characterization of the asymptotic behavior of the latter system is given.

It is proved with Lyapunov techniques. This work paves the way to many others. For instance, a first open and natural question would be the case of multidimensional wave equations, for which there does not exist any proof of well-posedness in the functional setting introduced in this paper.

Fig. 1 .

 1 Fig. 1. For any s ∈ [-5, 5], the figure illustrates the function σ given by (3)

  which is possible due to the differentiability of the function σ at 0. This system is in the form (A.1), with H = H 2 , U = H 2 , D(A) = D 2 , and the operators A and B defined as follows A : D

Appendix A. EXPONENTIAL CONVERGENCE RESULT FOR A LINEAR TIME-VARIANT SYSTEM

This appendix is devoted to the statement and the proof of a theorem dealing with a time-variant linear infinitedimensional system. Indeed, as it is illustrated in Section 3.2, we can transform (1) as a time-variant linear infinitedimensional system. This transformation is inspired by [START_REF] Chitour | On the continuity and incremental-gain properties of certain saturated linear feedback loops[END_REF] and [START_REF] Liu | On finitegain stabilizability of linear systems subject to input saturation[END_REF], where such a technique is applied for finite-dimensional linear systems subject to a saturation. To define it, let us introduce H (resp. U ), a Hilbert space which is equipped with the norm

• H and the scalar product •, • H . The system under study in this section is the following:

where A : D(A) ⊂ H → H, with D(A) the domain of the operator A that we suppose densely defined in H, B ∈ L(U, H), B ⋆ denotes the adjoint of B and d is a continuous function. We assume moreover that A and its adjoint A ⋆ are dissipative, and that there exist positive constants d 0 and d 1 such that d satisfies, for all t ≥ 0.

2) Due to these properties, the domain of A d (t) is equal to D(A) and, therefore, does not depend on t. Moreover, always because of these properties, and since A and A ⋆ are dissipative, one can prove that, for all t ≥ 0 and for all

3) which implies that each operator A d (t) generates a strongly continuous semigroup of contractions. Hence, due to the discussion provided in (Chicone and Latushkin, 1999, Page 123), there exists an evolution family (W (θ, τ )) θ≥τ solving (A.1). In particular, this means that there exists a unique strong solution v ∈ C(R + , D(A)) to (A.1) for every v 0 ∈ D(A).

We are now in position to state the following result.

Theorem 3. Consider the system given by (A.1). Supposing that the origin of the following system

is globally exponentially stable, then, for any initial conditions v 0 ∈ H, the origin of (A.1) converges exponentially to 0 with τ = 0. Remark 1. The global asymptotic stability is not ensured for the linear time-variant system (A.1). Indeed, for such systems, the global asymptotic stability has to be proven for every initial condition v τ and for every τ ≥ 0. This is not an issue for us. Indeed, we use this result to prove the attractivity of (1). The stability of (1) already holds thanks to Theorem 1. •

Proof. Since the origin of (A.4) is globally exponentially stable, then, due to [START_REF] Datko | Extending a theorem of A.M. Liapunov to Hilbert space[END_REF], there exist a self-adjoint operator P ∈ L(H) and a positive constant C such that the following inequality holds true

) Moreover, note that A d0 is also a dissipative operator, which means in particular that

(A.6) Now, consider the following candidate Lyapunov functional for (A.1):

where M is a positive constant which has to be defined. The time derivative of V along the trajectories of (A.1)