H Basson

M Bouneffa

M Matsuda

A Ahmad

D Chung

E Arai

Qualitative Evaluation of Manufacturing Software Units Interoperability using ISO 25000 Quality Model

Keywords: Manufacturing Software Units, Quality of Interoperability, ISO 25000 series, Quality Model, ISO 16100 series

In the context of development and evolution of hetergeneous industrial systems, the quality of interoperability among manufacturing software units is a major concern. Qualitative characteriscs of the interoperability such as reliability, functionality, performance, and security are necessary for the assurance of high quality of the developed manufacturing applications. The implemented interoperability among various software units of manufacturing applications often have various quality criteria. Therefore, an adequate qualitative modeling is required to satisfy the qualitative evaluation of the interoperability. This paper presents the use of quality model developed in respect of quality standard ISO 25000 series as a means to permit the comprehensive evaluation of interoperability of the applications developed regarding the ISO 16100 standard series.

Introduction

The functional and qualitative characteristics of interoperability cover a wide range of possible capabilities according to the considered types of system, their description level, and their organizations. In the manufacturing domain, along with the evolution of software applications in various activities domains, the interoperability has become a major critical aspect influencing the quality of working systems. Various definitions have been proposed for the interoperability, as illustration, Kurt Kosanke cited 22 different definitions extracted from the literature on the topic [START_REF] Kosanke | ISO Standards for Interoperability: a Comparison[END_REF]. For its specified domain, an important work has been realized by the US DoD to propose a schema called LISI (Levels of Information Systems Interoperability) [START_REF] Kasunic | Assuring Systems Interoperability: Challenges and Opportunities[END_REF] where the interoperability was defined as "The ability of systems, units or forces to provide services and accept services from other systems". The IEEE definition designates the interoperability as the "ability of two or more systems or components to exchange information and to use the exchanged information".

The present work considers mainly the manufacturing applications for which the constituting manufacturing software units may require interoperability facilities among units for the application development and use. More precisely, the interoperability mechanisms such as data exchange, messages communication, services calls, etc. may need to focus on the quality of interoperability and its functioning between concerned manufacturing application units.

The interoperability multiplicity of levels inevitably encourages the standardization activities [START_REF] Erwin | State of the art on semantic IS standardization, interoperability & quality[END_REF]. Effectively, the governing bodies have always encouraged and supported the standardization to insure an integration of multiple heterogeneous systems to operate as a coherent whole.

In this paper, we focus on the standards, dedicated to interoperability of manufacturing software units and the standards that can be used for the qualitative evaluation. The major goal is to use adequate recognized standards to examine the proposed practices for system integration through interoperability and to evaluate its quality using ISO recommended practices. Primarily, our work considers the ISO 16100 series standard [START_REF] Matsuda | Software Interoperability Tools: Standardized Capability-Profiling Methodology ISO16100[END_REF] to propose an approach and reference model to assure better qualitative level of interoperability solutions to reach better integration of manufacturing systems. The present work considers the association of these applications with the qualitative characteristics of the ISO/IEC 25000 standard [START_REF]Software engineering -Software product Quality Requirements and Evaluation (SQuaRE) -Data Quality model[END_REF] providing one of the most exhaustive models for software quality characteristics. The major goal remains to enhance the competency of application designer using the ISO 16100 series approach while considering the quality of interoperability of working application software units.

The rest of the paper is organized as follows: the section 2 is dedicated to describe the ISO 16100 series. The corresponding approach advocates the use of standardized manufacturing software units to build integrated manufacturing applications. The section 3 presents the ISO/IEC 25000 series software quality standards. In section 4, we briefly show how to associate, the quality characteristics as designed in reference to ISO/IEC 25000, with the manufacturing software units developed according to the ISO 16100. The section 5, describes the prototype scheme of the proposed approach where the implementation is based on the linked data and ontologies. The conclusion is given in section 6.

The interoperability of manufacturing applications: approach as per ISO 16100 standard

The ISO 16100 standard series defined an approach to insure the interoperability of software applications that can be used in manufacturing domain. The central element of this approach consists of the implementation of a repository or distributed catalogue of software units called MSUs (Manufacturing Software Units). The MSUs are used by the vendors and the application developers of the manufacturing systems to construct their applications. These MSUs are indexed by profiles so that they could be located according to a search criteria. These criteria describes the functionalities assured by the MSUs and other quality criteria such as reliability, performance, etc. Obviously, the MSUs are distributed on multiple vendors that can be geographically apart. It is therefore necessary to adopt a standardized vocabulary to elaborate the indexation profiles of these MSUs. In this regard, the ISO 16100 standard adopts the following approach:

• Define a data dictionary, called MDD (Model Data Definition), which can be considered as an ontology regrouping the most significant elements of a given domain. These elements represent the processes, activities, and the resources that can be used in a given domain.

• Elaborate the taxonomy of the regrouped capability elements in a hierarchical structure of capability classes. A capability class encapsulates actvities or functions i.e. "elaborate a fabrication sequence" to be performed. It must also take into account certain qualitative criteria such as response time, optimal use of resource use, etc. to be assured. In its definition the capability class is linked to the MDD elements. The profile of a software unit in this regard is an instantiation of one or more capabilities classes, which might be serialized in XML format, etc. A more detailed description of ISO 16100 can be found in [START_REF]) Industrial automation systems and integration -Manufacturing software capability profiling for interoperability[END_REF]. 1.1 shows the structure of a profile in terms of capabilities. This structure represents a template that a profile may instantiate with the associated values of each element. Different elements involved in a profile describe also the MSU identification, used language, and its vendor, etc. The various profile indications on MSU structure and some quality criteria are related to capability classes that are implemented by the MSU along with its associated constraints. We can also remark that the quality characteristics in regard to the interoperability (intrinsic to the MSU) can only be invoked across a list of objects or entities of the MDD. We can assume that such objects may represent a software artifact like a data bus, a database connection, or a web service, etc. For instance, it is difficult to establish the associated quality of interoperability not only within a software unit, but also in the constituted application. In the following section, we present our approach that emphasizes the use of quality standard ISO 25000 to elaborate the guidelines for the evaluation of interoperability of MSUs developed according to the ISO 16100 series.

Adaptation of ISO 25000 Quality Model for Interoperability Validation of MSUs

The interoperability validation process requires to examine the correspondance between the specified qualitative requirements of interoperability between MSUs and its relevant implementation.

A major aim of our work is to provide guidelines and to illustrate the series of ISO 25000 quality standards addressing all aspects related to: Quality requirements specification, Quality model, Product Quality, Quality evaluation, and Quality measurement. For each quality aspect, a set of ISO standards has been elaborated where a set of standards constitutes a "Division" aiming at a specific aspect related to system or software quality [START_REF]Software engineering -Software product Quality Requirements and Evaluation (SQuaRE) -Data Quality model[END_REF].

The ISO 25000 series of standards have been supported with the framework, SQuaRE (Software product Quality Requirements and Evaluation). The objective of SQuaRE is to help the practice of main concepts and models provided by ISO 25000. SQuaRE is composed of five divisions intended to cover the wide range of aspects related to System and Software Quality Specification, as well as its modeling, assessment, and measurement (Fig. 1.1).

Fig. 1.1. Global Architecture of ISO 25000 SQuaRE

The ISO norms of SQuaRE make distinction between three major types of quality (as shown in Fig. 1.2) reflecting the perception of the quality by the developers and users. The major quality types are the quality in use, the external quality, and the internal quality. SQuaRE proposes to examine the conformity of the each quality type between expected specified quality of system or software and the effective quality of implemented system or software, in order to validate the developed interoperability of manufacturing application. At each hierarchical quality level a quality model is built in terms of quality characteristics, subcharacteristics, and properties.

For this goal, ISO/IEC 25010 proposes a generic quality model along with the corresponding characteristics and sub-characteristics for the concerned major quality levels i.e. internal quality, external quality, and quality in use. These quality models are to be instantiated and adapted in respect to the interoperability of the MSUs of the manufacturing application under consideration. The generic quality model, to be instantiated, proposes six characteristics and 27 sub-characteristics. These indicate the links of dependency between each individual characteristic and the corresponding sub-characteristics. The six major quality characteristics are adapted to interoperability, as shown in Table 1.2. SQuaRE proposes the breakingdown of the characteristics into sub-characteristics, which is adapted to the interoperability quality, as stated below:

The quality engineer of the current application defines each individual subcharacteristic. It specifies its contextual meaning and the way to assess the extent to which each characteristic is met. Moreover, in a given application, subcharacteristics may have different priorities. The priority of each individual subcharacteristic depends on the hierarchical scale established between subcharacteristics according to the specific functional and qualitative priorities of the current manufacturing application.

Table 1.2 Characteristics and Sub-Characteristics of SQuaRE schema adopted

for the quality of interoperability between MSUs.

Quality Characteristics of MSU interoperability

Description

Quality Sub-Characteristics of MSUs Interoperability

Functionality

The capability of the MSUs to provide functions and interoperability which meet stated and implied needs when the MSUs are used under specified conditions.

Suitability Accuracy Security

Reliability

The capability of the MSUs to provide functions and interoperability which meet stated and implied needs when the MSUs are used under specified conditions.

Testability Fault Tolerance Recoverability

Usability

The capability of the MSUs interoperability to be understood, used, and appreciated by the developer.

Understandability Learnability Testability

Efficiency

The capability of the MSUs interoperability to provide the required performance relative to the amount of resources used, under stated conditions.

Time Behavior Resource Utilization

Maintainability

The capability of the MSUs interoperability to be modified.

Adaptability Analyzability Changeability Testability

Portability

The capability of the MSUs interoperability to maintain its behavior when hosted on a different hosting environment.

Adaptability Installability Replaceability

To each individual sub-characteristic the quality engineer adapts a set of metrics addressed to quantitatively assess the extent to which a sub-characteristic is met in reference to the expected values decided at the phase of qualitative requirements specifications.

The Interoperability quality evaluation is based on the three quality tree-like hierarchical structure instantiated by the quality engineer for the quality in use, external quality, and internal quality. Fig. 1.2 shows the procession of the interoperability validation as indicated by SQuaRE schema.

Fig 1.2. Evaluation of interoperability quality

For the selection of measures for the characteristics of interoperability, the Quality Measurement Division defined in ISO/IEC 25020 covers the mathematical definitions and guidelines for practical measurements of internal quality, external quality, and quality in use. In addition, it includes the definitions for the basic primitive measurements, and is able to formulate the all possible measures. By applying the guidelines of Quality Measurement Division, a set of basic and derived measures is to be defined to select metrics for evaluation of the internal quality, external quality, and the quality in use.

Classification of quality evaluation metrics

We propose to adapt a layered model [START_REF] Ahmad | Towards an integrated qualityoriented modeling approach for software evolution control[END_REF] for the qualitative evaluation of interoperability of MSUs. As shown in Fig. 1.3, it is comprised of a core and two layers. The core is called Basic Metrics Set (BMS). BMS is composed of elements where each basic metric can not be calculated using other defined metrics. Each metric examines the extent to which a quality characteristic (or sub-characteristic) of interoperability is reached. It can be observed that the base metrics are insufficient for evaluating diverse interoperability qualities. Two layers of metrics can be used to serve the purpose: the set of Widely-Used Metrics (WUM) and the set of User-Defined Metrics (UDM). The WUM is comprised of the proposed metrics in the literature and widely used in the industry. An element of WUM is a function parameter of either one or more MSUs for interoperability evaluation, or one or more metrics belongning to the set BMS.

The Table 1.3 summarizes basic metrics frequently used to measure software systems interoperability. Similarly, examples of mostly used metrics and user defined metrics are listed in Table 1.3.

Prototyping Issues

In order to validate the proposed approach of evaluating the qualitative characteristics of MSU interoperability, a prototype tool is under development to validate the proposed approach based on ISO 16100 and further extended in reference to ISO 25000 model. The general architecture of the framework and its components are described in Fig. 1.4. The architecture represents the modeling of interoperability quality. The implementation strategy considers that the vendors of MSUs publish their profile on Internet in form of linked data. It allows the construction of a large collection of MSUs, which can be accessed via the semantic web tools, such as the SPARQL queries [START_REF]The SPARQL 1.1 Query Language, W3C Recommandation[END_REF]. The adapted implementation approach considers mainly two constituents:

• A knowledge base which is composed of two major parts:

(1) A database of linked data which is a distributed collection of RDF (Resource Data Framework) [START_REF]RDF 1.1 Concepts and Abstract Syntax[END_REF] files, representing the template classes of capability, their instances, which in fact are the profiles of MSU and the interlinking qualitative characteristics.

(2) A set of three ontologies, specified by the OWL (Web Ontology Language) [START_REF]OWL Web Ontology Language Overview, W3C Recommandation[END_REF] and which explicitly describe the semantics of each capability class, the Model Data Dictionary (MDD) and the modeling of the interoperability quality. Indeed, the profile templates are the RDF files, where the elements or tags have the semantics defined by the ontologies of capability classes. These are referred to the entities defined by the MDD. Similarly, the semantics of the qualitative characteristics are defined by ontologies of quality. • Profiles and templates which allow the manipulation (creation, modification, and deletion) of the profiles and templates, along with a tool to search the MSU profiles. These two tools use the SPARQL language to query the RDF files and OWL. We also use Gravity 1 that allows a graphical exploitation of the linked data, in graph-oriented forms. The MSUs vendor may use a profile or template manipulation tool to find the best template instance, in order to create a profile for its MSU. In case if the template exists already, the vendor may proceed to instantiate it with the provision of respective specific data.

Conclusion and Perspectives

For an adequate modeling of the qualitative evaluation of the interoperability among the Software Units of a manufacturing application, we adapted and used a quality model developed in respect of quality standard ISO 25000 series. The used model is exhaustive, therefore, it requires a good experience in software quality evaluation. The proposed use of metrics examine the extent of each interoperability characteristic or sub charcateristic. Metrics are structured into layers for better traceability of adapted quality measurements. The work aims at permetting the developers to search the MSUs based not only on the functional capabilities characteristics but also on qualitative estimation of MSU interoperability characteristics. The proposed work is directly related to the activities of ISO-TC 184/SC 5/WG4 aiming at the development of ISO 16300 series with the perspective of integrating the work on Data Quality in ISO 8000, elaborated by ISO-TC 184/SC4.

Fig 1 . 3 .

 13 Fig 1.3. Classification of Interoperability quality metrics

Fig. 1 . 4 .

 14 Fig. 1.4. Global Architecture of the Framework

Table 1 .

 1

	Common Part
	Template ID
	Capability Class Name and Reference CCS
	Software Unit ID
	Vendor Name
	Version Number & History
	Computing Facilities Required
	Processor
	OperatingSystem&Options
	Language
	RuntimeMemory
	DiskSpace
	MultiUserSupport
	RemoteAccess
	AddOns&PlugIns
	Measured Performance of the Unit
	ElapsedTime
	NumberOfTransactionsPerUnitTime
	Reliability Data of the Unit
	UsageHistory
	…………….
	Support Policy
	Price Data
	Capability Class Reference Dictionary Name

1. Structure of a "Software Unit Profile".

Table 1 . 3 .

 13 Some Basic Metrics (BMS)

	Metric	Semantic	Formula
		The number of input data
	FUN_INDE	elements of MSU i (the ith MSU of the current	FUN_INDE(MSU i )
		application).
	FUN_OUTDE	The number of output data elements of MSU i .	FUN_OUTDE(MSU i )
		The number of ports of
	MSU_PORT_IN	message reception of	FUN_PORT_IN(MSU i )
		MSU i .
	MSU_PORT_OUT	The number of ports of message sending of the MSU i .	MSU_PORT_OUT (MSU i )
		Lowest number of
	NB_MinR_MSU	messages to be received	NB_MinR_MSU(MSU i )
		by an MSU i.
	MSU_XMLR	Number of XML files read by an MSU i .	MSU_XMLR(MSU i )
	MSU_XMLW	Number of XML files written by an MSU i .	MSU_XMLW(MSU i )

1http://semweb.salzburgresearch.at/apps/rdf-gravity/


Frédéric Besson

Thomas Jensen

Julien Lepiller

Modular Software Fault Isolation as Abstract Interpretation

Software Fault Isolation (SFI) consists in transforming untrusted code so that it runs within a specific address space, (called the sandbox) and verifying at load-time that the binary code does indeed stay inside the sandbox. Security is guaranteed solely by the SFI verifier whose correctness therefore becomes crucial. Existing verifiers enforce a very rigid, almost syntactic policy where every memory access and every control-flow transfer must be preceded by a sandboxing instruction sequence, and where calls outside the sandbox must implement a sophisticated protocol based on a shadow stack. We propose to define SFI as a defensive semantics, with the purpose of deriving semantically sound verifiers that admit flexible and efficient implementations of SFI. We derive an executable analyser, that works on a per-function basis, which ensures that the defensive semantics does not go wrong, and hence that the code is well isolated. Experiments show that our analyser exhibits the desired flexibility: it validates correctly sandboxed code, it catches code breaking the SFI policy, and it can validate programs where redundant instrumentations are optimised away.

Introduction

A fundamental challenge in system security is to share computing resources and run programs from various level of trusts, some untrusted or even malicious, on the same host machine. In this context, it is desirable to isolate the different programs, limit their interactions and ensure that, whatever the behaviour of imported code, the security of the host machine cannot be compromised. There exist many isolation mechanisms available at the hardware, virtual machine or operating system level. In this paper, we consider Software Fault Isolation (SFI), an isolation mechanism pioneered by Wahbe et al. [START_REF] Wahbe | Efficient software-based fault isolation[END_REF] and further developed in Google's Native Client (NaCl) [START_REF] Yee | Native client: A sandbox for portable, untrusted x86 native code[END_REF][START_REF] Sehr | Adapting software fault isolation to contemporary cpu architectures[END_REF] and others. SFI is a flexible and lightweight isolation mechanism which does not rely on hardware or operating system support. Instead, it relies on a static, untrusted, program instrumentation that is validated at load-time by a trusted binary verifier. Compared to other isolation mechanisms, SFI allows the safe execution of trusted and untrusted code within the same address space, thus avoiding costly context switches with kernel code.

The general SFI architecture is shown in Fig. 1 together with some typical sandboxing code. The SFI transformation is performed at compile-time. It s t a t i c i n l i n e i n t sandbox ( i n t p ) { r e t u r n (& s f i + ( p & 0 b11111111 ) ) ; } Fig. 1: SFI chain with typical sandboxing code instruments every memory access so that it is performed inside the memory sandbox. To ensure that a pointer p is within the sandbox variable sfi that is 2 8 bytes aligned and 2 8 bytes wide, the code increments the base address sfi of the sandbox with the 8 least significant bits of the pointer p extracted by masking p using a bitwise &. Control-flow transfers are instrumented so that the code does not jump outside the code sandbox. At load-time, a binary verifier rejects code that is not correctly instrumented. From a security standpoint, only the binary verifier is part of the Trusted Computing Base (TCB). State-of-the-art SFI verifiers trade precision for simplicity and speed, and only perform a linear scan of the binary code. Therefore, the verifiers enforce very strong sufficient conditions for isolation. This has the side-effect that the SFI transformation is performed late in the compiler backend and that the isolated code cannot be optimised. The verifiers perform very local reasoning, and hence cannot verify that function calls, especially between trusted and untrusted code, abide to calling conventions. As a result, trusted code needs to implement a specific protocol for parameter passing and set up its own private run-time stack. This requires low-level platform-specific support and, most notably, increases the run-time overhead of context switches between untrusted and trusted code.

In this paper, we propose a relaxed definition of SFI where trusted and untrusted code may share the same runtime stack but must still respect the isolation properties of the sandbox and abide to calling conventions. Based on this definition, we define an intra-procedural binary verifier which enforces isolation. The verifier implements a static analysis and is using a weakly relational domain in order to verify that calling conventions are satisfied. A difficulty is to ensure that the isolation property holds even in the presence of stack overflow. This is done by ensuring that all stack overflows are caught by so-called guard zones, placed at both ends of the stack. The binary verifier is more flexible than state-of-the-art SFI verifiers and, in particular, is able to validate code where redundant sandboxing instrumentations are optimised away by compiler passes. Our contributions can therefore be phrased as follows:

-A defensive semantics which formalises a relaxed Software Fault Isolation property where the runtime stack is safely shared between trusted and untrusted code. -An intra-procedural abstraction which ensures that the defensive semantics cannot go wrong. -An executable binary verifier, working on a per-function basis, that is more flexible than state-of-the-art binary verifiers for SFI.

The rest of the paper is organised as follows. In Section 2, we define our SFI property by means of a defensive, instrumented semantics. To enable a modular verification, we present in Section 3 an intra-procedural abstraction of the defensive semantics. It is further abstracted in Section 4 into an executable binary verifier. Section 5 presents our experiments based on the bincat [START_REF] Biondi | BinCAT: purrfecting binary static analysis[END_REF] binary analysis framework. We present related work in Section 6 and conclude in Section 7.

Software Fault Isolation as a Defensive Semantics

We define SFI and its sandbox property operationally, as a defensive semantics which includes a series of additional (dynamic) verifications. These dynamic checks express what it means for code to be properly sandboxed. Later, we define a static analysis for guaranteeing that the dynamic verifications will not fail at run-time, and hence that the code respects the SFI property.

Intermediate Language

We define our semantics on an intermediate representation (IR) obtained by disassembling the binary. In this approach, each binary instruction is typically translated into a sequence of instructions of the IR. For instance, for x86, a simple arithmetic operation has the side-effect of setting various flags e.g. the carry or overflow flag. For simplicity, we also assume that the IR only manipulates 32-bits values. The abstract syntax of the instructions is given below: The language features expressions e made of registers r, numeric constants n and binary operators . Binary operators range over typical arithmetic operators e.g. +, ×, bitwise operators e.g. xor and logical operators e.g. <. An instruction i consists of assigning an expression to a register (r = e); storing in memory the value e 2 at the address e 1 ([e 1 ] = e 2 ); loading in register r the value stored at address e (r = [e]). A conditional jump jmpif e 1 e 2 jumps to the computed address e 2 if the condition e 1 holds (e 1 = 0). The instruction call e is equivalent to the computed jump jmpif 1 e but identifies a function call; ret e is also equivalent to a computed jump but identifies a function return. The instruction halt immediately stops the program.

The operational semantics of the IR operates over a state ρ, µ, ι where ρ is an environment (Env = Reg → B 32 ), µ is the whole memory of the process and ι is the current instruction pointer. The memory is divided into regions and each region is granted access rights among read, write and execute that are checked for by the semantics. For instance, before reading in memory, we check that the address has the read permission r. The rules that give the semantics of each instruction are fairly standard and are given in Appendix A.

Semantic Domains

Our defensive semantics makes use of several semantic domains that we describe below. Our notations are fairly standard: the set B = {0, 1} is the set of booleans and we write B 32 for B 32 which reads bitvector of size 32. A stack frame is a pair bp, φ ∈ B 32 × B * 32 where bp represents the base pointer of the stack frame and φ is a list of 32-bits values modelling the content of the stack frame. The semantics is using several architecture-dependent constants. The constant d 0 is the base address of the sandbox, the constant s 0 is the top address of the stack, and the maximum size of a stack frame is f s .

In order to detect stack overflows at runtime, the runtime stack is surrounded by so-called guard zones. The concept of guard zone was already present in the original work on SFI [START_REF] Wahbe | Efficient software-based fault isolation[END_REF]. Semantically, this is modelled as memory regions which have no access rights. As a result, accesses within the guard zones are trapped, by letting the execution enter a specific "crash state" where it stays forever. In the following, gz is the size of the guard zone at the top of the stack and gz ⊥ is the size of the guard zone at the bottom of the stack. The guard zones are part of the stack. A call stack CS = (B 32 × B * 32 ) * is a list of stack frames such that the successive base addresses are decreasing (the stack grows downward). The length of the (intermediate) stack frames is given by the difference between two successive base pointers. A call stack is immutable but the content of the call stack can be read. This is modelled by the following judgement cs a v which reads the call stack cs contains the value v at address a. a ≤ bp φ(bp -a) = v cs :: bp, φ a v a > bp cs a v cs :: bp, φ a v .

Defensive Semantics

At binary level, the runtime stack and the code segment are no different from any other part of memory. Our defensive semantics must therefore explicitly enforce a stack discipline and ensure that function boundaries are respected.

The program text is located in memory. For this purpose, we identify a set of addresses Code ⊂ B 32 that correspond to the program code. Given an address i, the function instr(i) checks that i ∈ Code and returns the instruction stored at address i. Moreover, we assume given a set F ⊆ Code of function entry points, and a set T ⊆ B 32 of trusted functions that form the only authorized entry points of the trusted library. A semantic derivation occurs in a context cs, bp, ρ i ∈ CS × B 32 × Env where cs is the call stack, bp is the base pointer of the current frame and ρ i is the environment at the function entry. A judgement is of the form Γ s → s where Γ is an inter-procedural context and s, s are either intra-procedural states s, s ∈ State = Env × B * 32 × B * 32 × B × B 32 or the crash state . A state ρ, δ, φ (β) , ι ∈ State is made of an environment ρ mapping registers to values, a public data segment δ i.e. the sandbox, a stack frame φ, a boolean β which tells whether a write has occurred in the current frame, and the current instruction pointer ι. (We write ι + for the pointer to the next instruction.) The semantics also ensures that there is no overlap between the call stack (including the current stack frame), the code, and the data segment.

The semantics rules are found in Fig. 2. The Assign rule assigns a new value The rule StoreFrame similarly makes the checks necessary for storing securely into the run-time stack. Here, the value of e 1 is supposed to be a valid reference into the current stack which starts at the address designated by the base pointer bp. Because the stack grows towards smaller addresses, the relative offset o into the current stack frame is computed as bp -e 1 ρ . In order for the store to proceed normally, this offset must point into that part of the stack frame that is not making up the guard zone (0 ≤ o <| φ | -gz ⊥ ). It is also checked that the offset does not point into the guard zone at the beginning of the stack segment (bp -o ≤ s 0gz ). This rule also sets β to 1, which has the side-effect of ensuring the current base pointer is above the guard zone (there is some space to write to). The rule LdStCrash describes what happens on an attempt to write into or read from one of the guard zones. In that case, the program transits to the crash state and stays there forever due to rule Crash.

Assign instr(ι) = r = e Γ ρ, δ, φ (β) , ι -→ ρ[r → e ρ], δ, φ (β) , ι + StoreData instr(ι) = [e1] = e2 o = e1 ρ -d0 0 ≤ o <| δ | Γ ρ, δ, φ (β) , ι -→ ρ, δ[o → e2 ρ], φ (β) , ι + StoreFrame instr(ι) = [e1] = e2 o = bp -e1 ρ 0 ≤ o <| φ | -gz ⊥ bp -o ≤ s0 -gz cs, bp, R ρ, δ, φ (β) , ι -→ ρ, δ, φ[o → e2 ρ] (1) , ι + LdStCrash instr(ι) = [e1] = e2 ∨ instr(ι) = [r = [e1] e1 ρ = a (s0 -gz < a ≤ s0) ∨ (bp-| φ |< a ≤ bp-| φ | +gz ⊥ ) cs, bp, ρi ρ, δ, φ (β) , ι -→ LoadData instr(ι) = r = [e] e ρ = d0 + o 0 ≤ o <| δ | Γ ρ, δ, φ (β) , ι -→ ρ[r → δ(o)], δ, φ (β) , ι + LoadStack instr(ι) = r = [e] e ρ = a cs :: bp, φ a v bp-| φ | +gz ⊥ < a ≤ s0 -gz cs, bp, ρi ρ, δ, φ (β) , ι -→ ρ[r → v], δ, φ (β) , ι + Call instr(ι) = call e e ρ = f f ∈ F ρ(esp) = bp -o | φ1 |= o o < fs isret(ι + , ρ, φ1) ρ ∼ ρ instr(ι ) = ret e e ρ = ι + cs :: bp, φ1 , bp -o, ρ ρ, δ, φ (0) 2 , f -→ * ρ , δ , φ (β) 2 , ι cs, bp, ρi ρ, δ, φ1 • φ (1) 2 , ι -→ ρ , δ , φ1 • φ (1) 2 , ι + CallTrust instr(ι) = call e e ρ = f f ∈ T ρ(esp) = bp -o | φ1 |= o o < fs isret(ι + , ρ, φ1) ρ ∼ ρ cs, bp, ρi ρ, δ, φ1 • φ (1) 2 , ι -→ ρ , δ , φ1 • φ (1) 2 , ι + Cont instr(ι) = jmpif e1 e2 e1 ρ = 0 Γ ρ, δ, φ (β) , ι -→ ρ, δ, φ (β) , ι + Jump instr(ι) = jmpif e1 e2 e1 ρ = 0 e2 ρ ∈ Code Γ ρ, δ, φ (β) , ι -→ ρ, δ, φ (β) , e2 ρ Halt instr(ι) = hlt Γ ρ, δ, φ (β) , ι -→ Crash Γ -→
The two rules LoadData, LoadStack describe how data are read from the data segment and the run-time stack. Reading from the data segment uses verification similar to storing into it. Loading from the stack is, however, slightly different in that our version of SFI allow reads from all of the stack frames, and not just the current frame. This allows e.g. functions to read their arguments. It is still verified that the access does not fall in the guard zones, using checks similar to StoreFrame.

The rule Call for the function call instruction call e first verifies that the value e ρ belongs to the set of function entry points F. The current stack frame is divided into two parts φ 1 • φ 2 where φ 1 is local data of the caller and φ 2 is the new stack frame for the function call, which starts at the address contained in register esp. The offset o between the start of the old stack frame and the new is verified to be smaller than the maximal frame size f s . Because it is checked that β = 1, i.e. the frame has already been written to in this function, this check has the side-effect to ensure bp is above the guard zone gz ⊥ and therefore the new bp is still at least f s above the bottom of the stack. Note that enforcing a write before calls is not restrictive as writes are generated by compilers before function calls in any architecture. The actual method call is modelled as an execution starting at address f with the same environment ρ, the same data segment δ, and a stack frame φ (0) 2 where the 0 indicates that the frame has not yet been written into. The end of the call is identified by the execution reaching a ret e instruction. The value of e ρ is verified to be the return address using the architecture-dependent predicate isret. The return address is the next instruction to execute. The semantics verifies that callee-saved registers are restored after the function call. For instance on X86 assembly, registers esp, ebx etc are saved. For this same architecture, isret checks that the return address has indeed been pushed to the call stack. Calling a trusted function is modelled with the rule CallTrust. This rule follows the same pattern as the rule for ordinary calls, except that the trusted call is allowed to modify the sandbox data but should leave the callee's stack frame unchanged. We model this as a non-deterministic rule that can return any δ in its resulting state.

The rules Cont and Jump model the instruction jmpif e 1 e 2 for conditional jumps to a computed address. If the condition e 1 evaluates to zero, execution continues with the next instruction. Otherwise, the value e 2 ρ is computed and it is verified that this new jump target is in the code block Code. Finally, we use the (secure) crash state to model program termination in the rule Halt. The rule Crash states that once in a crash state the execution stays in this state forever. This semantic sleight of hand simplifies the statement of the overall security property, which becomes essentially a progress property. Employing a specific error state would be equivalent but slightly more cumbersome.

The Sandbox Property

The side-conditions of the rules performing memory accesses ensure that the defensive semantics gets stuck when memory accesses do not respect the sandboxing property. This means that we can state our sandbox property as a simple progress property of the defensive semantics: as long as the semantics can progress to a new state (possibly the crash state) no security violation has occurred.

There is one obstacle to this, though: due to our big-step modelling of function calls, the semantics also gets stuck as soon as a function call does not terminate. In other words, all infinite loops are deemed insecure, which is clearly not what we want. To remedy this, our sandbox property is defined over the set of reachable states induced by the defensive semantics where the transition relation → is extended with a relation which for each call instruction explicitly adds a transition to the callee state.

CallAcc instr(ι) = call e e ρ = f f ∈ F ρ(esp) = bp -o | φ 1 |= o o < f s isret(ι + , ρ, φ 1 ) cs, bp, ρ i , ρ, δ, φ 1 • φ (1) 2 , ι cs :: bp, φ 1 , bp -o, ρ , ρ, δ, φ (1)
2 , f Dually, we also add a transition stating that, for a ret instruction, the return state is not stuck provided that the calling conventions are respected. Since the next step is taken care of by the Call rule, the resulting state is just a witness that the execution can proceed; we reuse for this purpose the state .

RetAcc ρ i ∼ ρ isret(ret, φ 1 , ρ i ) instr(ι) = ret e e ρ = ret cs :: bp, φ 1 , bp -o, ρ i , ρ , δ, φ (β)
Definition 2 (Sandboxing as progress). Let ι 0 be the entry point of the program and let the initial state be Γ 0 , Σ 0 = [ s 0 , φ i ], s 0 -gz , ρ 0 , ρ, δ, φ (0) , ι 0 with | φ i |= gz . The program satisfies the SFI sandbox property if the set of reachable states Acc = {s | Γ 0 , Σ 0 ⇒ * s} satisfies ∀s ∈ Acc.∃s .s ⇒ s . We write Safe(Acc) if this is the case.

Intraprocedural semantics as an abstract interpretation

In order to derive a modular static analyser we abstract the defensive semantics into an intra-procedural semantics where the accessible states I -Acc are computed for each function separately: I -Acc = f ∈F I -Acc(f ). Our intraprocedural semantics abstracts away the data region and all of the call stack, except the frame of the caller. Thus the stack component is abstracted to two small zones of the stack above and below the current base pointer, representing the frames of the caller and the callee (the currently executing function). Both are modelled by memory regions of size f s where f s is a chosen maximum size of these abstract stack frames. Fig. 3 illustrates the abstraction of the stack segment. The current code can write to its own frame (the W zone) and read from both frames (the R zone). The size of the guard zones are set such that the abstract frames are always contained in the stack, possibly overlapping a guard zone. The judgement of the intra-procedural semantics is of the form: Γ s → s where the context Γ = φ i , bp, ρ i ∈ Ctx is constant. Here, φ i is the frame of the caller, bp is the base pointer and ρ i is the initial environment. The states s and s are either the crash state or of the form ρ, φ (β) , ι ∈ State .

The intra-procedural semantics has no knowledge about where it is in the stack segment so it cannot detect stack overflows per se. We solve this problem by a judicious use of the guard zones. The defensive semantics enforces that a successful memory write occurs within the current stack frame before any call. This entails the semantic invariants that 1. before a function call the base pointer is always inside the stack and outside of the guard zone, 2. at function entry point, the base pointer is always inside the stack or at most f s bytes inside the guard zone, 3. hence, there are at least f s bytes left between bp and the end of the stack segment (including the guard zone). These invariants are formally stated by Lemma 3 that is proved in Appendix C.

Similarly, we also guarantee that the call stack is at least of size f s , possibly overlapping the guard zone gz . Those invariants are enough to detect both stack overflows and underflows using the intra-procedural semantics: if all the stack accesses are proved to be within the bound of f s above and below the stack pointer bp, the accesses are either defined in the defensive semantics or lead to a crash because the access is performed inside the guard zone.

The intra-procedural and defensive semantics are linked by the concretization function γ : Ctx × State → P((Ctx × State) ∪ { }). The data segment is not represented in the intra-procedural semantics, so its concretization is any data segment of size d s . The concretization constructs the call stack and the current defensive frame in such a way that, once appended to one another, they form a memory region of size s s and f i and f are windows of size f s around the address pointed to by the base pointer. Formally, we have:

γ( f i , bp, ρ i , ρ, f (β) , ι ) = { } ∪    cs, bp, ρ i , ρ, δ, φ (β) , ι f = φ | [0,fs-1] f i = cs | [|cs|-fs,|cs|]   
where cs is obtained by concatenating the different stack frames of the call stack and φ | [a,b] extracts the sub-list between the indexes a and b.

cs = [] if cs = [] φ • cs if cs = bp, φ :: cs φ | [a,b] = [] if a > b φ(a) :: φ | [a+1,b] otherwise
Except for the handling of stack overflows and underflows, the rules for the intra-procedural semantics are fairly standard and can be found in Appendix B. When a memory component is absent from the abstraction i.e. the data region, the intra-procedural semantics non-deterministically picks a value. For the call instruction, the rule is similar to the defensive semantics rule Call with the notable exception that no recursive call is made.

FunCall instr(ι) = call e e ρ = f f ∈ F ∪ T ρ(esp) = bp -o 0 ≤ o < f s | φ 1 |= o isret(ι + , ρ, φ 1 ) ρ ∼ ρ φ i , bp, ρ i ρ, φ 1 • φ (1) 2 , ι → ρ , φ 1 • φ (1)
2 , ι +

The rule FunLdArg shows how to access the arguments of the function that are placed in the stack frame of the caller modelled by φ i .

FunLdArg

instr(ι) = r = [e] e ρ = (bp + f s ) -o 0 ≤ o < f s φ i , bp, ρ i ρ, φ (β) , ι → ρ[r → φ i (o)], φ (β) , ι +
The base address of φ i is obtained by incrementing the base pointer bp by the stack frame size f s and checking that the offset o is in range [0; f s [. The soundness of this rule exploits the fact that the defensive stack is guarded by gz . As a result, if FunLdArg succeeds, either the memory access also succeeds in the defensive semantics (rule LoadStack) or it accesses the guard zone gz and triggers a crash (rule LdStCrash).

For each function entry ι ∈ F, the initial states Init(f ) ⊆ Ctx × State are defined by:

Init(ι) = φ i , bp, ρ , ρ, φ (0) , ι | φ |=| φ i |= f s ∧ bp > s 0 -s s + gz ⊥ -f s .
As we already discussed, the frames φ and φ i have length f s . At the function start, the environments of the caller and the callee are the same; the base pointer is so that there is below it a stack frame of size at least f s and no memory write has been performed on the current frame φ. For a given function entry point f ∈ F, the reachable states are defined as

I -Acc(f ) = {(Γ, s) | Γ s 0 → * s ∧ (Γ, s 0 ) ∈ Init(f )}.
The intra-procedural semantics is also defensive and gets stuck when abstract verification conditions are not met.

Definition 3 (Intra-procedural progress). The intra-procedural states are safe (written I -Safe(I -Acc)) iff ∀f ∈ F, ∀(Γ, s) ∈ I -Acc(f ).∃s .Γ s → s .

The checked conditions are sufficient (but may not be necessary). For instance, the intra-procedural semantics gets stuck when an access is performed outside the bound of the current stack frame φ. However, because φ only models a prefix of the frame of the defensive semantics, the defensive semantics may not be stuck. As a result, the usual result Acc ⊆ γ(I -Acc) does not hold. Instead, we have Lemma 1 stating that if the intra-procedural semantics is not stuck, it abstracts the defensive semantics and ensures that the accessible states of the defensive semantics are safe.

Lemma 1 (Correctness of the Intra-procedural semantics).

I -Safe(I -Acc) ⇒ Acc ⊆ γ(I -Acc) ∧ Safe(Acc).
The proof can be found in Appendix C.

A Static SFI Analysis

To get a modular executable verifier, we abstract further the intra-procedural semantics. The verifier needs to track numeric values used as addresses, in order to guarantee that memory accesses are within the sandbox or within the current stack frame, hence we need domains tailored for such uses of numeric values. The verifier also needs to gather some input-output relational information about the registers and verify that, at the end of the functions, callee-saved registers are restored to their initial values.

Abstract Domains

As pioneered by Balakrishnan and Reps [START_REF] Balakrishnan | Analyzing Memory Accesses in x86 Executables[END_REF], we perform a Value Set Analysis (VSA) where abstract locations (a-locs) are data for the sandbox region and code for the code region. We also introduce an abstract location for the function return ret, the base pointer bp and for each register e.g. eax, ebx. To model purely numeric data, we have a dedicated a-locs zero with value 0:

a-locs = {zero, data, code, ret, bp, eax, ebx, . . .}.

a-locs are equipped with an arbitrary non-relational numeric domain. The abstract value domain B 32 is therefore a pair (L, o) made of an abstract location L and a numeric abstraction o ∈ D . For each concrete operation on values, the transfer function on abstract (L, o)-values is using the corresponding operation of the abstract domain. For instance, for addition and subtraction, we get:

(L, o 1 ) + (zero, o 2 ) = (L, o 1 + o 2 ) (zero, o 1 ) + (L, o 2 ) = (L, o 1 + o 2 ) (L, o 1 ) -(zero, o 2 ) = (L, o 1 -o 2 ) (L, o 1 ) -(L, o 2 ) = (zero, o 1 -o 2 )
When symbolic computations are not possible, it is always possible to abstract (L, o) by (zero, ) and use numeric transfer functions. As the usual sandboxing technique consists in masking an address using a bitwise & ([e 1 ] := e 2 [d 0 + e 1 &1 k ] := e 2 )1 we opt, in our implementation, for the bitfield domain [START_REF] Miné | Abstract domains for bit-level machine integer and floating-point operations[END_REF].

The abstract machine state at a program point is the product of an abstract environment Env , an abstract frame Frame , and a code pointer B 32 .

Env = Reg → B 32 Frame = (B 32 ) fs × B State = Env × Frame × B 32 .
The abstract frame is annotated by a boolean indicating whether a memory write has definitively occurred in the stack frame.

The concretization function is parametrised by a mapping λ : a-locs → B 32 assigning a numeric value to abstract locations and the concretization function γ : D → P(B 32 ) of the numeric domain. The concretization is then obtained using standard constructions:

γ λ (L, o) = {v + λ(L) | v ∈ γ(o)} γ λ (ρ ) = {ρ | ∀r.ρ(r) ∈ γ λ (ρ (r))} γ λ (φ ) = {φ | ∀i ∈ [0, f s ].φ(i) ∈ γ λ (φ (i))} γ λ ( ρ , φ (b) , ι ) = ρ, φ (β) , ι β ≥ b ∧ ρ ∈ γ λ (ρ ) ∧ φ ∈ γ λ (φ )
The mapping λ denotes a set of intra-procedural contexts such that a register r in the environment ρ i has the value λ(r) and the return address is constrained by the calling conventions.

γ(λ) = φ i , bp, ρ i ∀r, ρ(r) = λ(r), bp = λ(bp) = λ(esp), isret(λ(ret), ρ i , φ i ) .
Finally, the whole concretization γ : State → P(Ctx × State ) is defined as:

γ(s ) = { Γ, } ∪ { Γ, s | ∃λ, Γ ∈ γ(λ) ∧ s ∈ γ λ (s )}.

Abstract Semantics

The abstract semantics takes the form of a transition system that is presented in Fig. 4. The rule AAssign abstracts the assignment to a register and consists in evaluating the expression e using the abstract domain of Section 4.1. A memory

AAssign instr(ι) = r = e ρ, φ (β) , ι -→ ρ[r → e ρ], φ (β) , ι + AStD instr(ι) = [e1] = e2 e1 ρ = (data, o) γ(o) ⊆ [0; ds[ ρ, φ (β) , ι -→ ρ, φ (β) , ι + AStF instr(ι) = [e1] = e2 e1 ρ = (bp, o) off ∈ γ(o) γ(o) ⊆ ]-| φ |; 0] ρ, φ (β) , ι -→ ρ, φ[off → e2 ρ] (1) , ι + ALdD instr(ι) = r = [e] e ρ = (data, o) γ(o) ⊆ [0; ds[ ρ, φ (β) , ι -→ ρ[r → (zero, )], φ (β) , ι + ALdF instr(ι) = r = [e] e ρ = (bp, o) off ∈ γ(o) γ(o) ⊆]-| φ |; 0] ρ, φ (β) , ι -→ ρ[r → φ(off )], φ (β) , ι + ALdS instr(ι) = r = [e] e ρ = (bp, o) γ(o) ⊆]0; | φ | [ ρ, φ (β) , ι -→ ρ[r → (zero, )], φ (β) , ι + ACall instr(ι) = call e γ( e ρ) ⊆ F ∪ T ρ(esp) = (bp, o) off ∈ γ(o) | φ1 |= -off γ(o) ⊆] -fs; 0] isret(ι + , ρ, φ1) ρ ∼ ρ | φ2 |=| φ 2 | ρ, φ1 • φ (1) 2 , ι -→ ρ , φ1 • φ (1) 2 , ι + ARet instr
(ι) = ret e preserve(ρ) e ρ = (ret, o) {0} = γ(o) ρ, φ (β) , ι -→ ACont instr(ι) = jmpif e1 e2 0 ∈ γ( e1 ρ) ρ, φ (β) , ι -→ ρ, φ (β) , ι + AJump instr(ι) = jmpif e1 e2 c ∈ γ( e1 ρ) c = 0 e2 ρ = (code, o) ι2 ∈ γ(o) + c0 ι2 ∈ Code ρ, φ (β) , ι -→ ρ, φ (β) , ι2 AHalt instr(ι) = hlt ρ, φ (β) , ι -→ ACrash -→
Fig. 4: Abstract semantics store is modelled by the rules AStD and AStF depending on whether the address is within the sandbox or within the current stack frame. Both rules ensure that the offset is within the bounds of the memory region. A memory load is modelled by the rules ALdD, ALdF or ALdS depending on whether the address is within the sandbox, the current stack frame or the caller stack frame. Each memory access is protected by a verification condition ensuring that the offset is within the relevant bounds. For the ALdF rule, the memory offset off is used to fetch the abstract value from the abstract frame φ. As the sandbox and the caller frame are not represented, we get the top element of the abstract domain i.e. (zero, ). The rule ACall models function calls. It checks whether the target of the call is a trusted (f ∈ T ) or untrusted function (f ∈ F).

For the call to proceed, the stack pointer esp must be within the bounds of the current stack frame and the return address ι + needs to be stored according to the calling conventions (isret(ι + , ρ, φ 1 )). After the call, the resulting environment ρ satisfies that the callee-saved registers are restored to their values in ρ (ρ ∼ ρ ) and the suffix of the current frame φ 2 is arbitrary i.e. φ 2 = (zero, ) |φ2| . The rule ARet ensures that the expression e evaluates to the return of the current function ( e ρ = (ret, o) {0} = γ(o)), and also that the callee-saved registers are restored to their initial values. For instance, for ebx, preserve(ρ) ensures that ρ(ebx) = (EBX, o) with γ(o) = {0}. The rules ACont and AJump model control-flow transfer and check that the obtained code pointer is within the bounds of the code. The last two rules AHalt and ACrash model the crash state that is produced by the hlt instruction and is its own successor.

Like the intra-procedural semantics, the abstract semantics is safe if it is not stuck (Definition 4).

Definition 4 (Abstract progress). The reachable intra-procedural states are safe (written A-Safe(A-Acc)) iff ∀f ∈ F, ∀s ∈ A-Acc(f ).∃s .s → s .

The abstract semantics embeds abstract verification conditions that are only sufficient but not necessary for the intra-procedural semantics. As a result, it only computes a safe approximation under the condition that all the reachable abstract states are safe.

Lemma 2 (Correctness of the abstract semantics).

A-Safe(A-Acc) ⇒ I -Acc ⊆ γ(I -Acc) ∧ I -Safe(I -Acc)

The proof can be found in Appendix D. By transitivity, using Lemma 2 and Lemma 1, we get Theorem 1.

Theorem 1 (Correctness of SFI Verifier). A-Safe(A-Acc) ⇒ Safe(Acc) By definition of Safe, Theorem 1 means that the defensive semantics is not stuck.

Implementation and Experiments

We have implemented the static analysis on top of the BinCAT binary code analysis toolkit [START_REF] Biondi | BinCAT: purrfecting binary static analysis[END_REF]. First, our SFI analyser reconstructs the structure of the binary and in particular partitions the code into separate functions and transforms the binary instructions into the REIL [START_REF] Dullien | Reil: A platform-independent intermediate representation of disassembled code for static code analysis[END_REF] intermediate representation. Second, each previously identified function is analysed separately, using the abstraction described in Section 4. For each function, the analysis checks that all the intraprocedural jumps stays within the current function and that the abstract semantics never blocks. The analysis also checks that all calls are towards previously identified entry points thus validating a posteriori that the initial partition of the code into distinct functions is indeed correct.

The analysis has been tested on three test suites: correctly sandboxed programs, incorrectly sandboxed programs, and optimised, correctly sandboxed programs. The first test suite is built by compiling programs that are part of the CompCert test suite with a modified version of CompCert that includes sandboxing instructions. Because these binaries are correct by construction, the verifier should accept all of them. In our experiments, we have tested 10 programs, composed of 51 functions in total. 41 functions are verified in under 100ms, 9 functions are verified in less than 300ms and 1 function is verified in 3.5s. This last function occurs in sha3.c, and is responsible for the program being verified in 3.5s. This file is 200LoC long, while another file, aes.c, is 1.5KLoC long, composed of 7 functions and takes only 1s to validate. This suggests that the time complexity depends on the number of nested loops rather than on the size of the code to verify.

The second test suite for catching incorrect programs has been obtained by compiling incorrectly sandboxed programs with gcc and verifying they do not pass our verification. Each test in the suite aims at a different error: returning before the end of a function, writing above and below the frame, stack or sandbox and bypassing the guard zones. Overall, the test suite contains 9 programs and all are correctly identified as violating the sandbox property. Some of these programs can be found in Fig. 5.

asm ( " sub $5000000 , %e s p \n\ t " " push $1 " ) ; (b) Attempt to write outside of the sandbox i n t f ( i n t * e ) { i n t i ; asm ( " push $main \n\ t " "mov %1, %%ebp \n\ t " " add %%ebp , (%%e s p ) \ n\ t " " r e t " : "=r " ( i ) : " r " ( * ( ( i n t * ) ( sandbox ( e , 4 ) ) ) ) : "%ebp " ) ; r e t u r n i +5; } (c) Attempt to return before the end

Fig. 5: Violation of sandboxing

We have also evaluated the ability of the analysis to verify programs where redundant sandboxing instructions have been optimised away. For instance, the sandboxing of consecutive accesses to an array can be factorised and implemented by a single sandboxing instruction. In addition to masking the most significant bits, this sandboxing instruction also zeroes out several least significant bits thus aligning the base address of the array. The reasoning is that if an address a of the sandbox is aligned on k bits we have that a + i for i ∈ [0, 2 k -1] is also in the sandbox. We have sandboxed the programs manually and compiled them with gcc and verified whether they passed our verification. Our numerical domain is able to model alignment constraints and the analysis accepts programs where consecutive writes are protected by the previous sandboxing operation. Yet, the analysis rejects programs where the sandboxing instruction is factored outside loops because the information inferred about the loop bound is currently not precise enough. More precision could be obtained by using more sophisticated numerical domains. An example program that fails our verification is given in Fig. 6. The use of alloca(size t size) is another example of a code that respects the security property as defined by the defensive semantics, but cannot be understood by the analyser, unless more work is done by the programmer with the result of that function. Because we limit the maximum size of the stack frame, this function cannot work properly when its argument is bigger than this limit. The result is a pointer outside of the frame, and the module is rejected when a write at this address is detected.

c h a r * a = ( s f i + ( t & 0 b11111000 ) f o r ( c h a r i =0; i <5; i ++) { a [ i ] = i ; }

Related Work

Software Fault Isolation has been proposed by Wahbe et al. [START_REF] Wahbe | Efficient software-based fault isolation[END_REF] as a way to ensure that a binary code runs inside a sandbox. Native Client (NaCl) [START_REF] Yee | Native client: A sandbox for portable, untrusted x86 native code[END_REF][START_REF] Sehr | Adapting software fault isolation to contemporary cpu architectures[END_REF] is a state-of-the-art implementation that was part of chromium-based browsers in order to safely run binary plugins. The NaCl binary verifier only performs a linear scan of the code. It is very fast, simple and has a small TCB. As shown by the RockSalt project [START_REF] Morrisett | Rocksalt: Better, Faster, Stronger SFI for the x86[END_REF], it is also amenable to formal verification. The NaCl verifier requires setting up trampoline code to share a runtime stack between trusted and untrusted code. Using abstract interpretation, we propose a more flexible binary verifier where redundant sandboxing operations can be optimised away and where the runtime stack is safely shared between trusted and untrusted code. Our TCB is bigger than NaCl but could be reduced using certified abstract interpretation [START_REF] Jourdan | A Formally-Verified C Static Analyzer[END_REF].

Kroll et al. [START_REF] Kroll | Portable software fault isolation[END_REF] propose to implement SFI as a Cminor compiler pass of the CompCert [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] verified compiler. They show that proving both safety and security of the SFI pass is enough to get a secure binary. For their approach, redundant sandboxing operations can be optimised away by the compiler back-end; the runtime stack is managed by the compiler and therefore shared between trusted and untrusted code. A main difference with our work is that we explicitly state, using our defensive semantics, the security property that holds at binary level. Moreover, we propose a flexible binary verifier for this property.

The NaCl technology has recently been replaced by WebAssembly [START_REF] Haas | Bringing the Web Up to Speed with WebAssembly[END_REF]. Webassembly is an intermediate language, similar to Cminor, that is just-in-time compiled into binary code. As the code may be malicious, the just-in-time compiler adds runtime checks to make sure the code runs inside a sandbox. Compared to the previous approaches, the TCB includes the just-in-time compiler and there is no independent binary verifier.

Binary Analysis frameworks e.g. BAP [START_REF] Brumley | BAP: A Binary Analysis Platform[END_REF] and Angr [START_REF] Shoshitaishvili | SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis[END_REF] propose rich APIs to develop static analyses on top of an architecture independent intermediate language. We use BinCAT [START_REF] Biondi | BinCAT: purrfecting binary static analysis[END_REF] based on the REIL intermediate representation [START_REF] Dullien | Reil: A platform-independent intermediate representation of disassembled code for static code analysis[END_REF]. Our binary verifier has the rare feature of being intra-procedural. As a result, we have adapted their interprocedural analysis engine and implemented our own analysis domains. Our analysis domain is inspired from the a-locs domain of Balakrishnan and Reps [START_REF] Balakrishnan | Analyzing Memory Accesses in x86 Executables[END_REF] which we adapt to a purely intra-procedural setting and where a-locs are also used to model the initial values of registers. There are full-fledged, whole-program, binary analysers e.g. Jackstab [START_REF] Kinder | Static Analysis of x86 Executables[END_REF] and Bindead [START_REF] Mihaila | Adaptable Static Analysis of Executables for proving the Absence of Vulnerabilities[END_REF]. They both use a sophisticated combination of abstract domains. Our domains are simpler but specialised to prove the sandboxing property. Moreover, our analysis is intra-procedural and finely models the calling conventions.

Conclusions

We have shown that the Software Fault Isolation mechanism for safely executing untrusted binaries can be formalised as a defensive semantics of an intermediate representation of binary code. Our semantics generalises existing approaches and defines a relaxed SFI property where the runtime stack is safely shared between trusted and untrusted code. Using abstract interpretation, we derive from the defensive semantics an intra-procedural binary verifier which for each individual function can verify that memory accesses are sandboxed and that the code abides to calling conventions. The verifier is implemented and our tests show that it is able to validate programs even when compiler optimisations are enabled.

Further work will concern improving the robustness of the verifier and ensuring a degree of completeness w.r.t. more complex optimisations. To do so, we intend to enrich our abstract domains to cope specifically with program transformations based on code motion where sandboxing instrumentations are factored outside loops. In addition, we intend to extend the verifier to handle multithreaded applications. We expect that the data-local, intra-procedural design of the verifier will greatly facilitate the extension to such a multi-threaded setting.

e

  ::= r | n | e 1 e 2 i ::= r := e | [e 1 ] = e 2 | r = [e] | jmpif e 1 e 2 | call e | ret e | hlt

Fig. 2 :

 2 Fig. 2: Defensive semantics

Fig. 3 :

 3 Fig. 3: Abstraction of call stack

( a )

 a Attempt to write below the stack d a t a [ -5 ] = 0 ;

Fig. 6 :

 6 Fig. 6: Optimising array accesses in a loop

, ι cs :: bp, φ 1 , bp -o, ρ i , Definition 1 (Augmented defensive semantics). The augmented defensive semantics ⇒ is given by the union of the relation → and such that:Γ Σ 1 → Σ 2 Γ, Σ 1 ⇒ Γ, Σ 2 Γ 1 , Σ 1 Γ 2 , Σ 2 Γ 1 , Σ 1 ⇒ Γ 2 , Σ 2The SFI sandbox property can then be expressed as the progress property of the augmented defensive semantics.

This exploits the property that the range of the sandbox is a power of

A Concrete Operational Semantics

First we need an intermediate lemma:

Lemma 3 (Base pointer is contained).

Proof. We reason by induction on S ∈ Acc. In the inital state, we have bp = s 0gz and β = 0, so the property is true since s s > gz + gz ⊥ .

In the inductive case, we procede by case analysis on S ⇒ S , where S verifies the property. Because the property only depends on the context and β, most cases are trivial: they preserve the context and β. In the case of the StoreFrame rule, the context is preserved, and β is updated to 1. The property is still preserved because the property when β = 0 implies the property when β = 1.

The last case is when the extended call rule applies. In that case,

gz and the property holds.

Now we can prove the main lemma:

Proof. First, we prove that Acc ⊆ γ(I -Acc).

Let S ∈ Acc. By induction on S, we have the following cases:

-S = Γ 0 , Σ 0 = [ s 0 , φ i ], s 0gz , ρ 0 , ρ, δ, φ (0) , ι 0 with | φ i |= gz . By definition, ι 0 ∈ F, so we can construct Init(ι 0 ). By construction, S ∈ γ(Init(ι 0 )).

By induction hypothesis, we also have S such that Γ 1 , Σ 1 ∈ γ(S ). Since I -Safe(I -Acc), S → S 2 . By case analysis on the rule that allows → , we have:

The preconditions are the same as for (Assign), so there is S such that S → S . Furthermore, S ∈ γ(s ). • (FunStD, FunLdD, FunCont, FunIndirectJump, FunHalt, FunCrash) Similar reasoning. • (FunStF) Here, the preconditions are either true for (StoreFrame) or (StoreCrash) because of Lemma 3, so there is S such that S → S , with S = (writing in the guard zone) or S = ρ, δ, φ (β) , ι (writing in the frame). Futhermore, S ∈ γ(s ). • (FunLdS) Here, the preconditions are either true for (LoadStack) or (LoadCrash) because of Lemma 3, so there is S such that S → S , with S = (reading in the guard zone) or S = ρ, δ, φ (β) , ι (reading in the stack). Futhermore, S ∈ γ(s ).

• (FunCall) Here the preconditions are the same as for (CallAcc) because of Lemma 3, so there is S such that S ⇒ S . Furthermore, S ∈ γ s (Init(f )) ⊆ γ s (S ).

• (FunRet)

Here the preconditions are the same as for (RetAcc), so S ⇒ . Furthermore, ∈ γ(s ).

Hence our intermediate conclusion: Acc ⊆ γ(I -Acc). Let's now take S ∈ Acc. We use the previous conclusion to also choose S ∈ I -Acc such that S ∈ γ(S ). Because we have I -Safe(I -Acc), we can also take S 2 such that S → S 2 .

By case analysis with a similar reasoning as the previous property, we get that S ⇒ S with S ∈ γ(S 2 ).

Hence Safe(Acc).

D Proof of Lemma 2

Proof. First, we prove that I -Acc ⊆ γ(A-Acc).

Let S ∈ I -Acc. By induction on S, we have the following cases:

S ∈ A-Acc, so the property is true in that case. -S = Γ, Σ 2 with Γ, Σ 1 ∈ I -Acc and Γ Σ 1 → Σ 2 . By induction hypothesis, we also have S such that Γ 1 , Σ 1 ∈ γ(S ). Because we have A-Safe(A-Acc), we also have S 2 such that S → S 2 . By case analysis on →, we can see as before that the preconditions of the abstract semantics are the same or more restrictive than those of the intra procedural semantics. It is also built in a way that Γ, Σ 2 ∈ γ(S 2 ).

Hence our intermediate conclusion: I -Acc ⊆ γ(A-Acc). Let's now take S ∈ I -Acc. We use the previous conclusion to also choose S ∈ A-Acc such that S ∈ γ(S ). Because we have A-Safe(A-Acc), we can also take S 2 such that S → S 2 .

By case analysis with a similar reasoning as the previous property, we get that S ⇒ S with S ∈ γ(S 2 ).

Hence Safe(I -Acc).