Control-flow Flattening Preserves the Constant-Time Policy

Abstract

Obfuscating compilers protect a software by obscuring its meaning and impeding the reconstruction of its original source code. The typical concern when defining such compilers is their robustness against reverse engineering and the performance of the produced code. Little work has been done in studying whether the security properties of a program are preserved under obfuscation. In this paper we start addressing this problem: we consider control-flow flattening, a popular obfuscation technique used in industrial compilers, and a specific security policy, namely constant-time. We prove that this obfuscation preserves the policy, i.e., that every program satisfying the policy still does after the transformation.

Introduction

security policy (namely constant-time), and we prove that every program satisfying the policy still does after the transformation, i.e., the obfuscation preservers the policy.

For the sake of presentation, our source language is rather essential, as well as our illustrative examples. The proof that control-flow flattening is indeed secure follows the approach of [ 3 ] (briefly presented in Section 2), and only needs paper-and-pencil on our neat, foundational setting. Intuitively, we prove that if two executions of a program on different secret values are indistinguishable (i.e., they take the same time), then also the executions of its obfuscated version are indistinguishable (Section 3).

Actually, we claim that extending our results to a richer language will only require to handle more details with no relevant changes in the structure of the proof itself; similarly, other security properties can be accommodated with no particular effort in this framework, besides those already studied in [ 3 ], and also other program transformations can be proved to preserve security in the same manner.

Below, we present the security policy and the transformation of interest.

Constant-time policy An intruder can extract confidential data by observing the physical behavior of a system, through the so-called side-channel attacks. The idea is that the attacker can recover some pieces of confidential information or can get indications on which parts are worth her cracking efforts, by measuring some physical quantity about the execution, e.g., power consumption and time. Many of these attacks, called timing-based attacks, exploit the execution time of programs [ 17 ]. For example, if the program branches on a secret, the attacker may restrict the set of values it may assume, whenever the two branches have different execution times and the attacker can measure and compare them. A toy example follows (in a sugared syntax), where a user digits her pin then checked against the stored one character by character: here the policy is violated since checking a correct pin takes longer than a wrong one. 1 pin := read_secret(); 2 current_char := 1; 3 while (current_char stored_pin_length and pin(current_char) = stored_pin(current_char)) 4 current_char := current_char+1; 5 6 if (current_char = stored_pin_length+1) then print("OK!"); 7 else print("KO!"); Many mitigations of timing-based attacks have been proposed, both hardware and software. The program counter [ 19 ] and the constant-time [ 5 ] policies are software-based countermeasures, giving rise to the constant-time programming discipline. It makes programs constant-time w.r.t. secrets, i.e., the running times of programs is independent of secrets. The requirement to achieve is that neither the control-flow of programs nor the sequence of memory accesses depend on secrets, e.g., the value of pin in our example. Usually, this is formalized as a form of an information flow policy [ 13 ] w.r.t. an instrumented semantics that records information leakage. Intuitively, this policy requires that two executions started in equivalent states (from an attacker’s point of view) yield equivalent leakage, making them indistinguishable to an attacker.

The following is a constant-time version of the above program that checks if a pin is correct: 1 pin := read_secret(); 2 current_char := 1; 3 pin_ok := true 4 while (current_char stored_pin_length) 5 current_char := current_char+1 6 if (pin(current_char) = stored_pin(current_char)) then pin_ok := pin_ok 7 else pin_ok := false 8 9 if (pin_ok = true) then print("OK!"); 10 else print("KO!");

Control-flow flattening A different securing technique is code obfuscation, a program transformation that aims at hiding the intention and the logic of programs by obscuring (portions of) source or object code. It is used to protect a software making it more difficult to reverse engineer the (source/binary) code of the program, to which the attacker can access. In the literature different obfuscations have been proposed. They range from only performing simple syntactic transformations, e.g., renaming variables and functions, to more sophisticated ones that alter both the data, e.g., constant encoding and array splitting [ 12 ], and the control flow of the program, e.g., using opaque predicates [ 12 ] and inserting dead code.

Control-flow flattening is an advanced obfuscation technique, implemented in state-of-theart and industrial compilers, e.g., [ 16 ]. Intuitively, this transformation re-organizes the Control Flog Graph (CFG) of a program by taking its basic blocks and putting them as cases of a selective structure that dispatches to the right case. In practice, CFG flattening breaks each sequences of statements, nesting of loops and if-statements into single statements, and then hides them in the cases of a large switch statement, in turn wrapped inside a while loop. In this way, statements originally at different nesting level are now put next each other. Finally, to ensure that the control flow of the program during the execution is the same as before, a new variable pc is introduced that acts as a program counter, and is also used to terminate the while loop. The switch statement dispatches the execution to one of its cases depending on the value of pc. When the execution of a case of the switch statement is about to complete pc is updated with the value of the next statement to executed.

The obfuscated version of our constant-time example follows. 1 pc := 1; 2 while(1 pc) 3 switch(pc): 4 case 1: pin := read_secret(); pc:= 2; 5 case 2: current_char := 1; pc:= 3; 6 case 3: pin_ok := true; pc:= 4; 7 case 4: if (current_char stored_pin_length) then pc:= 5; else pc := 9; 8 case 5: current_char := current_char+1; pc:= 6; 9 case 6: if (pin(current_char) = stored_pin(current_char)) then pc:= 7; else pc := 8; 10 case 7: pin_ok := pin_ok; pc:= 4; 11 case 8: pin_ok := false; pc:= 4; 12 case 9: skip; pc:= 10; 13 case 10: if (pin_ok = true) then pc:= 11; else pc := 12; 14 case 11: print("OK!"); pc:= 0; 15 case 12: print("KO!"); pc:= 0;

Now the point is whether the new obfuscated program is still constant-time, which is the case. In general we would like to have guarantees that the attacks prevented by the constanttime based countermeasure are not possible in the obfuscated versions. 2

Background: CT-simulations

Typically, for proving the correctness of a compiler one introduces a simulation relation between the computations at the source and at the target level: if such a relation exists, we have the guarantee that the source program and the target program have the same observable behavior, i.e., the same set of traces.

A general method for proving that constant-time is also preserved by compilation generalizes this approach and is based on the notion of CT-simulation [ 3 ]. It considers three relations: a simulation relation between source and target, and two equivalences, one between source and the other between target computations. The idea is to prove that, given two computations at source level that are equivalent, they are simulated by two equivalent computations at the target level. Actually, CT-simulations guarantee the preservation of a particular form of noninterference, called observational non-interference. In the rest of this section, we briefly survey observational non-interference and how CT-simulations preserve it.

The idea is to model the behavior of programs using a labeled transition system of the form A !t B where A and B are program configurations and t represents the leakage associated with the execution step between A and B. The semantics is assumed deterministic. Hereafter, let the configurations of the source programs be ranged over by A; B; : : : and those of the target programs be ranged over by ; ; : : :. We will use the dot notation to refer to commands and state inside configurations, e.g., A:cmd refers to the command part of the configuration A.1

The leakage represents what the attacker learns by the program execution. Formally, the leakage is a list of atomic leakages where not cancellable. Observational non-interference is defined for complete executions (we denote Sf the set of final configurations) and w.r.t. an equivalence relation on configurations (e.g., states are equivalent on public variables): Definition 2.1 (Observational non-interference [ 3 ]). A program p is observationally noninterferent w.r.t. a relation , written p j= ONI ( ), iff for all initial configurations A; A0 2 Si and configurations B; B0 and leakages t; t0 and n 2 N,

A ! t0 n B0 ^ (A; A0) =) t = t0 ^ (B 2 Sf iff B0 2 Sf ):

t n B ^ A0 !

Hereafter, we denote a compiler/transformation with J K and with JpK the result of compiling a program p. Intuitively, a compiler J K preserves observational non-interference when for every program p that enjoys the property, JpK does as well. Formally, Definition 2.2 (Secure compiler). A transformation J K preserves observational non-interference iff, for all programs p

p j= ONI ( ) ) JpK j= ONI ( ):

To show that a compiler J K is secure, we follow [ 3 ], and build a general CT-simulation in two steps. First we define a simulation, called general simulation, that relates computations between source and target languages. The idea is to consider related a source and a target configuration whenever, after they perform a certain number of steps, they end up in two still related configurations. Formally, Definition 2.3 (General simulation [ 3 ]). Let num-steps( ; ) be a function mapping source and target configurations to N. Also, let j j be a function from source configurations to N. The relation p is a general simulation w.r.t. num-steps( ; ) whenever: 1. (8B; : A ! B ^ A 2. (8B; : A ! B ^ A p p =) (9 : ! ^ num-steps(A; ) = 0 =) jBj < jAj , 3. For any source configuration B 2 Sf and target configuration there exists a target configuration 2 Sf such that !num-steps(A; ) =) A p .

1Following the convention of secure compilation, we write in a blue; sans-serif font the elements of the source language, in a red; bold one those of the target and in black those that are in common. Given two configurations A and in the simulation relation, the function num-steps(A; ) predicts how many steps has to perform for reaching a target configuration related with the corresponding source configuration B. When num-steps(a; ) = 0, a possibly infinite sequence of source steps is simulated by an empty one at the target level. To avoid these situations the measure function j j is introduced and the condition 2 of the above definition ensures that the measure of source configuration strictly decreases whenever the corresponding target one stutters.

The second step consists of introducing two equivalence relations between configurations: c s relates configurations at the source and c t at the target. These two relations and the simulation relation form a general CT-simulation. Formally, Definition 2.4 (General CT-simulation [ 3 ]). A pair ( c s; c t) is a general CT-simulation w.r.t. p , num-steps( ; ) and j j whenever:

c c 1. ( s; t) is a manysteps CT-diagram, i.e., if ; 0, and (A; A0), then A c s A0 and c s A0 and c

and 0 !0num-steps(A0; 0) 0; p , A0 p 0, B p and B0

p 0 A A B A A t 0; c then then

t 0 and they are both final. = 0 and num-steps(A; ) = num-steps(A0; 0); c c

c

The idea is that the relations s and t are stable under reduction, i.e., preservation of the observational non-interference is guaranteed. The following theorem, referred to in [ 3 ] as Theorem 6, gives a sufficient condition to establish constant-time preservation. Theorem 2.1 (Security). If p is constant-time w.r.t. and there is a general CT-simulation w.r.t. a general simulation, then JpK is constant-time w.r.t. .

Proof of preservation

In this section, we present the proof that control-flow flattening preserves constant-time policy. We first introduce a small imperative language, its semantics in the form of a LTS and our leakage model. Then, we formalize our obfuscation as a function from syntax to syntax, and finally we prove the preservation of the security policy. 3.1

The language and its (instrumented) semantics We consider a small imperative language with arithmetic and boolean expressions. Let Var be a set program identifiers, the syntax is

AExpr 3 e ::= v j x j e1op e2

v 2 Z; op 2 f+ ; - ; * ; / ; % g; x 2 Var BExpr 3 b ::= true j false j b1or b2 j not b j e1 e2 j e1 = e2

Cmd 3 c ::= skip j x := e j c1; c2 j if b then c1 else c2 j while b do c We assume that each command in the syntax carries a permanent color either white or not, typically z. Also, we stipulate that each while statement and all its components get a unique non-white color, and that there is a function color yielding the color of a statement.

Now, we define the semantics and instantiate the framework of [ 3 ] to the non-cancelling constant-time policy. For that, we define a leakage model to describe the information that an attacker can observe during the execution. Recall from the previous section that the leakage is a list of atomic leaks. We denote with the list concatenation and with [a] a list with a single element a. Arithmetic and boolean expressions leak the sequence of operations required to be evaluated; we assume that there is an observable op, associated with the arithmetic operation being executed, but not with the logical ones (slightly simplifying [ 3 ]). Also we denote with absence of leaking. Our leakage model is defined by the following function leak ( ; ) that given an expression (either arithmetic or boolean) and a state returns the corresponding leakage: leak (v; ) = leak (x; ) = leak (true; ) = leak (false; ) = [ ] leak (not b; ) = leak (b; ) leak (e1op e2; ) = leak (e1; ) leak (e2; ) op leak (e1

e2; ) = leak (e1 = e2; ) = leak (b1or b2; ) = leak (e1; ) leak (e2; ) Accesses to constants and identifiers leak nothing; boolean and relational expressions leak the concatenation of the leaks of their sub-expressions; the arithmetic expressions append the observable of the applied operator to the leaks of their sub-expressions.

We omit the semantics of arithmetic and boolean expression [ ] because fully standard [ 20 ]; we only assume that each syntactic arithmetic operator op has a corresponding semantic operator op.

The semantics of commands is given in term of a transition relation !t between configurations where t is the leakage of that transition step. As usual a configuration is a pair c; consisting of a command and a state 2 Store assigning values to program identifiers. Given a program p the set of initial configurations is Si = fp; j 2 Storeg, and that of final configurations is Sf = fskip; j 2 Storeg.

Figure 1 reports the instrumented semantics of the language. Moreover, the semantics is assumed to keep colors, in particular in the rule for an z-colored while, all the components of the if in the target are also z-colored, avoiding color clashes (see the .pdf for colors). x := e;

leak(e; ) [x!] skip; fx 7! [a] g if b then c1 else c2; [b] = true leak(b; ) [true!] c1;

c1;

[ !] if b then (c; while b do c) else skip; Recall that the initial program being obfuscated is p. For the sake of presentation, we will adopt the sugared syntax we used in Section 1 and represent a sequence of nested conditionals in the obfuscated program as the command switch e : cs, where cs = [(v1; c1); : : :; (vn : cn)], with semantics

([e] ; c) 2= cs switch e : cs; leak(e; !) skip; switch e : cs; ([e] ; c) 2 cs leak(e; !) c; Now, let pc be a fresh identifier, called program counter. Then, following [ 8 ],the obfuscated version JcK of the command c is pc := 1; while 1 pc do

switch pc : labeled (pc; c; 1 ; 0 ) where labeled (pc; skip; n; m) = [(n; skip; pc := m)] labeled (pc; x := e; n; m) = [(n; x := e; pc := m)] labeled (pc; c1; c2; n; m) = labeled (pc; c1; n; n + size(c1)) labeled (pc; c2; n + size(c1); m) labeled (pc; if b then c1 else c2; n; m) = [(n; if b then pc := n + 1 else pc := n + 1 + size(c1))] labeled (pc; c1; n + 1; m) labeled (pc; c2; n + 1 + size(c1); m) labeled (pc; while b do c; n; m) = [(n; if b then pc := n + 1 else pc := n + 1 + size(c))] labeled (pc; c; n + 1; n) [(n + 1 + size(c); skip; pc := m)] with size( ) defined as follows

size(c) = 1 if c 2 fskip; := g size(c1; c2) = size(c1) + size(c2) size(if b then c1 else c2) = 1 + size(c1) + size(c2)

size(while b do c) = 2 + size(c) The obfuscated version of a program p is a loop with condition 1 pc and with body a switch statement. The switch condition is on the values of pc and its cases correspond to the flattened statements, obtained from the function labeled (pc; c; n; m). It returns a list containing the cases of the switch and it is inductively defined on the syntax of commands: the first parameter pc is the identifier to use for program counter; the second is the command c to be flattened; the parameter n represents the value of the guard of the case generated for the first statement of c; the last parameter m represents the value to be assigned to pc by the last switch case generated. For example, the flattening of a sequence c1; c2 generates the cases corresponding to c1 and c2, and then concatenates them. Note that the values of the program counter for the cases of c2 start from the value assigned to pc by the last case generated for c1, i.e., n + size(c1), where the function size( ) returns the “length” of c1. For a program p, we use 1 as initial value of n and 0 as last value to be assigned so as to exit from the while loop. 3.3

Correctness and security Since obfuscation does not change the language (apart from sugaring nested if commands); the operational semantics is deterministic; and there are no unsafe programs (i.e., a program gets stuck iff execution has completed), the correctness of obfuscation directly follows from the existence of a general simulation between the source and the target languages [ 3 ]. For that, inspired by [ 8 ], we define the relation p between source and target configurations shown in Figure 2. Intuitively, the relation p matches source and target configurations with the same behaviour, depending on whether they are final (third rule), their execution originated from a loop (Rule (Colored)) or not (Rule (White)). Note that we differentiate white and colored cases as to avoid circular reasoning in the derivations of p . More specifically, our relation matches a configuration A in the source with a corresponding in the target. Actually, :cmd is the while loop of the obfuscated program (fourth premise in Rule (White) and third in Rule (Colored)), whereas : is equal to A: except for the value of pc. Its value is mapped to the case of the switch corresponding to the next command in A (first premise in Rule (White) and fifth in Rule (Colored)).

To understand how our simulation works, recall the example from Section 1. By Rule (White) we relate the configuration reached at line (3) at the source level with that of the obfuscated program starting at line (2) and with a state equal to that of the source level with the additional binding pc 7! 3. Similarly, we relate the configuration reached at line (6) at the source level and its obfuscated counterpart (again at line (2) at the obfuscated level), using Rule (Colored) and noting that the source configuration derives from the execution of a loop.

The following theorem ensures that the relation p is a general simulation. Theorem 3.1. For all programs p, the relation p is a general simulation.

The correctness of the obfuscation is now a corollary of Theorem 3.1.

Corollary 3.1 (Correctness). For all commands c and store c; ! skip; 0 iff c ; J K ! skip; 0

The next step is showing that the control-flow flattening obfuscation preserves the constanttime programming policy. For that we define c below and we show that ( c ; c ) is a general CT-simulation, as required by Theorem 2.1.

Definition 3.1. Let A and A0 be two (source or obfuscated) configurations, then A A:cmd = A0:cmd . c

A0 iff

We prove the following:

ls = labeled(pc; p; 1; 0) color (c) = white c0 = while (1 c;

0 = [ fpc 7! ng pc) do (switch pc : ls) p c0; 0 (Colored)

0 = [ fpc 7! ng ls = labeled(pc; p; 1; 0) c0 = while (1 pc) do (switch pc : ls) while b do c00 2 p color (while b do c00) = color (c) 6= white ; pc ` while b do c00 ./ ls[n0]; m0 c; p c0; 0 ; pc ` c ./ ls[n]; m

n0; pc ` c ls[n]; m 0 = skip; [ fpc 7! ng p skip; 0 ls[n] = (n; x := e; pc := m) n0; pc ` x := e ls[n]; m n0; pc ` skip ls[n]; m n0; pc ` c1

ls[n]; m0 n0; pc ` c1; c2 n0; pc ` c2 ls[n]; m ls[m0]; m ls[n] = (n; if b then pc := n + 1 else pc := n + 1 + size(c1)) n0; pc ` c1 ls[n + 1]; m n0; pc ` c2 ls[n + 1 + size(c1)]; m n0; pc ` if b then c1 else c2 ls[n]; m ls[n] = (n; skip; pc := n0 c) n0; pc ` while b do c ls[n]; n0 n0; pc ` while b do c ls[n0]; n0 n; pc ` if b then (c; while b do c) else skip ls[n]; m ; pc ` while b do c ./ ls[n]; m where 2 f ; ./g, and the first parameter (n0) is immaterial in ./.

p relation on configurations and its auxiliary relations.

Theorem 3.2. The pair ( c ; c ) is a general CT-simulation w.r.t. p , num-steps( ; ) and j j.

The main result of our paper directly follows from the theorem above, because the transformation in Section 3.2 satisfies Definition 2.2:

Corollary 3.2 (Constant-time preservation).

The control-flow fattening obfuscation preserves the constant-time policy.

The proofs of the theorems above are available online [ 9 ]. 4

Conclusions

In this paper we applied a methodology from the literature [ 3 ] to the advanced obfuscation technique of control-flow flattening and proved that it preserves the constant-time policy. For that, we have first defined what programs leak. Then, we have defined the relation p between source and target configurations – that roughly relates configurations with the same behavior – and proved that it adheres to the definition of general simulation. Finally, we proved that the obfuscation preserves constant time by showing that the pair ( c ; c ) is a general CTsimulation, as required by the framework we instantiated. As a consequence, the obfuscation based on control-flow flattening is proved to preserve the constant-time policy.

Future work will address proving the security of other obfuscations techniques, and considering other security properties, e.g., general safeties or hyper-safeties. Here we just considered a passive attacker that can only observe the leakage, and an interesting problem would be to explore if our result and the current proof technique scale to a setting with active attackers that also interferes with the execution of programs. Indeed, recently new secure compilation principles have been proposed to take active attackers into account [ 1 ].

Related Work Program obfuscations are widespread code transformations [ 18, 12, 16, 11, 4, 25 ] designed to protect software in settings where the adversary has physical access to the program and can compromise it by inspection or tampering. A great deal of work has been done on obfuscations that are resistant against reverse engineering making the life of attackers harder. However, we do not discuss these papers because they do not consider formal properties of the proposed transformations. We refer the interested reader to [ 14 ] for a recent survey.

Since to the best our knowledge, ours is the first work addressing the problem of security preservation, here we focus only on those proposals that formally studied the correctness of obfuscations. In [ 23, 24 ] a formal framework based on abstract interpretation is proposed to study the effectiveness of obfuscating techniques. This framework not only characterizes when a transformation is correct but also measures its resilience, i.e., the difficulty of undoing the obfuscation. More recently, other work went in the direction of fully verified, obfuscating compilation chains [ 6, 8, 7 ]. Among these [ 8 ] is the most similar to ours, but it only focusses on the correctness of the transformation, and studies it in the setting of the CompCert C compiler. Differently, here we adopted a more foundational approach by considering a core imperative language and proved that the considered transformation preserves security.

As for secure compilation, we can essentially distinguish two different approaches. The first one only considers passive attackers (as we do) that do not interact with the program but that try to extract confidential data by observing its behaviour. Besides [ 3 ], recently there has been an increasing interest in preserving the verification of the constant time policy, e.g., a version of the CompCert C compiler [ 2 ] has been released that guarantees that preservation of the policy in each compilation step. The second approach in secure compilation considers active attackers that are modeled as contexts in which a program is plugged in. Traditionally, this approach reduces proving the security preservation to proving that the compiler is fully-abstract [ 21 ]. However, recently new proof principles emerged, see [ 1, 22 ] for an overview.

References

[1] Carmine Abate , Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault . Journey beyond full abstraction: Exploring robust property preservation for secure compilation . In 32nd IEEE Computer Security Foundations Symposium , pages 256 - 271 , 2019 .

[2] Gilles Barthe , Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu . Formal verification of a constant-time preserving C compiler. PACMPL, 4 (POPL): 7 : 1 - 7 : 30 , 2020 .

[3] Gilles Barthe , Benjamin Grégoire, and Vincent Laporte . Secure compilation of side-channel countermeasures: The case of cryptographic "constant-time" . In 31st IEEE Computer Security Foundations Symposium, CSF , pages 328 - 343 , 2018 .

[4] Mihai Bazon . Uglifyjs - javascript parser, compressor, minifier written in js . http://lisperator. net/uglifyjs/. Online; last access Dec 2019 .

[5] Daniel J. Bernstein . Cache-timing attacks on AES . https://cr.yp.to/antiforgery/ cachetiming-20050414.pdf, 2005 . Online; last access Nov 2019 .

[6] Sandrine Blazy and Roberto Giacobazzi . Towards a formally verified obfuscating compiler . In SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop , 2012 .

[7] Sandrine Blazy and Rémi Hutin . Formal verification of a program obfuscation based on mixed boolean-arithmetic expressions . In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs , pages 196 - 208 , 2019 .

[8] Sandrine Blazy and Alix Trieu . Formal verification of control-flow graph flattening . In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs , pages 176 - 187 , 2016 .

[9] Matteo Busi , Pierpaolo Degano, and Letterio Galletta . Control-flow flattening preserves the constant-time policy (extended version) . https://arxiv.org/abs/ 2003 .05836.

[10] Matteo Busi and Letterio Galletta . A brief tour of formally secure compilation . In Pierpaolo Degano and Roberto Zunino , editors, Proceedings of the Third Italian Conference on Cyber Security, ITASEC19 , volume 2315 of CEUR Workshop Proceedings. CEUR-WS.org , 2019 .

[11] Christian Collberg . The tigress c diversifier/obfuscator . http://tigress.cs.arizona.edu/. Online; last access Dec 2019 .

[12] Christian S. Collberg and Jasvir Nagra . Surreptitious Software - Obfuscation , Watermarking, and Tamperproofing for Software Protection . Addison-Wesley , 2010 .

[13] J. A. Goguen and J. Meseguer . Security policies and security models . In IEEE Symposium on Security and Privacy , pages 11 - 20 , 1982 .

[14] Shohreh Hosseinzadeh , Sampsa Rauti, Samuel Laurén, Jari-Matti Mäkelä , Johannes Holvitie, Sami Hyrynsalmi, and Ville Leppänen . Diversification and obfuscation techniques for software security: A systematic literature review . Information and Software Technology , 104 : 72 - 93 , 2018 .

[15] Catalin Hritcu , David Chisnall, Deepak Garg , and Mathias Payer . Secure compilation . https: //blog.sigplan.org/ 2019 /07/01/secure-compilation/, 2019 . Online; last access Dec 2019 .

[16] Pascal Junod , Julien Rinaldini, Johan Wehrli, and Julie Michielin . Obfuscator-llvm-software protection for the masses . In 2015 IEEE/ACM 1st International Workshop on Software Protection , pages 3 - 9 . IEEE, 2015 .

[17] Paul C. Kocher . Timing Attacks on Implementations of Diffie-Hellman, RSA , DSS, and Other Systems . In Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology , volume 1109 of LNCS , pages 104 - 113 . Springer-Verlag, 1996 .

[18] Tımea László and Ákos Kiss . Obfuscating c+ + programs via control flow flattening . Annales Universitatis Scientarum Budapestinensis de Rolando Eötvös Nominatae, Sectio Computatorica, 30 ( 1 ): 3 - 19 , 2009 .

[19] David Molnar , Matt Piotrowski , David Schultz, and David A. Wagner . The program counter security model: Automatic detection and removal of control-flow side channel attacks . In Dongho Won and Seungjoo Kim , editors, Information Security and Cryptology - ICISC 2005 , 8th International Conference, volume 3935 of LNCS , pages 156 - 168 , 2005 .

[20] Hanne Riis Nielson and Flemming Nielson . Semantics with Applications: An Appetizer . Undergraduate Topics in Computer Science . Springer, 2007 .

[21] Marco Patrignani , Amal Ahmed, and Dave Clarke . Formal approaches to secure compilation: A survey of fully abstract compilation and related work . ACM Computing Surveys , 2019 .

[22] Marco Patrignani and Deepak Garg . Robustly safe compilation or, efficient, provably secure compilation . CoRR , abs/ 1804 .00489, 2018 .

[23] Mila Dalla Preda and Roberto Giacobazzi . Control code obfuscation by abstract interpretation . In Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005 ), 7 -9 September 2005 , Koblenz, Germany, pages 301 - 310 , 2005 .

[24] Mila Dalla Preda and Roberto Giacobazzi . Semantics-based code obfuscation by abstract interpretation . Journal of Computer Security , 17 ( 6 ): 855 - 908 , 2009 .

[25] WebAssembly team. Binaryen - compiler infrastructure and toolchain library for webassembly . https://github.com/WebAssembly/binaryen. Online; last access Dec 2019 .