Frédéric Besson
email: frederic.besson@inria.fr

Alexandre Dang
email: alexandre.dang@inria.fr

Thomas Jensen
email: thomas.jensen@inria.fr

Information-Flow Preservation in Compiler Optimisations

Keywords: Secure compilation, Side-Channel, Information-Flow Preservation

Correct compilers perform program transformations preserving input/output behaviours of programs. Though mandatory, correctness is not sufficient to prevent program optimisations from introducing information-flow leaks that would make the target program more vulnerable to side-channel attacks than the source program. To tackle this problem, we propose a notion of Information-Flow Preserving (IFP) program transformation which ensures that a target program is no more vulnerable to passive side-channel attacks than a source program. To protect against a wide range of attacks, we model an attacker who is granted arbitrary memory accesses for a pre-defined set of observation points. We propose a compositional proof principle for proving that a transformation is IFP. Using this principle, we show how a translation validation technique can be used to automatically verify and even close information-flow leaks introduced by standard compiler passes such as deadstore elimination and register allocation. The technique has been experimentally validated on the CompCert C compiler.

I. INTRODUCTION

When it comes to security, compilers can not be trusted. They may perform aggressive optimisations which may exploit undefined behaviours [START_REF] Wang | Undefined Behavior: What Happened to My Code?[END_REF] or they may have subtle bugs and generate invalid code [START_REF] Yang | Finding and understanding bugs in C compilers[END_REF]. Compilers may turn secure constant-time source programs [START_REF] Almeida | Verifying constant-time implementations[END_REF], [START_REF] Blazy | Verifying Constant-Time Implementations by Abstract Interpretation[END_REF] into target programs vulnerable to timing attacks [START_REF] Kaufmann | When Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC 2015[END_REF]. Compilers may also increase the lifetime of sensitive data in memory and therefore make the target program more vulnerable to attackers with physical access. The pitfalls of so-called safe erasure in the presence of compiler optimisations is recognised by the CERT at CMU 1 and protections have recently been proposed e.g., [START_REF] Simon | What You Get is What You C: Controlling Side Effects in Mainstream C Compilers[END_REF], [START_REF] Yang | Dead Store Elimination (Still) Considered Harmful[END_REF]. The overall consequence of this unfortunate state-of-affairs is that for highly-critical code, manual inspection of the generated code is standard industrial practice. Furthermore, even if the proposed counter-measures are effective in practice, they do not come with a formal security guarantee.

Much progress has been made in the formal verification of compiler correctness, providing a semantic guarantee that the behaviour of the compiled program is compliant with the behaviour of the source code. Prominent examples are the COMPCERT C compiler [START_REF]Formal verification of a realistic compiler[END_REF], verified using the Coq proof assistant [START_REF]The Coq proof assistant reference manual[END_REF], CAKEML [START_REF] Kumar | Cakeml: a verified implementation of ML[END_REF], an ML compiler verified using 1 CERT MSC06-C HOL4 [START_REF]HOL4[END_REF] or seL4 [START_REF] Sewell | Translation validation for a verified os kernel[END_REF] a verified microkernel whose compilation was proven correct through translation validation [START_REF] Pnueli | Translation validation[END_REF]. Compiler correctness is often desired but non sufficient to preserve non-functional properties which are essential for the security of the compiled code [START_REF] Silva | The Correctness-Security Gap in Compiler Optimization[END_REF].

In this paper, we propose an end-to-end security property to ensure that a target program does not leak more information than a source language. We build on the previous work of Besson et al. [START_REF] Besson | Securing Compilation Against Memory Probing[END_REF] but enrich their model to a more realistic setting where an attacker may observe intermediate program states and a strengthened security model preventing the duplication of potentially sensitive data. We consider an attacker model in which an attacker is granted physical memory access at specific observation points, and is parametrised by the amount of information he is allowed to read. In our setting, a program transformation is secure if an attacker at the target language does not have an advantage with respect to an attacker at the source language. This is formalised using the standard information-flow notion of Attacker Knowledge [START_REF] Askarov | Gradual Release: Unifying Declassification, Encryption and Key Release Policies[END_REF].

The technical contributions of the paper can be summarised as follows:

• A formal definition of Information-Flow Preserving (IFP) transformation based on the notion of Partial Attacker knowledge. • A simulation-based proof principle for proving that a program transformation is IFP. • A translation validation algorithm which can be instrumented to automatically close information-flow leaks in case the transformation is not IFP. • An implementation and experiments with an IFP register allocation pass within the COMPCERT compiler.

The rest of the paper is organised as follows. Section II explains the rationale for our attacker model. Examples of security issues of compiler transformations with respect to this attacker model are presented in Section III. Section IV defines formally our notion of Information-Flow Preservation. In Section V, we introduce a necessary condition for IFP; this condition takes the form of a simulation-based principle. We use this principle in Section VI to design a translation validation approach for the Register Allocation pass of COM-PCERT and present our experimental results in Section VII. We compare with related work in Section IX and Section X concludes.

II. ATTACKER MODEL

Our overall goal is to prevent information leaks from being introduced by the compilation process. Compiled code should be no more vulnerable to passive side-channel attacks than the source code. Such side channels correspond to an attacker who is granted physical memory access at specific observation points, and who is parametrised by the amount of information he is allowed to read. At the semantic level, side-channels can be modelled using a leakage function exposing a partial view of the program state to the attacker [START_REF] Barthe | Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time[END_REF].

The typical example is the timing channel which can be modelled by leaking the program counter and the memory accesses [START_REF] Almeida | Verifying constant-time implementations[END_REF]. Another example is the power channel that can be modelled by the so-called Hamming Weight model [START_REF] Kocher | Differential Power Analysis[END_REF] where what is leaked is the Hamming Weight of the program state i.e., the number of information bits that are set to 1.

In our model, in order to protect against an arbitrary sidechannel, we quantify over a hierarchy of attackers A n who have access to the programs code and where n is the number of bits of information that the attacker is allowed to extract from the program memory during the program execution. Thus, we do not fix one leakage function a priori but rather consider protecting against a hierarchy of leakage functions.

This attacker model is sufficient to formally capture the leakage of information. However, it does not take into account the practical difficulty of a physical attack i.e. how hard it is to extract bits of information when the memory is indirectly observed through a noisy side-channel. For instance, an attacker would in practice have an advantage if sensitive data is duplicated multiple times across the memory. We address this problem by forbidding duplication of data. This, in turn, leads to the formal requirement that for a given information leakage, there is an injection between the target attacker observations and the source attacker observations.

Our attacker model and our notion of Information-Flow Preserving transformation are formally presented in Section IV. First, we present a few typical program transformations and explain informally whether they are Information-Flow Preserving or not.

III. INFORMATION FLOW PRESERVATION BY EXAMPLES

In Figure 1, we present a list of simple programs using the syntax of an imperative language where a • indicates program points where the program memory is leaked to the attacker. In terms of input/output semantics, the program are indistinguishable: they all return 0. As a result, they could all be compiled from the original canonical program f that sets the variable x to 0 and returns 0. The program f leaks its initial memory (• 1 ) and final memory (• 2 ) to the attacker. In Figure 1, we mark the programs that are IFP with a and those which are not with a . In the following, we write v• i for the observation of the value of the variable v at the leakage point • i . Consider Program g obtained by removing the assignment to the variable x from Program f . From a compiler point of view, this is a correct transformation because the value of x does not contribute to the result. However, removing such a dead store introduces an information-flow leak and should therefore be ruled out. Intuitively, the principle for a transformation to be safe is that any observation of a value made with the target program must have a corresponding observation in the source code. In particular, the observation x• 2 in g needs to be matched by an observation of x• 2 in f . As the observation of x• 2 in g has no counterpart in f for any v• 2 , the transformation is rejected. Note that it is of utmost importance for the source and target observations to be synchronised i.e. a target observation at • i needs to be matched by a source observation at the same observation point • i . Otherwise, Program g would be wrongly deemed secure under the fallacious argument that the observation of x• 2 in g leaks the same information as x• 1 in f . The synchrony of observations is our solution to make it impossible to remove or delay the erasure of some information.

Program h overwrites x with a different constant. As constants carry no information, the observation x• 2 in f and h leak the same (empty) amount of information and therefore the transformation is information-preserving.

Program i overwrites x with the variable y. Because y• 2 is already leaked, this does not introduce any additional information-flow leak. However, it does lead to duplication of information which we may want to forbid. In the example, the duplication may make it easier to get to the information of y• 2 in i (it is also present in x• 2 ) than in f (where it is only present in y• 2 ). To track duplication, our security definition can be adjusted to mandate the existence of a bijection between target and source observations. In the present case, constructing the bijection is impossible because there are two target observations i.e. x• 2 and y• 2 in i, leaking the value of y while there is a single source one i.e. y• 2 in f .

Program j (resp. Program k) leaks the initial value of x through the variable a using a direct (resp. indirect) flow. In either case, the observation a• 2 has no counterpart in f and the transformation is rejected. Our Information-Flow preserving definition is semantic in nature and immune to syntactic differences.

A. The "Full Information Flow" Paradox

We work with a parameterised attacker model where the attacker makes partial observations. Partial observations are essential, because they capture partial information flows that would go unnoticed if we only had an omniscient attacker observing the whole memory. In the context of dynamic information flow policies, Askarov and Chong [START_REF] Askarov | Learning is change in knowledge: Knowledge-based security for dynamic policies[END_REF] have already observed that a program could be secure against a powerful attacker but insecure for a weaker attacker. To see this, consider the program f and the transformed program g in Figure 2. Using a cryptographic analogy, Program f is encoding the plain-text y using the one-time pad key x and erases the key x. Program g performs the same encryption without erasing the key. If the attacker observes x• 2 in Program g, he obviously learns the key x. Perhaps surprisingly, the key x can also be learnt for Program f by an attacker observing both the plaintext y• 2 and the cipher-text a• 2 . The attacker obtains x by solving the equation a

• 2 = x ∧ y• 2 whose unique solution is x = a• 2 ∧ y• 2 .
Thus, no additional information flow is introduced and the transformation is (erroneously) deemed secure. To rule out this insecure transformation, we stipulate that both attackers need to observe the same amount of information i.e., the same number n of bits. If both attackers observe a single bit, the observation a• 2 in g cannot be simulated in f and therefore we conclude that the transformation is, as expected, not information-flow preserving.

IV. INFORMATION-FLOW PRESERVATION A. Execution model

Without loss of generality, we assume that the program state is only made of a bit-addressable memory:

Mem = Address → Bit Bit = {0, 1}
A structured program state s can always be mapped to a memory m ∈ Mem at the cost of some encoding. For instance, a language using program variables would represent them by reserving certain memory addresses. The semantics of a program p is given by a one-step deterministic transition relation • → e • ⊆ Mem × Mem where e ∈ E = { , o} is either , denoting a silent transition, or o indicating that the end state of the transition is leaked to the attacker. From an initial memory m 0 , a run of a program p is given by a sequence of memories

m 0 • m 1 e1 • • • m n en
such that for every i < n we have m i → ei m i+1 . Given such a run, the view of the attacker is given by the subtrace of leaked memories i.e. those memories resulting from a transition tagged o. Formally, we define the transition relation of the attacker

• • ⊆ Mem × Mem
as a sequence of silent transitions followed by a transition leaking its final memory:

m → * m m → o m m m
As a result, from an initial memory m 0 , the trace of memories t = m 1 • • • m n that is leaked to the attacker is such that for every i < n we have m i m i+1 . In the following, we write (p, c) ⇓ t for a trace of the attacker obtained by running the program p from an initial memory c.

B. Partial Attacker Knowledge

We next define precisely the information leaked through a (partial) trace of attacker observations, using the notion of Attacker Knowledge. Following [START_REF] Askarov | Gradual Release: Unifying Declassification, Encryption and Key Release Policies[END_REF], the Attacker Knowledge from a trace t of program p is defined by

K t (p) = {c ∈ Mem | (p, c) ⇓ t},
i.e., the attacker knowledge corresponds to the initial memories that may lead to (and hence are indistinguishable by) the observation of the trace t. We generalise the notion of Attacker Knowledge to partial observations of n bits of the trace t. A partial observation o is a trace of partial memories, i.e., a trace of partial maps from addresses to bits:

(Address → Bit) *
Partial memories m, m ∈ Address → Bit are ordered so that m m if m and m agree on all the addresses where m is defined. Formally, this is the standard (point-wise) ordering of partial functions:

m m = ∀x ∈ dom(m).m(x) = m (x).
Two partial traces are ordered if they have the same length and the memories (at the same position) are ordered using . Formally:

m m o o m • o m • o .
The number of bits n of a partial trace o is written |o| and is obtained by summing the number of bits defined by the partial memories m in o.

| | = 0 |m • o| = |dom(m)| + |o|.
We can then define the notion of partial observation formally as follows.

Definition 1 (Partial Observation). The set of partial observations of n bits of a trace t is defined by

Obs(t, n) = {o : (Address → Bit) * | o t ∧ |o| = n}
Definition 2 generalises the standard notion of Attacker Knowledge to partial observations. Definition 2. For a program p and a trace t, the Partial Attacker Knowledge for a partial observation o ∈ Obs(t, n) is given by

K t n (p, o) = o u K u (p).
In Definition 2, we quantify over all the complete traces u ∈ Mem * that are compatible with the partial observation o i.e., {o | o u} . The Partial Attacker Knowledge is therefore defined as the union of the Attacker Knowledge for all the complete traces that are indistinguishable from the point of view of o.

C. Information-Flow Preserving Transformation

We shall use Partial Attacker Knowledge to define precisely what we mean by a secure transformation of a source program into a target. Intuitively, a source program p is at least as vulnerable as a target program p if any partial observation o of a (target) trace of p can always be matched by a partial observation o of a (source) trace of p such that the source observation o leaks more information than the target observation o .

The notion of matching observation is formalised by a function mapping partial observations from Obs(t , n) to Obs(t, n). To forbid transformations that increase the lifetime of an information leak, we also enforce that the observations at the target and source level are performed in lock-step i.e., at each instant, both attackers observe the same amount of information. Definition 3. The set of lock-step observation mappings Ω is defined by

Ω (t , t, n) = {ω : Obs(t , n) → Obs(t, n) | ∀o , sup(o ) = sup(ω(o ))}
where the support of an observation is defined by

sup( ) = sup(m • o) = |dom(m)| • sup(o)}
Using lock-step mappings, we are ready to define the security refinement of a source program p by a target program p . Definition 4. A target program p is at least as secure as p for an attacker observing n bits (written

p n p ) iff ∀c, t, t .(p, c) ⇓ t ∧ (p , c) ⇓ t ⇒ ∃ω ∈ Ω(t, t , n).∀o .K t n (p, ω(o )) ⊆ K t n (p , o )
Because it quantifies over every partial observations and requires a lock-step mapping, Definition 4 ensures that if a target observation is matched by a source observation, so is every prefix observation.

In order to rule out the duplication of information, we can further restrict the function ω to be injective, by adding the constraint

Ω 1 (t , t, n) = Obs(t , n) Obs(t, n)
where denotes the set of bijective functions. In case of duplication of information, several target observations with the same Partial Attacker Knowledge would need to be mapped to the same source level observation. The fact that ω is injective rules out this possibility. In the following, we take the constraint on matching functions to be either Ω or Ω ∪ Ω 1 and discuss when the constraint Ω 1 is a too strong requirement.

A transformation T is IFP if T (p) is at least as secure as p for attackers with any level of observational power.

Definition 5. A transformation T

: P rog → P rog is IFP iff ∀p, n∈N (p n T (p))
V. A SUFFICIENT CONDITION FOR IFP AND ITS PROOF PRINCIPLE The definition of an IFP transformation does not suggest an immediate composition proof principle, and proving directly that a program transformation abides to Definition 5 would be a daunting task. To prove that a transformation is IFP, we present a simulation-based proof technique, ensuring that a source memory can be simulated by a target memory.

A. Partition and Simulation Relation

In order to facilitate concrete proofs, we partition the memories leaked to the attacker. In program terms, a typical partitioning would assign to the same partition index i all the memory leaked by a given syntactic observation point • i . To each partition index i, we attach a simulation function α i : Address → Address + Bit. Given a source memory m and a target memory m mapped to the same partition index i, the mapping α i explains how m can be effectively simulated by m . This is done by showing how any bit in m is either a constant (thus without any information) or a bit that is stored in m possibly at another address as indicated by α i .

Example 1. Consider the Programs f and h of Figure 1. For this simple case, each observation point • i (both in the source and target program) would be mapped to the partition index i ∈ {1, 2}. For the initial observation point • 1 , both memories are the same and therefore we would have α 1 would be the identity function λ a.a. For • 2 , the memories are the same except for the address x which carry the constant 1 in Program h. Therefore, we would have α 2 = λa. if a = x then 1 else a.

As we show in Theorem 1, these are sufficient conditions to ensure that m contains at most the same amount of information as m.

The source (resp. target) partition is characterised by a function sid (resp. tid ) : Memory → [1 , . . . , n]. Therefore, in the following, we write m.sid (resp. m .tid ) for the source index (resp. target index) of a memory m (resp. m ).

∀a .m (a ) = α(a ) if α(a ) ∈ Bit m(α(a )) if α(a ) ∈ Address
Lifted to traces we get,

∼ α m ∼ α m t ∼ α t m • t ∼ α m • t
In order to avoid duplication of information and enforce the constraint Ω 1 , the function α i needs to be further constrained to forbid mapping distinct target addresses to the same source address i.e., ∀a 1 , a 2 .α i (a

1 ) = α i (a 2 ) ∈ Address ⇒ a 1 = a 2 .
Using the previous definitions, our necessary conditions for IFP can be stated using Theorem 1.

Theorem 1. Consider two programs p and p , and an indexed simulation function α i :

Address → Address + Bit. If ∀c, t, t .   (p, c) ⇓ t ∧ (p , c) ⇓ t   ⇒ t ∼ α t
then ∀n, p n p , i.e., the transformation is IFP.

Proof: Suppose t ∼ α t . We need to prove, for any n,

∃ω.∀o . K t n (p, ω(o )) ⊆ K t n (p , o ) Let t = m 0 •• • ••m n and t = m 0 •• • ••m n .
Remember that ω has type Obs(t , n) → Obs(t, n) and that observations are made in lock-step fashion. As a result, it is sufficient to provide a mapping ω i : Obst(m i , k ) → Obs(m i , k ) which given a partial observation o of the target memory m i reconstructs an observation ω i (o ) of the source memory m i . As m i ∼ αi m i , this can be done as follows. Suppose that o (a ) = ⊥ for some address a . If α i (a ) ∈ Address, we can obtain the same observation from memory m i and ω i (o )(a ) = m i (α(a )). Otherwise, If α i (a ) ∈ Bit, the observation does not provide any information and therefore it suffices to pick an arbitrary fresh address a, and have

ω i (o )(a) = m i (a).
From this construction, for any partial observation o ∈ Obs(t , n) we can derive a partial observation of the source execution ω(o ) which contains at least as much information as in o . It follows that the target attacker knowledge obtained from an observation o is always bigger than the source attacker knowledge of the observation ω(o ) and therefore the property holds. Theorem 1 does not provide a complete characterisation of IFP transformations. It captures transformations where information is perhaps moved around but is otherwise unmodified. To illustrate the limitation, consider the following contrived example

x:=y → x := ∼ y

where the bit values of y are flipped bitwise. The variables x and x contain the exact same information i.e., the value of y. Yet, the transformation of values cannot be modelled by a simulation function α. We show that standard optimisations including register allocation and dead store elimination are in the scope of Theorem 1.

B. Simulation-Based Principle

The pre-condition of Theorem 1 can be proved using a lockstep backward simulation principle over the attacker semantics.

  (p, c) ⇓ t ∧ (p , c) ⇓ t   ⇒ t ∼ α t
Proof: Thee proof is by induction over the length of the trace t and follows using Condition 1 of Definition 7 for the base case and Condition 2 of Definition 7 for the inductive case.

VI. TRANSLATION VALIDATION FOR REGISTER ALLOCATION

Translation validation [START_REF] Pnueli | Translation validation[END_REF] is a verification technique which consists in validating a posteriori (and automatically) that a program p is obtained by a valid transformation of a program p. We adapt this principle and design a specialised algorithm to validate a posteriori whether programs obtained through the Register Allocation (RA) pass of the verified COMPCERT C compiler [START_REF] Leroy | Formal certification of a compiler back-end or: Programming a compiler with a proof assistant[END_REF] satisfy our IFP property. This is done by explicitly constructing a backward simulation using the sufficient condition of Section V. An interesting feature of our algorithm is that certain failures can be interpreted as potential information leak and that these leaks can be closed automatically by inserting erasing instructions.

A. Register Allocation in a Nutshell

Before RA, programs make use of an unbounded number of pseudo-registers. The role of RA is to explicit the constraint that the physical machine has only finitely many registers and therefore allocate each pseudo-register to a machine register. RA is also responsible for implementing calling-conventions i.e. passing arguments in the right register and restoring calleesaved registers. What makes RA a complex optimisation task is that this resource allocation task may be impossible due to a shortage of registers. In that case, a register may be spilled in the function stack frame i.e. its content copied, for later reuse. After the last use of a spilled register, a conventional RA algorithm has no reason to explicitly erase the stack location. This breaks our IFP property because i) the value is duplicated (it is stored in both a register and a stack location); ii) this introduces an information leak if the stack location is not erased after the last use of the register. This is illustrated by Example 2.

Example 2. Consider the simple function cipher of Figure 3 and the function cipher ' obtained by a typical RA pass for an hypothetical target architecture with only two registers r1 and r2. The code has been arranged to highlight the relation between a source instruction and the corresponding sequence of target instructions. For instance, the source instruction of Line 6 is compiled into the sequence of target instructions of Lines The LTL language is similar to RTL with the differences that i) so-called locations corresponding to stack slots or machine registers are used in place of the unlimited pseudo-registers called temporaries and; ii) call and return instructions are bounded by the calling conventions of the target architecture. As a result, in the program syntax, args and dest are locations made of either machine registers or stack slots used for spilling registers. Compared to temporaries, stack slots are pointers into the current stack frame and special care must be taken to make sure that spilled registers do not overlap. The calling conventions stipulate where function arguments and return must be stored and are represented by a list of locations. For instance, for x86_32, arguments are passed on the stack and the result is stored in eax while for x86_64, arguments are passed in different registers depending of the type of the argument.

2) Translation Validation of RA : COMPCERT is using an untrusted RA algorithm which output is verified using a specialised translation validation approach [START_REF] Rideau | Validating register allocation and spilling[END_REF], ensuring that each target LTL function is a sound compilation of the source RTL function. Observational correctness of the whole program is then achieved by composing the validation of each pair of functions. As our own IFP validator is reusing some key components, we give a brief overview of their algorithm.

The translation validator of COMPCERT exploits that the RTL and LTL functions have a very similar structure and only differ in that the LTL function introduces move instructions to materialise spills and reloads of stack slots; and data movements between registers.

The untrusted RA algorithm takes as argument a RTL function and returns a LTL function. The LTL function is structured in such a way that it is straightforward to rebuild a mapping from a single RTL instruction to the list of LTL instructions it is compiled into. Because RA is only using a few local transformations, the list of LTL instructions is always made of move instructions i.e. assignments between locations, followed by the actual instruction which is obtained from the original RTL instruction by replacing registers by locations. The only possibilities are presented in the first column of Figure 4. Each possible association of instructions are categorized into block-shape and form whole block-shape functions. Similar to RTL and LTL, block-shape functions are structured as a CFG and each block-shape is parametrised with the nodes of its successors. Moreover each possible blockshape contains a list of move instructions from the LTL code, labelled mv in Figure 4, which are executed before the core instruction.

COMPCERT translation validation algorithm is composed of two parts. The first one is a structural check which verifies that the LTL function respects a certain structure in regard to the RTL function. This check is carried while by constructing the block-shape function. For example to construct BSop the validator needs to find op instructions in both RTL and LTL and that the operations computed match. Another example with BScond where the condition and successors must be the same in both cond instructions. If an unexpected pattern is found between source and transformed functions then the structural check and the validation will fail. To complete the translation validation algorithm, COMPCERT performs an additional backward data flow analysis to verify that the two functions effectively compute and use the same values.

C. Modular IFP Validation Algorithm

Our security policy is determined by the location of observation points • in both the RTL and LTL programs. In order to get a translation validation algorithm integrated in the RA compiler pass, it is necessary to be able to process one function at a time. Our solution is to set observation points at function boundaries, more precisely at function calls and returns. From a security point of view, this ensures that the locations managed by register allocation do not leak information at function return i.e. the stack frame does not leak information not present in the pseudo-registers of RTL.

In the following, we detail our IFP validation algorithm. In Section V, we have shown that proving IFP preservation can be done by exhibiting some mapping α i : Address → Address + Bit used to establish a simulation between the source and the target memories at every observation point • i . To get to this point, our IFP validator needs to construct richer objects in order to accommodate for the RTL and LTL COMPCERT memory model [START_REF] Leroy | Formal verification of a C-like memory model and its uses for verifying program transformations[END_REF] and the fact that, for intermediate program points, the existence of such a α i mapping is a too strong requirement. Hence, the IFP validator constructs a set of associations between locations and temporaries β i ∈ P(Loc × Temp); computes the set of modified location γ i ∈ P(Loc) and performs a constant analysis cst i : Loc → Value +{ } such that, given a program point i, (l, t) ∈ β i iff the value of the LTL location l is the same value as the RTL temporary t; l ∈ γ i iff the location l may be modified by the current function and cst i (l) = v iff for any execution the location l always contains the value v.

The constant analysis cst i and the set of modified locations γ i are computed by solving standard forward data-flow equations that are solved iteratively using the data-flow framework of COMPCERT.

1) Inference of Location Mapping β i : Compared to the existing RA validator of COMPCERT, a difference is that we construct β i using a forward data-flow analysis over the block-shapes of Figure 4. The reason is that, for compiler correctness, it is just necessary to ensure that the return LTL register, say eax , is mapped to the return RTL temporary, say t. For IFP, we need a comprehensive mapping for all the RTL temporaries and LTL locations.

The transfer functions for the possible block shapes generated by RA can be found in Figure 4. The transfer functions are using the following notations. We write (l → t) for a pair (l, t) ∈ β i with the interpretation that the LTL location l is mapped to the RTL temporary t. We extend this notation to vectors of locations and temporaries and write (l 1 , . . . , l n ) → (t 1 , . . . , t n ) for the set {(l 1 → t 1 ), . . . , (l n → t n )}. Because of copy instructions, in both LTL and RTL, the mapping is not unique and there may be several pairs with l as first component and t as the second component. Given a temporary t, we write (_ → t) for the set of all pairs such that the second element is t. Symmetrically, for a given location, we write (l → _) for the set of all pairs such that the first element is l.

All block shapes have a sequence of move mv instructions on the LTL side. A move l 1 = l 2 assigns l 2 to l 1 . Given an initial mapping B, the effect of move l 1 = l 2 is to remove the existing mappings for l 1 ((l 1 → _)) and map l 1 to existing mappings of l 2 in B. As a result, we get

transfer l1 =l2 = B \ (l 1 → _) ∪ ({l 1 → x } | {l 2 → x } ∈ B ).
For valid code, there should always be an existing mapping for l 2 . If not, the analysis continues but l 2 and l 1 would be flagged as potential information leaks at the next observation point.

A BSnop only consists in a list of LTL move instruction and its effect is modelled by iterating the transfer function for a single move instruction. For BSop, we check after computing the consequence of the moves that the LTL arguments args are mapped to the RTL arguments args. If this is the case, we have the guarantee that the arguments args and args have the same values and therefore the destinations tmp and loc have the same value. After evaluating the effect of the moves, the transfer function invalidates the existing mappings for tmp and loc and add the mapping (loc → tmp). For BSLoad, the transfer function is similar but exploits the additional invariant that the memory of RTL and LTL agree for every address a that is neither a LTL location a / ∈ Loc nor a temporary a / ∈ Temp. For BSstore, we check that the computed addresses args and args compute the same value in both RTL and LTL. We also check that the stored value are the same i.e., the current mapping includes (loc → tmp). Except for the potential move instructions, a memory store has no effect on the current mapping. Yet, our verifications ensure that the LTL and RTL memory still agree for addresses that are neither temporaries nor locations. For BScall, we check that the arguments of the call are the same. In RTL, the arguments and return value are explicitly passed; in LTL, the functions Params(sig) and Ret(sig) implement the architecture dependent calling conventions of functions arguments and return. In RTL, all the temporaries are restored after a function call. In LTL, the calling conventions state that both stack locations and a subset of the registers i.e., so calleesaved registers, are restored after a call. This is modelled For BScond, we simply check that the conditions evaluate to the same value thus ensuring that both program have the same control-flow. For BSreturn, we also check that the return values are the same and only update the mapping to model due to move instructions.

In order to get β i , we iterate the data-flow equations until a fixpoint using data-flow framework of COMPCERT.

2) Verification of Sufficient Conditions: If the computation of β i succeeds, the next step consists in verifying, for every observation point, IFP verification conditions. For a given observation point • i , we verify that for every LTL location l ∈ γ i that may be modified by the current function, there exists either a mapping to a RTL register t i.e., (l → t) ∈ β i or the location l is constant cst i (l) = v for some v = .

Theorem 3. Let p be a RTL program and p be a LTL program. Suppose that we have successfully constructed β i , γ i and cst i for every program point of p. If for every observation point • i , the following condition hold:

∀l ∈ γ i .(∃t.(l → t) ∈ β i ) ∨ (∃v.cst i (l) = v ∧ v = )
Then RA transformation of p to p is IFP.

Moreover, if every pair (l 1 , l 2 ) of distinct locations is mapped to distinct to distinct temporaries, the transformation prevents data duplication.

In the following section, we give some key insights on how the previous verification conditions are sufficient to ensure the existence of a simulation function α i and a backward simulation between p and p .

D. Correctness of the Validation Algorithm

We suppose an execution of p and p where memories m 1 and m 1 are respectively leaked from observation point • 1 and there exists α 1 such that m 1 ∼ α1 m 1 . Similarly we note • 2 the observation point leaking m 2 . It remains to prove that we can construct a backward simulation according to Definition 7.

Hence we need to prove two goals: the existence of m 2 and α 2 such that m 1 m 2 and m 2 ∼ α2 m 2 . 1) ∃m 2 , m 1 m 2 : By definition of , there is a derivation of length n such that m 1 → n m 2 . We have to show that there is a derivation of length n such that m 1 → n m 2 . Such a proof is also needed by the original COMPCERT semantics preservation proof of the RA pass [START_REF] Rideau | Validating register allocation and spilling[END_REF] and we therefore inherit it for free.

2) ∃α 2 , m 2 ∼ α2 m 2 : The construction of α 2 partitions addresses in the following three categories:

• addresses which are not part of LTL locations;

• LTL locations that have been modified by the current function; • and LTL locations that have not been modified. First of all for every address that are not locations in the LTL memory model. These memory slots are only accessible with load and store instructions. While building β 2 we check that these memory accesses always agree on the values computed and memory chunk that is addressed. Therefore in p and p these memory chunks remain the same and α 2 corresponds to the identity function for these addresses.

Then we tackle the where addresses are part of LTL locations. γ 2 is the set of locations which may have been modified since the beginning of the function being analysed. We study the case where the location l was not modified in the function, e.g., l / ∈ γ 2 . We know that when reaching • 1 the memories m 1 and m 1 were leaked and that m 1 ∼ α1 m 1 . Moreover locations and temporaries are local to their functions and observation points are placed before function calls and returns. From these facts we deduce that α 1 (l) still holds at • 2 and gives us ∀(l / ∈ γ 2 ), α 2 (l ) = α 1 (l ). In the last case where l ∈ γ 2 , we know from our precondition of Theorem 3 that we are able to map l to either a temporary or a constant. Thus α 2 is equal to β 2 or cst 2 for every location of γ 2 .

Lastly we need to prove that α 2 is injective. For addresses which are not locations, α 2 is the identity function which is injective. For addresses not in γ 2 this is given by the fact that by induction α 1 is also injective. For the other addresses we have the hypothesis that every location maps to distinct temporaries which proves that α 2 is injective.

E. Validating Dead Store Elimination (DSE)

DSE is an optimisation which replaces an assignment to RTL temporary tmp by nop when the compiler is able to show that the value of tmp will not be used by the rest of the computation. When such instructions have the security purpose of erasing sensitive values from memory, DSE is introducing information-flow leaks. A particularity of COMPCERT is that dead store elimination is not a separate pass but is performed during RA. The rationale is that a liveness analysis is needed to both detect dead store and construct the interference graph of RA algorithms. Therefore the validator of COMPCERT is capable of validating both RA and DSE. Similarly, we also adapt our IFP validator to handle DSE. For most cases, DSE will not be IFP. To cope with this situation, we refer to Section VI-F where we show how to patch the program on the fly to close potential information leaks. A typical case where removing a store is not IFP occurs when it happens right before an observation point.

The only transformation that may occur in DSE is to replace an assignment by a nop. To deal with this situation, our validator considers the additional block shapes and transfer functions of Figure 5. Those blocks are BSopdead and BSloaddead where the corresponding core instructions in LTL has become a nop. In both cases, after evaluating the move instructions, the transfer functions remove the mappings for the target RTL temporary tmp.

With these extensions our IFP validator is now able to check the COMPCERT transformation composed of register allocation and DSE.

F. Patching algorithm

An interesting property of our IFP validator is that we can recover from certain validation failures; track down the origin of the information leak and apply a patch to a function f to automatically close the information leak. When this is the case, it is possible to run existing optimisations unmodified, and during a post-treatment, detect and remove potential information leaks. Suppose that, for a given observation point • i , the verification conditions needed by Theorem 3 do not hold. Typically, there is a location l that is neither a constant (cst i = ) nor has a mapping to some RTL temporary (β i (l) = ∅). In this situation either the validator is not precise enough or l is responsible for an information leak. To close the potential leak detected by the IFP validator, our patching algorithm inserts an erasure instruction and sets the location to the constant 0 just before the observation point • i . After the addition of those erasure instructions, we have the guarantee that the transformed program is IFP. Moreover, those erasure instructions cannot compromise the correctness of the transformation. The rationale is that an erasure instruction for location l is necessarily a dead store. To see this, consider by contradiction that l is live. In that case, to establish semantics preservation, the original COMPCERT validator needs to establish a mapping for location l and a RTL temporary t. As our forward validator always computes more mappings than the original backward validator of COMPCERT, it would establish the same mapping. This contradicts our assumption.

As a result, we have the guarantee that inserting erasure instructions, according to the rules above, is a sound algorithm to make COMPCERT RA a semantic preserving IFP transformation.

VII. EXPERIMENTS

The translation validation algorithm of Section VI has been integrated as part of the register allocation pass of COMPCERT [START_REF] Leroy | Formal certification of a compiler back-end or: Programming a compiler with a proof assistant[END_REF]. We run our IFP validator; close any potential information leak using the patching algorithm of Section VI-F. Afterwards, we run the existing validator of COMPCERT, thus, ensuring the semantics correctness of our security transformation.

Block Shape

Conditions

Transfer Function BSopdead(s) : In our model, the attacker can only observe the memory at so-called observation points. As explain in Section VI, observation points are set at function boundaries: the attacker may observe memory just before call and return instructions. With this policy, our IFP validator enforces that register allocation does not introduce information leaks due, for instance, to stack allocated variables (or spilled registers) not being properly erased at function return; an acknowledged security issue [START_REF] Silva | The Correctness-Security Gap in Compiler Optimization[END_REF], [START_REF] Simon | What You Get is What You C: Controlling Side Effects in Mainstream C Compilers[END_REF], [START_REF] Yang | Dead Store Elimination (Still) Considered Harmful[END_REF].

A. Results and analysis

The experiments have been conducted on a quad-core Intel i7-6600U at 2.60GHz with 16GB of RAM running Fedora 27. We have tested our IFP validator on 24 programs which are all part of the COMPCERT test suite. For every program, our validator detected potential information leaks introduced by COMPCERT RA. All the information leaks have been successfully closed by our patching algorithm and all the resulting programs have passed the COMPCERT validator.

The impact of the security transformation on the size of the programs and their efficiency are summarised in Figure 6. The first bar represents the runtime overhead of our secured RA compared to the original RA of COMPCERT. The benchmarks have a running time ranging from 1 to 10 seconds and are sorted by increasing overhead that is obtained by averaging 50 runs. The second (grey) bar is the overhead on the size of the program incurred by the insertion of erasure instructions. The third (dark) bar represents the overhead in the number of executed instruction.

As shown in Figure 6, the increase in program size can be large and is above 20% for most of the benchmarks. Yet, this increase is not always reflected in the execution overhead because even when many erasure instructions are inserted, they may be rarely executed. Actually, for most functions, the increase of the number of executed instructions is negligible and for more than half of the programs the execution overhead is within a range of ±5%. We believe that speed ups are a lucky side-effect, probably due to an improved behaviour of the cache of instructions. Yet, there 4 benchmarks for which the execution overhead is above 10%. For chomp, the overhead peaks at 51% but is not quite correlated with the increase in executed instructions which is less than 15%. Another extreme phenomenon is the speedup of 17% of lists for which there is no obvious explanation and require further investigations. Anyway, these results are encouraging and show that an improved security can often be obtained without sacrificing too much efficiency. For a few benchmarks, the number of inserted instructions can be quite large. For instance, for programs like almabench or fftsp we notice a 40% increase in program size. A reason for this phenomenon is that our IFP validator needs to be quite conservative about the behaviour of function calls relying exclusively on guarantees given by calling conventions. This is illustrated by Example 3 where a potentially spurious instruction needs to be inserted to protect against a potential information leak.

Example 3. Consider the code snippet of Figure 7. According r : = g ( x ) ; x : = 2 ; r e t u r n x ; e a x : = g ( e d i ) ; e a x : = 2 ; r e t u r n ; to standard x86 calling conventions, it is typically compiled as the LTL program of Figure 7. After the call of g, we only have the guarantee that registers are either overwritten or carry the same value as before. Therefore, our validator makes the conservative assumption that edi (that is not callee-saved) was not modified by g, may leak the initial value of the variable x and therefore needs to be explicitly erased, thus adding a potential spurious erasure instruction edi := 0.

As programs like almabench or fftsp are using a significant number of distinct registers, the patching algorithm introduces for each of them an erasing instruction for each call site.

B. Discussion

The validator is also verifying whether register allocation satisfies the absence of data duplication. This property is unfortunately currently violated and cannot be easily fixed because of constraints imposed by existing calling conventions. More precisely, calling conventions stipulate that arguments are copied into specific registers. Moreover, as arguments are not callee-saved, erasing the original register would be unsound and, therefore, this duplication is inevitable. At the price of breaking compatibility with existing code, a solution would be to adapt the calling-conventions so that arguments are callee-saved. Other sources of duplication are between a register and a spilled stack slot. In this case, either the register or the stack slot is dead and could be erased. The patching algorithm would have to be enhanced with a liveness analysis in order to perform this reasoning and erase the dead location.

Reducing the number of erasure instructions would require to give the validator additional information about the registers that are either preserved or erased by function calls. For functions in the same compilation unit, this could be done using standard static analyses computing unmodified registers or constant registers. Library calls are more problematic. A possibility would be to require extended calling conventions stipulating which registers are preserved (beyond callee-saved) or erased. However, if the client code is optimised for these extended calling conventions, it would only be secure if linked against this specific version of the library.

VIII. SECURING OTHER COMPILER PASSES

In their paper, D'Silva et al. [START_REF] Silva | The Correctness-Security Gap in Compiler Optimization[END_REF] mention that compiler passes such as Code Motion an Inlining, because they modify the lifetime of variables, may introduce information leaks. In the following, we explain how these transformations fit with our IFP property.

A. Inlining

In our experiments, observation points are attached to function calls. As inlining consists in replacing a function call by a function body, if has the effect of removing an observation point. As observations need to be synchronised, inlining breaks this property and therefore is simply not an IFP transformation. As this may seem overly restrictive, a first solution to accommodate some inlining would be to weaken the security policy and attach observation points only to security critical functions. As a result, those critical functions would not be inlined but other functions could be freely inlined without modifying observation points. In this restricted scenario, inlining would be an IFP transformation. Another tempting approach would be to detach the observation point from the function call. Yet, this raises the issue of code motion that we discuss below.

B. Code motion

The risk of code motion is that code, and therefore information, could move around observation points and thus modify the security policy. Consider for instance, the code of Figure 8 where observation points are detached from function calls and the code is subject to code motion. In this example, both erasure instructions and observation points have been delayed and moved at the end of the program. The result is that the transformation is formally IFP but defeats the intention of the security policy. It follows that a IFP-aware compiler needs to limit code motion within the bounds of observation points.

IX. RELATED WORK

The correctness-security gap was pinpointed by D'Silva et al. [START_REF] Silva | The Correctness-Security Gap in Compiler Optimization[END_REF]. In that work, dead-store elimination is identified as a program transformation that can cause security issues. Deng and Namjoshi [START_REF] Deng | Securing a Compiler Transformation[END_REF]- [START_REF]Securing a compiler transformation[END_REF] introduce an information flow notion of leaky triple and ensure that an adaptation of the standard DSE transformation [START_REF]Securing a compiler transformation[END_REF] and SSA transform [START_REF]Securing the SSA transform[END_REF] preserves this notion of information flow. Leaky triples do not capture the amount of information that is leaked. As a consequence, they ensure that a non-interferent program is transformed into another non-interferent program but a leaky program may be transformed into a more leaky program without violating their property. Because our IFP property is based on the notion of partial attacker knowledge, it will rule out this possibility and ensure that the transformed program is no more leaky.

Chong and Myers [START_REF] Chong | Language-Based Information Erasure[END_REF] propose semantics foundations for defining erasure policies. A main insight behind that work is that erasure can be seen as the dual of declassification [START_REF] Sabelfeld | Declassification: Dimensions and principles[END_REF]. Later on, Chong and Myers [START_REF]End-to-End Enforcement of Erasure and Declassification[END_REF], but also Hunt and Sands [START_REF] Hunt | Just Forget It: The Semantics and Enforcement of Information Erasure[END_REF], propose type-systems for verifying erasure policies of the source code. Askarov et al. [START_REF] Askarov | Cryptographic Enforcement of Language-Based Information Erasure[END_REF] enforce the erasure policies in the presence of so-called write-once locations which cannot be overwritten. The key insight is to store encrypted data in write-once locations and simulate erasure by the erasure of the cryptographic key. In our work, we do not consider erasure policies but ensure that program transformations do not introduce information leaks. We believe that our IFP definition has the potential to preserve such rich erasure policies. A difficulty is to specify the observation points relevant to the source property and make sure that they are preserved across compiler passes. An attacker observing all the intermediate memory states would probably suffice but may preclude too many transformations.

Yang et al. [START_REF] Yang | Dead Store Elimination (Still) Considered Harmful[END_REF] provides a list of techniques used by developers to prevent compilers from removing securitysensitive dead-store instructions. They present a secure deadstore elimination transformation that has been implemented for LLVM. This transformation verifies our IFP property. Simon, Chisnall and Anderson [START_REF]What you get is what you C: controlling side effects in mainstream C compilers[END_REF] investigate how compilers may break the security of cryptographic code because it is impossible to control side-effects of compiler optimizations. They propose compiler support for constant-time selection and for the secure erasure of secrets, which improves the security of the generated code.

Besson et al. [START_REF] Besson | Securing Compilation Against Memory Probing[END_REF] pursue a goal similar to ours, i.e., preserving information flow under program optimisations. The attacker in [START_REF] Besson | Securing Compilation Against Memory Probing[END_REF] is weaker because the attacker can only observe memory at the end of the execution. By basing our attacker model on traces of observations, we obtain a model that is more realistic and closer to the intuitive notion of an attacker that probes memory at specific moments during execution. From a formal point of view, the move to a trace-based model is necessary to analyse the security of intra-procedural optimisations. In addition, we show how it is possible to combine identification and patching of leaky transformations with a solution to the problem of identifying leaks due to the duplication of data. Finally, contrary to [START_REF] Besson | Securing Compilation Against Memory Probing[END_REF], we have experimentally validated our technique by analysing and enforcing information preservation properties of passes of a realistic compiler, the CompCert C compiler.

Barthe et al. [START_REF] Barthe | Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time[END_REF] propose a general framework for reasoning about the preservation of information leakage. Their approach is based on an instrumented semantics which explicitly leaks information to the attacker and which is used for deriving reasoning principles based on so-called 2-simulations. Our attacker model is stronger. As the attacker may perform arbitrary observations of memory, we quantify over the set of all leakage functions. Moreover, our reasoning principle is simpler and is sufficient to validate most transformations. Yet, it also has limitations and 2-simulations are more flexible when some leaked information of the source is gradually leaked in the target program.

X. CONCLUSION

We present a notion of Information-Flow Preservation ensuring that an attacker observing n bits of information during the run of a target program does not get an advantage over an attacker observing the same amount of bits of the source program. This is a strong property which is not tailored to a specific model of leakage but ensures that a compiler does not introduce any kind of information-flow leaks. We show that it is possible to adapt classic aggressive optimisations to this setting by inserting automatically erasing instructions before observation points. This approach has the advantage that the existing compiler code can be reused mostly unchanged. Our information-flow preservation property may prevent the spatial duplication of information using an injection between the observations of the target and source attackers. As future work, we will investigate how to characterise in the same framework both spatial and temporal duplication of data, thus modelling the lifetime of data as temporal duplication. The notion of injection is unfit for this purpose and would need to be generalised to allow up-to k duplications of the same data during the program execution. We also intend to push our security property to its limit and model an attacker observing memory at any time. Though the opportunities for optimisations will most probably be greatly reduced, we are nonetheless confident that programs can still be compiled in a reasonable manner under this stringent requirement, at the cost of some budget for temporal duplication of data.

Fig. 1 .

 1 Fig. 1. Example of compiled programs

f : • 1 Fig. 2 .

 12 Fig. 2. Safe Erasure of One-Time Pad

Definition 6 .

 6 Let α i : Address → Address + Bit be a simulation function indexed by i ∈ [1, . . . , n]. A source memory m is simulated by a target memory m (written m ∼ α m ) iff we have m.sid = m .tid and

Fig. 3 .

 3 Fig. 3. Original program (left) After register allocation (right)

Fig. 4 .

 4 Fig. 4. Transfer functions for β i

Fig. 5 .

 5 Fig. 5. Additional transfer functions for DSE

Fig. 6 .

 6 Fig. 6. Patched programs compared to original compared programs

Fig. 7 .

 7 Fig. 7. RTL program (left), LTL program (right)

Fig. 8 .

 8 Fig. 8. Code motion and detached observation points

  From the initial memory c, the first source memory m and target memory m leaked to the attacker are in relation (m ∼ α m ).2) Given memories m 1 ∼ α m 1 , for every attacker step of the target program m 1 m 2 there exists a memory m 2 in the source program such that m 1 m 2 and m 2 ∼ α m 2 .

	Theorem 2. Suppose two programs p and p and a simulation
	function α. If there is a backward simulation (according to
	Definition 7) for α, then the pre-condition of Theorem 1 holds
	i.e.,
	∀c, t, t .

Definition 7 (Backward Simulation). A simulation function α i : Address → Address + Bit is a backward simulation if: 1)

  4-6. The Function cipher ' contains additional spilling/loading instructions inserted by RA Lines 4,5 and 7. In Function cipher the secret value in key is overwritten Line 8, hence an attacker at • cannot observe its value. However in Function cipher ', the value of key in stored in register r2 and copied in variable key' (seeLine 4). As the variable key' is never erased, an attacker at • can observe its value. Hence this transformation is not IFP and will be rejected by our validation algorithm. In COMPCERT, the RA pass compiles a source in the Register Transfer Language (RTL) into a target in the Location Transfer Language (LTL). RTL and LTL are both fairly classic control-flow graph program representations where nodes are labelled with threeaddress code instructions.Instructions representative of RTL are given below.Each instruction i ∈ I, attached to a node n ∈ N, specifies its immediate successor s which is the node of the instruction to execute next. The nop instruction does nothing. The op instruction computes the value of the variable dest using the values stored in the vector of pseudo-registers args. The load instruction moves the value at the address computed by args with the addressing mode addr to the destination dest. Similarly store move the value from src to the address computed by args and addr. The call instruction calls the function fid with signature sig with parameters args; the result

	I i ::= nop(s)
	|	op(op, args, dest, s)
	|	load(addr, args, dest, s)
	|	store(addr, args, src, s)
	|	cond(cond, args, s true , s f alse )
	|	call(sig, f id, args, dest, s)
	|	return(arg)

B. Register Allocation in CompCert

1) Register Allocation Languages: of the call is stored in dest. The instruction cond models a conditional and has two successors. Depending on the value of arg, the instruction to execute next is either s true of s f alse . Finally, return exits the current function and return the value of arg.


Ahmad F Adel
email: ahmad.fadel@irisa.fr

Ahmad N Imr
email: ahmad.nimr@ifn.et.tu-dresden.de

Hsiao -Lan Chiang
email: hsiao-lan.chiang@ifn.et.tu-dresden.de

M Arwa Chaf Ii
email: marwa.chafii@ensea.fr

Bernard Cousin
email: bernard.cousin@irisa.fr

Cross-Layer Multi-User Selection in 5G Heterogeneous Networks Based on Hybrid Beamforming Optimization for Millimeter-Wave

Keywords: Cross-layer, user selection, 5G heterogeneous network, beamforming, millimeter waves, orthogonal steering vector

Lack of coordination between network layers limits the performance of most proposed solution for new challenges posed by wireless networks. To overcome such limitations, cross-layer physical and medium access (PHY-MAC) design for multi-input-multi-output orthogonal frequency division multiple access system in heterogeneous networks (HetNETs) is proposed. In this paper, we formulate an optimization problem for hybrid beamforming, in a multi-user HetNET scenario aiming to maximize the total system throughput. Furthermore, analog beamforming is selected from a codebook containing a limited number of candidates for steering vectors. The proposed problem is non-convex and hard to solve. Thus it is relaxed by transforming it into a subtraction form of two convex funcions. Afterward we apply a group of well-known metaheuristic algorithms to calculate the normalized hybrid beamforming vectors. The optimal solution is obtained using an exhaustive search (ES) algorithm that provides an ideal solution, but with high complexity. In addition, zero-forcing-based approach (ZFA), matched filter (MF), and QR-based approach (QR) are applied to get quick sub-optimal solutions. Hence, we analyze the performance of our systems using the throughput metric. The simulation results show that QR algorithm outperforms ZFA and MF in low and middle signal-tonoise ratio (SNR) regime, while ZFA outperforms QR and MF at higher SNRs. Moreover, QR is close to the optimal solution ES.

I. INTRODUCTION

One of the main 5th generation (5G) requirements is to support 1000 times larger capacity per area compared with current Long Term Evolution (LTE) technology, but with similar cost and energy dissipation per area as today's cellular systems. In addition, an increase in capacity will be possible if all the three factors that jointly contribute to system capacity are increased; 1) more spectrum using millimeter waves (mmWaves) spectrum band, 2) a large number of base stations per area by mean of densification, and 3) an increased spectral efficiency per cell [START_REF] Fallgren | Scenarios, requirements and kpis for 5g mobile and wireless system[END_REF]. Massive multi-inputmulti-output (MIMO) systems are considered essential in contributing to the latter factor, as they promise to provide a highly increased spectral efficiency per cell. Indeed, it takes advantage of the spatial degrees of freedom (DoF) that provide spatial multiplexing that inherently inherently minimize intra-cell and inter-cell interferences [START_REF] Marzetta | Noncooperative cellular wireless with unlimited numbers of base station antennas[END_REF]. Obviously, this can be achieved by applying the hybrid beamforming technique knowing that the system operates at mmWaves frequency bands. Thus, the gain realized through antenna beamforming can compensate for the high path at mmWaves frequencies. Accordingly, a combination of analog beamforming (operating in passband) and digital beamforming (operating in baseband) can be one of the low-cost solutions [START_REF] Chiang | Hybrid beamforming based on implicit channel state information for millimeter wave links[END_REF]. This is because using only digital beamforming requires more radio frequency (RF) chains, which leads to high implementation cost and power consumption. An effective beam finding mechanism is important in mmWaves communications. Accordingly, generating a codebook that is composed of limited steering angles and steering vectors could incarnate numerically the physical beams. It was reported in [START_REF] Chiang | Analyses of orthogonal and non-orthogonal steering vectors at millimeter wave systems[END_REF] that using orthogonal steering vectors provide higher data rates, because the spatial frequencies of the given angle-of-arrivals (AoAs) and the orthogonal steering angles have nearly the same distribution.

In a traditional network, the optimization is usually carried out considering a respective layer objectives based on only local information ignoring other layers' design parameters or information. This fact gives a locally optimal, but globally suboptimal solution. Crosslayer design refers to sharing information among layers for efficient use of network resources and achieving high adaptivity. This motivates us to formulate an optimization problem for a cross-layer design, having the hybrid beamforming as an optimization variable, knowing that the physical layer (PHY) is responsible for signaling and channel estimation, whereas medium access layer (MAC) is responsible for resource allocation and multiuser selection.

In the literature, the authors in [START_REF] Han | Large-scale antenna systems with hybrid analog and digital beamforming for millimeter wave 5g[END_REF] focused on optimal analog and digital beamforming designs in a multi-user beamforming scenario to study the impact of energy efficiency on spectrum efficiency, and they showed that hybrid beamforming achieves better channel estimation performance than the method solely based on analog beamforming. But they address only PHY layer to avoid complexity when dealing with a cross-layer design. The authors in [START_REF] Zamani | Beamforming optimization with hybrid association in c-rans under a limited backhaul[END_REF], [START_REF] Dimic | On downlink beamforming with greedy user selection: performance analysis and a simple new algorithm[END_REF], formulated an optimization problem to determine the hybrid beamforming in the downlink (DL) scenario, having a backhaul and a power constraint. Their formulation actually aims to maximize the throughput. But, the optimal solution was the standard zero-forcing technique without having any normalization which leads to an increase in power and resulting in a non-accurate outcome. In our previous work [START_REF] Chiang | Hybrid beamforming based on implicit channel state information for millimeter wave links[END_REF], we have only investigated PHY hybrid beamforming optimization which has been based on an implicit channel state of information for mmWaves links. Zero forcing ZFS, and QR-decomposition algorithms were applied in a single cell multi-user selection while using statistical channel model where path loss is normalized and the study is based on the 3rd technology of wireless communication networks.

In this paper, we address the issue of cross-layer in a heterogeneous network, where the PHY and MAC knowledge of the wireless medium is shared, to provide a hybrid beamforming optimization for a multi-user scenario. In order to meet the overwhelming demands of network throughput for a practically important case wherein the number of users, N u is larger than the number of transmit antennas N t , as we propose to select Q users among N u to attribute for them the resources. Our contributions are six-folds: i) Generate a new system model to support cross-layer design for multi-user selection, markedly it consists of both analog and digital beamforming at the transmission side. ii) Formulate an optimization problem for a cross-layer design, having the hybrid beamforming as an optimization variable. Indeed, the heterogeneous cellular network is based on two different technologies (4th generation (4G) and 5G), and the purpose of our formulation is maximizing the system throughput; iii) Transform the optimization problem in order to relax the non-convexity by applying the difference-of-convex functions (DC) programming [START_REF] Zhang | Joint design of multi-tap filters and power control for fbmc/oqam based two-way decodeand-forward relaying systems in highly frequency selective channels[END_REF]; iv) Compute the optimal solution by applying the ES algorithm that will be considered as the ideal solution, and has been proposed in our previous work [START_REF] Fadel | User selection in 5g heterogeneous networks based on millimeter-wave and beamforming[END_REF]; v) Propose a sub-optimal solution to reduce the complexity and produce solutions close to the optimal one; vi) Assess the performance of zero-forcing-based approach (ZFA), QR-based approach (QR) [START_REF] Dimic | On downlink beamforming with greedy user selection: performance analysis and a simple new algorithm[END_REF] and matched filter (MF) approach compared to that of exhaustive search (ES), versus throughput evaluation metric.

The rest of the paper is organized as follows: Section II outlines the proposed system and channel models. In Section III we formulate hybrid beamforming with a fixed analog beamforming optimization. Section IV describes the optimal and reduced-complexity algorithms. Furthermore, Section V provides a simulation-based comparison of the system throughput performance for ES, ZFA, QR and MF algorithms with respect to SNR and number of users. Conclusions and future work are mentioned in Section VI.

II. HETNET MULTI USER MIMO-OFDMA NETWORK MODEL

A. Heterogeneous Network Model

In a heterogeneous multi-user MIMO-OFDMA network, we assume to have M macrocells overlaid by P picocells with a N u user equipment (UEs) distributed overall the system area as depicted in Fig. 1. Indeed Q ≤ N u (UEs) will be selected to be served. Each base station (BS) is equipped with N t transmit antennas, and each UE with N r = 1 receive antenna.

One of the most attracted characteristics in MIMO systems is the spatial multiplexing, literally because each BS can serve up to Nt Nr UEs simultaneously for each radio ressource unit. The intra-cell interference is roughly negligible, due to the fact of associating the 4G frequency spectrum to the macrocell, while associating the mmWaves that fall in the spectrum range of 5G to picocells. Moreover, picocells are far enough from each other in order not to affect each other by any kind of interference. Thanks to fiber optic backhaul links, macro and pico BSs are connected to a centralized control unit. We assume that the wireless channel operates in time-division-multiplexing (TDD) system that relies on reciprocity, by which the uplink channel is used as an estimate of the downlink channel, and this occurs when receiving a pilot training sequence from terminal devices toward the base station where channel state information (CSI) is obtained.

B. MULTI USER MIMO-OFDMA System Model

In this subsection we consider only one BS with N t transmit antennas employing orthogonal frequency division multiplexing (OFDM) system. By means of digital beamforming (DBF) and analog beamforming (ABF), Q ≤ N t users can be simultaneously served with the same time and frequency resources. Following the multiuser (MU)-MIMO scheme as illustrated in Fig. 2

, let s[k] = [s 1 [k], • • • , s Q [k]]
T ∈ C Q×1 be the data symbol vector transmitted on the k-th subcarrier. The user data are precoded with a DBF matrix

W D [k] ∈ C Q×NRF , such that s d [k] = WD[k]s[k] ∈ C N RF ×1 (1)
which is a precoded data vector. The precoded data are transformed to the time domain with inverse discrete Fourier transform (IDFT) transform and passed to N RF RF chains, to generate the analog signal vector s d (t) ∈ C NRF×1 . After ABF with a matrix W A ∈ C NRF×Nt , the transmitted signal vector is given by

x(t) = WAsa(t) ∈ C Nt×1 . (2)
assuming that a cyclic prefix (CP) of sufficient length is inserted, and let H(t) ∈ C Nt×Q be the MU-MIMO channel states between each pair of N t transmitter antennas and each Q users. The received signal y q (t) of the q-th user can be expressed with the circular convolution

yq(t) = Nt n t =1 [H(t)] (q,n t ) [x(t)] (n t ) + vq(t), (3)
where v q (t) is the additive white Gaussian noise (AWGN). After the sampling of y q (t) and performing N -discrete Fourier transform (DFT), the circular convolution is translated to element-wise product with the channel coefficients in the frequency domain, which are defined by the channel matrix H[k] ∈ C Nt×Q . Thus, we get the signal

yq[n] = Nt n t =1 H[k] (q,n t ) [ x[k]] (n t ) + ṽq[k], (4)
where

x[k] = W A W D [k]s[k]
is the consequence of ( 1) and ( 2). The effective channel that can be regarded as a coupling of the channel having analog beamforming gain on both sides is defined by

H (e) = HWA ∈ C Q×N RF , (5)
assuming that the ABF is fixed during at least one OFDM symbol. The corresponding multiple-input single-output (MISO) channel of the q-th user is defined by

h H q [k] = H (e)
(q,:)

∈ C 1×Nt (6) then, yq[k] = h H q [n]WD[k]s[k] + ṽq[k]. (7)
The goal is to find the DBF matrix that maximizes the sum rate for the k-th subcarrier. First, we define the normalized DBF matrix

W [k] = [w 1 , • • • w Q ] ∈ C Nt×Q , w 2 = 1 as WD[k] = W [k]Λ[k], (8)
with Λ[k] ∈ C Q×Q is a diagonal matrix that defines the power allocation such that

[Λ[k]] (q,q) = [WD[k]] (:,q) = Pq[k]. (9)
From now on, the subcarrier index k is dropped for the simplicity of notation. In order to compute W D , first we need to find the unit-norm vectors {w q } in addition to P q . We assume that the data samples are uncorrelated with power E s , and the power constraint Q q=1 P q = Q must be fulfilled. The received signal model can be rewritten as

yq = Pqh H q wqsq + i =q √ Pih H q wisi IUI +ṽq. (10)

C. Channel Model

We considered a heterogeneous network, and the proposed system model is applied for each macro and picocell. Let h nq ∈ C 1×Nt be the channel vector between the (m, p)-th BS and the q-th user equipment (UE) of the (m , p )-th cell in the k-th resource unit.Here the shorthand notation n = (m, p) is used for simplicity. Where m and p are the indices of the distributed cells in the network, knowing that m ∈ {1, . . . , M } and p ∈ {0, . . . , P }, for clarification p = 0 corresponds to the BS macrocell. Then, the received signal at the q-th UE of the (m , p )-th cell in the k-th resource unit, y nq , is given by

y nq (k)= P nq (k)h(k) H nq (k)w nq (k)s nq (k) + i =q P ni (k)h H nq (k)w ni (k)s ni (k) IUI +ṽ nq (k), (11)
∀ n = (m, p)withm ∈ [1 . . . M ] andp ∈ [0 . . . P ] Moreover, h nq (k) = l nq (k)g nq (k) hnq (k)
, where l nq (k), g nq (k), denotes the path loss and shadowing, respectively. The channel is modelized using Rapapport model [START_REF] Akdeniz | Millimeter wave channel modeling and cellular capacity evaluation[END_REF], which take into account path loss and shadowing. hnq [k] is the small scale fading coefficients, which can be generated using the statistical channel model [START_REF] Alkhateeb | Limited feedback hybrid precoding for multi-user millimeter wave systems[END_REF]. In addition, ṽnq ∼ N (0, σ 2 nq ) is the AWGN noise and I nq (k) is inter-user interference (IUI).

III. PROBLEM FORMULATION

We formulate an optimization problem for a heterogeneous network, aiming to optimize hybrid beamforming techniques. We have used the mmWaves propagation characteristic for picocells to maximize the total average system throughput, due to the large frequency spectrum range.

A. System Performance Evaluation Metric

We consider the system throughput as the performance metric in this paper. The instantaneous channel throughput R nq (k) for the q-th user of the n-th cell in the k-th resource unit is given by

R nq (k) = B w log 2 (1 + SIN R nq ), ∀n = (m, p) with m ∈ [1 . . . M ] and p ∈ [0 . . . P ] (12)
where B w is the channel bandwidth, and SINR nq denotes the signal-to-interference-plus-noise ratio (SINR) for the q-th user, which is given by:

SINR nq = E s P nq w H nq h nq h H nq w nq i =q E s P i w H ni h nq h H nq w ni + σ 2 nq , (13)
The average system throughput, V in bit/s/Hz/BS is defined by

V({wnq}, {Pnq}) = 1 M * (P + 1) M m=1 P p=0 q∈Qn K k=1 Rnq(k) (14)
where {w nq } and {P nq } refer to the set of unit-norm vector of the digital beamforming matrix and power allocation of the served users, respectively. The number of served users in the n-th macro and pico BS is denoted as Q n ∀n = (m, p).

B. DBF Optimization Problem

After Q n the users in the n-th cell are selected, the DBF needs to be optimized. Because the logarithm function in ( 12) is an increasing function, then maximizing R nq , q = 1, • • • , Q n is equivalent to maximizing SINR qn . Therefore, the DBF optimization problem can be written as: max SINRq ({wq, Pq})

s.t. wq = 1, Q q=1 Pq ≤ Q, Pq > 0, q = 1, • • • , Q. ( 15
)
Note that, the index n is dropped for simplicity. For a given {w q } the problem turns to finding {P q }, i.e. solving a power allocation problem.

C. Power Allocation Problem

Let Ω q,i = w H i h H q h q w i , and p ∈ Q×1 , where

[p] (q) = P q . Then R(p) = Q q=1 log 2   1 + EsPqΩq,q i =q [EsPiΩq,i] + σ 2 q    = Q q=1 log 2      1 + Es σ 2 Q q=1 PiΩq,i 1 + Es σ 2 i =q PiΩq,i      = Q q=1 log 2 1 + a T q p 1 + b T q p (16)
where ,

[aq] (i) = Ωq,i, i = 1 • • • Q [bq] (i) = Ωq,i, i = 1 • • • Q, i = q. (17)
Thus, the sum rate maximization can be written as

max p R S.t. R ≤ Q q=1 log 2 1 + a T q p 1 + b T q p , Pq > 0, Q q=1 Pq = Q. ( 18
)
This problem is a difference between two convex functions. First, the problem is reformulated as

max p R, S.t. R ≤ Q q=1 log 2 1 + a T q p -t, Q q=1 log 2 1 + b T q p ≤ t, Pq > 0, Q q=1 Pq ≤ Q, (19)
Using the linear approximation to convert the second constraint, then we get the convex problem

max p R, S.t. R ≤ Q q=1 log 2 1 + a T q p -t, Q q=1 log 2 1 + b T q p0 + b T q 1 + b T q p0 [p -p0] ≤ t, Pq > 0, Q q=1 Pq ≤ Q. ( 20
)
This problem can be solved iteratively; first we set the initial power allocation p 0 to a uniform allocation, and this vector is updated after each iteration. The algorithm stops when |R i+1 -R i | < R i , where defines the change threshold.

IV. OPTIMAL AND LOW-COMPLEXITY ALGORITHMS

In this section, we present the analog beamforming selection phase, and we apply the four algorithms ES, ZFA, MF, and QR that take into consideration the same constraints and objective of the optimization problem. Accordingly, the distributed power between users should be less or equal the maximum power in each BS. The number of users Q that share the same resource unit k should not exceed the number of transmitted antenna N t installed on a BS.

A. Analog Beamforming Selection

A codebook based beamforming training procedure can balance the trade off between complexity and high performance. The N RF analog beamforming vectors of W A in Fig. 2 are selected from a predefined orthogonal codebook F = { fn f ∈ C Nt×1 , n f = 1, . . . , N F } with the n th f member given by [START_REF] Niu | A survey of millimeter wave (mmwave) communications for 5g: opportunities and challenges[END_REF] f

n f = 1 √ N t [1, e j2π λ 0 sin(φn f ) d , . . . , e j2π λ 0 sin(φn f )(Nt-1) d ] T
(21) where φ n f stands for the n th f candidate of the steering angles at the transmitter, d = λ0

2 is the distance between two neighboring antennas, and λ 0 refers to the wavelength for a specific carrier frequency.

1) Initial analog beam selection: This step is achieved by transmitting known pilot signals, and at the receiver they will include the effect of analog beamforming, then an observation used for the analog beam selection at subcarrier k for a specific beam fn f can be acquired by correlating the k th received pilot with its transmitted signal [START_REF] Chiang | Hybrid beamforming based on implicit channel state information for millimeter wave links[END_REF] as shown in the following equation

y n f [k] = fn f H[k] (e) + AW GN (22)
The idea from using the beamforming technique is to achieve the maximal signal-to-noise ratio (SNR) [START_REF] Yang | Dft-based beamforming weight-vector codebook design for spatially correlated channels in the unitary precoding aided multiuser downlink[END_REF],

and due to the assumption that the noise is signalindependent, the steering vector index can be selected individually and sequentially according to the sorted received energy estimates f = arg max

fn f ∈F \F K-1 k=0 | y n f [k] | 2 (23)
having F , is a cumulative set where the selected steering vectors are stored.

2) Steering angles selection: Having a limited codebook size, the way of designing the steering angles has a consequence effect on the beamforming performance, to compensate for the angles of arrival and departure (AoAs/AoDs). Therefore the steering angles are selected uniformly between the range (-π 2 , π 2 ).

B. Exhausitve Search Algorithm using Standard Zeroforcing

One of the most important targets of telecommunication operators in the next generation of cellular networks is to maximize the system throughput. To put it another way, higher throughput means replying quickly to user demands, thus it achieves their satisfaction.

The objective of the optimization problem is to optimize a hybrid beamforming for a selected Q ≤ N t users and respecting all the aforementioned constraints in a way to maximize the system throughput, while using hybrid beamforming (fixed analog and ZF for digital). It is important to realize that, getting the optimal solution by applying the exhaustive search algorithm, would be ideal to achieve the goal. Precisely, this algorithm checks all the possible combinations in a way to get the optimal solution by selecting a set of users that achieve the maximum total throughput, but it may have a severe drawback, the computational cost of ES may introduce a very long delay when the combinatorics of the problem is high.

In Algorithm 1, we propose to select q ∈ Q from N u users, by trying all the possible combinations to achieve the maximum total throughput. Power is uniformly distributed among the selected users.

C. Normalized beamforming vectors

Getting this optimal solution is of high complexity. Thus, computing normalized beamforming vectors to solve the hybrid beamforming optimization problem sounds a good solution. Accordingly, three cases of {w q } are to be compared.

1) Zero-Forcing based approach: In this approach, the interference is canceled such that H (e) WD = IQ thus, WD = H (e)H H (e) H (e)H -1

.

(24)

The normalized vector is given by wq =

[WD] (:,q)

[WD] (:,q) , SINRq = EsPqw H q hqh H q wq σ 2 q . (25) Algorithm 1 Exhaustive search [START_REF] Fadel | User selection in 5g heterogeneous networks based on millimeter-wave and beamforming[END_REF] Input: N u , N t , P max Output: The set S r 1: while Q ∈ C Nt Nu do

2:

Compute ∀q ∈ Q, p q = Pmax Nu 3:

Compute ∀q ∈ Q, H (e) = HW A Effective channel 4:

∀q ∈ Q, w q = H * (HH * ) -1 ZF-beamforming 5:

∀q ∈ Q, SIN R(q) (13) 6:
R(c) = ∀q∈Q R(q) (12)

7:

if R(S r ) < R(Q) then 8:

Let S r = Q 9:
end if 10: end while As a result, the sum rate optimization problem is reduced to water filling. The normalization preserves the power constraint, unlike the standard zero-forcing (ZF) approach, which may lead to the increase of the total power.

2) Matched filter: In this approach, the nominator of SNR q is maximized, such that w q = hq hq However, the interference can be sever, and it is simple in implementation knowing that it is useful for low SNR regime.

3) Compromised interference QR approach: In this approach, first we sort the users according to the maximum h H q h q . Then, we compute w q as follows: the solution for q = 1 is given by w 1 = h1 h1 . The solution for q > 1 is achieved by solving max w H q h q h H q w q S.t. w q = 1, h H 1 w q = 0, • • • , h H q-1 w q = 0.

(26)

Therefore, we reduce the interference from the later users. Actually, the optimal solution can be written as H (e) W = T , where T ∈ C Q×Q is lower triangular matrix. By computing the QR decomposition of H (e)H under the assumption that N t ≥ Q such that maH (e)H = QR ∈ C Nt×Q , where R ∈ C Q×Q is an upper triangular matrix, and

Q ∈ C Nt×Q is orthogonal matrix, Q H Q = I Q , thus, H (e) W = R H Q H W = T . (27)
By choosing W = Q, we get T = R H . Thereby,

SINRq = EsPqw H q hqh H q wq q-1 i=1 EsPiw H i hqh H q wi + σ 2 q . (28)

V. EVALUTION AND PERFORMANCE ANALYSIS

In this section, we evaluate the performance of ZFA, QR and that of MF. Afterward, we compare the proposed algorithms with the optimal one, the exhaustive search, via Monte-Carlos simulations. Hence we average the total system throughput over 100 random channel realizations. All base stations are assumed to transmit with identical power when using the exhaustive algorithm. The simulation parameters are taken from our previous work [START_REF] Fadel | User selection in 5g heterogeneous networks based on millimeter-wave and beamforming[END_REF]. Figure 3 depicts the total system throughput for ZFA, QR and MF to be compared with the optimal solution ES. As shown in the low SNR regime from 0 to 5 dB, QR outperforms MF and ZFA due to high noise. Then, in middle SNR regime from 5 to 10 dB, we can detect that QR still outperforms but with remarkable progress for ZFA where the latter preceeds MF. For high SNR regime from 10 to 20 dB, it can be seen that QR still outperforms MF but ZFA preceeds the proposed QR solution. We could say that QR is a good solution for low and middle SNR range, while ZFA is more suitable for high SNR. System Spectral Efficiency (bit/s/Hz) Figure 4 we show the average system spectral efficiency in bit/s/Hz for both macro and picocells, aiming to clear out the importance of using mmWaves links in increasing the system throughput. TShe bandwidth used for macrocell is B w = 180kHz and that of picocells is B w = 800M Hz. As illustrated in Figure 4, the spectral efficiency of picocells by applying ZFA, QR and MF is roughly high x gigabit/s/Hz comparing to that of the macrocell x megabit/s/Hz. This due to the huge bandwidth proposed by mmWaves spectrum band. We can conclude that the concept of densification and heterogeneous network plays a role in maximizing the total system throughput and spectral efficiency. Because it gives the opportunity for users located at the border of the cell to be served and at the same time to reply to their requests. Execution time is an important factor to be taken into consideration. Regarding Figure 5, execution time of QR does not exceed 5 s when N u = 40 users, while ZFA needs four more time for the same number of users. But regarding the ES algorithm, its curve increases exponentially and tends toward infinity as the number of users increases. To interpret this result, we can see that QR outperforms ZFA and ES using the criterion of time, and it gives an acceptable throughput in low and middle SNR regime compared to optimal thus it could be considered as a trade-off algorithm between ZFA and ES.

A. Total System Throughput versus SNR

B. Average System Spectral Efficiency for Macro and Pico Cells versus SNR

C. System Execution Time

VI. CONCLUSION

In this paper, we have formulated an optimization problem for a cross-layer design to optimize the hybrid beamforming. Notably, we have generated a new system model that supports the proposed scenario. The problem aims to maximize the total throughput for downlink multi-input-multi-output and orthogonal frequencydivision multiple access system, for 5G heterogeneous networks (HetNETs). We have proposed different metaheuristic algorithms to calculate the normalized beamforming vector, as we have applied the exhaustive search algorithm to get the optimal solution. Numerical results revealed that QR algorithm outperforms ZFA and MF in low and middle SNR regime while ZFA outperforms QR and MF as it provides higher system throughput. It is worth mentioning that QR outperforms ZFA, MF, and ES where it needs less execution time. As a conclusion, QR could be considered as a trade-off algorithm between ZFA and ES.

Figure 1 .

 1 Figure 1. Heterogeneous network with MIMO base stations.

Figure 2 .

 2 Figure 2. Multi-user System Model with Analogue and Digital Beamforming.

Figure 3 .

 3 Figure 3. Total system throughput versus SNR in dB.

Figure 4 .

 4 Figure 4. System spectral efficiency bit/s/Hz for macro & pico cells.

Figure 5 .

 5 Figure 5. Execution time versus Nu users

ACKNOWLEDGMENT

The project has been supported by the CNRS-GDR ISIS and doctor school MATHSTIC, to accomplish the collaboration between Vodafone chair and IRISA lab that tooks place at Dresden-Germany. Thanks for Abdul Karim Gizzini for all the technical support.