Jasmin: high-assurance and high-speed cryptography

Jasmin: High-Assurance and High-Speed Cryptography José Bacelar Almeida INESC TEC and Universidade do Minho, Portugal Manuel Barbosa INESC TEC and FCUP Universidade do Porto, Portugal Gilles Barthe IMDEA Software Institute, Spain Arthur Blot ENS Lyon, France Benjamin Grégoire Inria Sophia-Antipolis, France Vincent Laporte IMDEA Software Institute, Spain Tiago Oliveira INESC TEC and FCUP Universidade do Porto, Portugal Hugo Pacheco INESC TEC and Universidade do Minho, Portugal Benedikt Schmidt Google Inc. Pierre-Yves Strub École Polytechnique, France ABSTRACT Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant. Using the supercop framework, we evaluate the Jasmin compiler on representative cryptographic routines and conclude that the code generated by the compiler is as efficient as fast, hand-crafted, implementations. Moreover, the framework includes highly automated tools for proving memory safety and constant-time security (for protecting against cache-based timing attacks). We also demonstrate the effectiveness of the verification tools on a large set of cryptographic routines. CCS CONCEPTS •Security and privacy →Software security engineering ; Logic and verification;Software security engineering; KEYWORDS cryptographic implementations, verified compiler, safety, constanttime security 1 INTRODUCTION Cryptographic software is pervasive in software systems. Although it represents a relatively small part of their code base, cryptographic Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]. CCS ’17, October 30-November 3, 2017, Dallas, TX, USA © 2017 Copyright held by the owner/author(s). Publication rights licensed to Association for Computing Machinery. ACM ISBN 978-1-4503-4946-8/17/10...$15.00 https://doi.org/10.1145/3133956.3134078 software is often their most critical part, since it forms the backbone of their security mechanisms. Unfortunately, developing highassurance cryptographic software is an extremely difficult task. Indeed, good cryptographic software must satisfy multiple properties, including efficiency, protection against side-channel attacks, and functional correctness, each of which is challenging to achieve: • Efficiency. Cryptographic software must imply minimal overhead for system performance, both in terms of computational and bandwidth/storage costs. These are first-class efficiency requirements during development: a few clock-cycles in a small cryptographic routine may have a huge impact when executed repeatedly per connection established by a modern service provider; • Protection against side-channel attacks. In-depth knowledge of real-world attack models, including side-channel attacks, is fundamental to ensure that the implementation includes adequate mitigation. For example, one must ensure that the observable timing behavior of the compiled program does not leak sensitive information to an attacker. Failing to address these considerations is a major attack vector against cryptographic implementations [ 1 , 12 ]. Indeed, one prevailing view is that critical code must adhere to the “cryptographic constant-time” discipline, in particular its control flow and sequence of memory accesses should not depend on secrets [ 12 ]. High-assurance cryptographic software must be guaranteed to correctly adhere to this discipline. • Functional correctness. Specifications of cryptographic components are often expressed using advanced mathematical concepts, and being able to bridge the enormous semantic gap to an efficient implementation is a pre-requisite for the implementor of a cryptographic component. Moreover, implementations may involve unconventional tasks, such as domain-specific error handling techniques. Guaranteeing functional correctness in these circumstances is harder than for other software domains, but it is critical that it is guaranteed from day 1—contrarily to the usual detect-and-patch approach—as implementation bugs in cryptographic components can lead to attacks [18, 23]. Efficiency considerations rule out using high-level languages, since the code must be optimized to an extent that goes far beyond what is achievable by modern, highly optimizing, compilers. Furthermore, Programmed in Caml Certified in Coq Jasmin source Jasmin Jasmin Jasmin Jasmin-low Jasmin-lin Asm Parser, typechecker, simplifier Inlining, unrolling Stack sharing Linear scan Lowering, reg. array exp. Reg./stack alloc., lin. Linear scan Jasmin Certified Compiler Jasmin Source Analysis Annotated Jasmin AST Functional Embedding CT Instrumentation Dafny code Dafny code Dafny Dafny Boogie code Boogie code Boogie Product generator Boogie code Boogie Figure 1: Jasmin architecture. there are concerns that highly optimizing compilers may introduce security flaws [ 21 , 26 ]. As a consequence, the development of cryptographic software must be carried at assembly level, and is entrusted to a few select programmers. Moreover, these programmers rely on rudimentary tooling, that is often co-developed with the implementations themselves. For instance, securityand performancecritical parts of the OpenSSL library result from an ad hoc combination of pseudo-assembly programming and scripting, known as “perlasm”. Another alternative is to use the qhasm language [ 11 ], that simultaneously elides low-level details that are inessential for fine-grained performance tuning, and retains all performanceand security-critical aspects of assembly programming. qhasm achieves an excellent balance between programmability and efficiency, as evidenced by a long series of speed-record-breaking cryptographic implementations. Due to their nature, these approaches do not lend themselves to being supported by formal verification. Functional correctness and side-channel security requirements for high-assurance cryptography impose going significantly beyond the current practices used for validating implementations, namely code inspection, code testing (and in particular, fuzzing), and even static analysis. Code inspection is time-consuming and requires a high-level of expertise. Testing is particularly effective for excluding errors which manifest themselves frequently, but performs poorly at detecting bugs which occur with very low probability. Static analysis is useful for detecting programming errors, but does not discover functionality bugs. A better alternative is to create machine-assisted verification frameworks that can be used for building rigorous proofs of functional correctness and sidechannel security. However, and as stated above, these frameworks are not easily applicable to assembly languages. Our contribution. We propose a tool-assisted framework, called Jasmin, for high-speed and high-assurance cryptographic code. Jasmin is inspired by qhasm, but it specifically addresses the lack of independent validation that exists today and enables the creation of high-assurance high-speed and high-security software that can be used as a drop-in replacement for unverified routines in existing cryptographic libraries. Specifically, the Jasmin framework goes significantly beyond current practices in cryptographic engineering, by leveraging state-of-the-art methods from programming languages, without sacrificing efficiency considerations. More technically, we make the following contributions: • we define the Jasmin programming language. Jasmin is designed to significantly simplify the writing and verification of highspeed cryptographic programs. In particular, Jasmin supports within one single language: high-level features, including structured control flow such as loops and procedure calls, which lead to compact code that is also easier to verify; and assembly-level instructions (both generic and platform-specific), which give programmers tight control over the generated code. We give a formal, machine-checked, semantics of Jasmin in the Coq proof assistant; • we define and implement a formally verified compiler that transforms Jasmin programs into assembly programs. The compiler alternates between certified passes (function inlining, loop unrolling, constant propagation), which are proved and verified in Coq, and passes by translation validation (register allocation), which are programmed in a conventional programming language and whose results are checked in Coq. The compiler is carefully designed to achieve predictability, and to deliver efficient code; • we define and implement a sound embedding of Jasmin programs into Dafny [ 27 ], and use the embedding to support automated proofs of memory safety, constant-time security, and (potentially) functional correctness of Jasmin programs. The tool uses Boogie [ 7 ] to generate verification conditions and Z3 [ 20 ] to discharge them; for constant-time security, we use product programs as in [ 4 ]; we have also a proof-of-concept direct translation to SMT-Lib which we have used to replicate the correctness proof strategy of [19] using Boolector [30]. • we validate our framework with an implementation of scalar multiplication for Curve25519, the core cryptographic component in key exchange and digital signature algorithms recently adopted for widespread use in both TLS and the Signal protocol. We prove that the Jasmin implementation is memory-safe and is constant-time. This case study also serves as a point of comparison with prior work [ 19 ], which pursues the same goal using general-purpose verification tools; this comparison highlights the advantages of having a single integrated formal verification framework for high-speed cryptography. • we carry a practical evaluation of our tools on a representative set of examples, which comprises many qhasm implementations included in the supercop framework. To this end, we created a simple automatic translator from qhasm to Jasmin, which shows that one can actually use Jasmin to program in a style very similar to that used in qhasm. We benchmark the efficiency of the code generated by the Jasmin compiler and show that its efficiency matches the original implementations generated from qhasm. Figure 1 provides a high-level view of the workflow of our toolchain. On the left-hand side one can see the internal structure of the Jasmin compiler, which takes Jasmin code and produces assembly code that can then be further compiled and linked to larger programs/libraries. The various internal passes of the compiler will be explained in Section 5. On the right-hand side one can see the tool-chain for reasoning about Jasmin at the source level. This comprises a tool that can perform two types of translations of Jasmin programs into Dafny [ 27 ], which will be described in detail in Section 4. The first translation, which we call functional embedding, translates Jasmin programs into Dafny programs with consistent axiomatic semantics, including safety assertions that will cause any unsafe Jasmin program to be rejected. This embedding also permits translating typical functional correctness annotations into the Dafny program and take advantage of the Dafny/Boogie verification condition generator to discharge the associated proof goals using the Z3 SMT solver; 1 The second translation, which we call CT instrumentation, creates a Dafny program that will be translated into a Boogie program with special annotations. These will subsequently be intercepted by a sister program (product generator in the figure), which produces a product program whose safety implies the constant-time security of the original Jasmin program, using essentially the same theoretical principles of ct-verif [ 4 ]. The Jasmin compiler is proven in Coq to preserve safety and correctness properties, and we sketch a manual proof in Section 5 that it also preserves the constant-time property. Trusted Computing Base. The Trusted Computing Base (TCB) of the Jasmin framework currently includes Coq, the unverified parts of the Jasmin compiler (limited to parsing, type-checking and code pretty-printing), and the translator from Jasmin to Dafny code. Because we currently rely on Dafny for source-level verification, we also rely on the TCB of the Dafny verification infrastructure. Using a verified verification condition generator, together with foundational tools for constant-time and memory safety, would eliminate Dafny from the TCB. 1we have also developed a proof-of-concept translator to SMT-Lib in order to experiment with other SMT solvers, namely Boolector. Limitations. The emphasis of this work is on providing an endto-end infrastructure for high-assurance and high-speed cryptography, and to demonstrate the effectiveness of automated methods for memory safety and constant-time security. We also provide support for proving functional correctness, but do not exercise this component of the framework over substantial examples, such as scalar multiplication of Curve25519, for two main reasons. First, verifying functional correctness with our current infrastructure would replicate prior work—which we discuss in Section 2—and in particular would involve a cumbersome, hand-managed, process of combining SMT-based and interactive verification in the Coq proof assistant. Second, we are developing a verified verification condition generator, in the spirit of the Verified Software ToolChain [ 6 ], which provides an integrated and foundational environment for managing such proofs, and eventually connecting with existing mathematical formalizations of elliptic curves [9]. Moreover, Jasmin currently lacks features that are widely used in cryptographic implementations, e.g. floating-point arithmetic or vectorized instructions. Adding these instructions is orthogonal to the main contributions of this paper and is left for future work. Similarly, Jasmin currently supports a single micro-architecture, in contrast to qhasm and “perlasm” which support multiple ones. Nevertheless, we leave for further work to support different microarchitectures, and to provide stronger evidence that Jasmin offers (at least) the same level of portability. Access to the development. The Jasmin framework can be obtained from https://github.com/jasmin-lang/jasmin. 2 MOTIVATING EXAMPLE We will illustrate the design choices of the Jasmin framework and its workflow using a classic example from elliptic curve cryptography which we briefly introduce below. A primer on elliptic curve cryptography. Elliptic curve cryptography [ 24 ] relies on hardness assumptions on algebraic groups formed by the points of carefully chosen elliptic curves over finite fields. Let Fq be the finite field of prime order q . An elliptic curve is defined by the set of points (x,y)∈Fq×Fq that satisfy an equation of the form E : y2+a1xy+a3y=x3+a2x2+a4x+a6 , for a1 , a2 , a3 , a4 , a6∈Fq (with certain restrictions on these parameters). This set of points, together with a “point at infinity”, form a group of size l≈q . The group law has a geometric interpretation, which is not relevant for the purpose of this paper; what is important is that the group law can be computed very efficiently—particularly when compared to the computations underlying other algebraic structures used in public-key cryptography—using only a few operations in Fq . Similarly, scalar multiplication, 2 which is the core operation for elliptic curve cryptography, can also be computed very efficiently. Curve25519. X25519 is an elliptic-curve Diffie-Hellman key exchange protocol proposed by Bernstein [ 13 ]. It is based on the custom-designed curve Curve25519 defined as E : y2=x3+ 486662 x2+x over the field F2255−19 . This curve was chosen to 2 Given a curve point P and a scalar k∈Z , scalar multiplication computes the point Q=k·P=P+. . . +P | {z } ktimes . provide cryptographic security, but design choices also took into consideration the need for aggressive optimization. As a result of these choices, Curve25519 has been adopted for widespread use in various contexts, including the TLS and the Signal protocols. Scalar multiplication in Curve25519 is usually implemented using Montgomery’s differential-addition chain—a.k.a. Montgomery ladder—which permits performing the computation directly over the x -coordinate of elliptic curve points. This algorithm is shown in Algorithm 1. It is ideal for high-security and high-speed implementation for two reasons. First, it is much simpler than the generic algorithm for elliptic curves, so its overall efficiency essentially only depends on the cost of the underlying field operations, which can be computed very fast in modern architectures. Second, it is highly regular and can be implemented in constant-time by executing exactly the same code for each scalar bit (called a ladder step), making sure that the appropriate inputs are fed to this code via (constant-time) swapping of (X2,Z2) with (X3,Z3) . The computations of each step in the ladder, all over Fq , are shown in Algorithm 2. Typical implementations of the scalar multiplication operation implement the Montgomery ladder step in fully inlined hand-optimized assembly, and also include field multiplication and inversion as hand-optimized assembly routines (these are needed to recover the final x -coordinate of the result once the ladder is computed). The main difference between various implementations lies in the representation of F2255−19 field elements and their handling in the hand-crafted assembly code, as the optimal choice varies from one architecture to another due to word size and available machine operations, and their relative efficiency. The higher-level functions that call the assembly routines for the various ladder steps and finalize the results are usually implemented in C. This is inconvenient when formal verification is the goal, since the relevant routines are now split between two programming languages with very different characteristics. Algorithm 1 Curve25519 Montgomery Ladder Input: A scalar kand the x-coordinate xPof a point Pon E. Output: (XkP ,ZkP )fulfilling xkP =XkP /ZkP t← ⌈log2k+1⌉ X1←xP;X2←1;Z2←0;X3←xP;Z3←1 for i←t−1downto 0do if bit iof kis 1then (X3,Z3,X2,Z2)←ladderstep(X1,X3,Z3,X2,Z2) else (X2,Z2,X3,Z3)←ladderstep(X1,X2,Z2,X3,Z3) end if end for return (X2,Z2) 3 JASMIN LANGUAGE The claim of this paper is that it is possible to obtain the best of the two worlds, and to develop effective verification methodologies whose guarantees carry to assembly-level implementations. The key to achieving this goal is the Jasmin programming language, which is specifically designed to ease the writing and verification Algorithm 2 One step of the Curve25519 Montgomery Ladder function ladderstep(X1,X2,Z2,X3,Z3) T1←X2+Z2 T2←X2−Z2 T7←T2 2 T6←T2 1 T5←T6−T7 T3←X3+Z3 T4←X3−Z3 T9←T3·T2 T8←T4·T1 X3←T8+T9 Z3←T8−T9 X3←X2 3 Z3←Z2 3 Z3←Z3·X1 X2←T6·T7 Z2←121666 ·T5 Z2←Z2+T7 Z2←Z2·T5 return (X2,Z2,X3,Z3) end function of high-speed code, and the Jasmin verified compiler, which ensures that properties of programs provably carry to their assembly implementations. In this section, we detail the design rationale of the Jasmin language, and then give a formal overview of its syntax and semantics. 3.1 Language design Figures 3 and 2 show two illustrative snippets of a Jasmin implementation of scalar multiplication for Curve25519. This example highlights one fundamental design goal of Jasmin: one can implement complete cryptographic primitives within a single language and use different programming idioms for different parts of the implementation. On the one hand, the ladder step is implemented as hand-optimized code, using a convenient and uniform syntax for instructions. This style of programming is close to qhasm, with each statement corresponding to a single processor instruction. On the other hand, the ladder itself uses high-level control-flow structures, including for and while loops, function calls, array notation and the passing of arrays as parameters. This style of programming leads to compact and intuitive code, and also greatly facilitates safety, side-channel and functional correctness verification. We detail these choices next. Predictable pre-assembly programming. Jasmin aims to provide the highest level of control and expressiveness to programmers. Informally, the essential property that Jasmin aims to achieve is predictability: the expert programmer will be able to precisely anticipate and shape the generated assembly code, so as to be able to achieve optimal efficiency. Jasmin provides a uniform syntax that unifies machine instructions provided by different micro-architectures. The main purpose of this syntax is to ease programming and to enhance portability. However, platform-specific instructions are also available and can Figure 2: Snippets of Jasmin ladder step function (left) generated from qhasm (right). export fn ladderstep (reg b64 workp) { reg b64 addt0; reg b64 addt1; reg bool cf; reg b64 t10; reg b64 t11; reg b64 t12; reg b64 t13; reg b64 t20; reg b64 t21; reg b64 t22; reg b64 t23; ... t10 = [workp + 4 * 8]; t11 = [workp + 5 * 8]; t12 = [workp + 6 * 8]; t13 = [workp + 7 * 8]; t20 = t10; t21 = t11; t22 = t12; t23 = t13; cf, t10 += [workp + 8 * 8]; cf, t11 += [workp + 9 * 8] + cf; cf, t12 += [workp + 10 * 8] + cf; cf, t13 += [workp + 11 * 8] + cf; addt0 = 0; addt1 = 38; addt1 = addt0 if ! cf; cf, t10 += addt1; cf, t11 += addt0 + cf; cf, t12 += addt0 + cf; cf, t13 += addt0 + cf; addt0 = addt1 if cf; input workp int64 addt0 int64 addt1 int64 t10 int64 t11 int64 t12 int64 t13 int64 t20 int64 t21 int64 t22 int64 t23 ... enter ladderstep t10 = ∗(uint64 ∗)(workp + 32) t11 = ∗(uint64 ∗)(workp + 40) t12 = ∗(uint64 ∗)(workp + 48) t13 = ∗(uint64 ∗)(workp + 56) t20 = t10 t21 = t11 t22 = t12 t23 = t13 carry? t10 += ∗(uint64 ∗)(workp + 64) carry? t11 += ∗(uint64 ∗)(workp + 72) + carry carry? t12 += ∗(uint64 ∗)(workp + 80) + carry carry? t13 += ∗(uint64 ∗)(workp + 88) + carry addt0 = 0 addt1 = 38 addt1 = addt0 if !carry carry? t10 += addt1 carry? t11 += addt0 + carry carry? t12 += addt0 + carry carry? t13 += addt0 + carry addt0 = addt1 if carry be used whenever important, e.g., for efficiency. In particular, and similarly to qhasm, programmers may always use a Jasmin dialect where there is a strict one-to-one mapping between Jasmin instructions and assembly instructions. This is visible in Figure 2, where we show qhasm and corresponding Jasmin code side by side; these are snippets of the implementation of the ladder-step algorithm in Algorithm 2. Finally, to ensure predictability, the programmer must also specify the storage for program variables (stack, register) and must handle spilling explicitly. However, full register naming is not needed; the programmer only needs to ensure that there exists a mapping from register variables to machine registers (without spilling), but the actual mapping is later found by the compiler. At the source level, stack variables and register variables are interpreted simply as variables; the storage modifier is only used as advice for register allocation. In particular, at this level the memory is assumed to be disjoint from stack storage. The compiler will later refine this model and conciliate the fact that stack data must reside in memory as well. Verifiability. Formal verification of low-level code is extremely hard, because of complex side-effects (e.g. shift instructions have side-effects on flags), unstructured control-flow, and flat structure (i.e. code is often created by copy-and-paste followed by variable or register renaming). Jasmin includes several features that avoid these issues and enable a streamlined formal verification workflow. Jasmin ensures that side-effects are explicit from the program code, by not treating flags specially in the input language; instead, flags are simply boolean variables. This treatment of flags is illustrated in Figure 2, where the carry flag cf is declared as a boolean variable. The programmer is expected to ensure that writing and reading of these variables is consistent with the underlying machine instruction semantics, which is checked by the compiler using an extended form of register allocation. Treating flags as boolean variables allows all operators to be pure, and so state modifications are all explicit, e.g., code of the form (x1, . . . , xn) : =op(e1, . . . , ek) only changes (function local) variables xi . This approach makes verification of functional correctness and even side-channel security significantly simpler, since it avoids the intricacies of dealing with the side-effects associated with flags.3 Unlike qhasm,Jasmin supports function calls. The use of function calls is shown in Figure 3, where two functions are used for computing a single ladder step and for performing a constant-time swap. Function calls naturally lead to a style of programming that favours modularity, and thus is more easily amenable to modular verification. Functions are always inlined and must explicitly return all changed values. 4 The stack allocation procedure ensures that inlining is “zero-cost”, so that the extra benefits of modular code writing and analysis comes with no performance penalty. Jasmin also supports high-level control-flow structures, instead of jumps supported by qhasm. The use of control-flow structures can be seen in Figure 3, where a while loop is used to iterate over the bit representation of the scalar in constant-time. The choice of using high-level structures over jumps usually has no impact on the efficiency of the generated code; indeed, the translation to assembly, which is achieved by unrolling or trivial mapping to label-goto constructions, is simple enough to retain predictability and our structures are sufficient to express the control-flow typically found in cryptographic implementations. In contrast, it considerably simplifies verification of functional correctness, safety and side-channel security, and is critical to leverage off-the-shelf verification frameworks, which are often focused on high-level programs. Jasmin also supports functional arrays for describing collections of registers and stack variables. Figure 3 shows how arrays can be used to refer to various registers/stack positions holding the data as x [ i ]rather than hardwired variable names such as x 1, x 2, etc. This notation leads to compact and intuitive code and simplifies loop invariants and proofs of functional correctness. Arrays are meant to be resolved at compile-time, and so they can only be indexed by compile-time expressions. These can be used to describe statically unrollable for loops and conditional expressions, which permits replicating within the Jasmin language coding techniques that are typically implemented using macros in C. For example, one can write a for-loop ranging over the number of limbs for representing an element of Fq , as in Figure 3 whereas a qhasm 3 The exception are, of course, memory accesses, which are handled in the standard way by treating memory as a large chunk of shared state that can be accessed in an array-like form. However, memory access is often very simple in cryptographic implementations (particularly those dealing with algebraic operations) and so this has relatively low impact in the formal verification effort. 4This is expected to change in future versions of Jasmin. Figure 3: Constant-time Montgomery Ladder in Jasmin fn set_int(reg b64 v) −→ reg b64[4] { reg b64[4] res; inline int i; res[0] = v; for i=1to 3 { res[i] = 0; } return res; } fn mladder(stack b64[4] xr, reg b64 sp) −→ stack b64[4], stack b64[4] { reg bool cf; reg b64 tmp1, tmp2, bit, swap, i, j; stack b64 prevbit, is, js, s; stack b64[4] x1, x2, z2, x3, z3; inline int k; x1 = xr; x2 = set_int(1); z2 = set_int(0); z3 = set_int(1); x3 = xr; prevbit = 0; j = 62; i = 3; while (i >=s 0) { is = i; tmp1 = [sp + 8 * i]; s = tmp1; while (j >=s 0) { js = j; tmp2 = s; bit = tmp2 >> j; bit = bit & 1; swap = prevbit; swap ^= bit; prevbit = bit; x2, z2, x3, z3 = cswap(x2, z2, x3, z3, swap); x2, z2, x3, z3 = ladderstep(x1, x2, z2, x3, z3); j = js; j -= 1; } j=63;i=is;i-=1; } return x2, z2; } programmer would unroll such a loop by hand using error-prone “copy-and-paste” (or write the code in C). 3.2 Language specification This paragraph outlines the syntax of the Jasmin language. A formal description using BNF notation is available as Appendix A. Types. Jasmin features a simple type system, including types bi and bi [ n ]for i -bit values and for n -dimensional arrays of i -bit values, with i∈ { 1 , 8 , 16 , 32 , 64 } and n∈N , and int for unbounded integers. Unbounded integers are used only for compile-time expressions. The type b1 is used to represent booleans. The choice of the type system ensures that Jasmin values match the machine interpretation: types only distinguish between sizes, whereas signed and unsigned interpretations are associated with the semantics of operators. This is visible in the condition of the while loop in Figure 3. Storage types. Storage types are used by the compiler to fix how values are stored in memory. Storage types are: store in stack stack , store in register reg , resolve at compile-time inline . Integers are resolved at compile-time by default. Storage types are used in variable and function declarations; see Figure 3. For instance, the declaration reg bool cf introduces a boolean variable cf that will be stored in a register. The type of mladder indicates that the function will read and return from/to the stack two b64 arrays of size 4. Expressions. Expressions are built from variables using constants, operators, accessors for arrays and memory, casts from integers to b64 , and conditionals. Operators include integer constants, arithmetic ( +,−,∗, / ), comparison ( <, >, ≤,≥,= ), and logical ( ∧,∨,¬ ) operators and a rich set of generic and platform-specific assemblylevel operations: conditional move, signed/unsigned addition, add with carry, exact/truncated multiplication, increment/decrement, shifts, etc. Operators have a type which reflects their effect on flags; e.g. the type of shift operators is b64×b64 →b64×b1×b1×b1×b1×b1 , where the five booleans in the return type correspond to the flags modified by the instruction. 5 Syntactic sugar is used to offer a simplified syntax for common cases such as when only the carry flag is used at the operator output. Memory accesses are of the form [ x+e ], where x is variable of type b64 representing the pointer and e is an expression of type b64 representing the offset. Array accesses are of the form x [ e ], where x is a variable and e is an expression of type b64 . A simple type system is used to ensure that expressions are well-typed. Statements. Statements of the language are built from assignments, function calls, conditionals, for and (some mild generalization of) while loops, and the usual sequencing of statement “;”. Assignments are of one of the following form: d=e , or d1, . . . ,dk= op(e1, . . . , eℓ) , where d , d1 , ..., dk are destinations and e,e1, . . . , eℓ are expressions. A destination is either a variable x , an array destination x [ e ], a memory destination [ x+e ]or an underscore _ when the result can be discarded. Note that operator calls can have multiple destinations, according to their type. Function calls are also of the form d1, . . . ,dk=f(e1, . . . , eℓ) , where the number and nature of arguments and destinations is determined by the type of the function. The for loops have a body, a range of the form (e1..e2) and an iteration flag indicating if the loop ranges over e1,e1+ 1 , . . . , e2 or e1,e1− 1 , . . . , e2 . More interestingly, the syntax of the while loops is of the form while c1(e)c2 , where c1 is a statement that is executed before testing the expression e , and c2 is the loop body. This extended syntax is useful to capture different control-flow structures, including do-while and while-do loops. It also enables the use of arbitrary programs to express the loop guards. Statements must be well-typed; for instance, assigned expressions must match the type of their destination and loop guards must be boolean. Programs. Programs p are mappings from function names f to function declarations p(f) , comprising a command p(f)c and two lists of variables p(f)param and p(f)res describing, from the callee point of view, the variables in which the arguments will be stored and from which the return values will be fetched. Programs must be well-typed, following a typing discipline similar to that of statements. Each function declaration is annotated with either export or inline (the default). Only the first ones are compiled down to assembly. Calls to the second ones are meant to be fully inlined in the caller’s body; in that sense, these functions are a zero-cost abstraction provided to the programmer to structure the code. 5 We currently do not model some infrequently used flags such as AF since they are not used in our examples. 3.3 Semantics The behavior of Jasmin programs is given by a big-step operational semantics relating initial and final states. The semantics defines a partial function: for every initial state, there is at most one final state, reflecting that Jasmin programs have a deterministic behavior. Determinism of Jasmin programs is essential for predictability, and considerably simplifies the proof of correctness of the compiler, as discussed in Section 5. The semantics is fully formalized in the Coq proof assistant and is used as the basis for justifying the correctness of the compiler and of the source-level analyses (formally using the Coq proof assistant in the first case, and on paper in the second case). The semantics is defined in the context of a program, which is used to resolve function calls. To keep our notation readable, this ambient program is only shown when defining the semantics of function calls, which must resolve the called function. Values. Booleans are interpreted by the set { 0 , 1 ,⊥} , where ⊥ is used to model the behavior of some operations, e.g. shifts, on flags. Other types have the intended semantics. For instance, the type bi is interpreted as { 0 , 1 }i , and the type bi [ n ]is interpreted as { 0 , 1 }i [ n ], for i∈ { 8 , 16 , 32 , 64 } . The set of values is obtained by taking the union of the interpretation of types. States. States are pairs (m,ρ) consisting of a global memory m , shared between all functions, which maps addresses to bi values, and a local environment ρ , specific to each function, mapping variables to values. The environment is a functional map which associates to a variable (with a given type and identifier) a value (or an error). We use the usual notations · [ · ]for map access and · [ · : =· ]for map update. Memory. We use an axiomatic type for memories. This type is equipped with operations for reading and writing, which take a size i and an address of type b64 , and read or store a bi value (possibly returning errors). We use · [ · ]for reading and · [ ·←· ]for writing: m [ e ] i=v means that in memory m , reading a value of type bi from address e successfully returns the value v ; m [ e←v ] i=m′ means that in memory m , writing the value v with type bi successfully results in the memory m′ . In both cases, the optional subscript corresponds to the size of the value in memory (default is 64). Which addresses can or cannot be used by a Jasmin program is expressed through a predicate, validi(m,p) , that states that in memory m , pointer p can be safely used for accesses of size i . This predicate is under-specified; it is supposed to capture various architectural and system-specific constraints such as alignment requirements. The memory thus enjoys the following laws, which express the usual properties of memories: •valid addresses can be read: (∃v,m[p]i=v)⇐⇒ validi(m,p); •valid addresses can be written: (∃m′,m[p←v]i=m′)⇐⇒ validi(m,p); •a written value can be read back: m[p←v]i=m′=⇒m′[p]i=v; • a memory write leaves the remainder of the memory unchanged: m[p←v]i=m′=⇒ disjoint(p,i,p′,i′)=⇒m′[p′]i′=m[p′]i′ where disjoint expresses that two address ranges do not overlap. In addition to reading and writing, the Jasmin memory features a restricted form of dynamic allocation to model the life span of local variables: fresh memory is allocated on function entry, and released on function exit. This is modeled by means of two operations: alloc-stack(m,n) allocates a region of size n in memory m and free-stack(m,n) frees the top-most region in memory m , of size n . Such stack-allocated memory regions are handled through their base pointer. This stack is specified through three intermediate operators: •top-stack(m) returns the base pointer of the top-most stack region of memory m; •caller(m,p) returns, if any, the previous region, in the stack, of region starting at pin memory m; •frame-size(m,p) returns the size of the memory region starting at p , or nothing if it is not the base pointer of such a region in memory m. Writing to memory leaves these three properties unchanged; allocating and freeing update these properties to maintain the stack structure. The frame-size property enables us to implement allocation and freeing through addition and subtraction on a global stack pointer, without explicitly building a linked-list of frames. Finally, since the compiler needs to emit valid memory accesses, the memory model features an operation is-align(n,i) that tells whether a pointer with offset n is correctly aligned for memory access of size bi . The axiomatization of this operation mandates that, for stack memory regions, deciding whether a pointer is valid amounts to checking whether its relative offset (within this region) is aligned and in bounds. Expressions. The semantics of expressions is defined in the usual way, and is parametrized by a state s=(m,ρ) as described above. The evaluation of the expression e in the state s is noted JeK(s) , and is defined in the usual way. Even though we denote the evaluation of expressions as a function, their semantics is partial: ill-typed expressions never evaluate; out-of-bounds array accesses are not defined, as well as invalid memory accesses. Destinations. We will use the s [ · : =· ]notation for storing values in both the memory and environment, depending on the destination. Most of the rules are standard; the ones used for writing into memory and arrays are described in Figure 4. Statements. Formally, the semantics is captured by judgments of the form c,s⇓s′ , stating that executing command c on initial state s terminates in final state s′ . The rules, which are mostly standard, to the exception of the rules for functional arrays and procedure calls, are described in Figure 4. Sequences are defined in a standard way, with skip the empty command. Figure 4: Semantics of the Jasmin language (m,ρ)[[x+e] :=v]=(m[ρ[x]+JeK(m,ρ)←v],ρ) (m,ρ)[x[e] :=v]=(m,ρ[x:=ρ[x][JeK(m,ρ):=v]) d=e,s⇓s[d:=JeK(s)] op(Je1K(s), . . . , JeℓK(s)) =(v′ 1, . . . ,v′ k) d1, . . . , dk=op(e1, . . . , eℓ),s⇓s[dj:=v′ j] skip,s⇓s i,s⇓s1c,s1⇓s′ i;c,s⇓s′ c1,s⇓s′JeK(s)=true if (e)then c1else c2,s⇓s′ c2,s⇓s′JeK(s)=false if (e)then c1else c2,s⇓s′ c1,s1⇓s2JeK(s2)=true c2,s2⇓s3while c1(e)c2,s3⇓s4 while c1(e)c2,s1⇓s4 c1,s1⇓s2JeK(s2)=false while c1(e)c2,s1⇓s2 c,s⇓i∈range(JeloK(s),JehiK(s)) for s′ for(i=elo to ehi)c,s⇓s′ c,s⇓i∈[] for s s[i:=w],c⇓s2c,s2⇓i∈ws for s′ c,s⇓i∈w::ws for s′ a,(m,ρ)⇓vaf,va,m⇓p call vr,m′ r=f(a),(m,ρ)⇓(m′,ρ[r:=vr]) p(f)c,(m,∅[p(f)param :=va])⇓(m′,ρ′) f,va,m⇓p call Jp(f)resK(m′,ρ′),m′ Loops use two blocks of instructions, allowing to handle both do-while and while-do constructions at the same time: first the first block is executed, then the condition is evaluated: if it’s false we leave the loop, otherwise we execute the second block and then repeat from the first block. The semantics of for loops use another judgement ⇓for , where c,s⇓i∈ℓ for s′ describes the execution of the command c from the state s to the state s′ with the i integer variable taking all the values in ℓ . If the list ℓ is the empty list [], then the resulting state is the original state s . Otherwise, if the list ℓ has a head w and tail ws , the resulting state is the one after executing c in the state where the value w is assigned to the variable i , and then the rest of the values. Also, the function calls use the judgement ⇓call which describes the behavior of a function from the callee point of view: f,va,m⇓p call vr,m′ means that the function named f of the program p executed from the memory m with arguments va returns values vr in the memory m′ . Note that as said earlier, the environment between the caller and the callee are completely independent. 3.4 Memory safety and constant-time security Two essential properties of Jasmin programs are memory safety and constant-time security. In this paragraph, we introduce the two notions. Later, we will argue that both notions are preserved by compilation, and present automated methods for verifying that Jasmin programs are memory safe and constant-time. Memory safety. The Jasmin memory model is parameterized by the notion of validity. It must capture the various architectural constraints (e.g., alignment of pointers), and requirements from the execution environment (some memory regions might be reserved to the operating system, or to load the code text, which cannot be overwritten by Jasmin programs). Also, the allocation routine that is used to reserve memory for local variables on function entry must return fresh, valid memory addresses (or fail). AJasmin command c is safe if its semantics is defined for every initial state. Formally, ∀s· ∃ s′·c,s⇓s′ . This notion is rather strong; in particular, it entails that the program is well-typed, that it terminates on all inputs, that array accesses are always in-bounds, and that all memory accesses target valid memory. This definition of safety being very strong, we assume that programs may be equipped with preconditions that restrict the set of admissible initial states: enough free stack space, validity of input pointers, etc. Constant-time security. The semantics of Jasmin program can be instrumented to produce a leakage trace that records the branches that are taken and memory read/write operations performed during execution. Judgments of the extended semantics are of the form c,s⇓s′, ℓ where ℓ is the leakage trace. The extended semantics is used to formalize constant-time programs: specifically, a Jasmin command c is constant-time iff for every states s1,s2,s′ 1,s′ 2 and leakage traces ℓ1and ℓ2, we have: c,s1⇓s′ 1, ℓ1 c,s2⇓s′ 2, ℓ2 s1∼s2        ⇒ℓ1=ℓ2 where ∼ is an equivalence relation between states—as usual, ∼ is defined from security annotations specifying where secrets are held in the initial memory. We stress that our notion of constant-time security is terminationinsensitive and does not impose any condition on the program safety. However, it is well-known that naive error management is a main source of attacks in cryptographic implementations. In practice, we always check that programs are both safe and constanttime. 4 SAFETY AND CONSTANT-TIME ANALYSES This section describes how Jasmin source level analyses are deployed on top of the Dafny verification infrastructure. An annotated Jasmin intermediate program is translated into two complementary Dafny programs: the first encodes safety; the second, assuming safety, encodes constant-time security policies as annotations. 4.1 Safety analysis Dafny is a general-purpose verification language with support for procedures, loops, arrays and native bitvector theories. Our functional embedding of Jasmin into Dafny thus preserves the original program structure and is almost one-to-one. Most noteworthy, Jasmin functional arrays are encoded as fixed-size Dafny sequences, Figure 5: Annotated Montgomery Ladder in Jasmin (left) and Dafny translations for safety (middle) and constant-time (right). ... j=62;i=3; while (i >=s 0) //@ decreases i; //@ invariant i <=s 4; //@ invariant j == 62 || j == 63; //@ invariant i >=s 0 ==> valid(sp, 8 ∗i, 8 ∗i + 7); //@ security invariant public(i); { is = i; tmp1 = [sp + 8∗i]; s = tmp1; while (j >=s 0) //@ decreases j; //@ invariant j <=s 63; { ... j=js; j -= 1; } j=63;i=is;i-=1; } ... ... j := 62; i := 3; while (i >=s 0) decreases i; invariant (4 - i) >> 63 == 0; invariant (j == 62) || (j == 63); free invariant sp == old(sp); invariant i >> 63 == 0 ==> ValidRange(sp as int + 8 ∗i as int, sp as int + 8 ∗i as int + 7); { is = i; assert Valid(sp as int + 8 ∗i as int + 0); ...; assert Valid(sp as int + 8 ∗i as int + 7); ...; while (j >> 63 == 0) decreases j; invariant (63 - j) >> 63 == 0; { ... j=js;j:=j-1; } j:=63;i=is;i:=i-1; } ... ... j := 62; i := 3; while (i >=s 0) free ... invariant Public(sp); invariant Public(i); invariant Public(i > 1); { assert Public(sp as int + 8 ∗i as int + 0); ...; assert Public(sp as int + 8 ∗i as int + 7); ... while (j >> 63 == 0) free ... invariant Public(j); invariant Public(j >> 63 == 0); { ... j=js;j:=j-1; } j:=63;i=is;i:=i-1; } ... and memory encoded as a global array of byte blocks; reads and writes to memory are segmented into byte-wise operations, and require memory regions to be valid, axiomatized in Dafny as two ghost annotations Valid and ValidRange. Jasmin expressions and instructions are defined using mathematical integer and bitvector arithmetic, as precluded by the Coq semantics. An annotated snippet and its translation are shown in Figure 5. The safety of the Jasmin program is therefore reduced to the safety of the functional Dafny embedding. The Dafny verifier guarantees that a safe program terminates and is free of runtime errors such as memory accesses, array indices or shift amounts out of bounds or division by zero. For simple straight-line Jasmin programs, including most of our benchmarks, with no procedure calls, all loops unrolled and no memory operations, safety analysis can be performed fully automatically. Nevertheless, for more modular procedures, less well-behaved while loops or memory operations, programmers can supply additional annotations describing procedure contracts, loop invariants and valid memory regions. They can also express intermediate functional correctness properties seamlessly in the Jasmin annotation language. Taking a glance at Figure 5, both loops need invariants stating that the indices iand jdecrease until zero within the loop and that they stay within bounds. Moreover, the 64 bits addressed by sp + 8*i need to constitute a valid memory region. Under the hood, the Dafny verifier checks for correctness by translating to Boogie intermediate code. The Boogie verifier then generates verification conditions that are passed to the Z3 SMT solver. Alternatively, we have implemented a specialized verification condition generator for straight-line Jasmin procedures, in the style of [ 19 ]. This is more effective (specifically yields smaller verification conditions) for proving certain correctness properties of Jasmin programs, and targets specific SMT solvers such as Boolector that excels for bitvector arithmetic. We rely on the Haskell SBV 6 library as a universal interface with SMT-Lib. 6https://hackage.haskell.org/package/sbv 4.2 Constant-time analysis For constant-time analysis we instrument the generated Dafny program with special Public annotations on control flow conditions, memory accesses and array accesses, entailing that they do not depend on secrets. (Jasmin conditional assignments are compiled to constant-time instructions, so they do not require such safeguards.) As for safety, programmers can express additional security properties in Jasmin as boolean assertions using the public predicate. In the example from Figure 5, safety invariants are assumed to hold (marked with free or assume in Dafny) and the [sp + 8*i] memory read requires two security invariants stating that the values of sp and iare public inside the outer loop; the former is inferred from the procedure contract, and the second must be explicitly supplied by the programmer. The constant-time instrumentation departs from the functional embedding described in the previous paragraph in the sense that we explore the existing translation from Dafny to Boogie to propagate constant-time security policies from Jasmin to Boogie programs. The Boogie input language has a well-defined semantics and was designed to be a convenient backend for verification tools. There, procedures are defined as a sequence of basic blocks that start with a label, contain straight-line statements with no if or while statements, and may jump at the end. To verify constant-time, we adapt a technique used by the ct-verif tool [ 4 ] which reduces the constant-time security of a Boogie program to the safety of a product program that emulates two simultaneous executions of the original program. We implement a Boogie-to-Boogie transformation tailored to the translation of Jasmin programs that computes the product of each procedure by essentially making shadow copies of program variables and duplicating all statements inside basic blocks to mention shadow variables instead, with two exceptions: (1) procedure call statements are converted to single statements calling the product procedure with twice as many inputs and outputs, and (2) assertions corresponding to constant-time security policy annotations are translated to relational assertions expressing firstorder logic formulas that relate original and shadowed variables, Left-values (destinations of assignments) are either an underscore meaning that the value should be ignored (not assigned to anything), a variable, an array cell, or a memory address. ⟨plvalue⟩::=UNDERSCORE | ⟨var⟩ | ⟨var⟩ ⟨brackets⟨pexpr⟩⟩ |[⟨parens⟨ptype⟩⟩]⟨brackets(⟨var⟩+⟨pexpr⟩)⟩ Functions. A function body is, surrounded by braces, a sequence (maybe empty) of declarations of local variables, followed by a sequence (maybe empty) of instructions, followed by an optional return clause. Functions may return several values at once. ⟨pfunbody⟩::=LBRACE (⟨pvardecl⟩;)∗⟨pinstr⟩∗[RETURN ⟨tuple⟨var⟩⟩ ;] RBRACE ⟨storage⟩::=REG |STACK |INLINE ⟨stor_type⟩::=⟨storage⟩ ⟨ptype⟩ ⟨pvardecl⟩::=⟨stor_type⟩ ⟨var⟩ Global declarations. AJasmin module is a sequence of global declarations, each of them being the declaration of a function, of a parameter (value known at compile time) or of a global (read-only) variable. ⟨module⟩::=⟨top⟩∗EOF |error ⟨top⟩::=⟨pfundef⟩ | ⟨pparam⟩ | ⟨pglobal⟩ ⟨call_conv⟩::=EXPORT |INLINE ⟨pfundef⟩::=[⟨call_conv⟩] FN ⟨ident⟩ ⟨parens_tuple(⟨stor_type⟩ ⟨var⟩)⟩[-> ⟨tuple⟨stor_type⟩⟩]⟨pfunbody⟩ ⟨pparam⟩::=PARAM ⟨ptype⟩ ⟨ident⟩=⟨pexpr⟩; ⟨pglobal⟩::=⟨ident⟩=⟨pexpr⟩; BJASMIN X25519-4LIMB IMPLEMENTATION This section provides more detailed information regarding our optimized X25519-4limb-jasmin implementation in Jasmin. Figures 6 and 7 show the complete source code for the iterated_square and mladder procedures – that exemplify the use of high-level control flow structures in Jasmin – including the respective programmer annotations needed for automatic verification. The remaining procedures consist of simple straight-line code and only require top-level procedure contract annotations. Our full X25519-4limb-jasmin implementation comprises a total of 16 procedures and 798 lines of code. These include 24 lines of programmer annotations split into procedure contracts (13 lines) and loop invariants (11 lines). Figure 6: Complete iterated_square procedure from our X25519-4limb-jasmin implementation. fn iterated_square(stack b64[4] xa, stack b64 n) −→ stack b64[4] //@ requires n >=s 3 && n <=s 98; //@ security requires public(n); { reg b64[8] z; reg b64[4] r; reg b64[5] t; reg b64 xa0, xa1, xa2, rax, rdx; reg bool cf; reg b64 n_r; //@ cf = false; while //@ decreases n; //@ invariant !cf == (n >=s 0); //@ invariant n <=s 98; { xa0 = xa[0]; xa1 = xa[1]; xa2 = xa[2]; rax = xa1; rdx, rax = rax * xa0; z[1] = rax; z[2] = rdx; rax = xa2; rdx, rax = rax * xa1; z[3] = rax; z[4] = rdx; rax = xa[3]; rdx, rax = rax * xa2; z[5] = rax; z[6] = rdx; z[7] = #x86_MOV(0); rax = xa[2]; rdx, rax = rax * xa0; cf, z[2] += rax; cf, z[3] += rdx + cf; _, z[4] += 0 + cf; rax = xa[3]; rdx, rax = rax * xa1; cf, z[4] += rax; cf, z[5] += rdx + cf; _, z[6] += 0 + cf; rax = xa[3]; rdx, rax = rax * xa0; cf, z[3] += rax; cf, z[4] += rdx + cf; cf, z[5] += 0 + cf; cf, z[6] += 0 + cf; _, z[7] += 0 + cf; cf, z[1] += z[1]; cf, z[2] += z[2] + cf; cf, z[3] += z[3] + cf; cf, z[4] += z[4] + cf; cf, z[5] += z[5] + cf; cf, z[6] += z[6] + cf; cf, z[7] += z[7] + cf; rax = xa0; rdx, rax = rax * xa0; z[0] = rax; t[0] = rdx; rax = xa1; rdx, rax = rax * xa1; t[1] = rax; t[2] = rdx; rax = xa[2]; rdx, rax = rax * xa[2]; t[3] = rax; t[4] = rdx; cf, z[1] += t[0]; cf, z[2] += t[1] + cf; cf, z[3] += t[2] + cf; cf, z[4] += t[3] + cf; cf, z[5] += t[4] + cf; cf, z[6] += 0 + cf; _, z[7] += 0 + cf; rax = xa[3]; rdx, rax = rax * xa[3]; cf, z[6] += rax; _, z[7] += rdx + cf; r = reduce(z); xa = r; n_r = n; cf, n_r -= 1; n = n_r; } (! cf) return xa; } Figure 7: Complete mladder procedure from our X255194limb-jasmin implementation. fn mladder(stack u64[4] x2, stack u64[4] z2, stack u64[4] xr, reg u64 sp) →(stack u64[4], stack u64[4]) //@ requires valid(sp,8∗0,8∗4 - 1); //@ security requires public(sp); { stack u64 s; reg u64 tmp1; reg u64 tmp2; reg u64 bit; reg u64 swap; stack u64 prevbit; stack u64[4] x1; reg u64[4] x2r; stack u64[4] x3; stack u64[4] z3; reg u64 i; reg u64 j; stack u64 is; stack u64 js; reg bool cf; reg u64[4] buf; buf = xr; x1 = buf; x3 = buf; x2[0] = 1; x2[1] = #x86_MOV(0); x2[2] = #x86_MOV(0); x2[3] = #x86_MOV(0); z2[0] = #x86_MOV(0); z2[1] = #x86_MOV(0); z2[2] = #x86_MOV(0); z2[3] = #x86_MOV(0); z3[0] = 1; z3[1] = #x86_MOV(0); z3[2] = #x86_MOV(0); z3[3] = #x86_MOV(0); j = 62; i = 3; prevbit = #x86_MOV(0); while //@ decreases i; //@ invariant i <=s 4; //@ invariant j == 62 || j == 63; //@ invariant (i >=s 0) ==> valid(sp,8∗i,8∗i + 7); //@ security invariant public(i); { tmp1 = [sp + 8∗i]; is = i; s = tmp1; while //@ decreases j; //@ invariant j <=s 63; { tmp2 = s; bit = tmp2 >> j; js = j; bit = bit & 1; swap = prevbit; swap ^= bit; prevbit = bit; x2r,z2,x3,z3 = cswap(x2,z2,x3,z3,swap); x2r,z2,x3,z3 = ladderstep(x1,x2r,z2,x3,z3); x2 = x2r; j = js; j -= 1; } (j >=s 0) j = 63; i = is; i -= 1; } (i >=s 0) return x2, z2; }