Xavier Boës
email: xavier.boes@inrap.fr

Sandrine Prat

Vincent Arrighi

Craig Feibel

Jason E Lewis

Sonia Harmand

Bereket Haileab

Lake-level changes and hominin occupations in the arid Turkana Basin during volcanic closure of the Omo River outflows to the Indian Ocean -Response to comments by

Lake-level changes and hominin occupations in the arid Turkana Basin during volcanic closure

INTRODUCTION

We welcome the comments offered by Schuster and Nutz on our publication [START_REF] Boës | Lakelevel changes and hominin occupations in the arid Turkana basin during volcanic closure of the Omo River outflows to the Indian Ocean[END_REF]. We are glad to interact with our peers and we are open to any fair comments, remarks, and criticisms that could give us a chance to improve our understanding of the evolution of the Turkana Basin. Here, we are very pleased to give our point of view on the scientific questions they raise.

Schuster and Nutz (this issue) base their comment on the work by [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF].

That article presents photointerpretations of some eroded coarse sedimentary facies (very high-energy systems) observed at the bottom of the Kaitio Member (Nachukui Formation, West Turkana, Kenya). The dating of their geologic sections (~40 m thick) is based on one ash layer (1.87 Ma, "KBS Tuff") that is not demonstrated by a geochemical analysis. This chronostratigraphy is interpreted in terms of 400 ka eccentricity and 20 ka precession cycles.

The article by [START_REF] Boës | Lakelevel changes and hominin occupations in the arid Turkana basin during volcanic closure of the Omo River outflows to the Indian Ocean[END_REF] that Schuster and Nutz criticize presents a geologic section (110 m thick) going from the top of Lokalalei Member up to the bottom of Kaitio Member (below the eroded high-energy systems). Ash layers at 2.4 Ma (Kokiselei Tuff) and 1.87 Ma ("KBS Tuff") date the bottom and top. Two other intermediate dated ash layers constrain the chronostratigraphic model at 2.33 Ma and 2.27 Ma (Kalochoro Tuff and Tuff G; see the geochemistry of the ash layers in [START_REF] Boës | Lakelevel changes and hominin occupations in the arid Turkana basin during volcanic closure of the Omo River outflows to the Indian Ocean[END_REF]). The stratigraphy measured with a total station ends 15 m below the "KBS Tuff," because Boës et al. studied the section 1 presented by [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF], and because the high-energy facies above the "KBS Tuff" are eroded (and undated). The cross-study of volcanic and sequence stratigraphy with the total station allows Boës et al. to investigate the cyclostratigraphy between 2.4 and 1.87 Ma.

In their comment, Schuster and Nutz say that we [START_REF] Boës | Lakelevel changes and hominin occupations in the arid Turkana basin during volcanic closure of the Omo River outflows to the Indian Ocean[END_REF] did not properly transcribe their stratigraphic facies and that we transformed their periodicities. Here, we would like to underline that the imputation of misrepresenting the data from Nutz et al.

THE RELATIONSHIPS BETWEEN STRATIGRAPHIC FACIES AND

BATHYMETRY IS OVERINTERPRETED

Schuster and Nutz (this issue) question the identification of a "prominent sandstone" as a foreshore (shallow-water) facies, preferring a deeper-water turbidite origin (first remark on their comment). However, in their original work [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] they note that these sand beds lack any of the internal structures diagnostic of turbidites and instead rely on their interpretation of water depth as the defining criterion ("offshore muds" termed "U1"; depth below 15 m). In fact, these sandstones are rich in the trace fossil Piscichnus, interpreted to be fossil fish nests excavated in relative shallow-water environments [START_REF] Feibel | Fossil fish nests from the Koobi Fora Formation (Plio-Pleistocene) of northern Kenya[END_REF]. This is not compatible with the permanent deep system interpreted by Schuster and Nutz.

The "coastal sand and shells" of the sequence reported by [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] should be strictly interpreted as upper shoreface and foreshore (-3 to 0 m) according to Schuster and Nutz (second remark on their comment). Their recommendation is in contradiction with their own original work [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] where this unit (termed "U2") is associated with shoreface, foreshore, beach, and backshore (-3 to +2 m ; see the photointerpretations of beach berms and paleosols presented by [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF]).

The "oncolites rich silts and sands" of the sequence reported by [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] is also problematic. Schuster and Nutz consider as an "established geologic fact" that oncolites are associated with a bathymetry of -15 to -5 m. However, it is an overinterpretation of the initial work of Nutz et al. (2017, p. 238), which mentions for this unit (termed "U3") that "wave or storm reworking is suspected to have taken over oncolites in the shore zone and to have deposited them in the lower shoreface to the transition zone." Schuster and Nutz's bathymetric reconstruction is overinterpreted and impossible given the archaeological context and the magnetostratigraphy presented by [START_REF] Lepre | An earlier origin for the Acheulian[END_REF] see also [START_REF] Roche | Les sites archéologiques plio-pléistocènes de la formation de Nachukui, Ouest-Turkana, Kenya: bilan synthétique 1997-2001[END_REF] and Fig. 1). Oncolites are well known to form within the foreshore (-2 to 0 m), and they can even be emerged.

THE INTERPRETATION OF THE CHRONOLOGY AND PERIODICITIES IS

OVERINTERPRETED

Schuster and Nutz's chronology and periodicities (third remark on their comment) are based on problems with the chronostratigraphic model originally reported by [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF]. Their "long-term trend" is based on three segments ("U1, U2, and U3") separated by disconformities of variable temporal significance. Although these segments are separated by erosion features and undated time gaps, they considered their sections as "continuous" and "complete," and they inferred an age span of 1.95-1.72 Ma. Nutz et al. lacked any direct age control on their "observed" chronostratigraphic gaps (see "RSE, FS, SU" in [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] and "RSLE" in Schuster and Nutz [this issue]; see also Fig. 1). Each truncated sedimentary pile is placed end to end (U1/1.95-1.87 Ma; U2/1.87-1.76 Ma; U3/1.76-1.72 Ma), and their "observed regressive and transgressive trends" are built from that technique.

Apart from the problem of applying a continuous chronostratigraphic model in discontinuous and incomplete time series, the total duration of the sections investigated by [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] appears to be of 70 to 130 ka maximum (Fig. 1). The offset is nearly equivalent to a 100 ka insolation period, or three to five precession cycles. Even in their original publication, [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] have overinterpreted their data. How could the 400 ka periodicity be "observed" from their "230 ka" (1.95-1.72 Ma) time series? In [START_REF] Harris | Stratigraphy and Palaeontology of the Nachukui Formation, Lake Turkana Region, Kenya[END_REF], Brown and[START_REF] Brown | Geochronology of the Turkana depression of northern Kenya and southern Ethiopia[END_REF][START_REF] Mcdougall | New single crystal 40Ar/39Ar ages improve time scale for deposition of the Omo Group, Omo-Turkana Basin, East Africa[END_REF], the sediment accumulation rate is multiplied by a factor of 2 above "KBS," and the type section dated between 1.87 and 1.76 Ma represents 130 m of sediments. How could only 20 m of eroded "U2" sediments in Nutz et al.'s (2017) sections represent a "complete record" with four to five consecutive 20 ka cycles? What Shuster and Nutz consider as "established geologic facts" presents an offset of 50% with the sedimentation rates of [START_REF] Harris | Stratigraphy and Palaeontology of the Nachukui Formation, Lake Turkana Region, Kenya[END_REF][START_REF] Brown | Geochronology of the Turkana depression of northern Kenya and southern Ethiopia[END_REF][START_REF] Mcdougall | New single crystal 40Ar/39Ar ages improve time scale for deposition of the Omo Group, Omo-Turkana Basin, East Africa[END_REF]. The offset is of 50-100% with the magnetostratigraphy of [START_REF] Lepre | An earlier origin for the Acheulian[END_REF] (see Fig. 1).

Finally, we do not think that Schuster and Nutz's remarks are justified because they have few arguments for challenging other scientists based on their 2017 article (see also the reply from Lupien et al. [2018b] and the original work by Lupien et al. [2018a]).

(

  2017) in Boës et al. (2019) is baseless. That Schuster and Nutz lay claim to "observed geologic facts" in contradiction with the interpretations of Boës et al. is based on shaky documentation presented in their original work. Schuster and Nutz's criticisms are addressed subsequently.

ACKNOWLEDGMENTS

Our research is funded by the ANR-12-CULT-0006 (Agence Nationale de la Recherche), by the Ministère des Affaires Etrangères (Direction générale de la mondialisation, du développement et des partenariats, N°681/DGM/ATT/RECH, N°986/DGM/DPR/PRG), the LSB Leakey Foundation, OASIC/AAP2017-UMI-CNRS-France (Project MobHom), and NTM INDIGO-France. We thank Rachel Lupien for constructive discussions.

LIST OF FIGURES

Figure 1. (color online) Problems with the geologic sections from [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] partially reported in [START_REF] Boës | Lakelevel changes and hominin occupations in the arid Turkana basin during volcanic closure of the Omo River outflows to the Indian Ocean[END_REF]. (A) Comparison between the sedimentation rate in [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] and in [START_REF] Harris | Stratigraphy and Palaeontology of the Nachukui Formation, Lake Turkana Region, Kenya[END_REF], Brown and[START_REF] Brown | Geochronology of the Turkana depression of northern Kenya and southern Ethiopia[END_REF][START_REF] Mcdougall | New single crystal 40Ar/39Ar ages improve time scale for deposition of the Omo Group, Omo-Turkana Basin, East Africa[END_REF]. By contrast, the sedimentation rate applied by Nutz et al. (22 cm/ka) in their highenergy facies above the "KBS Tuff" is almost divided by a factor of 2. According to the method summary in [START_REF] Lepre | An earlier origin for the Acheulian[END_REF], a more correct sedimentation rate is 38 cm/ka, which is in agreement with the other published rates for these high-energy facies observed in the Kaitio Member. The sedimentation rate of "22 cm/ka" mentioned by Nutz et al. for the coarse sediment package (U2 and U3) resembles the sedimentation rate attributed to the much lower energy environments (10 to 20 cm/ka), typical for the Kalochoro Member (~15 cm/ka). Note the ages calculated with the sedimentation rate of 22 cm/yr are not correct in the original article by [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF]. For example, we should obtain 1.76 Ma at 24 m and not at 20 m.

(B) Compared with [START_REF] Lepre | An earlier origin for the Acheulian[END_REF], the magnetostratigraphy of [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] is divided by a factor of 2. Nutz et al. have represented the Olduvai and Matuyama transition, although this transition is not even present in their sections (see also the supplementary material in [START_REF] Lepre | An earlier origin for the Acheulian[END_REF]. Consequently, the position of the Olduvai-Matuyama transition in Nutz et al. presents an offset of 100% with the magnetostratigraphy of [START_REF] Lepre | An earlier origin for the Acheulian[END_REF]. The correlation with the archaeological context of KS4 (1.76 Ma; [START_REF] Lepre | An earlier origin for the Acheulian[END_REF] is wrong. The top part (U2-U3) of the sections of [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF] presents a very bad correlation with [START_REF] Lepre | An earlier origin for the Acheulian[END_REF] and [START_REF] Boës | Lakelevel changes and hominin occupations in the arid Turkana basin during volcanic closure of the Omo River outflows to the Indian Ocean[END_REF]. Note that Lepre et al. completed the correlation between their sections following the magnetostratigraphy only and not according to the stratigraphic facies that changes laterally because of disconformities and erosional features. Observed erosion features and disconformities: RSE, regressive surface of erosion; RSLE, regressive surface of lake erosion; SF, surface flooding; SU, subaerial unconformity (see [START_REF] Nutz | Orbitally-driven evolution of Lake Turkana (Turkana Depression, Kenya, EARS) between 1.95 and 1.72 Ma: a sequence stratigraphy perspective[END_REF]Schuster and Nutz, this issue).


Yoonseok Ko
email: yoon-seok.ko@inria.fr

Tamara Rezk
email: tamara.rezk@inria.fr

Manuel Serrano
email: manuel.serrano@inria.fr

SecureJS Compiler: Portable Memory Isolation in JavaScript *

Keywords: Security and privacy → Software security engineering, Web application security, • Software and its engineering → Syntax, Semantics, Compiler, Memory Isolation, JavaScript

The memory isolation mechanism plays an essential role to provide security enforcement in JavaScript programs. Existing secure interaction libraries such as Google Caja, SES, and VM2 rely on built-in memory isolation mechanisms provided by Node.js and browsers, yet most of the other engines such as JerryScript and Duktape, which are implementations for IoT devices, do not support such isolation mechanisms.

In this paper, we report about the design and implementation of SecureJS, a portable JavaScript-to-JavaScript compiler that enforces memory isolation. As it only uses standard features, the compiled code it generates can be used by any JavaScript engine. We validated empirically the semantics preservation and memory isolation of SecureJS compiled programs by using 10,490 test programs of ECMAScript Test262 test suite. We also developed a novel experiment to evaluate memory isolation property of compiled code by instrumented JavaScript engines.

INTRODUCTION

JavaScript has been growing at a rapid pace over the years due to its easy manipulation and deployment in development. The dynamic nature of the language provides a smooth environment for the integration of code, and it contributes to the easy and fast development of complex applications [START_REF] Nikiforakis | You are what you include: large-scale evaluation of remote javascript inclusions[END_REF].

Whereas the dynamic features of JavaScript play an essential role in the language popularity by simplifying application developments, they also enable malicious JavaScript libraries to exploit these dynamic features to break the integrity and confidentiality of the applications [START_REF] Bodin | A Trusted Mechanised JavaScript Specification[END_REF]. Within a single JavaScript program execution all components share a global object and intrinsic objects such as Object and Object.prototype. Due to the idiosyncratic JavaScript semantics whose primitive operations implicitly access these global and intrinsic objects, all the components that form an application are tightly bond together. This gives opportunities to a malicious third-party code to pervert or extract undue pieces of information from others execution.

Various researches have been carried out so as to provide security enforcement achieved by memory isolation [START_REF] Bhargavan | Language-based Defenses Against Untrusted Browser Origins[END_REF][START_REF] Luo | Mashic Compiler: Mashup Sandboxing Based on Inter-frame Communication[END_REF][START_REF] Miller | Caja -safe active content in sanitized JavaScript[END_REF][START_REF] Gibbs Politz | ADsafety: Type-based Verification of JavaScript Sandboxing[END_REF][START_REF] Simek | VM2 npm package[END_REF][START_REF] Swamy | Gradual Typing Embedded Securely in JavaScript[END_REF][START_REF] Terrace | Sandboxing Third-Party Scripts[END_REF][START_REF] Vasilakis | BreakApp: Automated, Flexible Application Compartmentalization[END_REF]. Total isolation is the simplest way to run programs without unintended interplay. However, more complex programs that need interactions between programs cannot enjoy the benefit of isolation. The practical secure JavaScript programming solutions such as Google Caja [START_REF] Miller | Caja -safe active content in sanitized JavaScript[END_REF], SES [START_REF] Agoric | SES: Proposal for Secure EcmaScript[END_REF], and VM2 [START_REF] Simek | VM2 npm package[END_REF] rely on such an isolation mechanism provided by Node.js or browsers and provide secure interactions between isolated programs by controlling the interactions. Still, such built-in isolation mechanisms are not supported other popular JavaScript implementations such as JerryScript 1 and Duktape2 , which are JavaScript implementations for micro-controllers, and thus, it limits the use of these secure interaction solutions in a practical use. It motivates the need for portable isolated JavaScript environments independent from JavaScript implementations.

A basic building block for JavaScript memory isolation is a realm (as it is defined in the latest ECMAScript specification 3 ), which consists of a global object and intrinsic objects. Programs running in the same realm share the global and intrinsic objects, and isolated realms initially do not share any references between the realms. Running programs in different isolated realms guarantees that their memory accesses do not interfere with each other. However, programs in a realm are able to interact with programs in another realm by intentionally exporting a value, and it breaks the isolation. Thus, isolated realms are a basic and essential unit for secure program executions, and they can achieve security enforcement on further interactions by combining with the existing secure JavaScript programming solutions. Unfortunately, JavaScript realms are only supported by some JavaScript implementations, such as Node.js and browsers, and it limits the use of the existing secure programming solutions in other JavaScript implementations.

Our Approach. In this paper, we propose a novel technique, based on a JavaScript-to-JavaScript compilation, to run JavaScript programs in an isolated realm. Our method focuses on rewriting the semantics of implicit field accesses of the given program and achieves memory isolation by using revised field access operations. For that, we define a subset of JavaScript language, JS explicit , in which primitive operations do not involve implicit field accesses. The translation from JavaScript to JS explicit replaces all the implicit field accesses of the source program with explicit operations. JS explicit programs are meant to run in a dedicated secure runtime environment that creates an isolated virtual realm and provides secure primitive operations that implicitly access the isolated virtual realm.

We have implemented a secure JavaScript-to-JavaScript compiler, SecureJS. It transforms programs into equivalent ones, but which would execute as if they were running inside an isolated memory. The compilation relies on the translation to JS explicit and replaces primitive operations to secure versions and thus execute in an isolated memory, which simulates a JavaScript realm. The program running in the isolated memory can interact with others by intentionally exporting a value of the isolated memory to outside. This compiler is portable and only uses standard features so it can be used by any JavaScript engine that complies with ECMAScript 5.1 specification. Thus, the compiler provides an isolation mechanism independently of JavaScript implementation, and it enables us to use existing secure interaction libraries in any JavaScript engine.

Contributions.

• We propose a subset of the JavaScript language JS explicit , in which primitive operations do not involve implicit field accesses, and we present a translation from JavaScript to JS explicit (Section 3). • We provide a secure JavaScript-to-JavaScript compiler, Se-cureJS, as a tool. This compiler transforms programs into equivalent ones but which would execute as if they are running inside an isolated realm without relying on any built-in mechanisms. This implementation is portable to any EC-MAScript 5.1 compliant implementations and the isolated realm supports all features of ECMAScript 5.1 4 (Section 4). • We provide instrumented JavaScript engines that detect implicit field accesses and field accesses to intrinsic objects. We have used it to test empirically the semantic preservation and memory isolation of the SecureJS compiled programs.

The instrumented engines can be used independently of Se-cureJS to test memory isolation. Our tool and the patch for the instrumented engine are publicly available5 (Section 5).

OVERVIEW

We give an overview of our approach with an overly simple example that only use a field access operation that involves a dynamic type conversion and prototype chain field lookup. We demonstrate the evaluation of a JavaScript program construct. An evaluation of a single JavaScript program construct consists of a series of JavaScript internal primitive operations. We consider the following code fragment:

1 Boolean . prototype . x = 10; 2 var o = { toString : function () { return " x " ; }}; The evaluation of the field lookup operation true[o] used in the test at line 4 consists of a series of JavaScript primitive operations as follows:

(1) It applies ToObject to true to dynamically converts the value to an object. (3) The field lookup operation searches a field named "x" from the instance of Boolean intrinsic object. Since the instance does not have a field named "x", it implicitly accesses the field "x" of the object Boolean.prototype, which is the prototype chain object of the instance. Since the field value of the object Boolean.prototype is 10 as we defined at line 1, the result of the field lookup operation is evaluated to 10 and the equality test succeeds. The evaluation of a field lookup operation in JavaScript involves two implicit field accesses, and by one of these field accesses reads a field value of the intrinsic object Boolean.prototype.

Our goal is to run programs as if they were running in isolated realms. For that we will actually run them in isolated virtual realms that rely on two ingredients: i) newly created controlled global and intrinsic objects, and, ii) a rerouting of the implicit field accesses from the original intrinsic objects to the controlled intrinsic objects.

In order to reroute field accesses, we use the two steps code transformation. First, we transform programs into equivalent ones but were implicit operations have be replaced with equivalent explicit ones. For instance, in the above example, the implicit field accesses are involved in the dynamic type conversion. For example, the code true[o] === 10 is converted as follows: This code uses the SJSLoad instead of Load for the field lookup operation. The crucial point is line 4. When a field access reaches an intrinsic object Boolean.prototype, it reroutes the field access to the controlled intrinsic object isolated.Boolean.prototype (line 5). Thus, the rewritten code runs as if the code is running with the controlled intrinsic object.

In the rest of the paper, we propose a core JavaScript language, JS explicit , that does not involve implicit field accesses, and we present a translation from JavaScript to JS explicit (Section 3). Then, we implement a secure runtime environment that consists of an isolated virtual realm and secure primitive operations which reroute field accesses to the virtual realm (Section 4).

JS explicit , A CORE JAVASCRIPT LANGUAGE

In this section, we define JS explicit , a core language for JavaScript, whose semantics is simpler than that of JavaScript in that its primitive operations do not involve implicit field access.

Syntax

We use the following formal syntax for JS explicit :

] | x = λ( ì x n ).i | return e | x = ⋄apply(x 1 ,x 2 ,[ ì y n ]) | while x do i | if (x ) i 1 else i 2 | try i 1 catch(x ) i 2 finally i 3 | throw e | {i } | i 1 ;i 2 | ϵ | ⋄defineOwnProperty(x ,e 1 ,e 2 ) | x = ⋄getOwnPropertyDescriptor(e 1 ,e 2 )
where ⊕ and ⊖ are the binary and unary operators of the JavaScript language, respectively.

Expressions. An expression e is either a local variable access x, a global variable access x д , a constant value v ∈ V prim , this value this, binary operators, or unary operators.

Non-standard Expressions. The operators whose name starts with the ⋄ symbol are non-standard operators. Their semantics follow those of the corresponding JavaScript built-in functions, but they do not involve implicit type conversion. The field test operator ⋄hasOwnProperty e 1 e 2 returns true if an object designated by e 1 has a field named e 2 , and otherwise, returns false. This operator requires an object value for e 1 and a string value for e 2 . The operator ⋄getPrototypeOf e returns a prototype chain object of the given object e. The operator requires an object value for e. The primitive type conversion operators ⋄toString e, ⋄toNumber e, and ⋄toBoolean e take a primitive value e as its argument and return a string, a number, and a boolean value, respectively.

Instructions. JS explicit uses non-standard semantics for the field lookup and update operations. The field update operation e 1 [e 2 ] = e 3 updates a field designated by the value of e 2 of an object e 1 to the value of e 3 . Note that the update operation does not access a prototype chain of the given object and does not involve a dynamic type conversion. Thus, e 1 must be evaluated to an object, and e 2 must be evaluated to a string value. The field lookup operation x = e 1 [e 2 ] reads a field designated by e 2 of an object e 1 and assigns the result to the local variable x. Like the field update operation, the field lookup operation does not access a prototype chain object and does not involve a dynamic type conversion. Thus, e 1 must be evaluated to an object, and e 2 must be evaluated to a string value.

The semantics of the rest of the instructions follow the standard semantics but these instructions do not involve dynamic type conversions. The variable declaration var x declares a variable in a local scope. The assignment instructions x = e and x д = e assign the value of expression e to the local variable x and the global variable x д , respectively. When the instruction assigns a value to a global variable, it updates to the new value if its writable property is true; otherwise, it ignores the update operation. The object allocation x 1 = ⋄alloc(x 2 ) allocates an object whose a prototype chain designates x 2 , and it assigns the newly allocated location to x 1 . The function declaration x = λ( ì x n ).i allocates a new function object with its argument names ì

x n and the function body instruction i. We assume that all the program flows in the function body i end with a return instruction return e. The return instruction return e returns the value of the expression e to its caller site. The function call

x = ⋄apply(x 1 ,x 2 ,[ ì y n ]
) calls a function x 1 with a this value x 2 and its arguments ì y n , and it assigns the return value of the function to the variable x. The loop while x do i iterates its body i while the value of its condition x is true. The branch instruction if (x ) i 1 else i 2 executes the instruction i 1 or i 2 depending on the value of variable x. The instruction try i 1 catch(x ) i 2 finally i 3 executes the instruction i 1 , and if there is an exception from the instruction i 1 , it catches the exception value, bind it to a local variable x, and run the instruction i 2 . Then, it executes the instruction i 3 . The throw instruction throw e throws an exception with an exception value e.

Once an exception is thrown, it ignores instructions until it reaches to the catch clause. The sequence i 1 ;i 2 executes the instructions i 1 and i 2 in order. The no-op instruction ϵ does nothing.

Non-standard Instructions. JS explicit uses non-standard instructions: ⋄defineOwnProperty and ⋄getOwnPropertyDescriptor. In Java-Script, they are supported by built-in functions Object.defineProperty and Object.getOwnPropertyDescriptor. The immediate field update operation with attributes ⋄defineOwnProperty(x ,e 1 ,e 2 ) assigns the value of the expression e 2 to an object x of a field e 1 . The value of expression e 2 is either a data descriptor object that has fields value, enumerable, configurable, and writable attributes or a accessor descriptor object that has fields get, set, enumerable, and configurable. The immediate field lookup x = ⋄getOwnPropertyDescriptor(e 1 ,e 2 ) reads a field e 2 of an object e 1 and assigns the field value record as an object to the variable x.

For the sake of simplicity, we use the following notations in the rest of the section: x = f (y 1 ,...,y n ) denotes x = ⋄apply(f , null, ì y n ), and we use a function isObject defined as follows:

1 isObject = λ [ x ]. { SAC'21, March 22-March 26, 2021, Gwangju, South Korea Y. Ko et al. 2 return ( typeof x === " object " && x !== null ) || 3 typeof x === " function " ; 4 }
We omit else branches of if statements when empty.

Semantics

We define the semantics of a program by the means of a big-step semantics. The semantics of the JS explicit follows the semantics of JavaScript language, but they do not involve dynamic type conversion and implicit field access. The configurations have the form µ, l s , i, t ⇓ µ ′ , t ′ , where µ, µ ′ ∈ M are memories, l s ∈ V loc is a current scope object location, i is an instruction, and t is either a normal state or an exception state with a value exc(v) where v ∈ V. The state tag normal denote that the program state is in a normal state, and the state tag exc(v) denote that the program state is in an exception state with an exception value v. A memory M = V loc → O is a map from locations to objects and an object o ∈ O = V fld → R is a map from field names to field values where V fld = V str ∪ V i and V str are strings and V i are special values used to name internal JavaScript fields such as @env and @proto, and R = V str → V is a map from record names to values and we write {name 1 : v 1 , name 2 : v 2 } to denote a record that has two elements of names name 1 and name 2 respectively with its values v 1 and v 2 .

The evaluation of an expression e has the form µ, l s , e ⇓ E v, where µ ∈ M is a program memory, v is a value of the expression in the memory.

The auxiliary function Put(l s ,x,v) either updates the current scope object with x = v or walks the scope chain designated by the outer scope @env to update the value of a local variable x as defined by:

µ ′ = µ[l s → µ(l s )[x → v]] µ, Put(l s , x, v) ⇓ A µ ′ x ∈ dom(µ(l s )) µ, Put(µ(l s )(@env).1, x, v) ⇓ A µ ′ µ, Put(l s , x, v) ⇓ A µ ′ x dom(µ(l s ))
Figure 1 presents an excerpt of the formal semantics containing only the essential rules. It shows the semantics of object allocation, field lookup, and update operations. Unlike the standard JavaScript semantics, the field lookup and update operations only accept that a receiver is an object and a field name designator evaluates to a string value, and the operations do not search a field in a prototype-chain of the given receiver object.

• Alloc rule. The instruction x 1 = ⋄alloc(x 2 ) evaluates the argument x 2 to a value v, allocates a new object in a new location l n with a prototype chain value v, and assigns the allocated object reference to the local variable x 1 . The instruction requires the prototype value x 2 to either be a location value or a null value. • Lookup rule. The instruction x 1 = x 2 [e] first evaluates the receiver object x 2 and field name designator e respectively to a location l and a string value k. The semantics do not search a prototype chain, but merely read a field of the receiver object µ(l)(k). In this rule, the field must be a record, which has four fields value, enumerable, configurable, and writable, and it assigns the value of the field value to the left-hand side variable x 1 by calling the auxiliary function Put.

• Update rule. The instruction x [e 1 ] = e 2 also evaluates the receiver object x to a location l, the field name e 1 to a string value k. It evaluates the expression e 2 to a value v, and it assigns the value v as a record with enumerable, configurable, and writable fields to the field k of the receiver object designated by the location l. This rule is applied when there was no field named k in the receiver object, and it creates a new field. The semantics of non-standard instructions and operators follows the semantics of the corresponding JavaScript built-in functions, but they do not apply dynamic type conversion. Figure 2 shows three additional semantics rules:

• hasOwnProp1 and hasOwnProp2 rules. The binary operation ⋄hasOwnProperty tests whether the object e 1 has a field designated by the string name e 2 or not. • getPrototypeOf rule. The unary operation ⋄getPrototypeOf e returns the internal prototype chain value of the given object.

The unary operations ⋄toString, ⋄toNumber, and ⋄toBoolean take a primitive value as an argument and returns their corresponding typed value. The conversion algorithm is defined in the ECMAScript specification 7 [START_REF]ECMA-262: ECMAScript Language Specification[END_REF], and these conversion algorithm do not involve implicit field access.

JavaScript Primitive Operations in JS explicit

In this section, we present JavaScript primitive operations written in JS explicit . Each primitive operation is devised by a corresponding internal method or operation defined in ECMAScript specification.

We write [[A]] and B to denote an internal field or method named A and an operation named B, respectively. Figure 3a shows the [[Get]] internal method of ECMAScript specification that defines the essential semantics of a field lookup operation in JavaScript. For a given code is o[s], o is passed as base and s is passed as P in the specification. Figure 3b shows the code of Get function which mimics the semantics of [[Get]] internal method in JS explicit . Each step of the auxiliary function Get is designed with the specification and written in JS explicit .

First, the [[Get]] internal method of the specification converts the receiver value base to an object by calling the ToObject operation (step 1). In the Get function, it calls the function ToObject which mimics the semantics of the operation ToObject in the specification. This operation returns the input value if a type of the input value is already an object. Otherwise, it allocates a typed object if a type of the input value is one of string, number, and boolean types. This semantics is defined by the auxiliary function ToString written in JS explicit . Then, it calls [[GetProperty]] internal method to search the field named P from the object base and its prototype chain (step 2). The result is either undefined value when it fails to find a field or a descriptor object. If the result is undefined, it returns undefined value (step 3). The descriptor object has value field if the field is an ordinary value field. Otherwise, the descriptor object has to have the get field and it is the getter value. Thus, it first checks whether the descriptor object has a field "value", and it returns the value of the field "value" when the descriptor object has the field (step 4). 7 ToBoolean: https://www.ecma-international.org/ecma-262/5.1/#sec-9.2, ToNumber: https://www.ecma-international.org/ecma-262/5.1/#sec-9.3, ToString: https://www.ecma-international.org/ecma-262/5.1/#sec-9.8 Alloc

µ, l s , x 2 ⇓ E v l n fresh in V loc µ ′ = µ[l n → {@proto → {value : v } }] µ ′ , Put(l s , x 1 , l n ) ⇓ A µ ′′ µ, l s , x 1 = ⋄alloc(x 2 ), normal ⇓ µ ′′ , normal Lookup µ, l s , x 2 ⇓ E l µ, l s , e ⇓ E k v = µ(l )(k ).value µ, Put(l s , x 1 , v) ⇓ A µ ′ µ, l s , x 1 = x 2 [e], normal ⇓ µ ′ , normal Update µ, l s , x ⇓ E l µ, l s , e 1 ⇓ E k µ, l s , e 2 ⇓ E v µ ′ = µ[l → µ(l )[k → {value : v, enumerable : true, configurable : true, writable : true}]] µ, l s , x [e 1 ] = e 2 , normal ⇓ µ ′ , normal
where k dom(µ(l ))

Figure 1: An excerpt from semantics rules for instructions When the [[Get]] internal method is called using base as its this value and with property name P, the following steps are taken:

hasOwnProp1 µ, l s , e 1 ⇓ E l µ, l s , e 2 ⇓ E k k ∈ dom(µ(l )) µ, l s , ⋄hasOwnProperty e 1 e 2 ⇓ E true hasOwnProp2 µ, l s , e 1 ⇓ E l µ, l s , e 2 ⇓ E k k dom(µ(l )) µ, l s , ⋄hasOwnProperty e 1 e 2 ⇓ E false getPrototypeOf µ, l s , e ⇓ E l v = µ(l )(@proto).value µ, l s , ⋄getPrototypeOf e ⇓ E v
(1) Let O be ToObject(base).

( Otherwise, it loads the field "get" (step 5). If the getter function is undefined, it just returns undefined value (step 6). Otherwise, the getter function is a function value, and it calls the getter function with base as its this value and returns the result (step 7). Figures 4a and4b show the [[GetProperty]] internal method specification and its meaning written in JS explicit . The [[GetProperty]] method defines the field search in a prototype chain. It first tries to access the field P from the given object O (step 1). If the object O has a field named P, it just returns the field record (step 2). Otherwise, it loads the value of a prototype chain object of the object O (step 3). If the given object does not have a prototype chain object, it fails to find a field and returns undefined value (step 4). Otherwise, it recursively searches the field named P from the prototype chain object of the object O (step 5). The auxiliary function GetProperty implements the semantics in JS explicit .

Figures 5a and5b show the [[DefaultValue]] internal method specification with hint String and its meaning written in JS explicit . The [[DefaultValue]] method defines the dynamic type conversion when a given value is an object. In a field lookup operation o[s], when the given field name designator s is an object, it converts the field name value s to a string typed value by calling the [[De-faultValue]] method. In the [[DefaultValue]] method, it first calls [[Get]] internal method with the argument toString and we define its corresponding auxiliary function in Figure 3a (step 1). If the result is a callable, that is, if the value is a function (step 2), it calls the result function with O as the this value (step 2a). If the result of toString is a primitive value, it returns the result (step 2b). Otherwise, it calls [[Get]] internal method with an argument valueOf (step 3). If the result is a callable (step 4), it calls the result function with O as the this value (step 4a). If the result of valueOf is a primitive value, it returns the result (step 4b). If both result values of toString and valueOf are not a primitive value, it throws a TypeError exception (step 5). In the auxiliary function written JS explicit , it creates an instance of TypeError, which designates a built-in function of TypeError object.

Figure 6 presents the semantics of ToString and ToNumber operations defined in ECMAScript specification. If the value is not an object, it converts the primitive value respectively to a string value and a number value by ⋄toString and ⋄toNumber operations. Otherwise, it calls DefaultValue with a hint "String" or "Number", which mimics the semantics of [[DefaultValue]]. Then, it again calls the function itself ToString or ToNumber with the result of DefaultValue. Since the auxiliary function DefaultValue always returns a primitive value, this recursion does not create a loop, and the auxiliary with accesses to the global object, and later on, we will present a revised operation to reroute these accesses to a virtual global object. When an identifier expression does not have a corresponding variable declaration binding, the expression is considered as a global variable access. compile⟦x_g⟧ transforms a global variable access x_g into an auxiliary function call Loadvar("x_g") defined as follows:

1 Loadvar = λ ( id ) .{ 2 Get ( global , id ) ; 3 }
The variable global designates the global object. Note that the semantics of a global variable read searches the global object and its prototype chain.

We consider a translation of a field lookup operation compile⟦x = e1[e2]⟧ where x is a local variable. The translated code to JS explicit is as follows: A field lookup operation first ensures that the given receiver o is a coercible value. If the receiver object is null or undefined, it throws a TypeError exception. Otherwise, the value is either an object value or able to be converted to an object value in the auxiliary function Get. Then, it converts the field name designator s to a string value by calling an operation ToString, and we use corresponding auxiliary function ToString presented in 6a. At last, it uses an auxiliary function for a field lookup operation Get and assigns the result to the local variable x.

1 fn = λ (o ,s) .{ 2 if (o === null || o === undefined )
Rewriting explicit field accesses is not enough to prevent implicit field accesses as JavaScript accesses fields implicitly in many situations. For instance, let us consider the binary operation e1-e2. According to the JavaScript semantics, e1 and e2 have to be converted to a number before applying the subtraction. How to make the conversion depends on the type of e1 and e2. If it is an object, its valueOf field is used, That is, if one of e1 and e2 is an object, the subtraction operation involves implicit access to the valueOf field. This access has to be intercepted and replaced as explicit field accesses. For that, a translation of compile⟦e1-e2⟧ to JS explicit is defined as follows:

1 fn = λ ( lhs , rhs ) .{ The auxiliary function ToNumber presented in Figure 6b guarantees that the result is a number value. Thus, the actual subtract operation lhs -rhs at line 4 of the translated code does not involve implicit field access.

In JavaScript, a function invocation is considered as a method invocation if and only if the syntactic form of the function is an object field access. That is, "obj.met(arg)" is a method invocation and the pseudo argument this will be bound to obj in the body of obj.met. On the other hand, in "var f=obj.met; f(arg)" is not a method invocation but as a regular function call and this will not be bound to obj. This difference between function invocation and method invocation demands the JS explicit compilation to specially treat method invocation. We consider a translation of a method call expression compile⟦x = e1[e2](e3)⟧ where x is a local variable as follows:

1 fn = λ (o , s ) .{ 2 var f ; 3 f = compile⟦o[s]⟧; 4 return ⋄apply(f , o , compile⟦e3⟧) ; 5 }; 6 x = fn (compile⟦e1⟧, compile⟦e2⟧) ;
First, the syntactic part e1[e2] is transformed as regular field lookup operation. Second, when the function is found in the object, the function is invoked in such a way that e1 (the first argument o) is bound to this and e3 as the argument.

IMPLEMENTATION: SecureJS

In this section, we present the SecureJS implementation. SecureJS compiled programs execute as if they were in isolated realms, which do not share any references with other realms. Thus, if a compiled program does not export value to others, executions of the compiled program preserve total memory isolation, and it guarantees that running a compiled program with other uncompiled programs does not interfere with each other.

This isolation relies on a secure runtime environment, which consists of an isolated virtual global object and intrinsic objects, and secure primitive operations, which reroute field accesses for the global and intrinsic objects to corresponding virtual ones. This section details the implementation the secure primitive operations and the runtime environment.

Secure Primitive Operations

The SecureJS compiler rewrites JavaScript programs in such a way that no expression can ever access, explicitly or implicitly, objects created by uncompiled code. For that, the compiled code replaces normal object field access and normal prototype chain lookups with custom operations that enforce memory isolation. Let us detail these operations.

First of all, explicit references to global variables must be replaced with accesses to secure objects that proxy these global plain objects. For that, the compiler transforms a global variable access x into a library function call SJS.Loadvar("x") defined as:

1 SJS . Loadvar = function SJSloadvar ( id ) { 2 return Get ( SJS . global , id ) ; 3 }
The object SJS.global is a secure version of the global object. It ensures that all the interactions with the global object will not be exposed to the uncompiled code.

Second, object field accesses have to be intercepted in order to prevent the normal prototype chain inspection to access objects of the uncompiled environment. For that, we provide a secure version of GetProperty auxiliary function defined as: The crucial point is line 8. It ensures that the field lookup will never escape the memory controlled by the compiled environment. If the search for the field hits the global object that belongs to the uncompiled code, it reroutes the search to another object (line 9) under the control of SecureJS.

For compatibility with current IoT platforms such as JerryScript [START_REF] Gavrin | Ultra Lightweight JavaScript Engine for Internet of Things[END_REF], SecureJS compiles and targets ECMAScript 5 but it also supports a restricted version of the ECMAScript 6 module export form. The export instruction to establish communication channels between compiled and uncompiled code. The compiler transforms a declaration "export id" into:

id = SJS . Loadvar ( " id " )
where the left-hand side id designates the global variable id outside the realm.

The last role of the compiler is to create a secure execution context for the compiled code. For that, the compiled code will be embedded into an anonymous function that will start creating the secure environment and that will then execute client code. That is, all compiled programs have the following shape: ... client compiled code ...

}) () ;

SecureJS compiled code guarantees that any uncompiled expression cannot ever access objects created by compiled code. The variable SJS is hidden in the local scope of the compiled code, and the function SJSbootstrap is immutable and returns a new isolated realm whenever it is called.

Secure Runtime Environment

SecureJS compiled code initializes a secure environment by invoking the SJSbootstrap (see Figure 7, line 42) function at the very beginning of the execution. This function is defined in a library sjs.js that captures native built-in objects and provides secure interfaces for compiled programs. In this section, we present the implementation of that library.

The sjs.js library executes before any other computation. It captures the standard JavaScript functions (line 2-5) and stores them in a function local variables so that they cannot be tampered from outside the library. It creates an immutable field @call to SJScall with the built-in value of Function.prototype.call (line 6) so that the semantics of the call expression SJScall['@call'] also cannot be tampered, and the SJScall['@call'](f,obj,args) implements ⋄apply(f,obj,args) in JS explicit . The library defines the function SJSbootstrap (line 9) that is bound to the global JavaScript variable SJSbootstrap (line 42). The function definition requires two steps, as this is the only way ECMAScript 5 proposes to define read-only variables. The function SJSbootstrap creates a regular JavaScript object (line 18) that will act as a replacement of the standard JavaScript global object inside the secure code.

EVALUATION

This section seeks for an experimental validation that the SecureJS compiler preserves the semantics of the original program and the compiled code complies with memory isolation. First, we test that SecureJS compilation preserves the semantics of the original program in practical JavaScript engines V8 [START_REF]V8 JavaScript Engine[END_REF], Hop [START_REF] Serrano | A Glimpse of Hopjs[END_REF], and Jer-ryScript [START_REF] Gavrin | Ultra Lightweight JavaScript Engine for Internet of Things[END_REF] using the Test262 test suite. Second, we test that a SecureJS compiled program complies with memory isolation by testing that execution of the compiled program does not cause implicit field accesses. For this, we used the Test262 test suite in Hop and JerryScript JavaScript engines.

Experimentation Settings

We implemented SecureJS on top of the front-end of the open-source JavaScript engine Hop compiler [START_REF] Serrano | A Glimpse of Hopjs[END_REF]. SecureJS takes a JavaScript program and generates an ECMAScript 5th specification compatible JavaScript program. Executions are done with state-of-the-art JavaScript engines V8, Hop, and JerryScript.

We use the Test262 test suite and use the es5-tests branch from the github repository. Since the test programs of the Test262 test suites check the program states and flows by means of the assert function, the comparison of the resulting state confirms the equivalent execution of the programs. The Test262 programs also test the semantics of all the ECMAScript built-in functions and the semantics of the strict mode functions. We consider 10490 numbers of the test programs as our target test programs of the Test262 test suite and exclude 1082 numbers of the test programs from the target programs. In particular, we excluded tests using the eval function, the with statement. SecureJS does not support eval and with. Additionally, we excluded tests checking syntactic errors. The latest version of ECMAScript specifies less strict syntactic rules than the syntactic rules specified in ECMAScript 5th. Since the front-end parser of SecureJS supports the latest ECMAScript specification for compatibility, it parses the program that follows the latest EC-MAScript specification and translates it into an ECMAScript 5th compatible program when possible.

Testing Semantic preservation

The goal of this experiment is to show that SecureJS compiler preserves the semantics of an original program. For that, we compiled target test programs of the Test262 suites and ran them on V8, Hop, and JerryScript JavaScript engines, and we checked whether the resulting states of both the program and the corresponding compiled program are equivalent.

Among 10490 numbers of the test programs, V8 passed 10386 successfully. 104 failed because of the semantics differences between the source language test 262 assumed and the latest JavaScript evolutions V8 supports. SecureJS preserves this result. That is, the 10386 successful tests remain successful after SecureJS compilation, and the 104 failed tests remain failed. Hop passed 10414 numbers of the test programs and failed in 76 tests, and JerryScript passed 10474 numbers of the test programs and failed in 16 tests. SecureJS also preserves these results.

Testing Memory Isolation

The SecureJS compiled programs run as if they were running in an isolated realm. If the compiled programs do not intentionally export values for interaction with others, the compiled and other uncompiled programs cannot reference each other. In this section, we test that such SecureJS compiled programs that do not use export comply with this isolation property. For that, we empirically verify that compiled programs ever access objects outside the controlled realm.

For the experiment, we modified the Hop and JerryScript implementations to log all accesses to the [[Prototype]] field that is needed to walk prototype chains. We have used two radically different JavaScript implementations in order to reduce the probability of unnoticed [[Prototype]] accesses that would be removed by the JavaScript engine's optimizer, independently of SecureJS. In addition, we modified the JerryScript engine also to log all accesses to global and intrinsic objects, which are outside of the controlled realm.

We executed all the 10490 programs from the Test262 suite with the instrumented JavaScript engines. We confirmed that there is no field access attempt to global and intrinsic objects. We observed a single situation where [[Prototype]] is implicitly accessed by the programs compiled by SecureJS. During the initialization of a program, an empty object is created with an empty prototype chain by the expression Object.create(null). Later on, this object is used to optimized SecureJS field accesses. Since this object has no prototype chain, the accesses are harmless but are logged by the instrumented engines.

RELATED WORK

A number of studies have been carried out so as to provide memory isolation in JavaScript.

Bhargavan et al. [START_REF] Bhargavan | Language-based Defenses Against Untrusted Browser Origins[END_REF] proposes defensive JavaScript (DJS), which is a small subset of the JavaScript language satisfying static typing constraints. DJS achieves memory isolation by the use of a small subset of the JavaScript language that does not involve dynamic features. The main limitation of DJS is that legacy code needs to be manually rewritten in the DJS subset and be typable in order to achieve memory isolation. A program written in DJS does not rely on a realm and cannot use built-in functions defined in ECMAScript specification.

Swamy et al. [START_REF] Swamy | Gradual Typing Embedded Securely in JavaScript[END_REF] proposes JS ⋆ , which is a programming language supporting various dynamic features of JavaScript, while ensuring type safety in the presence of an untrusted JavaScript program. As it requires type-annotations for the trusted programs, legacy code needs to be manually rewritten in the JS ⋆ , and it supports only a small subset of JavaScript language in terms of the support of built-in functions. It implements a limited form of interfaces for inter-communication since the interface requires typeannotations and must implement the interface functions with the compiled interpreter programs.

Terrace et al. [START_REF] Terrace | Sandboxing Third-Party Scripts[END_REF] implements a JavaScript interpreter written in JavaScript. It supports interactions that use primitive values, typed objects, and functions that has typed argument and return values, and it does not work on the JerryScript engine. For these reasons, it cannot be applied to IoT environments in particular.

Vasilakis et al. [START_REF] Vasilakis | BreakApp: Automated, Flexible Application Compartmentalization[END_REF] proposes BreakApp, which provides isolation and interaction policies between programs. It relies on various levels of built-in isolation primitives, yet the isolation mechanisms strongly depends on Node.js. One of the isolation mechanisms BreakApp relies on is the isolated realm supported by Node.js.

Guha et al. [START_REF] Guha | The Essence of JavaScript[END_REF] proposes a formal semantics of a core calculus, λ J S , and provides a reduction step of JavaScript to λ J S . This reduction step is similar to our translation to JS explicit , but our translation to JS explicit focuses on rewriting primitive operations to their secure versions in order to simulate a JavaScript realm.

CONCLUSION

We presented SecureJS, a secure JavaScript-to-JavaScript compiler. It transforms programs into equivalent ones but that would execute as if they were running inside an isolated realm. This compiler is portable and only uses standard features so it can be used by any JavaScript engine. In order to rewrite the semantics of dynamic features of JavaScript language, we presented JS explicit , which does not involve implicit field accesses, and presented translation from JavaScript to JS explicit . In the evaluation, we showed that the compilation preserves the semantics of the original programs that use full-features of ECMAScript 5.1 and achieves memory isolation if a given program does not export a value. In order to show that executions of the compiled programs preserve memory isolation, we use instrumented JavaScript engines, and to the best of our knowledge, no one has attempted to test such properties before by JavaScript engine instrumentation. SecureJS compiler provides an essential building block to use JavaScript security enforcement libraries that rely on isolated realms, in particular, it enables us to use such libraries in JerryScript JavaScript implementation, which does not support a built-in isolation mechanism.

3 4

 3 true [ o ] === 10;

e

  ::= x | x д | v ∈ V prim | this | e ⊕ e | ⊖ e | ⋄ hasOwnProperty e 1 e 2 | ⋄ getPrototypeOf e | ⋄ toString e | ⋄ toNumber e | ⋄ toBoolean e i ::= var x | x = e | x д = e | x 1 = ⋄alloc(x 2 ) | e 1 [e 2 ] = e 3 | x = e 1 [e 2

Figure 2 :

 2 Figure 2: An excerpt from semantics rules for expressions

2 var result , getter ; 3 O 8 return result 9 } else { 10 getter 13 return result 14 } 15 }

 238910131415 ) Let desc be the result of calling the [[GetProperty]] internal method of O with property name P. (3) If desc is undefined, return undefined. (4) If IsDataDescriptor(desc) is true, return desc.[[Value]]. (5) Otherwise, IsAccessorDescriptor(desc) must be true so, let getter be desc.[[Get]] (see 8.10). (6) If getter is undefined, return undefined. (7) Return the result calling the [[Call]] internal method of getter providing base as the this value and providing no arguments. (a) [[Get]] internal method 1 Get = λ (O , P ) . { = ToObject ( O ) ; /* (1) */ 4 var desc = GetProperty (O , P ) ; /* (2) */ 5 if ( desc === undefined ) return undefined ; /* (3) */ 6 if (⋄hasOwnProperty desc " value " ) { /* (4) */ 7 result = desc [ " value " ]; = desc [ " get " ]; /* (5) */ 11 if ( getter === undefined ) return undefined ; /* (6) */ 12 result = ⋄apply( getter , O , []) ; /* (7) */ (b) The function Get written in JS explicit

Figure 3 :

 3 Figure 3: The specification of [[Get]] internal method and its meaning written in JS explicit

3 throw

 3 TypeError () ; 4 s = ToString (s ) ; 5 x = Get (o , s); 6 }; 7 fn (compile⟦e1⟧, compile⟦e2⟧)

2 lhs=

 2 ToNumber ( lhs ) ;

1 6 O 9 O

 69 SJS . GetProperty = function SJSGetProperty (O , P) { 2 var prop ; 3 prop = SJS . getOwnPropertyDescriptor (O , P ) ; /* (1) */ 4 if ( prop !== undefined ) return prop ; /* (2) */ else { = SJS . getPrototypeOf ( O ) ; /* (3) */ 7 if (O === null ) return undefined ; /* (4) */ 8 if ( SJS . securePrototypeOf ( O ) !== undefined )

(

  function () { var SJS = SJSbootstrap () ;

1 ( function () { 2 var 3 var 4 var 5 var 7 {

 23457 SJScreate = Object . create ; SJScall = Function . prototype . call ; SJSObjProto = Object . prototype ; SJSFunProto = Function . prototype ; ... 6Object . defineProperty ( SJScall , ' @call ', value : SJScall , configurable : false , 8 writable : false , enumerable : false }) ; SJScreate ( null ) ; 19 var SJS = SJScreate ( null ) ; 20 SJS . global = global ; 21 function CheckObjectCoercible ( o ) {...}; 22 function Get ( x ) {...}; 23 function DefaultValue_S ( x ) {...}; 24 function ToString ( o ) {...}; 25 function ToNumber ( o ) {...}; 26 function ToInteger ( o ) {...}; 27 SJS . Loadvar = function ( id ) {...}; 28 SJS . GetProperty = function (O , P ) {...}; 29 global . Object = function ( v ) {...}; , configurable : false , 45 writable : false , enumerable : false }) ; 46 }) () ;

Figure 7 :

 7 Figure 7: An excerpt of sjs.js.

SAC' 21 ,

 21 March 22-March 26, 2021, Gwangju, South Korea Y. Ko et al.

  The semantics of ToObject creates an instance of Boolean intrinsic object by calling new Boolean(true), and an internal field [[Prototype]] 6 of the created object is set to the reference of Boolean.prototype.(2) It applies the internal operation ToString to the field name designator o to dynamically convert the value to a string. The semantics of ToString implicitly accesses the field toString of the object o and calls it. As we defined at line 2, the function returns a string "x".

https://jerryscript.net

https://duktape.org

https://www.ecma-international.org/ecma-262/#sec-code-realms

We intentionally do not provide eval and with constructs.

https://gitlab.inria.fr/securejs/sjs-compiler

In ECMAScript specification, internal field and method names are presented with a double square brackets [[Name]]. These methods and field names are not allowed to be called or accessed directly from JavaScript programs but callable or accessible from other internal methods or operations.

* This research has been partially supported by the ANR17-CE25-0014-01 CISC project, the Inria Project Lab SPAI, and the European Union's Horizon 2020 research and innovation programme under grant agreement No 830892.

Y. Ko et al.

When the [[GetProperty]] internal method of O is called with property name P, the following steps are taken:

(1) Let prop be the result of calling the [[GetOwnProperty]] internal method of O with property name P. Support for ECMAScript built-in functions. The ECMAScript builtin functions also rely on the primitive operations defined above, and the semantics involves implicit field access. For instance, let us consider the slice method of the String API. According to the specification [START_REF]ECMA-262: ECMAScript Language Specification[END_REF], when this method is invoked, the this argument must be converted into a string and the arguments into integers. These conversions have to be protected too. For that, the original slice function (String_prototype_slice) is protected by a JS explicit wrapper defined as: All JavaScript functions involving conversion and field accesses are wrapped similarly.

Translation to JS explicit

We present translation function compile⟦P⟧ that takes JavaScript code P and translates it into JS explicit .

First, we consider explicit references to global variables, e.g., Object, Function, or String. These explicit references are replaced


Olivier Allix
email: olivier.allix@ens-paris-saclay.fr

Maxime Blanchard
email: maxime.blanchard@safrangroup.com

Pierre Gosselet
email: pierre.gosselet@univ-lille.fr

Lmt

Safran

A non-intrusive global/local cycle-jumping techniques: application to visco-plastic structures

I've had the privilege to interact closely with Peter Wriggers for fifteen years or so, as for the IRTG 1627 [11]. I now have the great pleasure and honor to work with him on exciting projects, for example on the Virtual Element Method. I am every year more impressed by the depth and breadth of his research, but also by his avant-gardiste

Introduction

In order to correct the drawbacks of the submodeling technique while keeping its simplicity and flexibility, a non-invasive method was proposed which allows exact local/global analysis while making use of the same basic tools inside an iterative procedure [START_REF] Gendre | Non-intrusive and exact global/local techniques for structural problems with local plasticity[END_REF]. It was extended in several directions, notably in [START_REF] Passieux | Local/global non-intrusive crack propagation simulation using a multigrid x-fem solver[END_REF][START_REF] Guguin | Nonintrusive coupling of 3d and 2d laminated composite models based on finite element 3d recovery[END_REF][START_REF] Duval | Non-intrusive coupling: recent advances and scalable nonlinear domain decomposition[END_REF][START_REF] Gerasimov | A non-intrusive global/local approach applied to phase-field modeling of brittle fracture[END_REF][START_REF] Noii | An adaptive global-local approach for phasefield modeling of anisotropic brittle fracture[END_REF]. Safran Aircraft Engines was interested in exploring its potential for the detailed analysis of complex structures undergoing viscoplastic strains that can spread over the whole structure.

The quality of the integration of viscoplastic models is very sensitive to the time step. The global and local models do not need the same type steps to achieve the same precision. To handle this issue, we proposed in [START_REF] Blanchard | Space/time global/local noninvasive coupling strategy: Application to viscoplastic structures[END_REF] a space/time global/local non-invasive coupling strategy that we try to extend to cycle-jumping.

For the class of material that we study, one may observe locally accommodation (elastic response around the hardened position), adaptation (stable viscoplastic cycle), or even ratcheting (the viscoplastic cycle evolves continuously). In general, the structure experiences large variations during the firsts cycles, with potentially strong stress redistribution. After that, the evolution is much smoother. The principle to reduce the computational cost is, after the first cycles, to extrapolate the response of the structure over a certain number of cycles [START_REF] Saï | Modèles à grand nombre de variables internes et méthodes numériques associées[END_REF][START_REF] Dunne | Efficient cycle jumping techniques for the modelling of materials and structures under cyclic mechanical and thermal loading[END_REF]. As such, the technique has the potential for high efficiency but depends strongly on the choice of the criteria to decide the number of cycles which can be skipped. In [START_REF] Cognard | A large time increment approach for cyclic viscoplasticity[END_REF][START_REF] Bhattacharyya | A kinetic two-scale damage model for high-cycle fatigue simulation using multi-temporal latin framework[END_REF] such drawback is alleviated by controlling the time interpolation using the Latin Method but the latter is quite intrusive.

The paper is organized as follows. In Section 2, the constitutive law, the structural example and the reference model are presented. The main lines of the proposed cycle-jumping method are given in Section 3. The principle of the coupling with the two-scale in time and space global/local approach is discussed and illustrated in Section 4. Conclusion and perspectives are provided in Section 5 on the basis of the cycle-jumping procedure applied to a 3D example.

Reference problem and solution

The material model used is the one proposed in [START_REF] Longuet | Incremental lifing method applied to high temperature aeronautical component[END_REF], adapted from the Marquis-Chaboche's behavior [START_REF] Chaboche | Constitutive equations for cyclic plasticity and cyclic viscoplasticity[END_REF].The elasticity itself is linear and isotropic. The nonlinear part of the model is ruled by the yield function based on von Mises criterion. The plastic strain tensor 𝜖 𝑝 is split into a fast part ( 𝑓 ) and a slow part (𝑠) with the associated values of the cumulated plasticity 𝑝 as follows:

𝜖 𝑝 = 𝜖 𝑝 𝑓 + 𝜖 𝑝 𝑠 𝑎𝑛𝑑 𝑝 𝑖 = ∫ 𝑡 0 √ 3 2 𝜖 𝑝 𝑖 : 𝜖 𝑝 𝑖 𝑑𝜏 with for 𝑖 ∈ { 𝑓 , 𝑠} (1)
The kinematic hardening 𝑋 = 𝑋 𝑓 is only related to the fast cumulated plasticity and follows an Armstrong-Frederick's formulation. The fast plasticity dominates for strain rates in the range 10 -5 , 10 -2 𝑠 -1 whereas the slow one dominates in the range 10 -9 , 10 -5 𝑠 -1 . The material of interest being confidential, we make use of the parameters given in [START_REF] Lemaitre | Mécanique des matériaux solides 3 • édition[END_REF] for a nickel based superalloy IN100 evolving at 800 • C which is the mean temperature value during a flight.

In order to precisely assess the lifespan of the structure, a damage criterion should be added as in [START_REF] Yue | A fatigue damage accumulation model for reliability analysis of engine components under combined cycle loadings[END_REF]. The 2D example of Figure 1 is used in the paper. The example of this paper corresponds to fatigue with adaptation because the viscous effects due to large plasticity dominate the response at the considered high temperature regime. As a first approximation, we consider that the structure is stabilized when the maxima of both total plastic strain and displacement increments are respectively below 10 -6 and 10 -5 , which occurs at about 150 cycles in this example.

Summary of the chosen cycle-jumping technique

In what follows, 𝑌 𝑖 (𝑐) denotes the value of the internal variable 𝑌 𝑖 at the end of cycle number 𝑐, 𝑌 𝑖 (𝑐) = 𝑌 𝑖 (𝑐) -𝑌 𝑖 (𝑐 -1) approximates its "derivative" and 𝑌 𝑖 (𝑐) = 𝑌 𝑖 (𝑐) -𝑌 𝑖 (𝑐 -1) its "second derivative". In this section, we try to summarize the chosen cycle-jumping technique which is adapted from [START_REF] Cojocaru | A simple numerical method of cycle jumps for cyclically loaded structures[END_REF]. Note that the straight procedure as described in that paper fails in our examples, which stresses the difficulty of setting a proper cycle-jumping procedure:

1. The first aspect is the choice of a pertinent internal variable, or set of internal variables, to estimate the number of cycles Δ𝑐 which can be skipped. In our case, it appears that the best choice is the fast cumulated plasticity 𝑝 𝑓 computed at the end of cycles (the evolution of this quantity constitutes the shakedown curve as shown in Figure 2). 2. At any stage of the process, the computation of the possible jump is made after the full computation of three cycles. To compute the jump Δ𝑐, one first eliminates the Gauss points that are stabilized, that is for which 𝑝 𝑓 < 10 -12 . The remaining set of Gauss points is denoted by GP. The chosen value is then

Δ𝑐 = 𝑞 𝐸 𝑥𝑡𝑟 𝑀𝑒𝑎𝑛 𝐺 𝑃 𝑝 𝑓 [𝑐 ] 𝑝 𝑓 [𝑐 ] .

Coupling with the global/local method

The nonlinear global/local non-invasive coupling proposed in [START_REF] Blanchard | Space/time global/local noninvasive coupling strategy: Application to viscoplastic structures[END_REF] is used in order to insert structural details given by local models into the global coarse representation of the whole structure, see Figure 1. Thanks to an iterative coupling the solution obtained by the separate models converges toward the reference. In order to improve the performance, as explained in the introduction, the solutions are weakly coupled in time: the synchronization only occurs at the time steps necessary for the global model, see [START_REF] Blanchard | Space/time global/local noninvasive coupling strategy: Application to viscoplastic structures[END_REF] for more details.

The quality of the integration of viscoplastic models is very sensitive to the size of the time steps. The global and local models do not need the same type steps to achieve the same precision regarding the integration. Moreover, if one does not achieve a compatible precision between the two models, the local-global procedure may not converge to the reference. To handle this problem, we proposed and compared in [START_REF] Blanchard | Space/time global/local noninvasive coupling strategy: Application to viscoplastic structures[END_REF] various space/time global/local non-invasive coupling strategies. The most efficient one, called weak time-coupling, which allowed us to achieve the desired precision, is schematized in Figure 3. Figures 5 and6 compare the von Mises stress and the cumulated plasticity at the last cycle for the reference and cycle-jumping procedures. The maximum relative errors are respectively about 2% and 0.4% compared to a fine monolithic computation. Note that the computation is never stopped just after a jump, but after few normal cycle computations in order to let plastic redistribution smooth the solution.

Conclusion

Our experience of cycle-jumping is that it is still an art to define a proper procedure. Maybe this is due to the severity of the chosen example which reaches nearly perfect viscoplasticity on some critical areas of the structure. For too large jumps or not precise enough extrapolations, rebalance may not even be possible. Our proposed procedure leads to satisfactory results in terms of precision even if the factor of 4 for the gain that we obtained is not as high as what can be observed on examples from the literature about plasticity.

Let us note that it seems that 2D cases are more severe than 3D cases. This may be due to the fact that in 3D examples, a whole section never fully evolves in a plastic manner. This is at least what appears from our first experiments concerning the application of the proposed cycle-jumping procedure on a global 3D example of 1.510 6 degrees of freedom over 50 cycles (see Figure 7). In this example, the exact same procedure as the one defined in section 3 was applied. What is still lacking, and which would probably imply a more intrusive procedure, is to include an evaluation of the quality of the solution within the process.

Fig. 1 :

 1 Fig. 1: Monolithic approach: reference model and definition of one cycle.

3 .

 3 The quality factor 𝑞 𝐸 𝑥𝑡𝑟 is computed once for all from the previous formulae by forcing a first jump of fixed length Δ𝑐 = 2 after the first three cycles. 4. To extrapolate the whole set of internal variables, we consider a first approximation, denoted Ỹ 𝑖 , of the slope after the jump of any internal variable Ỹ 𝑖 𝑌 𝑖 (𝑐) +𝑌 𝑖 (𝑐)Δ𝑐. The slope used to extrapolate 𝑌 𝑖 is defined as 0.7𝑌 𝑖 + 0.3 Ỹ 𝑖 that is 𝑌 𝑖 (𝑐 + Δ𝑐) ≡ 𝑌 𝑖 (𝑐) + (0.7𝑌 𝑖 + 0.3 Ỹ 𝑖 )Δ𝑐. 5. After the jump, one computation is needed to rebalance the structure starting from the extrapolated values of the set of internal variables, before computing the next three cycles.

Figure 2

 2 Figure 2 illustrates the first three aspects of the process.

Fig. 2 :

 2 Fig.2: The values at the end of cycles (left, red dots), constitute the shakedown curve (middle), for the selected Gauss point (right).

Fig. 3 :

 3 Fig. 3: Schematization of the weak-time coupling strategy

Fig. 4 :

 4 Fig. 4: Overall view of the computed and skipped cycles.

Fig. 5 :

 5 Fig. 5: Accuracy obtained with the cycle-jumping method: von Mises stress.

Fig. 6 :

 6 Fig. 6: Accuracy obtained with the cycle-jumping method: total cumulated plasticity.

Fig. 7 :

 7 Fig. 7: Application of the proposed cycle-jumping procedure to a 3D global model.

Acknowledgements This work was supported by Safran Aircraft Engines as part of the MAIA-MM1 research program.