M Eddy

Caron M Christian

Toinard Après

M Nicolas

Anciaux M Gilles

Dequen Devant Le Jury

M Nicolas Anciaux

Rapporteur M Eddy Caron

M Gilles

Rapporteur M Marc Lacoste

Membre Mme Christine Morin

Jean-Marc Pierson

Paul Sabbatier

Membre M Jonathan

Chapter 1 Introduction

In our contemporary society, most IT services are going online. Nowadays, any user of a service such Gmail expects to access it from anywhere on earth, without delay, at any time and in a responsive and efficient manner.

To cope with our growing needs, the infrastructures hosting these services have continuously evolved taking the shape of distributed systems, the most recent being the Cloud computing. The idea behind Clouds is simple: mutualize the resources to decrease the cost and mutualize the expertise to propose robust platforms offering on-demand resources. The key technology enabling these concepts is virtualization. It gives the impression to a user of having dedicated resources where in fact the underlying real resources are shared amongst several independent users.

Cloud providers offer many promises such as highly available platform (e.g., up to 99.999999999% over a year for Amazon S3 1 ). But one fundamental aspect is left behind this gigantic trend: security. And this negligence is a bargain for hackers. In 2009, numerous systems of the major Cloud provider Amazon were hijacked to run Zeus botnet nodes. In April 2010, the same Amazon experienced a Cross-Site Scripting (XSS) bug that allowed attackers to hijack credentials from the site. On April 20, 2011, Sony Playstation Network, which is Cloud-based, was break down and nearly 77 million accounts were compromised due to an external intrusion few days before and the network was operational again only on May 1. These examples concern major stakeholders which should have the means to protect themselves. With similar stories covering national newspapers, people start realizing that security is critical.

Despite that virtualization has slightly improved security by providing a sense of isolation, many studies have demonstrated some flaws in virtualization that allow the exfiltration of critical information. Moreover, if we look at current security practices, we will find out that security configurations are usually done by hand with all the problems it implies: human errors, gap between the user requirements and the understanding of the security expert, lack of adaptability, and absence of scalability.

Nevertheless, many companies outsource their applications/services to these virtualization-based infrastructures. However, the provider security does not always match tenants' concerns. For instance, Amazon Web Services (AWS) have the following terms of use:

"AWS products that fall into the well-understood category of Infrastructure as a Service (IaaS) -such as Amazon EC2, Amazon VPC, and Amazon S3 -are completely under your control and require you to perform all of the necessary security configuration and management tasks. For example, for EC2 instances, you're responsible for management of the guest OS (including updates and security patches), any application software or utilities you install on the instances, and the configuration of the AWS-provided firewall (called a security group) on each instance. These are basically the same security tasks that you're used to performing no matter where your servers are located."

In short, the tenant has to do the same effort as for on-premise infrastructures to secure its outsourced business. Meanwhile, because the massive adoption of Clouds makes them a much more attractive target for hackers, the tenant's application is more at risk than before. Moreover, in case an application is compromised and it is determined that the source of the infection is a weakly secured component, the tenant of the last may be held responsible.

In this Thesis, our goal is to provide an end-to-end security of virtualized distributed systems: from the user modelization to the deployment of its application and security.

Motivations

This Thesis revolves around two ideas. The first idea is to follow a user-centric approach which is an alternative to the security by default or by design model usually proposed by most providers and many researchers. We are interested in the security of the enduser application and not in the security of the provider platform. The second idea is to bridge the gap between the user's ability to specify security requirements and complex configurations of security mechanisms.

We believe that virtualized distributed systems such as Clouds are to become massively adopted in the near future. It follows that our first goal is to offer an end-to-end security for real applications deployed on such distributed systems. Moreover, a security is relevant only for the application it protects i.e., each application may have different security requirements. Therefore, a second goal is to facilitate the expression of the users' requirements for both the application and its security. Also, the security offered to the end-user should be supported by strong guarantees. A strong security cannot be a patchwork of mechanisms configured by hand. Moreover, the end-user should not manage the complexity of the underlying middleware and related security services. Instead, our third goal is to provide an automatic deployment of the application and automatic enforcement of its security with a formal basis to demonstrate a safe enforcement. Our solution must be as flexible and generic as possible to encompass a wide range of security mechanisms.

In the next sections, we discuss security foundations and targeted infrastructures: distributed systems. First, we explain what is security in computer sciences, what does this term cover and what kind of security we are interested in. Then, we review the evolution of computing infrastructures and highlight their specificities i.e., what makes their security different.

Information Security

Information security means protecting information and information systems from unauthorized access, use, disclosure, disruption, modification, or destruction. An information system (or system for short) is the combination of people and computers processing or interpreting information. Information security is a general term that can be used regardless of the form the data may take (e.g., electronic, physical). When applied to computing devices, the term used is Cybersecurity (or Information Technology security). Cybersecurity may include physical security i.e., preventing theft of equipments. In this Thesis, our concern is information security on digital data against logical threats i.e., attacks conducted using software tools. Accordingly, protecting physical access to equipments is out of scope. In the rest of this document, the term Security is used for information security on digital data.

In the rest of this section, we lay the basis of security and determine our scope of interest for this Thesis.

Security Policy

The definition of what it means to be secure is expressed by the Security Policy. A policy constrains actions between entities in a system. An action is any operation changing the state of the system when performed e.g., reading a file, sending a packet over the network, modifying permissions, log in. An entity is anything existing concretely or abstractly regardless of its nature or complexity e.g., a user, a process, a piece of data, a network.

Central to security is the protection of assets. An asset is anything of value either substantial like data, computing resources, storage space but also intangible like reputation. For example, disrupting access to service will damage the reputation of the brand and users will be more willing to go for a competitor if it provides a more reliable service.

A key concept of security is the notion of authorization. A security policy can be seen as a set of authorization or denial rules. Enforcing these rules requires preliminary steps. The first step of a security process is identification: assigning an identity to an entity. For example, an individual (Bob) wants to attend a conference, he declines his identity by telling his name. Because his word should not be taken for granted, his identity must be verified: this is the authentication. Therefore, the conference organizer authenticates Bob by asking for his ID card. Next, an authorization is delivered based on a control mechanism. The conference organizer checks if Bob is on the participants' list before allowing him to attend the event. Even if the first 2 steps are mandatory, they are already well covered and solutions exist even for distributed systems. Thus, in this Thesis, we will focus on the control mechanisms itself i.e., the authorization step.

Security Properties

A security policy may be composed of basic rules defining what it is to be secure. Nevertheless, subsets of rules may enforce more general objectives called security properties. For example, you may install sensors and alarms in your house. Your rules are to activate the sensors whenever you are away from home and trigger the alarms if someone is detected by a sensor. But your general objective i.e., the property you want to hold, is to be protected from theft and your installation is a mean to enforce this property. A security policy may be directly stated as a set of security properties.

In security, three main concepts commonly known as the CIA-triad (not to be confused with the US agency) has been widely used for decades: Confidentiality, Integrity and Availability. Both the Department Of Defense guidelines (TCSEC/Orange Book) [START_REF] Tcsec | Trusted Computer System Evaluation Criteria[END_REF] edited in 1985 and the more recent Common Criteria (ISO/IEC 15408) international standard define security as an integration of availability, confidentiality and integrity. They define the three as follows.

Confidentiality

It is the absence of unauthorized disclosure of information. Often companies have internal confidential documents for the sole use of agents with appropriate clearance. These documents can contain trade-secrets or marketing strategies and their public disclosure may result in loss of competitive advantages or loss of reputation. It should not be confused with privacy which is the right of individuals to hold information about themselves in secret, free from the knowledge of others [START_REF] O'brien | Privacy, confidentiality, and security in information systems of state health agencies[END_REF]. For example, improper enforcement of confidentiality of healthcare records may arise privacy issues, especially if records are not anonymized.

Integrity

It is the absence of unauthorized system alteration. Information has values only if we are sure that it has not been tampered with. For example, if you are transferring $100.00 to a remote account, you do not want the amount to be changed to $10,000.00. Integrity ensures the absence of malicious or unintentional modification or destruction of an asset.

Availability

It is the absence of unauthorized denial of use. A service or data is available if any authorized entity accessing it is served in a reasonable timeframe. Availability may be related to fault-tolerance and reliability [START_REF] Laprie | Dependable computing and fault-tolerance[END_REF]. For example, an attacker floods the network to saturate accesses to a website. The website would not be able to serve all users in timely manner due to the huge proportion of dummy requests. The attacker has disrupted the ability of the website to deliver its service in the expected timeframe. In particular, he has not necessarily read or modified any unauthorized data but he has prevented an authorized user to do so and thus has broken the availability property.

Isolation

It is the absence of unauthorized disclosure and/or modification of information. It is a composition of integrity and confidentiality properties. In the general sense, isolation is used to refer to the absence of any possible interactions (except intended ones e.g., public interfaces) between two entities. As a straightforward example, isolating two antagonistic persons may be done by putting them into two separate rooms. This idea is used for isolating applications from each other or from the rest of the system.

Mandatory and Discretionary Control

The enforcement of security properties depends on the environment they apply to. At first, information security was a critical matter for the military. Typically, information was classified into top-secret, secret or public domains and an agent with top-secret clearance could access all three domains whereas an agent with public clearance would be limited to accessing public domain information. These constraints on the information are part of the security model. Nowadays, information security is critical to everyone and these models are not suitable outside the military domain.

A Security Model specifies the entities of the system, the classification/hierarchization of entities, how permissions are set or may be updated. It usually focuses on one or few security properties.

A Control Model defines who is in charge of delivering permissions.

The most widely used control model is the Discretionary Control model where controls on access to an object may be changed by the owner of the object itself. For example, in the traditional read-write-execute GNU/Linux permissions, a file's owner may change its permissions as he wishes. Moreover, the privileged (root) user is allowed to update permissions for any object in the system. Consequently, a juicy situation for an attacker is to obtain the root identifier. Furthermore, as human configuration of security permissions is error-prone, it often leads to globally insecure systems.

In opposition to the discretionary control model is the Mandatory Control model. In it, a third-party distinct from any user of the system (privileged or not) regulates the set of permissions. Consequently, even the most privileged user must follow the security policy and has no ability to modify it. For instance, SELinux [START_REF] Loscocco | Integrating flexible support for security policies into the linux operating system[END_REF] is a mandatory access control implementation on Linux-based systems developed by the NSA where even the root user may be constrained by its permissions. Originally, SELinux was an implementation of the Flask operating system security architecture [START_REF] Spencer | The flask security architecture: System support for diverse policies[END_REF] which focuses on providing an administratively-defined security.

Access Control

In an Access Control (AC) model, permissions about accesses to entities are explicitly stated. Typically, the question you ask is: "Can I read this file?" and the answer depends on your identity, your affiliations (e.g., groups, domains), for example: "Because you are an administrator, access is granted to you". Access control models may be classified as discretionary or mandatory.

Lampson The first Discretionary Access Control (DAC) model was formalized by Lampson in 1971 [START_REF] Lampson | Protection[END_REF]. He divided entities into active and passive entities, respectively called subjects and objects. A subject is typically a user or a running process whereas an object is a file or a binary code. Subjects are grouped into domains. He proposed an access matrix with domains in rows and objects in columns to define permissions. Lampson's model was improved by Harrison et al. [START_REF] Harrison | Protection in operating systems[END_REF] with the HRU model introducing generic permissions (e.g., own, read, write, execute), system commands (e.g., create file, update rights), and actions to add/delete permissions/entities. Harrison et al. demonstrated that, in the general case, verifying a discretionary control model is undecidable. This proof is essential to discard discretionary approaches for guaranteed security properties.

Bell-Lapadula The Bell-Lapadula model [START_REF] Bell | Secure computer systems: Mathematical foundations[END_REF] focus on data confidentiality in a military context. It is a Mandatory Access Control (MAC) model. It relies on the concept of state machine where all possible states of the system are divided into secure and insecure states. Consequently, It is proven that a secure system can only transit from a secure state to another secure state. A state is secure when permissions of subjects to objects comply with the security policy that includes the following main security properties:

• A subject at a given security level may not read an object at a higher security level (no read-up).

• A subject at a given security level must not write to any object at a lower security level (no write-down).

Bell-Lapadula model only applies to multilevel security systems based on clearance or need-to-know principles. As a result, it is not suited for any collaborative/competitive structure not representable by a lattice. Furthermore, without declassification process, the data tends to go up the security clearance level without any chance to go down.

Biba The Biba model [START_REF] Biba | Integrity considerations for secure computer systems[END_REF] is a MAC model focusing on data integrity. It is the direct inverse of Bell-Lapadula confidentiality model adapting no-read-up and no-read-down properties into no-write-up and no-write-down. Again, it only applied to multilevel security systems.

Role-based Access Control

In previous models, permissions are set for each user and users may be attached to groups. It was noticed that computing permissions or group membership does not scale in a decentralized model (e.g., discretionary). For example, in the read-write-execute Linux model, determining the right for accessing a file requires computing the traversal of all directories. To support larger systems, Rolebased Access Control (RBAC) was proposed [START_REF] Sandhu | Role-based access control models[END_REF]. Instead of having groups of users, users have roles. A major difference between groups and roles is that groups are typically treated as a collection of users but not as a collection of permissions. A role, serving as an intermediary, is both a collection of users and a collection of permissions. Role-based access control model tackles delegation [START_REF] Wainer | W-RBAC-a workflow security model incorporating controlled overriding of constraints[END_REF]: allowing a lower-level user to do an action in the upper-level user stead. For example, the grant permission is implemented in most databases to add a permission to users. OASIS [START_REF] Bacon | A model of OASIS role-based access control and its support for active security[END_REF] is a RBAC architecture for secure interoperation of services in an open, distributed systems. RBAC eases the specification and administration of security by structuring entities around roles and emphasizing on delegation of rights, but it does not improve security.

Information Flow Control

In an Information Flow Control (IFC) model, the goal is to understand and control how information flows between entities that is how entities interfere with each others. To the same question "Can I read this file?", an IFC mechanism will wonder: "It depends on what you and the other entities have done before".

Information Flow Control and Access Control can be seen as different but complementary approaches to security [START_REF] Kafura | An information flow control meta-model[END_REF]. Access Control makes explicit statements about permissions for a subject to realize a specific action on a resource whereas information flows are implicit. However, IFC makes explicit statements about permitted information flows whereas permissions for a specific action are implicit.

In short, Access Control checks place restrictions on the release of information but not its propagation. Once the information is released from its container, a program may (maliciously or unwillingly) leak the information to an unauthorized entity. Denning [START_REF] Denning | A lattice model of secure information flow[END_REF] performed basic research on IFC in 1976. He defined the concept of an information flow policy as a triple ă SC, Ñ, ' ą where:

• SC is a set of security classes.

• ÑĎ SC ˆSC is a binary may-flow relation.

• ' : SC ˆSC Ñ SC is a binary class-combining or join operator on SC.

An important property in IFC research is non-interference [START_REF] Goguen | Security Policies and Security Models[END_REF]. It means that a group of users, using a certain set of commands will not interfere with another group of users if what the first group does with those commands has no effect on what the second group of users can see. This property demonstrates the key difference with access control by looking at effects and consequences rather than permissions.

IFC allows enforcing end-to-end security policies: from the place information originates to leaving the system [START_REF] Sabelfeld | Language-based information-flow security[END_REF]. It is studied at two levels: language and system.

Language-based Information Flow Control

A Language-based IFC focuses on flows inside a program, in particular between variables [START_REF] Sabelfeld | Language-based information-flow security[END_REF]. Flows can be explicit or implicit. Suppose the following programs with 2 variables (secret and public): public := secret An explicit flow is created between the two: public contains the secret value.

if secret then public := 1

An implicit flow is created between secret and public: inspecting the value of public allows inferring the boolean value of secret.

It is particularly important for a cryptographic library not to expose critical information such as secret keys used to encode data. For example, in [START_REF] Brumley | Remote timing attacks are practical[END_REF], Brumley et al. has shown that extracting private AES keys from a remote client based on OpenSSL implementation is practical.

One direction envisioned to tackle explicit and implicit flows is Security-Type Systems [START_REF] Smith | A sound type system for secure flow analysis[END_REF]. In this approach, the types of program variables and expressions are augmented with annotations that specify policies on the use of the typed data. Then, information flows are statically checked at compile-time to guarantee that no paths exhibit an insecure flow. In [START_REF] Myers | JFlow: Practical mostly-static information flow control[END_REF], Myers proposes JFlow: an extension to the Java language permitting static checking of flow annotations. For example, to the previous implicit flow, he proposes to attach labels to types and he obtains the following solution: Language-based solutions cannot cope with system-wide security which is essential to tackle large systems involving multiple organizations.

System-based Information Flow Control

A System-based IFC focuses on controlling flows of a system. The goal is to track and control how information flows between entities e.g., processes, files, sockets. The approach is less invasive than language-based IFC i.e., it does not require any modifications of the application. However, it comes with a loss of granularity and cannot cope with the previous example of cryptographic library leaks.

System-based IFC has been popular for building Intrusion Detection Systems (IDS) where the objective is to monitor activities in a system and detect potential intrusion by a malicious user/program [START_REF] Hofmeyr | Intrusion detection using sequences of system calls[END_REF][START_REF] Qin | Lift: A low-overhead practical information flow tracking system for detecting security attacks[END_REF][START_REF] Yin | Panorama: Capturing system-wide information flow for malware detection and analysis[END_REF][START_REF] Zimmermann | An improved reference flow control model for policy-based intrusion detection[END_REF]. PigaOS [START_REF] Briffaut | Formalization of security properties: enforcement for MAC operating systems and verification of dynamic MAC policies[END_REF] is a context-based IFC system originally designed as an IDS supervising indirect flows within a SELinux policy but it has evolved into a control mechanism later on. The complexity of writing a policy often leads PigaOS to detect false positives (i.e., normal flows detected as malicious).

Most models relies on Tainting techniques. The idea is to attach colors to entities and to propagate them whenever an interaction is made [START_REF] Clause | Dytan: a generic dynamic taint analysis framework[END_REF]. For example, if a sensitive file is tainted in red and as a user you read it, you will inherit the red color. If now you write another non-sensitive file, it will be contaminated by the red color too. In [START_REF] Enck | Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones[END_REF], Enck et al. propose TaintDroid: a system information-flow tracking system for realtime privacy monitoring on smartphones. Information is tracked at multiple-levels: variablelevel, method-level and file-level. The process itself is not purely system-based: variables and methods are tracked. But this is only possible for a system based on a single language e.g., Java for Android.

Decentralized Information Flow Control

A Decentralized Information Flow Control (DIFC) is an approach to security that allows application writers to control how data flows between the components of an application and the outside world [START_REF] Krohn | Information flow control for standard OS abstractions[END_REF]. In a DIFC approach, part of the security is managed independently by multiple components.

In [START_REF] Myers | Protecting privacy using the decentralized label model[END_REF], Myers proposed JIF (previously JFlow), a language-based DIFC dedicated to privacy protection in Java. JIF is based on decentralized labels where labels are attached to variables. Example of a label is to 1 : r 1 , r 2 ; o 2 : r 2 , r 3 u where o 1 , o 2 are owners and r 1 , r 2 , r 3 readers. Owners and readers are principals: groups or roles composed of entities, and principals are ordered under a lattice. The particularity of decentralized labels is that a principal may choose to selectively declassify its own data, but does not have the ability to weaken the policies of other principals.

The decentralized labels of JIF are reused in AsbestOS [START_REF] Efstathopoulos | Labels and event processes in the asbestos operating system[END_REF], HiStar [START_REF] Zeldovich | Making information flow explicit in HiStar[END_REF] (which is based on AsbestOS) and Flume [START_REF] Krohn | Information flow control for standard OS abstractions[END_REF] at the system level. AsbestOS and HiStar implement labels as a combination of categories (similar to principals) and security levels. Flume uses secrecy and integrity as distinct labels.

All these works focus on a limited set of security properties (i.e., confidentiality and/or integrity) in multi-level security systems.

Access Control and Information Flow Control

It is not easy to see if an AC policy can leak information to a potential attacker and many studies have been led in this direction, namely AC policy analysis [START_REF] Bertolissi | Automated analysis of rule-based access control policies[END_REF]. In [START_REF] Guttman | Verifying information flow goals in security-enhanced linux[END_REF], Guttman et al. use model checking to determine whether information flow security goals hold in a system running SELinux. Information flow statements are expressed in Linear Time Logic [START_REF] Pnueli | The temporal logic of programs[END_REF] i.e., a logic with temporal modalities where formulas are statements about the future of executions e.g., , a condition will be true or will be after another fact becomes true. Similarly, Hicks et al. [START_REF] Hicks | A logical specification and analysis for SELinux MLS policy[END_REF] check SELinux policies against information flow properties formalized as a logic implemented in Prolog. Nevertheless, this analysis process is done offline and must be redone every time the policy changes. Accordingly, it is impossible to do it on a dynamic system where some actions may impact the policy (e.g., creating or deleting a user).

At the opposite, in [START_REF] Kahley | Factoring high level information flow specifications into low level access controls[END_REF], Kahley et al. factorize high-level information flow specifications into low-level access controls. Their model is limited to confidentiality and integrity labels to cope with composable specifications.

Discussions

Access control approaches are easy to verify and thus incur low overhead. But they lack the ability to control the propagation of information in a system which is important to guarantee end-to-end security. Static analysis of access controls may permit verifying information flow properties but it cannot cope with dynamic systems where users, groups, roles are created or removed at runtime (i.e., elasticity is out of the scope of this Thesis).

Most AC or IFC approaches tackle small sets of properties, usually confidentiality and integrity (or both). Adapting them to integrate more flexible properties seems at least difficult. Most models are based on multi-level security which we believe is too rigid to represent multi-organizational systems where security levels alone have no sense.

Languaged-based IFC and system-based IFC can be seen as complementary. The first is suitable to control flows between programs' variables and can deny implicit flows but to provide system-wide security the second is more appropriate. The downside of IFC is the computation complexity graving performances.

Most of the literature tends to associate discretionary or mandatory terms to access control and neglects the fact that information flows can also be controlled in a discretionary or mandatory fashion. Discretionary approaches cannot provide strong, provable security guarantees despite their are widely available and somehow necessary.

In this Thesis, we mainly consider on Mandatory Information Flow Control at system level and see it not only as a standalone security mechanism but also as a way to configure other security mechanisms such as access controls, firewalls, cryptographic protocols and placement algorithms. That is why the considered formal logic mainly deals with Information Flows. However, that formal logic enables to automatically compute or configure the underlying security mechanisms even if mandatory mechanisms are not available.

Distributed Systems

Distributed Systems [START_REF] Gregory | Foundations of multithreaded, parallel, and distributed programming[END_REF] are groups of interconnected computers. Physical machines (computers) are distributed across different locations from the room next door to the other side of the globe and communicate through a network. Each machine has its own local storage and processing power and shares information with other machines to complete a common objective. Machines may collaborate to process a complex computationalintensive task such as weather forecast. Each machine may deliver more lightweight services e.g., webmail, data storage to users and thus share resources to diminish costs and/or provide high availability. In a distributed system, each machine is referred as a node of the system.

In this section, we focus on major targeted infrastructures and highlights their key characteristics.

Clusters

A Cluster consists of a set of loosely or tightly connected computers working together. Initially, the idea was to interconnect commodity hardware to build a cost-efficient distributed system at a time when a single computer was not powerful enough to deal with users' needs. Clusters exist in all possible scales: from two to thousands of nodes.

Nowadays, web giants build and maintain large Clusters to sustain users growing demand in high quality services processing massive data sizes. For example, in 2003, Google [START_REF] Barroso | Web search for a planet: The Google cluster architecture[END_REF] reported combining more than 15,000 commodity-class computers in multiple Clusters in order to handle web search queries all over the world. Their high-throughput solution is more cost-effective than a comparable system built out of a smaller number of high-end servers such as mainframes.

In private sector, a Cluster is typically for the sole use of a single company (e.g., Google, Facebook, Yahoo) and must be secured against external threats: cyberattacks conducted through Internet.

Grids

As Clusters are very popular and widely adopted by many organizations, a natural question is whether it is possible to federate the resources of organization to build an even more powerful distributed system. Grids provide a solution to this issue. The term originated as a metaphor: any user should be able to access computing resources as easily as on US electrical power grid and in a standard fashion. In [START_REF] Foster | The Anatomy of the Grid: Enabling Scalable Virtual Organizations[END_REF], Foster et al. define that Grids solve the problem of coordinated resource sharing and problem solving in dynamic, multi-institutional virtual organizations.

The key shift is the virtual organizations characteristic. In [START_REF] Foster | A security architecture for computational Grids[END_REF], Foster et al. discuss a security architecture for Grids. They devise a security policy integrating an heterogeneous collection of locally administered users and resources but fall short in sound and scalable solutions. In particular, the question of interoperability between local access control policies is left open.

In practice, Grids in production are mostly scientific national or international platforms where users are supposed to be honest i.e., no intentional misbehavior. Therefore, security are mainly strengthened for authentication and credentials [START_REF] Butler | A national-scale authentication infrastructure[END_REF][START_REF] Foster | A security architecture for computational Grids[END_REF][START_REF] Jin | VO-sec: An access control framework for dynamic virtual organization[END_REF][START_REF] Ramakrishnan | An authorization framework for a Grid based component architecture[END_REF][START_REF] Yan | Daonity: An experience on enhancing Grid security by trusted computing technology[END_REF]. The Grid is an highly heterogeneous platform from the hardware infrastructure, the middleware to provision resources, and the security managed locally by each organization. In such environment, providing strong security guarantees over the whole Grid is more than difficult.

Clouds

The concept of Cloud Computing [START_REF] Zhang | Cloud computing: state-of-the-art and research challenges[END_REF] goes back to 1960 with the introduction of Utility as a service [START_REF] Parkhill | Challenge of the computer utility[END_REF] by John McCarthy speaking at the MIT Centennial. The goal was to bill computing power as water or electricity. The computing power would have been provided by a large infrastructure such as a shared Grid. In the past, building such infrastructure was impossible due to high costs and the lack of network efficiency. However, nowadays with affordable and efficient hardware, it has become possible.

The mainly considered characteristics are:

• On-demand resources. Users can use computing or storage resources as needed automatically without requiring human interaction with the service provider.

• Elasticity as dynamic scaling. Users can automatically adjust their resources upward or downward depending on the current workload hence reducing costs.

• Multi-tenants provisioning. Utilization of resources is maximized by sharing them between multiple tenants.

• Pay-as-you-go. Most widely known economical model, users pay per time slice ( 1 hour) of provisioning.

Cloud Computing enables cost reductions due to resource sharing. Instead of investing into on-premises infrastructures they have to manage, maintain and secure, companies can take advantage of Cloud elasticity and scalability to dynamically adjust (and pay) their resources according to their business. For example, an online tickets shop has a peak demand during the few days whenever an event is open for tickets sale. Cloud Computing is well-suited and promising in such cases. Without, it would have bought and managed resources according to the peak thus having an overdimensioned infrastructure for normal periods.

Four organizational models have been identified for Cloud architectures:

• Public. The service is available to the general public and managed by a third party.

• Private. The service is dedicated to a company but may be managed by a third party.

• Community. The service is shared between a common community composed of multiple parties and may be managed by a third party.

• Hybrid. The service is orchestrated between at least two Cloud models (public, private or community). Usually, an organization provides and manages some resources in-house (private) and has others provided externally (public).

Cloud computing is usually divided into three service models. Figure 1.1 illustrates the differences between each model and in respect to on-premises infrastructures where the provider manages the entire stack. Service as a Service (SaaS) Also referred to as on-demand software, it proposes services for end-users. For example, Google Drive and Dropbox provide SaaS solutions.

The main enabling technology for Cloud computing is virtualization. It allows offering homogeneous virtual resources to the tenant on top of heterogeneous physical resources. Shared resources are efficiently managed and, to some extent, isolate tenants between each other. We detail virtualization techniques in Section 1.4.

Federated Clouds

A single Cloud provider is bounded in number of clients. If he wants to sustain a huge peak demand, he must invest in a larger infrastructure at the risk of overprovisioning, otherwise he will be forced to refuse new clients at the risk of loosing reputation and potential business. A profit-oriented approach consists in building a Cloud federation [START_REF] Celesti | How to enhance cloud architectures to enable cross-federation[END_REF]. In this approach, the benefit is mutual: a saturated provider could delegate extra requests to other providers; the first keeps satisfying the demand and the second generates new revenues from its underused infrastructure. Federated Clouds are also supposed to provide users with better quality of service.

Federated Clouds face many obstacles. Because Clouds provider have different architectures, technological choices, pricing models, etc., building a unified interoperable federation is a challenge. Moreover, how can one be sure that each provider of the federation is able to ensure the same security guarantees.

Cloud Security

In a 2015 security survey in collaboration with 250,000+ contributors2 , security is still the biggest perceived barrier to further Cloud adoption. Yet, 22% of the contributors have experienced less security breaches in public Clouds compared to on-premise whereas 28% have experienced more breaches. This result could be explained as small and mediumsized enterprises cannot afford costly security solutions for their in-house infrastructures. As a result, for them Clouds concentrate security expertise and thus improve their overall security even if Clouds providers secure their infrastructures and not what is deployed (e.g., VMs, applications, data) on top.

However, Clouds present a real challenge to security researchers [START_REF] Zissis | Addressing cloud computing security issues[END_REF]. With the augmentation of parties, threats of data compromises increase as well. Outsourcing data in the Cloud is similar to delegating control over data to the provider. Then, the question is how much do you trust your provider. Furthermore, multitenancy is at several levels including hardware: an attacker may provision resources to sit next to his victim and conduct exploits.

In short, Clouds must face both external threats (as on-premise data centers do) and internal threats due to multitenancy.

In Clouds, resources provisioning is opaque. It means the provider may arbitrarily provision resources located in the US or in Europe. However, depending on the country the resources are located, the legislation may differ and it matters [START_REF] Pearson | Taking account of privacy when designing cloud computing services[END_REF]. The risk exists that personal data may be used for profiling using data mining techniques or that business secrets are revealed to foreign competitors. For example, nothing forbid the US government to take a look at your data if you are not a US citizen and the problem is that major public Cloud providers have their infrastructures located in the US.

Virtualization

Virtualization consists in creating a virtual (rather than actual) version of computing components. It includes (but not limited to) hardware components (e.g., CPU, memory, devices), networks, operating systems, file systems, databases and applications. Virtualization is used to multiplex a single resource into multiple virtual ones. Accordingly, it allows the sharing of physical resources while virtual resources seem to be dedicated.

Hardware Virtualization is the virtualization of hardware components and operating systems. For example, virtualization allows for running Windows OSes on top of a Linux-based OS.

Figure 1.2 illustrates the principle of hardware virtualization. Compared to nonvirtualized systems, the operating system is replaced by an Hypervisor (or Virtual Machine Monitor) which role is to manage and run Virtual Machine (VM). A virtual machine is a virtual container for an operating system called Guest OS in opposition to the hypervisor sometimes referred as the Host OS.

Full Virtualization

In Full Virtualization, the hardware is almost completely simulated to allow the guest OS to run unmodified. The guest OS is not aware it is being virtualized and it does not require any modifications to run correctly.

Because guest OS and hardware are completely decoupled, full virtualization provides good security and performance isolation for virtual machines. Furthermore, migration (i.e., moving the guest OS from one hypervisor to another) is simple and portability is ensured: the same OS can run in a virtual machine or on a native hardware.

A key challenge for full virtualization is the interception and simulation of privileged operations, such as I/O instructions. A privileged operation has the ability to modify the state of other virtual machines. To keep privileged operations contained, binary translation [START_REF] Rosenblum | Virtual machine monitors: current technology and future trends[END_REF] techniques analyze the guestOS binary code to trap such operations and replace them with safe equivalent instruction sequences. The downside of binary translation is the high overhead it incurs.

Existing full virtualization technologies include Parallels, VMware, VirtualBox, Qemu/KVM.

Hardware-assisted Virtualization

The concept of hardware-assisted virtualization first appears on the IBM System/370 in 1972. To improve full virtualization (but also paravirtualization) efficiency and in particular overcome privileged instructions issues, hardware manufacturers have developed new processor extensions to specifically support virtualization. Intel and AMD have independently designed Intel VT-x and AMD-V for virtualization on x86 architectures. For instance, they both allow for direct access to I/O devices bypassing the hypervisor.

Paravirtualization

In Paravirtualization, the guest OS is offered a software virtualization interface to run. Therefore, the hardware is not simulated, instead the guest OS needs to be ported for the paravirtualization API (Application Program Interface). The value proposition of paravirtualization is in lower virtualization overhead: some instructions are non-virtualizable thus providing an API makes their execution by the hypervisor much more efficient. Hence, non-virtualizable instructions are replaced by hypercalls. Critical kernel operations (i.e., memory management, interrupt handling and time keeping) can also be managed through hypercalls.

In resume, a conventional OS distribution that is not paravirtualization-aware cannot be run on top of a paravirtualizing hypervisor. Paravirtualized OSes have better performance compared to full virtualization and also ensure isolated executions.

Existing paravirtualization technologies includes Xen and VMware.

Operating-system-level Virtualization

Operating-system-level virtualization is a shared-kernel virtualization technique. As such, it is not an hardware-based virtualization. In classic OS architectures, addresses space is divided into one user space and one kernel space. With operating-system-level virtualization, the kernel allows for multiple isolated user-space instances called containers. All containers share the same kernel but run as if they were standalone operating systems. Operating-system-level virtualization does not interpose any hypervisor or interface and contained applications run with native performances. Existing operating-system-level virtualization includes chroot, LXC (linux containers), Solaris Containers, FreeBSD Jails. Docker is a recent yet popular software based on LXC to easily build, package and distribute applications.

Currently, containers are not recommended for strong security isolation [START_REF] Reshetova | Security of OS-level virtualization technologies[END_REF]. As they share the kernel, applications can exploit any vulnerabilities to pierce through the container's boundaries and infect the rest of the system3 . However, with popularization, more effort will be put to provide additional security features to containers.

Discussion

Nowadays, most current applications are distributed to either process huge sets of data or offer highly available services. In the mean time, the evolution from Clusters to Grids then to Clouds demonstrate the need for systems supporting multiple organizations with the inherent risk of antagonistic concerns. In these shared environments, security is a key issue: how to store, process or exchange data in a securely manner. Clouds inherit major security concerns from Grids and Clusters plus introduce new ones. These new issues are 1.6. USE CASE CHAPTER 1. INTRODUCTION due to massive multitenancy but also to virtualization as a milestone to effectively build Clouds. We believe future systems design will all be about virtualization as it comes with large benefits e.g., flexibility, portability and interoperability.

Therefore, in this Thesis, we tackle any virtualization-based distributed system with multiple organizations sharing the infrastructure.

Virtualized Application Use Case

We need to have a good understanding of what to protect before designing any solution.

In this Thesis, we focus first on virtualized static n-tier applications even if our approach can tackle other classes of applications providing some adaptations. By virtualized, we suppose that the applications (processes, data, etc.) are packed into virtual machines and deployed on a virtualization-based infrastructure. Static, as opposed to dynamic, suppose that the application does not need any scale (up or down) at runtime. Once the application is deployed, it will run indefinitely without changing its resource requirements. Finally, n-tier characterizes an application usually composed of a set of low-level services (i.e., tier) offering a high-level one. The most common n-tier application is the 3-tier web service. It is composed of 3 low-level services: a frontend, a processing service and a backend database. Each of the low-level service can be instantiated multiple times to sustain the load, requiring a load-balancing mechanism to spread it between instances. Figure 1.3 illustrates a 3-tier architecture where the user sends requests to a web server (e.g., Apache). The request is relayed to an application server (e.g., Tomcat) providing a service. Finally, the service stores and retrieves its data from/to a database server. This Thesis has been conducted within the Seed4C project [START_REF] Blanc | Mandatory access protection within cloud systems[END_REF] where several use cases have been proposed. To better picture the kind of constraints and needs such applications may require, we present thereafter Ikusi's Advertising Content Manager for Airports: a multi-organizational n-tier use case for airport-related content.

Advertising Content Manager for Airports (Ikusi)

The Ikusi company offers a broad range of operational management solutions for smart cities, airports, security, mobility (including railways) and health. In particular, it proposes airport management systems coupled with public information and entertainment systems. These systems manage all airport services such as check-in/boarding, automatic processing of baggage delivery, public information (i.e., gates, announcements) and advertisements. Ikusi solutions are highly mutualized: the company proposes an external management of multiple airports with the same virtualized infrastructure. Airlines send information messages to an airport database application like planes routes, delays, passengers, then these information are exposed to airports operators and devices.

Because Airport management is complex, our use case focuses on the Advertising Content Manager called Musik4 . This use case is highly multi-tenant with several airports organized in groups. Each group has private information and data exposed by the Content Manager. For instance, employees information must be kept confidential to the airport they work for.

Contributions

Our problem is how to allow an end-user to specify a secured application and how to automatically enforce and guarantee the required security. In this Thesis, we propose a user-centric approach providing an automatic deployment of virtualized applications with an automatic enforcement of security policies. Our approach is materialized as a toolbox called Sam4C (Security-Aware Models for Clouds).

The contribution of this Thesis is to propose an end-to-end framework from an easyto-use modelization interface for the end-user to the deployment and enforcement of this model. First, we propose a unified model including the virtualized application i.e., the end-user application to deploy, and security requirements i.e., the application security properties to enforce. The idea is to model a virtualized distributed system i.e., a set of interconnected virtual machines, and the associated security policy. This modelization does not rely on any characteristic of the infrastructure. In particular, the user does not know about available security mechanisms. He specifies what he wants and the satisfaction of his requirements, how to implement them, is up to the deployment engine. Using Sam4C Modeling (implemented as a standalone Eclipse application5 ), the application can be modeled graphically and the security properties are textually specified with direct references to entities of the application model.

Second, the security enforcement relies on the hosting infrastructure, therefore we propose an infrastructure model i.e., a set of physical machines and networks, and a microarchitectual model i.e., the internal architecture of physical machines. The microarchitecture is used to compute our risk-metric quantifying how much information can leakage between two VMs sharing the same physical machine.

Third, we propose a formalization of the security properties called IF-PLTL. This formalization serves as a proof basis to divide a global property (securing a set of entities) into local typed properties (securing a single specific entity) during a phase called preprocessing. Indeed, existing enforcement solutions enforce properties on specific types of entities (e.g., VMs, Data, Network) whereas a property specified by the end-user protects different types of entities and cannot be enforced directly. Furthermore, we propose a dynamic monitor enforcing any property expressed in IF-PLTL and show that this monitor is effective but at the cost of complexity in time and space.

Fourth, using these models (obtained after preprocessing) as input, we propose a deployment with two different but complementary enforcement solutions: by placement and by automatic configuration. In the placement solution, the objective is to guarantee that the microarchitectural resources (CPU, RAM, etc.) allocated to the end-user satisfy the security policy. Indeed, shared resources may be used as a channel to illegally exfiltrate information. In the automatic configuration solution, security agents are dispatched in the virtual machines or at the infrastructure level. The idea is that each agent has a list of properties it knows how to enforce. Indeed, it knows the predefined security tools and policies and can select the right ones automatically. The deployment phase is realized by Sam4C Scheduler (implemented as a Java application). Sam4C Scheduler has been integrated with an open source Cloud software platform called OpenStack 6 .

Fifth, we illustrate our entire end-to-end workflow on a real industrial use case where the modelization has been realized by the company itself.

Structure of this Document

This Thesis' structure is mapped on our solution architecture depicted in Figure 1.4. In Chapter 2, we present our modelization composed of the virtualized application and the infrastructure detailed in Section 2.2, plus the security requirements detailed in Section 2.3. Then, Chapter 3 presents our IF-PLTL language formally defining security properties. In Chapter 4, we describe the deployment phase. This phase includes first the preprocessing (Section 4.1) which transforms the specified global security requirements into local security properties using formally proved equivalences, then the placement (Section 4.2) which maps VMs to physical hosts while satisfying some security properties, and finally the automatic configuration (Section 4.3) which enforces properties using mechanisms at the VM or host level. Lastly, Chapter 5 run through each previous steps with an Airport Content Manager use case.

Modelization of Security Requirements for Virtualized Distributed Systems

In the previous chapter, we have motivated the need to bridge the gap between security enforcement methods and specification requirements. To do so, we need to rely on a description of the characteritics of the application to secure and a description of these security requirements. To construct an house, an architect needs its plans and not the house itself. Similarly, we need a simplified representation (i.e., a model) of the application in order to deploy it and enforce a security relevant to this application. Besides, a model exposes an easy-to-use interface to the user to describe its application and the requirements (including the security).

This chapter discusses existing modelization methods. Using the efficient modeldriven engineering approach, we propose a modelization of virtualized distributed systems, their security requirements and infrastructures they are deployed on.

State of the Art

A model is a simplified view of the reality. A model focuses on some aspects of the system it represents. For example, to build a house, an architect will use different plans: some for describing how the building will look like including the dimensions of each room and others to describe accesses to electrical, water and telecommunication networks. In our case, our goal is to describe how the user's application is structured and what security the user needs. The level of details must be sufficient to automatically deploy the application and enforce the security requirements. The last model to provide is the infrastructure hosting the application. Indeed, some security issues are due to insecure configurations at the host level. For example, sharing too many resources with a malicious tenant is dangerous. Having a comprehensive infrastructure resource model is critical to control which resources may be shared.

In this section, we review existing works on security models for virtualized distributed systems and show that despite many approaches have been proposed to model applications, security models are mainly limited to RBAC policies and there is little effort to propose a sound and formal global security view of a complex distributed application.

Security Requirements Models

Many models have been proposed to model security requirements (also security properties). In the previous chapter, we have presented the main security models (e.g., access control, information flow) but they are mathematical models which are too complex to be exposed to a user as is (we will discuss them in the next chapter). In this section we are interested in approaches for specifying security properties of a complex application in a user-friendly fashion with automatic enforcement procedures whenever possible.

Security Level-Agreements

One trend is to consider security as a service which can be qualified i.e., measured and evaluated.

A Service-Level Agreement (SLA) [START_REF] Keller | The WSLA framework: Specifying and monitoring service level agreements for web services[END_REF] is a service contract between service provider and service user. A SLA is composed of a list of Service-Level Objectives (or Service-Level Target) where each objective is a quality-of-service value for a specific characteristic. For example, a user may require a minimum network bandwidth measuring in Mbps (Mega bits per second). As a SLA is a contract, it also mentions the responsibilities of the involved parties (i.e., penalties), especially in case the provider fails to delivery the expected level of service. If the approach sounds compelling for security, one major issue is how to evaluate the quality of protection and know whether the objectives are fulfilled.

In [START_REF] Henning | Security service level agreements: Quantifiable security for the enterprise?[END_REF], Henning discusses the possibility of establishing a security SLA for enterprises. His approach is based on standards and recommendations and focuses on contingency planning and user training. For example, one service requirement is Security violations introduced by individuals due to oversight or intentional introduction to the systems and it is measured as a percentage of security incidents introduced by users within target systems. Then, the best quality of service is achieved if there is less than 2% of security incidents. The author himself asked whether such metric is relevant to indicate the quality of the organization security.

In [START_REF] Bernsmed | Security SLAs for federated cloud services[END_REF], Bernsmed et al. propose a security SLA for federated Clouds. Their approach is based on security mechanisms divided into three resource types i.e., Storage, Processing and Network. For instance, one network security mechanism is integrity protection but the objective is stated in textual form e.g., All text messages will be digitally signed.

To our knowledge, security service requirements works are aligned on standards and recommendations (e.g., Cloud Security Alliance, NIST, Common Criteria) where security is expressed in natural language. These work can be viewed as a list of good practices which may relatively improve the security but cannot enforce end-to-end security with strong guarantees (e.g., with formal proof).

Security Policy Standards

Specific standards have been elaborated to express security policies for distributed web services.

WS-Security [START_REF] Atkinson | Web services security (ws-security)[END_REF] aims at providing quality of protection to SOAP (Simple Object Access Protocol) messages 1 . The WS-Security standard describes for example how to encrypt a message (for confidentiality), how to sign a message (for integrity) or how to attach security tokens to a message. Therefore, it contains a low-level specification of how the security is implemented (e.g., which cryptographic algorithm, what size of keys) and do not focus on the security objectives to achieve.

XACML [START_REF] Moses | Extensible access control markup language (XACML) version 2.0. Oasis Standard[END_REF] (for eXtensible Access Control Markup Language) is an OASIS standard defining access control policies in XML. It comprises access rules, roles and delegation concepts. One goal is to promote interoperability between access control implementations by multiple vendors. In XACML, a rule may be conditional to be triggered in reaction to a situation or event. The functionalities are similar to Ponder [START_REF] Damianou | The ponder policy specification language[END_REF]. Both XACML and Ponder focus on access control which is not sufficient to enforce end-to-end security objectives (i.e., information flows).

Model-Driven Security

For a decade, model-driven security has been investigated as a mean to help engineers integrate security concerns at design. SecureUML [START_REF] Basin | A decade of model-driven security[END_REF][START_REF] Lodderstedt | SecureUML: A UML-based modeling language for model-driven security[END_REF] is designed to specify authorizations policies based on RBAC extended with constraints. Constraints are expressed in OCL (Object Constraint Language) and mapped to a first-order logic to be able to use formal verification such as theorem-proving tools. This is a good step toward automatic security. But, SecureUML is limited to expressing access controls for applications. It cannot help secure with existing applications and cannot tackle high-level objectives such as information flows.

Interestingly, Nguyen et al. have conducted a system review of model-driven security in [START_REF] Nguyen | A systematic review of modeldriven security[END_REF] by selecting the 80 most relevant papers from 10.633 relevant papers. They found that:

• Most papers focus on authorization and confidentiality while only a few address other security concerns (e.g., integrity, availability, authentication).

• Most security modeling languages lack a thorough semantic foundation (which the authors recognized to be important).

• An integrated approach for the generation of functional code and security infrastructures was incomplete.

According to the authors, the literature is limited to specific, isolated security concerns, and lack formality, automation, process-integration and evaluation.

Most of the literature focuses on designing secure applications whereas our goal is to design secure systems composed of applications. To our knowledge, no model-driven work has tried to tackle larger systems with information flows as security objectives.

Component-based Models

Many frameworks and models have been proposed to design applications in virtualized distributed systems.

A popular approach is to use component-based models [START_REF] Szyperski | Component Software: Beyond Object-Oriented Programming[END_REF]. A component is a functional piece of code exposing its interfaces to communicate or coordinate with other components. The idea is to have reusable modules.

One approach is to use components to automatically deploy and configure the application stack within virtual machines. These tasks are traditionally done using hand-made scripts. For example, in [START_REF] Etchevers | Self-configuration of distributed applications in the cloud[END_REF], Etchevers et al. presents VAMP, a Virtual Applications Management Platform. Automated steps are the generation of VM images2 , launch of VM instances3 , local configuration of software and global configuration of dependencies between components. The OASIS standardization consortium has defined a Topology and Orchestration Specification for Cloud Applications (TOSCA)4 [START_REF] Binz | TOSCA: Portable automated deployment and management of cloud applications[END_REF] to enhance the portability and management of Cloud applications and services across Clouds and during their whole lifecycle. Many works are based on TOSCA to propose a runtime for TOSCAbased Cloud applications [START_REF] Binz | OpenTOSCA -a runtime for TOSCA-based cloud applications[END_REF] or provide a modeling tool to ease the specification [START_REF] Kopp | Winery -a modeling tool for TOSCA-based cloud applications[END_REF]. In [START_REF] Waizenegger | Policy4tosca: A policyaware cloud service provisioning approach to enable secure cloud computing[END_REF], Waizenegger et al. define security policies in TOSCA and propose a mechanism for automatic processing of these policies. As an example, the authors describe a region policy constraining VMs to be instantiated in specific geographical regions (e.g., EU, US). We do not consider geographical constraint as security. It does not provide any security feature and cannot fit alongside properties like confidentiality or integrity. Instead, we consider it as an environmental constraint such as energy power. Similar to TOSCA is MODAClouds [START_REF] Silva | Model-driven design of cloud applications with quality-of-service guarantees: The modaclouds approach, micas tutorial[END_REF] which supports the design of multi-cloud applications and aims at automatic provisioning, deployment and adaptation at runtime on the basis of an application model.

Component-based models are sound and appealing. Many complex frameworks have been developed. However, as our primary concern is security, we prefer to focus first on designing a much simple but security-centric model rather than investing extensive engineering effort to adapt existing frameworks for security. Integrating our findings back to standard frameworks is part of our future work though.

As model-driven security before, component-based models follow a model-driven approach we detail thereafter.

Model-Driven Engineering and Metamodeling

Thanks to object-oriented programming, engineers and computer scientists are familiar with the notions of abstraction and representation. They define classes or objects and instantiate them i.e., each attribute has a value. For example, one can define vm alice and vm bob : instances of a class VM where attribute vcpu is set to 2 and 4 respectively. A metamodel is a model of models and a model is designed to be an instance of a metamodel. In the previous example, VM is a model of vm alice , vm bob and the object Class is a model of VM. Indeed, we can define other classes e.g., Network, Data instances of Class.

As depicted in Figure 2.1, metamodeling is divided into 4 levels (from M0 to M3) with:

• M0 -System. It is the real system without simplification or abstraction. In our context, M0 includes the real (physical) infrastructure, the virtual machines (as implemented in KVM or Xen) and virtual networks.

• M1 -Model. It is a simplified representation of the reality. As presented above, the representation of two VMs (called vm alice , vm bob ) is a model.

• M2 -Metamodel. It is an abstraction of models. Using the previous example, the object V M is a metamodel of the model (vm alice , vm bob ).

• M3 -Metametamodel. Also called Meta-Object Facility (MOF), it is a model to describe metamodels. For example, UML (Unified Modeling Language) allows us to define the object V M and thus, it falls into the metametamodel category. There is no need for upper levels as metametamodels can represent themselves e.g., UML can be modeled in UML. We have previously said that component-based models and model-driven security follow a model-driven engineering methodology. Model-Driven Engineering (MDE) is a software development methodology that aims at automating complex programming tasks such as providing support for system persistence, inter-operability, and distribution [START_REF] Atkinson | Model-driven development: a metamodeling foundation[END_REF]. Its foundation is the metamodeling paradigm. Reducing complex programming tasks can be achieved by abstracting system-specific constraints and providing automatic transformation. For example, an engineer often faces the problem of designing a multi-platform application. In a model-driven approach, he will design a generic model of the application and use automatic tools to refine it into system-specific versions.

M3 -Meta-meta-model M2 -Meta-model M1 -Model M0 -System

Our Unified Metamodel

Security specification is often complex and requires field expertise. For instance, SELinux exists for decades and is recognized as a great security mechanism. But writing a correct SELinux policy is complicated even for a knowledgeable administrator. We believe that if a security specification tool is simple to use, it will be an incentive to a wider adoption. Therefore, we acknowledge this challenge and work toward a more user-friendly interface.

To do so, we follow a MDE approach to have a unified view of a security-aware system and automatically process it to obtain a secure deployment. In addition, we benefit from MDE to generate a multi-platform (Windows, Linux and MacOS) modeling tool with automatic upgrades as metamodels are progressively enriched with new constraints or features. For this purpose, we use the Eclipse Modeling Framework (EMF) to generate and maintain our modeling toolbox called Sam4C (Security-Aware Models for Clouds) 5 [START_REF] Lefray | Security-aware models for clouds[END_REF].

Sam4C is designed to be easy to pick up for end users like the Seed4C partners hence it offers a graphical interface to model the application and a textual language to specify the security requirements. The graphical interface is generated using GMF 6 (Graphical Modeling Framework) and the textual language (called Domain Specific Language) is generated using Xtext 7 . Both frameworks are based on EMF as illustrated in Figure 2.2. An EMF resource is a persistent document containing modeled contents. It is abstract: it is only a template (i.e., list of classes and methods). We depicted two existing implementations: XMIResource and XtextResource which generate respectively an XMI file (XML Metadata Interchange) and a text file. It implies that the same model may be exported in XMI (this is the default implementation) or text (providing a grammar). Finally, the model can be manipulated graphically with a GMF Editor.

The underlying metamodel is described in UML and stored in an ecore file. The security part is presented as a DSL (Domain Specific Language) using Xtext whereas the application part is presented graphically using GMF. The important point is that every element (textual, graphical or none of the two) are specified in single unified UML model: our metamodel.

Figure 2.2: Integration of GMF and Xtext with EMF

To begin with our presentation, Figure 2.3 is part of the UML metamodel for securityaware virtualized applications (without the infrastructure). In a MDE approach, all objects must be contained in a root object. In Sam4C, All is the root object containing our two-fold description:

• The architecture part describing the components of an application and their relations

• The security part describing the components of security requirements and their relations. In the following of this chapter, we present our metamodels of virtualized distributed systems (virtualized application and infrastructure) in Section 2.2 and their security in Section 2.3.

Modelization of Virtualized Distributed Systems

In this section, we present our metamodels of a virtualized distributed system which is composed of the tenant's virtualized application and the virtualization-based infrastructure it is deployed on.

Virtualized Application Metamodel

Our virtualized application metamodel is composed of two layers: the virtual layer and the application layer. Our metamodel must be able to represent a n-tier virtualized application.

Virtual Layer

At the virtual layer, the modeling consists in describing a set of interconnected virtual machines. Our model contains several node types:

• VM (Figure 2.4a). It encapsulates the application data and processes. As depicted in Figure 2.6, it is characterized by:

image. This is the disk image from which the VM is instantiated.

vcpus. The processing power requirement is usually specified as a number of virtual cpus in Clouds.

ram. The VM requires memory space to run.

storage. This is the disk space attached to the VM.

location. A VM may be constrained to be deployed only in a specified region (e.g., France, USA) for legal purpose. • Security Domain (Figure 2.4c). It is an abstract container for virtual machines and networks. It is useful to specify security properties on a group rather than on each individual entity. For example, one may want to specify that part of his application is isolated from the other.

The last entities of our virtual layer are networking components. As depicted in Figure 2.5, instead of representing a graph of VMs, we explicitly model the network, called VNet, as a circle (intranet on the figure). A VM has (one or multiple) virtual interfaces called Veth (eth0 on the figure) where each virtual interface is linked to a single virtual network via a VLink. Such modelization allows modeling two VMs to communicate through two different virtual networks e.g., a "public" network and an administration network, with distinct security properties.

Application Layer

At the application layer, the modeling consists in describing Data (e.g., files, databases) and Services (e.g., processes such as database engines) composing the application at a

Infrastructure Metamodel

Our virtualization-based infrastructure metamodel describes the platform virtualized applications are deployed on. It is divided into two layers, the infrastructure layer and the microarchitecture layer.

Infrastructure layer

Figure 2.9 is the root part of the infrastructure metamodel. Our model comprises:

• Node. Also referred as host or physical machine, it is characterized by disk space and a location. The location is not sensu stricto a security concept, and thus not included in the security part. However, due to differences in region or country legislation, it is important for users to specify a location constraint.

• INet (Infrastructure Network). In a virtualized infrastructure, virtual networks such as Software Defined Networks (SDN) [START_REF] Gude | Nox: Towards an operating system for networks[END_REF] can be instantiated between virtual machines. Multiple VNets may be mapped to the same INet. We discuss in Section 4.4 a preliminary solution where any constraint-free VNet with an external endpoint (e.g., a client) may be mapped on the same public INet. § ¤ <? xml version = " 1.0 " encoding = " UTF -8 " ? > < i n f r a : I n f r as t r u c t u r e xmi:version = " 2.0 " xmlns:xmi = " http: // www . omg . org / XMI " xmlns:infra = " http: // avalon . inria . fr / infra / " > < hasNodes name = " taurus -0 " disk = " 598.0 " location = " lyon " > </ hasNodes > < hasNodes name = " taurus -1 " disk = " 598.0 " location = " lyon " > </ hasNodes > < hasINets name = " Public " / > </ i n f r a : I n f ra s t r u c t u r e > ¦ ¥

Listing 2.1: Infrastructure XML with 2 Nodes and 1 INet

The infrastructure metamodel has no graphical view as it is not exposed to the client and can be automatically generated. Listing 2.1 is the XML representation of an infrastructure composed of 2 Nodes (i.e., taurus-0 and taurus-1) located in Lyon with 598Gb disk storage each and a single public INet.

Microarchitecture layer

In our approach, one way of satisfying isolation security properties is by placement. A class of security attacks consists in exploiting the shared microarchitecture to conduct cross-VM exploits (more details in Section 4.2). Traditional approaches from the literature ensure isolation through collocation/anti-collocation constraints [START_REF] Caron | Smart resource allocation to improve cloud security[END_REF][START_REF] Jayasinghe | Improving performance and availability of services hosted on IaaS clouds with structural constraint-aware virtual machine placement[END_REF]. These approaches never consider a more fine-grained allocation i.e., exploiting the microarchitecture to improve the consolidation and tackle the very reason for cross-VM attacks.

The microarchitecture is the internal organization of a physical machine. It includes the implementation of the processor and peripheral devices (e.g., I/O devices).

Nowadays, most physical machines are multiprocessors i.e., computers with two or more processing units sharing main memory and peripherals, in order to simultaneously process programs. Our model comprises both the two existing shared memory access models: SMP (Symetric MultiProcessing) and NUMA (Non-Uniform Memory Access).

A SMP architecture possesses multiples parallel cores connected to a single main memory (usually accessed uniformly across cores) through a memory bus and multiple levels of cache in between as illustrated in Figure 2.10.

A NUMA architecture is a logical evolution of the SMP architecture where shared memory is decomposed in multiple sockets and memory access latencies differ when a core accesses a local NUMA node or a remote NUMA node. As depicted in Figure 2.11, access to distant memory is done through an interconnection network.

For instance, Figure 2.12 is a model of a traditional SMP architecture as obtained from the Hwloc tool8 [START_REF] Broquedis | hwloc: A generic framework for managing hardware affinities in HPC applications[END_REF]. There is a single memory of 8005MB and 2 processor sockets each one composed of 4 cores with a private level 1 (L1) cache of 32KB per core and a level 2 (L2) cache of 6144KB per pair of cores. The element PU is a processing unit. It can be seen as a thread inside a core. In the architectures we address, there is one or two PUs. This element is irrelevant to our model as we do not take them into account for our placement decision. Indeed, as explained in [START_REF]Cache missing for fun and profit[END_REF], nearly all providers disable the possibility of sharing PUs due to the easiness of building a L1 covert channel.

Figure 2.13 is a NUMA architecture with two NUMA nodes of 16GB each (total of 32GB). Each processor socket has 6 cores sharing a level 3 (L3) cache of 15MB with private L1 (32KB) and L2 (256KB) caches per core.

To represent both architecture types, our microarchitecture metamodel depicted in Figure 2.14 explicitly defines two types of micro-elements, Core and Numa, as part of Figure 2.12: Intel Xeon E5420 QC Uniform Memory Access topology (Grid'5000 Genepi Node) from Hwloc a Node. We view the SMP architecture as a NUMA architecture with a single memory. The placement of a VM onto a host is realized by selecting a configuration of NUMAs and Cores that will be allocated to the VM.

As an example is Listing 2.2, the extension of the infrastructure model presented in Listing 2.1 with microarchitectural elements (i.e., cores and NUMAs). As the reader may notice, Taurus nodes are the simplified representation of the Intel Xeon E5-2630 presented in Figure 2.13. § ¤ <? xml version = " 1.0 " encoding = " UTF -8 " ? > < i n f r a : I n f r as t r u c t u r e xmi:version = " 2.0 " xmlns:xmi = " http: // www . omg . org / XMI " xmlns:infra = " http: // avalon . inria . fr / infra / " > < hasNodes name = " taurus -0 " disk = " 598.0 " location = " lyon " availableNumas = " // @hasNodes .0/ @hasNumas .0 // @hasNodes .0/ @hasNumas .1 " availableCores = " // @hasNodes .0/ @hasCores .0 // @hasNodes .0/ @hasCores .1 // @hasNodes .0/ @hasCores .2 // @hasNodes .0/ @hasCores .3 // @hasNodes .0/ @hasCores .4 // @hasNodes .0/ @hasCores .5 // @hasNodes .0/ @hasCores .6 // @hasNodes .0/ @hasCores .7 // @hasNodes .0/ @hasCores .8 // @hasNodes .0/ @hasCores .9 // @hasNodes .0/ @hasCores .10 // @hasNodes .0/ @hasCores .11 " > < hasNumas name = " 0 " memtotal = " 16384.0 " memfree = " 16384.0 " / > < hasNumas name = " 1 " memtotal = " 16384.0 " memfree = " 16384.0 " / > < hasCores name = " 0 " / > < hasCores name = " 1 " / > < hasCores name = " 2 " / > < hasCores name = " 3 " / > < hasCores name = " 4 " / > < hasCores name = " 5 " / > < hasCores name = " 6 " / > < hasCores name = " 7 " / > < hasCores name = " 8 " / > < hasCores name = " 9 " / > < hasCores name = " 10 " / > < hasCores name = " 11 " / > </ hasNodes > < hasNodes name = " taurus -1 " disk = " 598.0 " location = " lyon " availableNumas = " // @hasNodes .1/ @hasNumas .0 // @hasNodes .1/ @hasNumas .1 " availableCores = " // @hasNodes .1/ @hasCores .0 // @hasNodes .1/ @hasCores .1 // @hasNodes .1/ @hasCores .2 // @hasNodes .1/ @hasCores .3 // @hasNodes .1/ @hasCores .4 // @hasNodes .1/ @hasCores .5 // @hasNodes .1/ @hasCores .6 // @hasNodes .1/ @hasCores .7 // @hasNodes .1/ @hasCores .8 // @hasNodes .1/ @hasCores .9 // @hasNodes .1/ @hasCores .10 // @hasNodes .1/ @hasCores .11 " > < hasNumas name = " 0 " memtotal = " 16384.0 " memfree = " 16384.0 " / > < hasNumas name = " 1 " memtotal = " 16384.0 " memfree = " 16384.0 " / > < hasCores name = " 0 " / > < hasCores name = " 1 " / > < hasCores name = " 2 " / > < hasCores name = " 3 " / > < hasCores name = " 4 " / > < hasCores name = " 5 " / > < hasCores name = " 6 " / > < hasCores name = " 7 " / > < hasCores name = " 8 " / > < hasCores name = " 9 " / > < hasCores name = " 10 " / > < hasCores name = " 11 " / > </ hasNodes > </ i n f r a : I n f ra s t r u c t u r e > ¦ ¥

Listing 2.2: Infrastructure XML with 2 Nodes and 1 INet

Modelization of Security Requirements

There is a vast range of security mechanisms which have been proven efficient in practice.

Each mechanism can guarantee specific security properties (e.g., confidentiality, integrity) for particular entities. For example, cryptography may protect data in transit or at rest against unauthorized accesses but cannot be employed for controlling applications' behavior. We believe a key concept is to deliver on-demand security: a user should be able to specify what is the required secure behavior of his system. To do so, we rely on existing security mechanisms to enforce security properties. The process of specifying/configuring a security policy is usually very complex and error-prone. Even with security expertise, a human can still realize unintended misconfiguration leading to security breaches. For this very reason, security policies should be enforced in an automatic fashion i.e., , where human intervention only occurs if strictly necessary. Though the intended behavior of a system i.e., what a system should or should not do, falls into human knowledge.

In this Thesis, we follow a specification-driven approach: the user specifies the security he wants without knowledge of how it will be enforced. Halpern et al. [START_REF] Halpern | Using first-order logic to reason about policies[END_REF] state that security policies described in a natural language have quite ambiguous semantics. On the other hand, a formal language or logic can provide clear syntax and semantics. Therefore, our specification language should be logic-based.

In this section, we review existing models and languages to specify security properties and discuss important security properties. Then, we present our security metamodel: how to uniformly address different security mechanisms to enforce the same property. Finally, we define precisely what does mean a security property by proposing a new logic-based formalization.

In our specification-driven approach, the user describes components of a virtualized application and its security. Similar to our system-agnostic modelization of applications, we propose an enforcement-agnostic modelization of security requirements. As depicted in Figure 2.15, though the enforcement process itself is driven by the security policy, it applies to the real system. Therefore, we must link entities described in the model to their real implementation counterpart. To do so, we propose a domain-specific language (DSL) to specify security policies.

Attribute-based Contexts

Our security DSL must address any entities/resources independently from system-specific resources naming to address any systems. For example, one can describe a Service entity called SSH without specifying what SSH is or where it is physically located. In most Linux architectures, the SSH service daemon is located in /usr/sbin/sshd and the configuration files are in /etc/ssh. For security specification, we want the real path to be abstracted. Our solution is to use attribute-based contexts.

A context is an identifier referring to a (single or) group of entities. Security properties of our language apply to contexts. Therefore, entities with the same context are constrained by the same properties. An attribute-based context is composed of key-value pair of attributes where each attribute provides information about the resources it identifies. In a virtualized application model, the user can specify components of an application using names. For instance, Figure 2.16 is the model of a service named SSH contained in an application domain named System and packed into a virtual machine named VM1. Then, the context identifying the SSH service is (VM="VM1"):(AppDomain="System"):(Service="SSH").

Figure 2.16: Model of a SSH service in a System application domain inside VM1 virtual machine

Any node elements of our virtualized application metamodel is an attribute: Domain, VM, Client, VNet, Veth, AppDomain, Data and Service. This metamodel contains only static architectural elements and it is often useful to refer to other characteristics. Typically, a system user has different rights whether he is a standard user or an administrator. Therefore, our language allows defining new attributes as follows: § ¤ # attribute Role = ( StandardUser , SystemAdmin , SysnetAdmin ) ;

¦ ¥

In the above example, a new attribute Role has been defined and it accepts 3 values StandardUser, SystemAdmin, SysnetAdmin.

Using attributes, new contexts can be defined. Here is an example with a context ctxAdmins addressing any entity with the SystemAdmin role: § ¤ # context ctxAdmins = ( Role =" SystemAdmin ") ;

¦ ¥
Any context may be reused to form new, more precise contexts. Here is an example with ctxSSH_Admin referring to the SSH service (of System of VM1) with the SystemAdmin role: § ¤ # context ctxSSH_Admin = ( VM =" VM1 ") :( AppDomain =" System ") :( Service =" SSH ") : ctxAdmins ;

¦ ¥
Attributes values are regular expression strings. In the previous scenario Figure 2.16, instead of specifying SSH of VM1, any VMs' SSH service may be selected using the star character: (VM="*"):(AppDomain="System"):(Service="SSH").

To uniquely address an element defined in a virtualized application model, a context is derived from the model's hierarchy. In our example, SSH derived context is VM1.System.SSH. It follows the same grammar as other contexts, for example: § ¤ # context ctxSSH_Admin = VM1 . System . SSH : ctxAdmins ;

¦ ¥
To sum up, Figure 2.17 presents the metamodel security part limited to context and attribute definition. In our metamodel, a Context is a list of either:

• References i.e., contexts' names defined with the #context keyword.

• or ContainmentReferences.

It can be a ValuedAttribute (e.g., (AttributeKey=Value)) or an ElementList which is a list of Elements from the virtualized application metamodel (e.g., VM, Domain, Data, Service). In our metamodel, the binding relation is depicted in Figure 2.18 where a binding is a path and multiple bindings can be associated to the same context.

Security Properties

In our language, a security property is a property on contexts we model as a security function with parameters (i.e., contexts). Semantics of properties are explained after in Their template is Property(ctxSecured, ctxAuthorized). For example, the confidentiality property protects against unauthorized read accesses. Suppose only a user with Admin role is allowed to read a Log file. In our language, the property is: § ¤ # property Confidentiality (( Data =" Log ") , ( Role =" Admin ") ) ;

¦ ¥
Authentication This property has the particularity of changing an entity's context. Typically, a user can log as an admin hence changing his role from standard user to admin. This authentication is realized by a third entity. The authentication property has 3 parameters that are what is the source context, what is the authentication process and what are the valid destination contexts. Suppose an unknown user wants to authenticate using SSH and acquire system-user or admin rights, then the corresponding property is: § ¤ # property Authentication (( Username ="") , ( Service =" SSH ") , ( Role =" Admin | SystemUser ") ) ;

¦ ¥
Model-based Authorization Inference One of our goals is to ease the specification for the user. The virtualized application model provides useful operational information which could appear redundant in the security policy. For example, Figure 2. Suppose we want V M 1 to be isolated from any network, the implicit exceptions (Internet and Intranet) can be deduced from the model. Therefore, we introduce the concept of implicit properties with only one parameter i.e., what is secure; authorizations are deduced from the virtualized application model. Hence, the following implicit property can be written: § ¤ # property Isolation ( VM1 ) ;

¦ ¥
Then, an automatic transformation procedure (presented in Section 4.1 )infers the list of exceptions (i.e., authorized elements) from the virtualized application model to produce an equivalent explicit property:

§ ¤ # property Isolation ( VM1 , { Internet , Intranet } ) ; ¦ ¥
This transformation is only viable for simple properties (i.e., Confidentiality, Integrity, Isolation) without user-defined attributes (e.g., Role).

Properties with Grades As explained after in Chapter 3, our security properties have a unique and clear interpretation. Intuitively, the enforcement of a security property should guarantee a secure system. However, in practice, there is no perfect security but rather a scale from weak to strong security. Indeed, nearly all systems rendering a service can be exploited providing sufficient time and resources. For example, cryptography is used to guarantee Confidentiality and Integrity of data. The quality of protection differs depending on the cryptographic algorithm used (e.g., AES, RSA) and the size of the key(s). It is said to be computationally secure i.e., it is theoretically possible but either it would take too much time or there is no known solutions yet. Even if a protection mechanism is considered to be foolproof, humans using the system are far from it. This quality of protection is encompassed in security practices by the notion of risk. Many riskevaluation frameworks have been proposed for virtualized environments [START_REF] Saripalli | Quirc: A quantitative impact and risk assessment framework for cloud security[END_REF][START_REF] Zhang | Information security risk management framework for the cloud computing environments[END_REF]. The common principle is to associate the likelihood of an asset to be attacked with a security counter-measure of equal or superior strength thus diminishing the risk by making the attack "not worth it". The vast range of existing risk metrics highlights the difficulty of defining a good and sound one. The main reason for evaluating risks is to deploy costeffective security measures. For an organization, security is often disregarded due to its cost and its absence of visible benefits.

In this Thesis, we do not want to improve generic risk metrics and evaluations State of the Art. Yet, as we tackle Cloud-like platforms, we must consider the financial impact of security and thus allow a user to specify his security requirements with different quality of protection. Accordingly, we propose to simply extend our properties with a grade. The grade is specified by the end-user hence it should be independent from the type of the protected entities or the enforcement mechanism. We believe a coarse-grain grading system (e.g., Low, Medium, Strong) is more relevant and offers a good compromise. For future flexibility, we implement a grade as an integer value. Informally, a higher grade means a stronger security and a lower grade means a weaker security. Then, our grades can be specified as follows: § ¤ # property Isolation ( VM1 , grade ) ;

¦ ¥
Properties without explicitly specified grades are implicitly associated with the highest value (e.g., 100). In preliminary work [START_REF] Caron | Definition of security metrics for the cloud computing and security-aware virtual machine placement algorithms[END_REF], we have first envisioned the grade as a vector of security mechanisms but this approach has been discarded in this Thesis as it is not mechanism-agnostic. However, in Chapter 4, we propose a metric for a specific type of attacks called covert-channels and we discuss its relation to our grading system. Nevertheless, the problem of defining more relevant grades or generic risk metrics is part of our future work.

Conclusion

We have shown the necessity of a specification-driven approach where a user expresses its security constraints in a simple and clear way. These constraints are high-level security objectives, agnostic of any enforcement mechanisms, that apply to elements of an application which needs to be modeled as well. In the literature, there is no security aware application models suitable to enforce the end-to-end security of virtualized applications. Instead, the literate only exhibits application models without security or security models without application descriptions. Accordingly, we have proposed a unified metamodel embracing both the virtualized application and its security policy.

Furthermore, we have detailed the infrastructure metamodel hosting virtualized applications. This metamodel is used and extended in Chapter 4 to integrate security solutions. In particular, we will show how to enforce security properties between VMs with a security-aware placement algorithm and how to configure security mechanisms according to the security policy.

But before, as the main drawback of the literature is the lack of formalism, we propose in the next chapter a logic giving a unique and clear description of what confidentiality, integrity or isolation means. Then, this logic is used in Chapter 4 to refine our global security policy into multiple local properties enforceable by placement or by configuring local security mechanisms.

Our models could be enriched in the future. In particular, one of the key feature of the Cloud we do not support is elasticity. It would be interesting to study the integration of component-based approaches to tackle dynamic applications. For example, a broad class of applications spawns replicas of services depending on the load. Besides, a complete approach would be able to add or remove part of the application at runtime resulting in a completely different architecture.

Chapter 3 Formalization of Security Properties

In the previous chapter, we have presented a list of security properties a user can use to specify the security policy of a virtualized application. This policy defines what a secure system is i.e., what this system is allowed or forbidden to do. But one question is left aside: what is the meaning of a security property. Previously, we have given general definitions in a natural language (i.e., English) as formulated by standardization institutes (e.g., Common Criteria, NIST). But as stated by Halpern et al. [START_REF] Halpern | Using first-order logic to reason about policies[END_REF], security policies described in a natural language have quite ambiguous semantics. On the other hand, a formal language or logic provides clear syntax and semantics. By formal, we mean the specification is based on a strong mathematical foundation. The syntax is the grammar of the language, how a correct sentence is structured. The semantics is the meaning of the sentence. For example, "He was the first" and "He was the last" have the same structure (i.e., subject, verb, noun) but not the same meaning.

Our goal is to use existing (maybe future) protection mechanisms to enforce information flow properties. It implies our formal language must be expressive enough to map a property to a configuration of a protection mechanism. However, the security properties modeled using Sam4C are global whereas existing security mechanisms are mostly local. For instance, it is easy to state that our house must be globally secured but this statement shall be implemented with local solutions such as putting locks on doors, installing an alarm, etc. Similarly, the most important application of our logic is to prove the equivalence between a global property and a set of locally enforceable properties. This transformation, occuring during the preprocessing step of our approach, is detailed later in Section 4.1.

In this chapter, we first lay the foundation for understanding advanced logic notions. Then we review related work on logics for security properties. After, we present our logic called IF-PLTL to specify information flow properties for concurrent and distributed systems. Finally, because IF-PLTL is strictly more expressive than any existing mechanisms, we give a complete algorithm to dynamically monitor any IF-PLTL formula. This monitor can be viewed as a potential "ideal" mechanism but due to its complexity (in space and time), an implementation of this monitor would incur an high overhead.

Logic 101

This section is intended to help readers with no logic background to grasp basic notions and go through the rest of this chapter more handily. For the ones that have such background, you can skip this section.

First, many definitions of the term logic have been given and it seems the debate is still going on. Instead, we prefer to present three principles of logic (or guidelines) as defined by Ferreiro in [START_REF] Ferreirós | The road to modern logic-an interpretation[END_REF]:

1. Logic is concerned with an analysis of (valid and invalid) deduction.

2. Logic does not depend on how things are, it is independent of considerations of existence. Logic should enjoy universal applicability.

3. Logic only studies the form of arguments and deductions, never the matter. The basic idea was embodied in the use of variables A, B by Aristotle.

Formal logic encompasses a wide variety of logic systems from Aristotle's classical logic to modern systems emerging in the mid-19th century.

Syllogistic or Classical Logic

Syllogic or Classical Logic refers to Aristotle logical system based on syllogism. A syllogism is a two-premise deductive argument in which a conclusion is inferred from two premises. Let's take an example:

All men are mortal Socrates is a man Therefore, Socrates is mortal

The two first sentences are premises and the third the conclusion. This construction is called an argument. The premises and the conclusion are called propositions. What is important is to decorrelate the notion of Truth from the argument itself. First, we must consider the construction (the form) of the argument to determine if it is valid. An argument is valid if considering the premises are true then the conclusion must be true. But it does not tell us if the premises are true or false, just if you admit them, you must admit the conclusion. Classical logic is founded on three laws called axioms:

• The identity: If a proposition is true, then it is true.

• The excluded middle: A proposition is either true or false. There is no other possible outcome.

• The non-contradiction: A proposition cannot be both true and false.

Propositional Logic

Some logicians found Classical logic to be limited: indeed not every argument could fit in 3 lines. So they introduced new symbols, the most common being: negation ( ), conjunction (^), disjunction (_), conditional (Ñ) and equivalence ("). These are connectives: they connect propositions to make more complex propositions. An atomic proposition is usually a single letter e.g., p, q. Then, a complex proposition could be: pp _ qq.

In Classical logic, determining a valid or invalid argument is based on forms (i.e., patterns). In propositional logic, there are no forms, instead we can rely on Truth tables (but not only) to analyze all permutations of true and false for every atomic proposition. For example, suppose these two statements pp _ qq and p p ^ qq to be logically equivalent. By dressing the truth table, you will see that whenever the first is true, the second is also true and whenever the first is false the other is false as well. This is one of De Morgan's theorems and it is a tautology: the logical equivalence is true whatever the truth-values of p and q. In propositional logic, an argument is valid if and only if its conditional form (i.e., using Ñ) is a tautology.

Predicate or First-Order Logic

Propositional logic is not suited to formalize some valid arguments. The previous example All men are mortal;Socrates is a man;Therefore, Socrates is mortal in propositional logic yields p ^q Ñ r. Because, there are no relations between the 3 atomic propositions (p, q and r), this argument is not valid. For instance, we can assign truth-values to p, q and r to obtain true ^true Ñ f alse which is intuitively wrong. In predicate logic, propositions are enriched with predicates i.e., boolean functions. For example stating that Socrates is a man would be M anpsocratesq with M an a predicate and socrates an individual. In addition, logicians introduce the notion of quantification with "for all" (@) and "it exists"(D). Now, the three statements of our example can be expressed as follows: @xM anpxq Ñ M ortalpxq, M anpsocratesq and M ortalpsocratesq.

Individuals are referred to using a constant (e.g., socrates) or a variable (e.g., x). The difference between the two is that M anpsocratesq is either false or true but the truth-value of M anpxq depends on the individual represented by x. The replacement of x by a constant is called an assignment. Hence, the truth-value of M anpxq only exists after assignment. In addition to constants, variables and predicates, predicate logic may contain functions. For example, the statement 2 `2 " 4 may be formalized using a function P lus and a predicate Equals. It can be written as EqualspP lusp2, 2q, 4q.

Predicate logic is a generic term encompassing first-order (and higher) logics, modal logic and others. The set of elements under discussion is called the domain of discourse. It can be the set of natural numbers, the set of species on Earth or the set of processes in a system. In first-order logic, variables (i.e., x) can only range over these elements e.g., "It exists an individual x who have donated more than 100$ to charity" is pDxqpDonationpxq ą 100q. In second-order logic, quantifiers may range over sets of functions and predicates as well e.g., "It exists an organization O such as all organization's members have donated more than 100$ to charity" is pDOqp@x P OqpDonationpxq ą 100q. Second-order logic is strictly more expressive than first-order logic and cannot be reduced to first-order logic. It means that a second-order formula cannot be transformed into a first-order formula (e.g., by adding relations).

Modal Logic

In 1918, Clarence Irving Lewis introduced a formal modal logic system. Modal logic integrates the modalities of necessity and possibility. Modalities allows expressing propositions such as "It will rain today" (necessity) or "It might rain today" (possibility). A statement can be possible but not true. To clearly picture this notion, it can be viewed as possible worlds (or alternate universes). Then, the necessity modality is true if the related proposition is true in every possible world and the possibility modality is true if the proposition is true in at least one world.

Modal logic includes deontic and temporal logic.

Deontic Logic

In deontic logic, the modalities are related to the concept of obligation. "You must do this" and "You may do this" are close to necessity and possibility. One particularity of deontic logic is the concept of necessitation. This property says that whatever is necessitated by a moral requirement is itself a moral requirement. Suppose that you are morally required to break a door to save someone surrounded by fire. You are logically necessitated to break the door in order to save the person. The necessitation property tells you that you are obliged to save this person so you have an obligation to break the door. This is contestable because taken independently you have no obligation to break this door. This principle is the reason for many paradoxes in deontic logic [START_REF] Hansson | Ideal worlds -wishful thinking in deontic logic[END_REF].

Temporal Logic

In temporal logic, the modalities are related to the notion of time. A proposition is qualified by when it occurs, for example "It will eventually rain", "It will always rain" or "It has rain yesterday". In 1977, Pueli [START_REF] Pnueli | The temporal logic of programs[END_REF] proposed using temporal logic to formalize the behavior of concurrent programs of a system. He expressed properties like the mutual exclusion i.e., two processes cannot enter the same critical section. To do so, he models the system as a state-transition system: an execution is a sequence of transitions (e.g., actions, commands) where a transition changes the state of a system to another. He introduced two operators F and G to express respectively that something will eventually happen and something will always happen. In our previous example, "It will eventually rain" is captured by F prainq and "It will always rain" by Gprainq. Later, new operators have been introduced to discuss past events, namely P (once in the past) and H (always). For instance, "It has rained one day" is captured by P prainq and "It has always rained" by Hprainq.

Verification of Logics

One interest of logics is verification: showing that a system satisfies its specification. A system is described as a model and the specification is a formula of a formal language.

We consider two types of verifications: model-checking [START_REF] Clarke | Model checking[END_REF] and runtime verification [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF].

In model-checking, all executions of a given system are examined to answer whether these satisfy a given property (i.e., formula). The verification against all possible executions is typically been carried out by generating the whole state space of the underlying system, which often becomes unfeasible due to its huge size. Model-checking suffers from the state explosion problem.

In runtime verification, we examine a single execution, the one currently under scrutiny. The objective is to check if the current execution satisfies (or violates) a given property. Runtime verification does not suffer from state-explosion as there is no systematic exploration of multiple executions. This verification can be achieve offline by replaying recorded traces or online by making decisions as events occur. In the rest of this manuscript, we always refer to online runtime verification.

State of the Art

In this thesis, we propose a formalization of information flow security properties. We recall that Information Flow Control focuses on the propagation of information in a system. In this section, we review related work on formalization of security properties and present important information flow properties.

Information Flow Control properties

The main question is what kind of properties are needed to control information flows or rather what properties can we consider.

Trace properties

Security properties are properties of the system's behavior. In [START_REF] Lamport | Specifying concurrent program modules[END_REF], Lamport has shown that a concurrent system's behavior can be modeled by all execution traces generated by this system where an execution trace is a sequence of state transitions.

It follows that a security property can be defined as a property on individual traces called traces properties. In [START_REF] Alpern | Defining liveness[END_REF], Alpern and Schneider have proved that a trace property is an intersection between a safety and a liveness property. The safety property ensures that nothing bad will happen and the liveness that something good will always happen. The safety is quite straightforward: a security policy forbid any "bad" behavior of the system. The liveness is more delicate to apprehend. It is somewhat close to the concept of availability. While being protected, it means the system keeps delivering its service as it should. As the availability, we believe it has more to do with reliability and quality of service than strict protection. Proposed by Pnueli in [START_REF] Pnueli | The temporal logic of programs[END_REF], Linear Temporal Logic (LTL) is a well-known formalism to express safety and liveness properties in concurrent systems.

Hyperproperties

It has been pointed out that some important security policies could not be captured by traces properties [35]. For example, stipulating a bound on mean response time over all executions is an availability policy that cannot be specified as a property of individual traces. Each execution response time is conditioned by the others. Another property is the noninterference introduced by Goguen and Meyers [START_REF] Goguen | Security Policies and Security Models[END_REF]. This confidential property stipulates that commands executed by a user with high-level clearance has no observable effects for users with low-level clearance. Noninterference has been revisited by Haigh and Young [START_REF] Haigh | Extending the noninterference version of MLS for SAT[END_REF] then Rushby [START_REF] Rushby | Noninterference, transitivity, and channel-control security policies[END_REF]. Noninterference would seem to be a fundamental notion in information security. It arises from the need to understand why a program would leak some bits of information. But noninterference seems to characterize the absence of information flows when in reality we want to control flows not forbid any of them. We discard noninterference as a system-level property based on the following argument stated in [START_REF] Ryan | Non-interference: Who needs it?[END_REF]:

Most "real" security policies are concerned with specifying who has access to what resources under what circumstances. Non-interference is never mentioned. Furthermore, non-interference is in practice impossible to realize in any real system: contention for resources, etc. render it unfeasible.

In [35], Clarkson and Schneider have described these properties as hyperproperties. They observed that there is a vast range of security properties that cannot be stated on individual traces but rather on sets of traces. For example, noninterference typically involves 2 traces (i.e., high and low) and the mean response time property applies to k traces. Informally, an hyperproperty is a property on sets of traces while a trace property is a property on traces. Hyperproperties are considered as really powerful. They are more general than security properties (in the sense of confidentiality and integrity); they allow making statements on quality of service for instance. Now, the question is whether modelchecking and runtime verification of hyperproperties are decidable. A problem is said decidable if there exists an effective method to give an answer (e.g., yes or no) in finite time to this problem. Therefore, providing an algorithm for modelchecking of hyperproperties implies that it is decidable. Clarkson and Schneider noted that the full power of second-order logic is necessary to express hyperproperties and thus it does not exist any general methods to verify an hyperproperty [35]. However, considering a fragment (i.e., subset) may be decidable. Thus, in [START_REF] Clarkson | Temporal logics for hyperproperties[END_REF], Clarkson et al. have proposed temporal logics for some hyperproperties called HyperLTL, HyperCTL and HyperCTL* and detailed a modelchecking procedure to verify them.

We recall that modelchecking is a static method that necessitates a model to represent (or generate) all executions. For hyperproperties, it must represent all sets of all executions. This state explosion problem is an impediment to tackle existing production systems.

More importantly, in his thesis "Reasoning about hyperproperties" [START_REF] Milushev | Reasoning about Hyperproperties[END_REF], Milushev discusses the possibility of dynamic enforcement of hyperproperties: even if some enforcement methods have been proposed for single specific hyperproperties, decidability of dynamic enforcement of broader classes is still an open question.

Nevertheless, we argue that HyperLTL (and their extensions) cannot tackle runtime verification for security properties. The argument is simple. Consider the following example of a trace property, the reachability problem. It is defined as: Does it exist an execution (a trace) where a given state is reached i.e., it appears in the trace. It is clear that such trace property is satisfiable in the static case i.e., with complete knowledge of states of the system but it is not the case for runtime verification. In the latter, the question must be answered at a time when a trace only represents what has occurred but never what will occur. This problem has been circumvented by Bauer in [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF] when monitoring LTL formulas at runtime by introducing a three-state output: true, false or inconclusive. Applied to security, it would mean that if one requests access to a file, the answer is either "yes", "no" or "cannot decide yet" which is not acceptable.

With dynamic traces (i.e., runtime verification), it is generally impossible to know in advance the next state of the system or make decisions based on the future.

In conclusion, we will focus on security properties verifiable at runtime i.e., trace properties.

Logic-based Policies

Access Control Logics

Access control may be viewed as a simple trace property where the decision is generally independent from previous or future states of the system.

Many work use logic to model access control. Halpern et al. [START_REF] Halpern | Using first-order logic to reason about policies[END_REF] apply First-Order (FO) logic to digital rights management. Datalog [START_REF] Huang | Datalog and emerging applications: an interactive tutorial[END_REF] is a logic programming language oftenly used to query databases. It is reducible to FO logic. Cassandra [START_REF] Becker | Cassandra: distributed access control policies with tunable expressiveness[END_REF] is a role-based trust management system based on Datalog with constraints. It specifies AC policies for large-scale systems. Binder [START_REF] Detreville | Binder, a logic-based security language[END_REF] also uses and extends Datalog to express distributed security statements. It can express operations like certification or delegation. Bruns et al. [START_REF] Bruns | Access control via belnap logic: Intuitive, expressive, and analyzable policy composition[END_REF] propose a specification in Belnap logic for analyzable AC policy composition. Finally, the authors of [START_REF] Barker | Flexible access control policy specification with constraint logic programming[END_REF] specify and implement (Temporal) Role-Based Access Control policies in constraint logic programming. Despite that all previously cited works exclusively tackle access control models (and not IFC), they are very interesting for their strong formalism allowing static analysis and modelchecking e.g., for Operating System policies analysis [START_REF] Guttman | Verifying information flow goals in security-enhanced linux[END_REF]. Again, the issue with modelchecking approaches is the need to represent a complex system with an automaton-like model. Indeed, to be able to do so, the system must be a whitebox. Moreover, if the application/system changes, then the automaton changes as well. This leads to redo all analyses. Putting aside the question of the model size, this modeling constraint does not seem to suit current virtualized architectures where dynamicity and multitenancy are key-features.

Direct and Indirect Flows

Many attack patterns circumvent access controls by making indirect accesses.

As depicted in Figure 3.1, information may be transferred either directly or indirectly from an entity to another. Suppose the direct flow A to B is followed by the flow B to C then it creates an indirect flow from A to C. If the flows were to happen in reverse order (i.e., B to C, then A to B), it would not have created an indirect flow as the information of A would have been carried only to B and not relayed thereafter. An indirect flow can involve a sequence of direct flows of arbitrary length.

Indirect flows are important as they allow controlling the path of propagation of information. In this chapter, we are interested in expressing properties depending on previous actions. One of our contributions is to consider all indirect paths resulting from entities interactions instead of controlling indirect flows by construction.

To our knowledge, the closest work from ours has been proposed by Basin et al. in [START_REF] Basin | Policy monitoring in first-order temporal logic[END_REF]. The authors propose a runtime monitoring with a Metric First-Order Temporal Logic (MFOTL) and provide algorithms to enforce formulas. Their approach is similar in the way that MFOTL includes the Linear Time Logic temporal modalities and the system behavior is modeled as (sets of) traces. Our formalization is noticeably inspired from this work. Nonetheless, the authors' proposal differs from ours in the language expressiveness. Indeed, there is a class of properties expressible with our approach and not with MFOTL.

In short, the indirect flow relation is the transitive closure of the flow to relation (i.e., direct flow). Without the transitive closure, it is not possible to express an unbounded chain of flows with a finite formula. Suppose Alice wants to transfer information to Bob and to do so communicates through a chain of intermediates. Without the transitive closure relation, forbidding this indirect communication would necessitate specifying every possible chain of intermediates of any length. This is an infinite enumeration thus not expressible. Even with a bounded chain of flows, the formula's size is linear in the size of the chain. More generally, both MFOTL and our approach is reducible to First-Order (FO) formulas. Ronald Fagin [START_REF] Fagin | Generalized first-order spectra and polynomial-time recognizable sets[END_REF] has shown that first-order logic extended with Transitive Closure (TC) is strictly more expressive than FO. It's called FO(TC) and yields NL i.e., the problems solvable in nondeterministic logarithmic space. In consequence, we choose to trade more expressiveness for more complexity.

Discussion

Our goal is to formalize traditional security properties such as confidentiality or integrity as information flows. This formalization must encompass direct and indirect flows, and be strictly more expressive than most security mechanisms. The idea is to have a mapping between a security mechanism and a formula in our logic without targeting specific security mechanisms. Nonetheless, we limit our scope of mechanisms to runtime verification (i.e., monitors) in opposition to modelchecking which is an offline analysis.

Multiple formal systems have been proposed to reason about security properties. First, there is not a single definition of a security property. We have presented two formulation mainly adopted: trace properties and hyperproperties. Hyperproperties are too expressive for our protection point of view e.g., they allow for statements on quality of service. Moreover, there are serious doubts on the possibility of monitoring hyperproperties at runtime. On the other hand, trace properties can be monitored at runtime and existing security mechanisms enforce trace properties though they enforce simple ones.

As we focus on system-level information flow, it seems unrealistic to modify applications or assume a complete and perfect representation of them (like it would be needed for modelchecking). Instead, we consider applications to be blackboxes i.e., we do not know their internal operating or logic. However, we suppose to have a partial knowledge i.e., though applications are blackboxes, we can capture their system-level operations (e.g., read, write) and we know how they ought to interact with other entities. Let's illustrate what we call partial knowledge with a simple example drawn in Figure 3.2. Two users, Alice and Bob, are using the same application hosted on a server. We want the following information flow property:

Alice and Bob are isolated from each other i.e., information cannot flow from Alice to Bob (and vice versa). From a specification point of view, this system-wide isolation property is expressed on a blackbox i.e., without any knowledge of the application. As a consequence, our approach is specification-driven in opposition to configuration-driven approaches where the property is realized by a thorough configuration of credentials, labels or tags. From an enforcement point of view, information flow events must be interposed to either allow or deny them with respect to their consequences. In short, any event leading Bob to have information from Alice must be denied.

Considering the gap in related work to express information flows with our requirements, in particular the transitive closure, we propose a new logic called Information Flow Past Linear Time Logic (IF-PLTL). Our logic is based on the past fragment of LTL (PLTL) which is known to be suited for describing the behavior of a concurrent system.

Overview

In the rest of this chapter, we detail our formalization of information flow properties namely IF-PLTL. Even though our goal is to encompass a vast range of protection mechanisms, we present our logic as an "ideal" protection mechanism by providing a monitoring algorithm to verify properties at runtime in a concurrent system (e.g., an operating system) as shown in Figure 3.3.

As we have stressed in Section 3.2, it is mandatory to take into account direct and indirect information flows to control the propagation of information. But a system like an operating system do not have any abstraction to capture information flows directly. It is why we explain in the next section how to reconstruct information flow traces (including indirect information flows) from low-level System Events. In Figure 3 The Information Flow Event is received by the Decision box. But it is not always possible to reason on a single Information Flow Event. Indeed, it would mean taking a decision without any knowledge of the past decisions (and the related information flows that have happened). Consequently, the Decision box takes a second input: the Memory i.e., IF-Trace. Its formalism is described in the next section. On top of the Information Flow Event, this box also receives as input a Policy. In Section 3.5, we present our logic and its semantics allowing expressing such policy. Moreover, as we need to reason on past events, the logic is based on PLTL that brings such ability without the cost of too much complexity. Our logic allows expressing global security property with partial knowledge. It means that a user can express its security requirements without the need of a fine grained knowledge of the underlying systems and applications (as explained in Section 3.2.3).

The Accept and Refuse octagons in Figure 3.3 reflect the fact that the System Event (and the related Information Flow Event) satisfies (or not) the Policy. In the first case (Accept), the event is allowed to happen and the Memory is updated with the related information flow to keep track of it. If the event does not satisfy the policy, the event is not allowed and thus does not happen. Accordingly, there is no need to update the Memory. We describe how our logic can be used to implement such dynamic monitoring in Section 3.6. In Section 3.7, we conclude by presenting how our approach can be used to enforce a simple yet widely spread security requirement: the isolation between 2 users (or groups of users).

To summarize, our proposal can be classified as a System-based Information Flow Control mechanism. At the best of our knowledge, it is the only System-based Information Flow Control with a strong theoretical logic that considers all the direct and indirect information flows.

System Model: Traces Acquisition

To recapitulate, our goal is to decide whether the system's behavior modeled as traces satisfies a security policy using logic formulas as formal representation. In this section, Trace Computation part in Figure 3.3 details how to construct information flow traces from low-level system events.

As shown in Figure 3.4, a system (App) does not directly produce information flows but low-level observable events instead. These events are transformed into functional events and finally into information flows.

System behavior as traces

Every entity inside the Operating System (OS) environment can be viewed as systems e.g., files, processes, databases. As previously said, a concurrent system behavior can be modeled by all execution traces generated by this system [START_REF] Lamport | Specifying concurrent program modules[END_REF], where an execution trace is a sequence of state transitions. We give afterwards a general definition (Definition 3) of traces including the concept of observer (Definition 4). Let's suppose a system with only three entities (a,b,c). a has a partial trace including all events from or to itself but does not see events between b and c. Moreover, an event from a to b is both in a and b traces. As a result, the union of all partial traces forms a complete trace of the system. Definition 3 (Trace). A sequence of state transitions triggered by events, as viewed by an observer. Definition 4 (Observer). A passive entity with a system view (potentially partial).

Contexts

As entities are heterogeneous, they are identified using contexts (Definition 5). We suppose the existence of a method to map a context to every entity, where two entities with the same context have a set of common characteristics e.g., behavior, security domain, type. These expressiveness of the contexts can be used to mimic the labels and tags proposed in other approaches. Nevertheless, the contexts are as expressive as the system allows and as it is required to enforce the security. Indeed, with finer-grained contexts, the security policy can specify finer-grained properties. For example, a context file-editor could be associated to the path /usr/bin/vim and/or C:\Windows\bin\notepad.exe In the following, we note SC the set of all contexts.

SC:

The set of all contexts.

Definition 5 (Context). An abstract concept to refer to entities with a (set of ) common characteristic(s).

Traces with Observable Events

The execution platform has a complete view of all traces of the system. For the sake of clarity, let's take the example of processes running on top of the OS kernel. System calls (executed in kernel space) e.g., sys_read, sys_write, sys_fork, are made from an entity to another one (potentially newly created in the fork case). In current Linux kernels, the Linux Security Module (LSM) [START_REF] Wright | Linux security module framework[END_REF] provides all needed kernel hooks to generate system traces from system calls. However, these hooks only occur before system calls and cannot see whenever a call ends. These pre-call hooks are not sufficient to represent the duration of an event and a fortiori the concurrency between two overlapping calls. In the following, we suppose to be able to capture begin and end events of any call. One should note it is possible to implement such module in any Linux kernel [START_REF] Blanc | Mandatory access protection within cloud systems[END_REF]. The same could be done for network flows by creating a netfilter plugin 1 .

An observable event (Definition 6) is an atomic event viewed by an observer e.g., the kernel. It is a triple pa, eop, bq where a, b are contexts and eop is an elementary operation, for instance palice, begin_read, logsq.

EOP: set of elementary operations (begin_read, . . . ) OE: set of observable events (SC ˆEOP ˆSC) Definition 6 (Observable Event).

oe P OE " def pa, eop, bq where

# a, b P SC eop P EOP
The low-level trace (Definition 7) produced by the system is a set of observable events. Figure 3.5 shows an example of trace for a system composed of three entities (a, b, c), a read operation has finished and a write operation is still occurring (no ending event).

Definition 7 (Trace of observable events).

T " def toe 1 , oe 2 , . . . , oe n u where oe i P OE

Traces with Functional Events

Observable events are discrete events: they occur at a precise point in time. Nevertheless, read and write operations programmers are familiar with, last for a certain period of time: they are continuous events we call functional events.

With begin and end events, we can build the corresponding functional event (Definition 8) including the functional operation e.g., read, write. An entity may perform multiple functional operations in parallel. Let's suppose a context a is reading twice a context b e.g., two entities with the context a read a file with the context b. To correctly associate the end event and the begin event, an observer must discriminate the two parallel read operations even if the sources and the destinations are identical. Therefore, we suppose two functions is_begin_event and is_end_event, determining respectively if an observable event oe i is the beginning of a functional operation op and if an observable event oe j is the ending of a functional operation op starting at oe i . For example, suppose eo 1 " palice, begin_read, logsq. It is the begin event of a read but eo 2 " palice, end_read, logsq may be the end event of eo 1 read operation.

All events in the functional trace (Definition 9) are in the set FE and all operations in the set FO.

FO: set of functional operations (read, write, . . . ) FE: set of functional events (SC ˆFO ˆSC)

The two functions is_begin_event and is_end_event are defined as follows:

is_begin_event: OE ˆFO Ñ ttrue, f alseu is_end_event: OE ˆOE Ñ ttrue, f alseu A functional event is a continuous event and thus considering a timeframe ri, js, it occurs at every instant k if the begin event appears before or exactly at time i and the end event after or exactly at time j. Definition 8 (Functional Event).

@k P ri, js, pa, op, bq k P FE " def $ ' & ' %
a, b P SC, op P FO Di 1 ď i, oe i 1 " pa, eop begin , bq i 1 ^is_begin_eventpoe i 1 , opq Dj 1 ě j, oe j 1 " pa, eop end , bq j 1 ^is_end_eventpoe j 1 , oe i 1 q Definition 9 (Trace of functional events). T " def tf e 1 , f e 2 , . . . , f e n u where f e i P FE

Traces with Information Flows

Information flow models differ by their expressiveness and their relations. Nonetheless, we can outline two common relations/operators:

• The flow-to relation e.g., an information flows from a to b.

• The relabeling operator e.g., an entity labeled with a is relabeled with b.

Relabeling is a classic operator allowing a user to change his identity (e.g., su command in Linux). In terms of information flow, when transiting from label a to label b, the entity brings to b all the information he has as a. Therefore, there is a flow from a to b; the relabeling operation is classified as a write operation.

As a result, we consider only one relation in our information flow traces:

A flow from a to b is defined as pa ą bq

To transform functional events into information flows, we introduce two functions determining if an arbitrary functional operation (op P FO) is equivalent to a read or a write operation:

is_read_like: FO Ñ ttrue, f alseu is_write_like: FO Ñ ttrue, f alseu
The informal semantics of the previous operations are:

• a reads from b: information flows from b to a.

Summary

Instead of directly dealing with IF-traces, we have shown how to obtain them over more concrete traces. The two functions is_begin_event and is_end_event are sufficient to model continuous operations (functional events) over atomic ones (observable events). Then, with the two functions is_read_like and is_write_like, we have described how to finally obtain IF-traces.

The reader should note that despite we used the OS/kernel trace, the approach is not limited to this type of systems and has been historically applied to mobile systems (Android), JVM clusters and hypervisors [START_REF] Blanc | Mandatory access protection within cloud systems[END_REF] and could be applied to network flows, application services [START_REF] Fonda | Mandatory access control for web applications and workflows[END_REF] or even to cryptographic primitives.

Security Properties: Information Flow Past Linear Time Logic

After presenting how to transform "real" low-level events into information flows, we can now reason solely on these flows.

In runtime verification, we consider a unique finite trace representing the history of the current execution. Our goal is to verify a vast range of trace properties. We adopt the same definition of trace properties (Definitions 11) as defined by Clarkson et al. in [35]. We recall that a trace property is expressed on traces that come from a single observer e.g., the kernel.

Definition 11 (Trace Property).

A set of infinite traces.

Temporal Many-Sorted Logic with Information Flow

In order to model trace properties, we need a many-sorted first-order temporal logic on information flows.

Temporal A temporal logic implicitly defines the flow of time over which formulas are evaluated. It allows making statements on past events such as "Alice cannot get information from Charlie if Bob has previously sent information to him".

First-Order A first-order logic allows using quantifiers to express properties such as:

There is a context a from which flows are initiated.

Many-sorted Finally, a many-sorted logic, as opposed to a single-sorted logic, allows defining several sorts of domains instead of an homogeneous domain of discourse over which a quantifier iterates. With single-sorted logic, in the formula @xP pxq, variable x can range over any value under a single domain of discourse. To make sense, this domain should contain entities of same "kind" e.g., contexts. But, in practice, we need to represent logical groups of contexts called domains e.g., assign Alice and Bob to groups like Users or Admins. One possibility would be to represent groups as predicates e.g., Adminspaliceq would be true if Alice is an administrator. But then, iterating over domains and expressing properties such as "Any contexts of any domains other than Admins may not send information to Alice" would require the power of second-order logic which poses several decidability and complexity issues we would not detail here.

Instead, using multiple sorts easily allows us distinguishing contexts and domains without requiring to use a second-order logic. Quantifiers are sorted and iterate over a single sort e.g., contexts with @ ctx x or domains with @ dom d.

In the following, we first give general definitions of a many sorted signature i.e., the non-logical symbols of a many-sorted logic, to further detail the concrete signature of IF-PLTL.

Let's describe a many-sorted signature (Definition 12).

Definition 12 (Many-Sorted Signature). A many-sorted signature is a tuple Σ " pS, C, F, P q where:

• S " tσ 1 , . . . , σ n u where n ą 0 and σ i is a sort.

• C " tc 1 , . . . , c n u where n ě 0 and c i is a constant symbol of sort σ P S.

• F " tf 1 , . . . , f n u where n ě 0 and f i is a function symbol of arity2 m ě 0 with sorts pσ 1 ˆ. . . ˆσm q Ñ σ where σ i P S and σ P S.

• P " tp 1 , . . . , p n u where n ě 0 and p i is a predicate symbol of arity m ě 0 with sorts pσ 1 ˆ. . . ˆσm q where σ i P S.

Past-LTL

We can make implicit temporal information by using PLTL (Past-LTL) modalities [START_REF] Bozzelli | On decidability of LTL model checking for process rewrite systems[END_REF][START_REF] Pnueli | The temporal logic of programs[END_REF]. PLTL is a well-known formalism to express safety and liveness properties in concurrent systems. As a many-sorted logic is well-suited to specify IF properties, PLTL is well-suited to express temporal IF properties. We would like to highlight that the goal is to decide if an event is allowed/forbidden according to past (and current) flows. Moreover, as explained before, we construct the trace as the system progresses i.e., the future has yet to happen; any property on the future is unsatisfiable. Therefore, only pure-past PLTL modalities are satisfiable on dynamic traces. As a result, we consider the following PLTL modalities:

1. Y pϕq (Previous): ϕ had to hold at the previous state.

2. Hpϕq (Globally in the past): ϕ had to hold on the entire subsequent path.

3. P pϕq (Eventually in the past): ϕ eventually had to hold (somewhere on the subsequent path).

4. pϕ 1 qSpϕ 2 q (Since): ϕ 1 had to hold since ϕ 2 held.

The modalities P and H are derived modalities and can be defined from the S modality as follows: P ϕ " JSϕ Hϕ " P ϕ

In the rest of this chapter, we will only use the past modalities S and Y as others can be rewritten into S-only formulas.

Although only pure-past modalities can be used in formulas, a security policy must be true at any point in time from the initialization of the system. Accordingly, we add LTL modality G:

• Gpϕq (Globally in the future): ϕ has to hold on the entire subsequent path.

As a result, a policy Ψ is defined as Gpϕq where ϕ is a closed pure-past IF-PLTL formula. A closed formula (also ground formula) is a formula without any free variables. For instance, P pxq is not closed as x is a free variable i.e., there is no quantifier preceding x whereas @xP pxq is a closed formula. A free variable is not quantified and can take any values.

IF-PLTL Syntax

The syntax describes how to construct well-formed formulas of our logic. A formula is well-formed when it is part of our formal language. In other words, a non-well-formed formula cannot be interpreted by our system: the formula has no meaning.

We first give the signature for temporal information flows and then describe the formation rules. To define the set C of constants, we use SC the set of contexts and introduce SD the set of domains. We consider two sorts ctx and dom to designate contexts and domains i.e., sets of contexts. Similarly to IF-traces, the flow-to relation (ą) is naturally defined between contexts. We also introduce the indirect flow relation ("), the transitive closure of the direct flow-to relation (ą); it is inferred from a sequence of direct flows. For example, the IF-trace in The set membership relation (P) is firstly defined between a context and a domain but also between domains to allow the specification of hierarchical sets. For example, suppose a context a, a domain Set and a domain SuperSet, we can define hierarchical relations where a P Set is true, Set P SuperSet is true and a P SuperSet is false.

Signature

Finally, we consider the equality relation («) defined between either contexts or domains.

As we do not need any function, the set of functions F is empty.

Formation rules

Σ-TERM t ::"

x σ | c σ | f pt 1 , . . . , t n q where $ ' ' ' & ' ' ' % x σ is a variable of sort σ. c σ is a constant symbol of sort σ. f : σ 1 ˆ. . . ˆσn Ñ σ is a function symbol with Σ-TERM t i of sort σ i .
Σ-ATOM a ::" ppt 1 , . . . , t n q where p : σ 1 ˆ. . . ˆσn is a predicate symbol with t i Σ-TERM of sort σ i .

Σ-FORMULA ϕ ::" a | ϕ | ϕ 1 ^ϕ2 | D σ xϕpxq | Y pϕq | ϕ 1 Sϕ 2
where a is a Σ-ATOM and x a variable of sort σ

Atoms and formulas can be enriched with the classical syntactic sugar, namely:

ϕ 1 _ ϕ 2 " p ϕ 1 ^ ϕ 2 q @ σ xϕpxq " pD σ x ϕpxqq pa R sq " pa P sq
We give some abbreviations for simplicity in formulas expression: p@x P yqϕpxq " p@xq `px P yq Ñ ϕpxq pDx P yqϕpxq " pDxq `px P yq ^ϕpxq Well-formed formula Let's give an example of a well-formed formula:

Gpp@ ctx a, bqpD dom sqpa ą bq ^pa P sq Ñ pb P sqq This formula states that at every moment of the execution, for any pair a, b of contexts, there is a domain s such as if information flows from a to b and a is in domain s, then b is also in domain s.

IF-PLTL Semantics

The semantic describes how to evaluate any well-formed formula of IF-PLTL. First, we define a FO many-sorted structure (Definition 13) obtained at every moment of the execution; there is no temporal notions in such structure. Next, we define a FO temporal structure (Definition 14) interpreting the flow of time. Then, we give the definition of the satisfaction relation (|ù) between an IF-PLTL structure and an IF-PLTL formula.

A FO many-sorted structure M 1 is composed of a domain D and an interpretation function I. The domain is a set of all objects of sorts ctx, dom. The interpretation function defines the meaning of all symbols appearing in a formula (without temporal modalities).

Definition 13 (A First-Order Many-Sorted Structure).

A FO-many-sorted Σ IF ´P LT L -structure (or model) is a tuple M 1 " pD, Iq with:

1. D " Ť σPS D σ a many-sorted domain with D σ a non empty domain. @σ 1 , σ 2 P S, D σ 1 X D σ 2 " H. 1. F " T, ă a strict linear order representing intended flow of time with T Ď N.

I an interpretation function over

D "

Ť σPS D σ a many-sorted domain with D σ a non empty domain. @σ 1 , σ 2 P S, D σ 1 X D σ 2 " H.

3.

A a function associating with every moment k P T a first-order many-sorted structure Apkq " D, I k with I k the interpretation at moment k.

We use the notation pM, kq for the FO many-sorted structure at moment k. Let's clarify observations 1 and 2. Suppose a theory forbidding information to directly flow from an entity a to another entity b i.e., pa ą bq. If at moment k, a has never sent any information to b, then the theory is satisfied. Now, if a sends information to b at moment k `1, then the property is not satisfied, which concludes Observation 1. In the opposite, suppose a theory compelling information to directly flow from an entity a to another entity b that is pa ą bq. If at moment k, a has never sent any information to b, then the theory is not satisfied. Now, if a sends information to b at moment k `1, then the property is satisfied, which concludes Observation 2.

Isolation

An important problem in distributed systems with a large number of users such as Clouds is the isolation between users. We propose the following definition of isolation: Definition 15 (Isolation). Two entities A and B are isolated from each other in a system if there is no direct or indirect flow between A and B inside this system.

Applied to groups, this property can be translated in IF-PLTL as:

(@u 1 P D 1 qp@u 2 P D 2 q pu 1 " u 2 q ^ pu 2 " u 1 q Accordingly, to enforce the isolation between the two users of our example shown in Figure 3.2, we just need to specify 2 groups: D Alice (that contains the Alice user) and D Bob (that contains the Bob user).

Dynamic Monitoring

Even if our primary goal is to prove the equivalence between a global property and a set of local properties (see Section 4.1), a dynamic monitor can be designed to encompass the full expressivity of IF-PLTL with higher complexity in space and time than traditional mechanisms.

This section describes the Decision and Memory boxes of the IF-PLTL monitoring architecture depicted in Figure 3.3. To that end, a valuation operator v.w k is introduced to better understand what data needs to be kept from time step to time step and then a full decision algorithm is given and its complexity discussed.

Memory

In order to evaluate if a system's trace satisfies a given IF-PLTL formula at a given moment k, some information from previous moments (before k) is required. Storing the complete trace up to moment k would be correct but would require a linearly increasing amount of memory as time passes. The present section introduces a more efficient way to store information.

A first thing to notice is that, according to the satisfaction relation (defined in Section 3.5.3), only three relations require information from the past: S, Y and ".

For example, suppose

ψ " p@ ctx xqY px ą Aliceq ^pBob ą xq
The satisfaction of ψ at moment k depends on moment k ´1 due to the Y operator. More specifically, the satisfaction of ψ depends on occurrences of events of the form x ą Alice at moment k ´1. Since there is no other occurrence of S, Y or " in ψ, only these events are relevant to compute the satisfaction. All other events can safely be forgotten.

To generalize this observation, we introduce a valuation operator vϕw pM,kq which associates to a formula ϕ with free variables all the assignments for these variables which satisfy ϕ at moment k according to model M. We simplify this notation by writing vϕw k , the model M being implicitly defined.

The valuation vϕw k can take up to three forms:

• trsu the tautology;

• trx 1 : δ 1 . . . x n : δ n s ˚u the list of valid assignment vectors (substitutions such as ϕ is true);

• H the falsity.

The operators Y, X and t.u are defined as the usual sets operators, namely the set union, the set intersection and the set complement over domain of discourse D. However, we introduce a small subtlety: the compact vector.

Let's suppose two sets of compact vectors (S 1 , S 2 ) with x 0 , . . . , x i , x i`1 free variables:

S 1 " t » - -
x 0 : v 0 . . .

x i : v i fi ffi flu and S 2 " t " x i`1 : v i`1 ‰ u
The free variable x i`1 does not appear in S 1 meaning that it is not a free variable in the formula whose valuations are S 1 . Thus, any value of x i`1 in S 1 is also a solution. As a result, S 1 can be unfolded with all values v j i`1 P |D|. The unfolded result S unf old 1 is given herebelow:

S unf old 1 " t » - - - - x 0 : v 0 . . . x i : v i x i`1 : v 0 i`1 fi ffi ffi ffi fl , » - - - - x 0 : v 0 . . . x i : v i x i`1 : v 1 i`1 fi ffi ffi ffi fl , . . . , » - - - - x 0 : v 0 . . . x i : v i x i`1 : v |D| i`1 fi ffi ffi ffi fl u
The same unfolding operation can be applied on S 2 and thus the set operators apply without changing their semantics. For example, the compact results of X and Y are:

S 1 X S 2 " t » - - - - x 0 : v 0 . . . x i : v i x i`1 : v i`1 fi ffi ffi ffi fl u and S 1 Y S 2 " t » - - x 0 : v 0 . . . x i : v i fi ffi fl , " x i`1 : v i`1 ‰ u
This compact form is compliant with our tautology and falsity definitions. And finally, removepL, xq is the vector operator removing key x from vector L.

The rules to compute the valuation can be directly deduced from the IF-PLTL satisfaction relation: va « bw k " tra : x I , b : x I s | @x I P D ctx u va ą bw k " tra : x I , b : y I s | @x I , y I P D ctx , px I ą y I q P I k u va P sw k " tra : x I , s : y I s | @x I P D ctx , @y I P D dom , x

I P y I u v ϕw k " vϕw k vϕ 1 ^ϕ2 w k " vϕ 1 w k X vϕ 2 w k vD σ xϕpxqw k " tremovepL, xq | L P vϕpxqw k u vY pϕqw k " vϕw k´1 vpϕ 1 qSpϕ 2 qw k " vϕ 2 w k Y pvϕ 1 w k X vpϕ 1 qSpϕ 2 qw k´1 q
So far, all valuations at moment k depend only on moment k and valuations at moment k ´1. This is a desirable property since we want to limit memory usage. The case x " y is more difficult and building a rule for it straight from the satisfaction relation would require storing events further in the past. To avoid this, we propose to compute vx " yw k from a reachability list. If pa ą bq P I k pąq i.e., event pa ą bq occurs at k then: @x, if a P reachpxq then reachpxq Ð reachpxq Y tbu As a result, px " yq valuations are defined as:

vx " yw k " tpx, yq | y P reachpxq ^Dz, pz ą yq P I k pąqu Overall, it is possible to compute satisfaction of a formula from an up-to-date reachability list and from up-to-date valuations of every subformula ψ such that Y pψq or Spψq appears in Ψ. We denote subf m pΨq this set of subformulas which is the set of all formulas to be monitored.

Memory-wise, this is a more efficient approach than storing all events. Its complexity is discussed further in Section 3.6.3.

Monitoring Algorithm

This section presents the decision algorithm itself and how memory is updated. Let's recall that decision occurs within the architecture presented in Figure 3.3. More precisely, the Decision box receives information flow events one-by-one and is responsible for accepting or rejecting them and for updating the memory.

Let's assume that the policy to be enforced is GpΨq where Ψ is a closed formula.

Initialization

At startup, the list of subformulas whose valuations are to be computed is established.

As we have seen in the previous section, this list comprises the subformulas of subf m pΨq. This list is initialized at startup as a list of vectors of valuations and is denoted val pre . The initial (empty) reachability list is also initialized at startup and is denoted reach pre .

During Execution

Upon reception of an information flow event, the Decision box of our monitoring architecture executes the following algorithm: Upon reception of an event, it is not yet known if this event is going to be accepted or not. Thus, the algorithm cannot update val pre and reach pre right away and must work with local copies called val new and reach new . The INIT function initializes an empty val new in a way similar to the initialization of val pre . The function ADDREACH updates the reachability list with a new event (as described in Section 3.6.1) and returns the new updated list which is stored in reach new .

Variables: reach pre ,
Then, updated valuations are computed using the valuations rules given in Section 3.6.1 which are implemented by function COMPUTEVAL. To achieve that, the valuations of the monitored subformulas are computed in a depth-inverse fashion (i.e., smaller subformulas first). Valuations of subformula ψ at moment k depend on valuations at moment k and k ´1 of subformulas which appear in ψ itself. By ordering the computations, we make sure that computed valuations depend only of valuations already computed.

After the valuations have been computed, the satisfaction of Ψ is evaluated with the SAT function. SAT is based on the same valuation rules as COMPUTEVAL but it does not need to compute all valuations for Ψ and its result is not stored. Indeed, a single valuation which satisfy Ψ is enough to return true while f alse is returned if there is no such valuation.

If SAT returns true then the event satisfies Ψ and is thus accepted. ACCEPT transmits the information that the event is accepted to the Event interposition box of the monitoring architecture. In this case, the event will take place and the memory must be updated accordingly. The UPDATE function accomplishes this by simply storing val new and reach new instead of val pre and reach pre in the Memory box.

If SAT returns f alse then the event does not satisfy Ψ and must be rejected. REFUSE transmits the information to the Event interposition box of the monitoring architecture. In this case, the event will not take place and thus memory is not updated.

Complexity Analysis

Let Ψ be a formula to evaluate with regard to model M and D be the domain of discourse of M. The complexity of the algorithm presented above can be decomposed as follows:

Space

The overall space required by the algorithm consists of the space taken by val pre , val new , reach pre and reach new . val pre and reach pre are the contents of the Memory box in Figure 3.3 while val new and reach new are temporary spaces initialized upon reception of an event and freed upon decision (see Section 3.6.2). In the following, we simply denote val and reach and do not distinguish between memory and temporary structures (since they have the same size).

First, we can decompose the size of val into the sizes of its elements: spacepvalq " ÿ ϕPsubfmpΨq spacepvalrϕsq At worst, the space taken by the valuations for a given subformula ϕ (using compact vectors) is all the possible valuations for the free variables of ϕ:

spacepvalrϕsq " |D| f reepϕq ď |D| maxf reempΨq
Where f reepϕq is the number of free variables in ϕ and: maxf ree m pΨq " max ϕPsubfmpΨq f reepϕq This gives us the following upper bound overall:

spacepvalq ď ÿ ϕPsubfmpΨq |D| maxf reempΨq ď |subf m pΨq| ˆ|D| maxf reempΨq
The space taken by reach is easier to assess. Indeed reach is a function from D ˆD to t0, 1u. Thus:

spacepreachq " Op|D| 2 q

Overall, the space complexity of our algorithm is:

Op|subf pΨq| ˆ|D| maxf reempΨq `|D| 2 q

Time

The overall time to process an event depends on ADDREACH, COMPUTEVAL and SAT.

ADDREACH consists in adding a new context (a Op1q operation) to the reachability list of every context (of which there are at most |D|). Thus:

timepADDREACHq " Op|D|q As we noted in Section 3.6.2, SAT is a simpler problem than COMPUTEVAL. The overall complexity of both functions will thus be dominated by COMPUTEVAL.

COMPUTEVALpϕq consists in going recursively through the subformulas of ϕ and applying valuation rules (see Section 3.6.1).

The bottom cases of this recursion are 1) encountering a valuation which can be computed immediately (i.e., «, ą or P); 2) encountering a S or Y operator whose valuation has already been computed. It is not possible to encounter a S or Y operator whose valuations have not yet been computed since we have sorted the monitored subformulas so as to avoid this case (see Section 3.6.2). Consequently, over the execution of all the COMPUTEVAL instances (i.e., the entire for loop), the number of valuation rules applied is exactly the number of operators in Ψ which we denote nbopspΨq.

Even with naive implementations of the set operations, their complexity is in Opp|D|m axsq 2 q where maxs is the size of the largest valuation vector set which appears in the operation. The maximum number of valid valuation compact vectors for subformula ϕ is |D| f reepφq since only free variables appear in compact vectors.

Let us denote: maxf reepΨq " max ϕPsubf pΨq f reepϕq where subf pΨq is the set of all subformulas of Ψ. Note that subf and thus maxf ree are different from subf m and maxf ree m since they consider all subformulas instead of only those which must be monitored.

With this notation, we can write the following upper bound on the size of a valuation set in Ψ:

@ϕ P subf pΨq, |vϕw k | ă |D| maxf reepΨq
So the overall complexity of a full for loop of COMPUTEVAL runs is bounded by:

OpnbopspΨq ˆ|D| 2ˆpmaxf reepΨq`1q q
Which dominates the complexity of ADDREACH and is thus the overall time complexity of our algorithm.

Discussion

Neither space nor time complexity depend on k which is a very important property. It means that, even in very long executions, monitoring time and memory overheads stay below a bound which depends only on the policy formula and the domain of discourse.

The efficiency of the set operations could very likely be improved and would reduce the exponent in the time complexity.

The exponents which depend on the number of free variables in subformulas cannot easily be improved. Indeed, a large maxf ree means that a large number of quantificators are nested which is an intrinsically complex case.

Evaluation

This section presents an evaluation of our dynamic monitoring algorithm on the Alice-Bob use-case, where the goal is to enforce the isolation policy between Alice and Bob. Thereafter, we discuss specification of security policies.

Isolation Policy

The wanted isolation policy can be described, with IF-PLTL, as follows:

Ψ " Gp pAlice " Bobq ^ pBob " Aliceqq Let's suppose the scenario depicted in Figure 3.8 with two domains A (Alice, WorkerA, AppA) and B (Bob, WorkerB, AppB ). Moreover, AppA and AppB share File. The needed sets are configured as follows: 3.1 shows each monitoring step of the isolation policy Ψ on the trace represented by Figure 3.8. Upon a new flow event, the reach structure is augmented with it. For example, at k " 2, the flow pW orkerA ą AppAq implies that AppA is reachable from W orkerA but also from Alice due to the presence of W orkerA in Alice's reachability list. However, at k " 6, as a consequence of the flow pW orkerB ą Bobq, Bob becomes reachable from Alice. Then, the formula Alice " Bob is true leading the policy Ψ to be unsatisfied. Therefore, the event generating the flow pW orkerB ą Bobq must be denied and our monitor rollbacks to the previous state k " 5. This concludes the enforcement of policy Ψ.

D dom " tA, Bu A " tAlice, W orkerA, AppAu B " tBob, W orkerB, AppBu D ctx " A Y B Y tF ileu Table

Discussion

As shown previously, the isolation policy is enforced regardless of what event happens; it encompasses many unexpected scenarios other monitors cannot. Let's suppose an other scenario where File is a legit configuration file this time; it should not receive any information. Then, the policy can be modified as follows:

Ψ 2 " Ψ ^Gpp@ ctx xq px ą F ileqq
With policy Ψ 2 , any attempt to write File will be denied but any other indirect path will still be taken into account. In our opinion, it is up to the security officer to specify a policy in accordance with the system's expected behavior.

We have presented our logic as an "ideal" security mechanism. But one of our goal is to have a correspondence between a configuration of a protection mechanism such as SELinux and a formula in IF-PLTL. Though configurations are out of the scope of this Thesis as they are achieved by project partners, we want to show the intuition in Table 3.2.

Conclusion

In this chapter, we have hightlighted the lack of suitable formalism of security policies for distributed systems. Indeed, we need to encompass direct and indirect information flows while having a mechanism agnostic language. Therefore, we have proposed IF-PLTL (Information-Flow Past Linear Time Logic). We have shown that information flow cannot be captured directly but they are obtained from low-level events. Accordingly, in Section 3.4, we have detailed how to construct Information Flow Traces from Observable Events Traces. Then, we have described IF-PLTL syntax and semantics.

Moreover, we have shown the merit of IF-PLTL and its capacity to express any information flow trace property which are inherently temporal. Our primary goal is to distribute a global property into multiple local properties we know how to enforce using several local mechanims. Using IF-PLTL, we present in Section 4.1 the equivalences enabling this transformation.

Nonetheless, we have presented a dynamic monitor that can enforce any IF-PLTL formula. However, the complexity in time and space of this monitoring algorithm is too high to become popularized in practice.

In the future, we will propose methods to ensure the composability of different properties. We will also work on how IF-PLTL properties can be split to be used by a set of collaborating observers, in particular, with observers at different Cloud layers (IaaS, PaaS and SaaS). An interesting work would be to determine whether an IF-PLTL theory is coherent or not.

Chapter 4 Security Deployment for Virtualized Distributed Systems

In Chapter 2, we have presented our model of virtualized applications and their security requirements. These requirements are security properties which formal semantics have been detailed in Chapter 3. In this chapter, we present how to deploy virtualized applications on a virtualization-based infrastructure.

Our deployment must consider the enforcement of the application security but also the underlying infrastructure security. Multiple approaches may be envisioned to enforce security properties. We propose two complementary solutions. The first one (described in Section 4.2) is a security-aware placement to enforce security between virtual machines (inter-VM security) which may belong to the same or different applications. Then, the second (described in Section 4.3) is the configuration of security mechanisms to provide security within applications' virtual machines (intra-VM security). But first, we explain how a global property can be preprocessed to be enforced by a set of security mechanisms.

Preprocessing of Security Requirements

A requirement or property may be specified on a set of entities to simplify the specification step. Typically, a user requires his virtualized application to be isolated from others. This application may be arbitrarily complex but the isolation property protects the whole virtualized application from other tenants. It is much easier for the tenant to state the property relatively to the application rather than to each element of this application. However, a property on an abstract group cannot be directly enforced (i.e., by a single security mechanism), especially if the group combines different types of entities e.g., virtual machines and virtual networks.

In this section, thanks to our formal system which allows for reasoning about (explicit) properties, we first give some equivalences between a property on a set of entities and a set of properties on each individual entity. Then, based on these equivalences, we detail our algorithms to extend an implicit property presented in Section 2.3.2 to explicit properties. Finally, still using the equivalences, we propose splitting algorithms which transform a global property into locally enforceable properties.

Equivalence for Confidentiality, Integrity and Isolation

In this subsection, we detail the equivalence relations for the Confidentiality property. The approach (and proof) is strictly the same for Integrity and Isolation properties.

Our confidentiality property states that information may flow from a secured set S to itself or an authorized set A. In our Sam4C modeling language, the property has the signature (in the sense of function signature) Conf identialitypS, Aq. The corresponding definition in IF-PLTL is:

Conf identialitypS, Aq " def p@ ctx x P Sqp@ ctx yqpx ą yq Ñ py P S Y Aq

According to this definition, information may flow from any context x in S to any context y if y is either in the authorized domain A or in the secured domain S. The splitting procedure is valid if there is an equivalence between protecting the confidentiality of the set S and protecting the confidentiality of each entity x in S.

Suppose the set S can be divided into disjoint subsets S 1 and S 2 that is S " S 1 Y S 2 and S 1 X S 2 " H, then we have the following equivalence:

Conf identialitypS, Aq " Conf identialitypS 1 , A Y S 2 q ^Conf identialitypS 2 , A Y S 1 q
Proof. In this proof, we simplify the notation @ ctx by @ as we do not quantify over other sorts. We start with the definition of Conf identialitypA, Sq that is: p@x P Sqp@yqpx ą yq Ñ py P S Y Aq (P0)

We define S " S 1 Y S 2 such as S 1 X S 2 " H, then:

(P0) " p@x P S 1 Y S 2 qp@yqpx ą yq Ñ py P S 1 Y S 2 Y Aq (P1)

In the previous chapter, we have introduced the simplification: p@x P yqϕpxq " p@xq `px P yq Ñ ϕpxq Then we obtain:

(P1) " p@xq `px P S 1 Y S 2 q Ñ `p@yqpx ą yq Ñ py P S 1 Y S 2 Y Aq ˘˘(P2)
Due to the equivalence between union set and logical disjunction, namely:

px P S 1 Y S 2 q " px P S 1 q _ px P S 2 q

We have:

(P2) " p@xq `ppx P S 1 q _ px P S 2 qq Ñ `p@yqpx ą yq

Ñ py P S 1 Y S 2 Y Aq ˘˘(P3)
The implication operator Ñ is defined as:

p Ñ q " p _ q
Accordingly, we have:

(P3) " p@xq `p px P S 1 q ^ px P S 2 qq _ `p@yqpx ą yq Ñ py P S 1 Y S 2 Y Aq ˘˘(P4)

Because of the distributivity of the logical operators ^and _ that is:

pp ^qq _ r " pp _ rq ^pq _ rq
We obtain:

(P4) " p@xq $ ' & ' % ` px P S 1 q _ pp@yqpx ą yq Ñ py P S 1 Y S 2 Y Aqq ˘ px P S 2 q _ pp@yqpx ą yq Ñ py P S 1 Y S 2 Y Aqq ˘(P5)
We use the previous implication operator equivalence:

(P5) " p@xq $ ' & ' % `px P S 1 q Ñ pp@yqpx ą yq Ñ py P S 1 Y S 2 Y Aqq px P S 2 q Ñ pp@yqpx ą yq Ñ py P S 1 Y S 2 Y Aqq ˘(P6)
Finally, the universal quantifier distributes over conjunction, that is: @xpϕpxq ^ψpxqq " p@xϕpxqq ^p@xψpxqq It gives us the result:

(P6) " $ ' & ' %
p@xq `px P S 1 q Ñ pp@yqpx ą yq Ñ py P S 1 Y S 2 Y Aqq p@xq `px P S 2 q Ñ pp@yqpx ą yq Ñ py P S 1 Y S 2 Y Aqq ˘(P7)

Which concludes our equivalence:

(P7) " Conf identialitypS 1 , A Y S 2 q ^Conf identialitypS 2 , A Y S 1 q
For the Integrity and Isolation, the same proof (hence split) hold providing the IF-PLTL definitions given afterwards.

Our integrity property states that information may flow to a secured set S from itself or an authorized set A, that is: IntegritypS, Aq " def p@ ctx x P Sqp@ ctx yqpx ą yq Ñ py P S Y Aq Our isolation property is the conjunction of confidentiality and integrity, that is:

IsolationpS, Aq " def Conf identialitypS, Aq ^IntegritypS, Aq
Therefore, we obtain the following equivalences:

IntegritypS, Aq " IntegritypS 1 , A Y S 2 q ^IntegritypS 2 , A Y S 1 q IsolationpS, Aq " IsolationpS 1 , A Y S 2 q ^IsolationpS 2 , A Y S 1 q
In summary, we have presented some equivalences for Confidentiality, Integrity and Isolation properties stated with direct flows. For more complex properties e.g., with indirect flows or temporal modalities, new specific yet not trivial equivalences must be devised. In the next following subsections, we use these equivalences in two ways. First, we present how to split an implicit property which is easy to specify for a user into explicit properties we must enforce. Then, we detail how to split an explicit property into locally enforceable properties i.e., that we know some security mechanisms can enforce directly and locally on a VM or host.

Implicit to Explicit Properties

As previously said, our Confidentiality, Integrity and Isolation properties have two parameters, the secured set and the authorized set. In Section 2.3.2, we have discussed the possibility of specifying implicit properties such as the user does not express the authorized set but only the secured set. In this subsection, we show how an implicit property can be extended into an explicit property.

We have introduced in Chapter 2 the Security Domain as an abstract group. Informally, the virtualized application model (see Figure 4.1) shows that the three VMs (i.e., VM1, VM2 and VM3) should be able to exchange information through Intranet and only VM1 should also communicate with Public meaning the authorized set will be different for both cases. These characteristics must be preserved when extending the implicit isolation property.

To do so, we consider the model as a graph where VMs and VNets are nodes and VLink are edges. The security domain Dom is abstract i.e., it is an alias for the set tV M 1, V M 2, V M 3, Intranetu. Then, the equivalent property is:

§ ¤ # property Isolation ( { VM1 , VM2 , VM3 , Intranet } ) ; ¦ ¥
We distinguish two secured sets: the border set and the internal set.

Definition 16 (Border Set). Given a set S of nodes, the border set of S includes all nodes n i such as it exists at least one edge between n i and a node not in S.

Definition 17 (Internal Set). Given a set S of nodes, the internal set of S includes all nodes n i such as it does not exist any edge between n i and a node not in S.

In Figure 4.1, VM1 is in the border set of Dom, and the others (i.e., VM2, VM3 and Intranet) is in the internal set of Dom.

The virtualized application model is a graph G " pV, Eq where G is a pair pV, Eq with V the set of nodes and E the set of edges. We formalize the model's constraints as a function Authpx, S, Gq with x a node, S a set of nodes (including x) and G the model graph. Auth is defined as follows:

Authpx, S, pV, Eqq " # S if p@x i P V qpx, x i q P E Ñ x i P S S Y tx i | p@x i P V qpx, xiq P Eu otherwise

We can see that Auth returns S if x is in the internal set and the list of neighbors union S if x is in the border set. As a result, Auth returns the same set (i.e., S) for any internal entities and specific sets for any border entities. Then, using our property equivalences, we define S 1 as the border set S border and S 2 as the internal set S internal . The conditions S " S 1 Y S 2 and S 1 X S 2 " H both hold. Thus, we have (P rop stands for Confidentiality, Integrity or Isolation):

ImplicitP roppSq " $ ' & ' % p@x i P S internal qpP ropptx i u, Authpx i q Y S internal Y S border ´tx i uqq p@x b P S border qpP ropptx b u, Authpx b q Y S internal Y S border ´tx b uqq
Because Authpx i q " S for all x i P S internal , we have:

p@x i P S internal qpP ropptx i u, Authpx i q Y S internal Y S border ´tx i uqq " p@x i P S internal qpP ropptx i u, S Y S internal Y S border ´tx i uqq " p@x i P S internal qpP ropptx i u, S ´tx i uqq " P roppS internal , S ´Sinternal q " P roppS internal , S border q Therefore, we finally obtain:

ImplicitP roppSq " $ ' & ' % P roppS internal , S border q p@x b P S border qpP ropptx b u, Authpx b q Y S internal Y S border ´tx b uqq
This equation is used in Algorithm 4.1 to compute the set of explicit properties from implicit properties. In this algorithm, an implicit property p i is tuple pT, S, gq where T is the type of property (i.e., Confidentiality, Integrity or Isolation), S the secured set and g the grade. The grade is the quality of protection as discussed in Section 2.3.2. It can be viewed as an annotation that is preserved during the procedure.

Model-based Property Split

We have presented how to extend an implicit property to an explicit one. Now, the problem is to determine the result of splitting an explicit property into individual properties.

To do so, we make use of our previous equivalences in two ways. Firstly, we show how to split a global property i.e., a property with a secured set of entities, to local properties i.e., properties on individual secured entities. Secondly, the previous local properties are specified on multiples types of entities e.g., VMs and VNets but most mechanisms are dedicated to a single type e.g., either to protect VMs or to protect networks. Therefore, we show how to discriminate different types of entities and split a property into typed properties i.e., properties where the secured set only contains entities of the same type.

Local properties split

A local property is a property with an individual secured entity. Therefore, if we denote e an individual entity in the secured set S then we can instantiate S " S 1 Y S 2 with S 1 " teu and S 2 " S ´teu. Accordingly, we obtain the following equivalence:

P roppS, Aq " P roppteu, A Y pS ´teuqq ^P ropppS ´teuq, A Y teuq Let a property P be a tuple pP rop, S, A, gq with P rop the type of property (e.g., Confidentiality), S the secured set, A the authorized set and g the grade. We include the grade (as introduced in 2.3.2) to demonstrate that it is preserved through the procedure, meaning any global property with a required quality of protection (i.e., the grade) is split into local property with exactly the same quality. Algorithm 4.2 splits a global property into singleton properties i.e., with a unique element in the secured set.

Typed properties split

In the result given above, the singleton properties contain entities of different types in the authorized set e.g., Intranet, VM1. Typically, a security mechanism is dedicated to protect a single type of entity: different mechanisms are used to protect a VNet or a VM. Accordingly, we propose a second procedure to split our properties into typed properties that is properties with a single type. First, we must consider all existing types. In a Security Domain, only two types exist namely VM and VNet. Then, the IF-PLTL definitions of Confidentiality, Integrity and Isolation are adapted to reflect the types, we obtain:

Conf identiality type pS, Aq " def p@x P Sqp@y P typeqpx ą yq Ñ py P S Y Aq Integrity type pS, Aq " def p@x P Sqp@y P typeqpx ă yq Ñ py P S Y Aq Isolation type pS, Aq " def Conf identiality type pS, Aq ^Integrity type pS, Aq

We consider that information may flow between a combination of VNet or VM e.g., VNet to VM or VM to VM. Providing the authorized set is divided into VMs and VNets (i.e., @y range only on VMs and VNets), we can easily prove the equivalence: Then, the result of this typed splitting procedure is:

P roppS, A vm Y A vnet q " P rop V M pS, A vm q ^P rop V N et pS, A vnet q Algorithm 4.
§ ¤ # property IsolationVM ( { VM1 } , { VM2 , VM3 } ) ; # property IsolationVNet ( { VM1 } , { Public , Intranet } ) ; # property IsolationVM ( { VM2 } ,{ VM3 , VM1 } ) ; # property IsolationVNet ( { VM2 } ,{ Intranet } ) ; # property IsolationVM ( { VM3 } ,{ VM1 , VM2 } ) ; # property IsolationVNet ( { VM3 } ,{ Intranet } ) ; # property IsolationVM ( { Intranet } ,{ VM3 , VM1 , VM2 } ) ; # property IsolationVNet ( { Intranet } ) ; ¦ ¥
Consequently, given these local typed properties, we must find a mechanism to enforce each one. For example, we show in Section 4.2 how to enforce the isolation of VM1 from any other VMs except for VM2 and VM3 using a placement-based strategy. Similarly, we could enforce the isolation of VM1 from any VNet except for Public and Intranet by simply configuring only two network interfaces in VM1.

Conclusion

In resume, we have first detailed how to split an implicit property into explicit properties. Then, we have shown how to split a global (explicit) Confidentiality, Integrity or Isolation property on VMs and VNets into their local typed counterparts. In future work, this approach could be extended to other kinds of properties or for properties on entities within virtual machines e.g., Data, Service. In Section 4.2, we present our solution to enforce the isolation between VMs only. Then in Section 4.3, we detail our generic solution based on the configuration of security mechanisms for other properties in particular those protecting entities within VMs. Enforcing properties on virtual networks is part of our future work though we discuss a potential solution in the conclusion of this chapter.

Placement-based Security

In virtualized distributed systems such as Clouds, multitenancy and shared resources facilitate attacks and thefts by altering the level of isolation between tenants, processes or virtual machines. While virtualization could be seen as an isolation mechanism between tenants, we show in this section that it is not the case [START_REF] Ristenpart | you, get off of my cloud: exploring information leakage in third-party compute clouds[END_REF]. Accordingly, it is required to have another mechanism to enforce the isolation.

Furthermore, the security of a system is as strong as the weakest link. And, even with a perfect information flow (or access) control mechanism at the system level (e.g., Hypervisor or Operating system), information can be silently leaked out (or accessed) by exploiting (unwillingly) unsecured design or implementation; this is called covert channels. The literature exhibits multiple covert channels attacks that have been successfully conducted in Cloud environments [START_REF] Ristenpart | you, get off of my cloud: exploring information leakage in third-party compute clouds[END_REF][START_REF] Wu | Whispers in the hyper-space: high-speed covert channel attacks in the cloud[END_REF][START_REF] Xu | An exploration of L2 cache covert channels in virtualized environments[END_REF]] (e.g., Amazon EC2) thanks to the shared hardware components between an attacker and a victim. Previous works opt for different approaches to tackle this issue: detection of attacks, fine-grained tracking of resources usage and placement algorithms. Placement algorithms under collocation/anticollocation constraints specify if 2 VMs can share the same Physical Machine (PM) or not. Accordingly, they do not take into account any scenarios where sharing resources is reasonable when measuring information leakage.

In this section, we propose a new resource allocation mechanism under information leakage constraints. Our mechanism takes into account microarchitectural components as they are one of the main reasons of covert channels. Moreover, it allows to have a finergrained allocation than previous approaches and thus reduces the quantity of resources wasted due to security constraints. But first, we need a way to present the quantity of information that can be leaked between 2 applications. While our allocation algorithm could use any covert-channel metric, due to the lack of proper metric, we propose a new information leakage metric that can be used by a tenant and is both application and hardware independent. This metric quantifies information leakage through microarchitectural covert channels based on the achievable bitrate between 2 applications [START_REF] Lefray | Microarchitectureaware virtual machine placement under information leakage constraints[END_REF][START_REF] Tcsec | Trusted Computer System Evaluation Criteria[END_REF].

Using this metric, a tenant can express its isolation properties and specify the acceptable leakage that fits his security needs. For example, banks, governments and medical establishments usually require more secure setups than research institutes running experiments. Using the virtualized application model and our metric, we propose our new resource allocation mechanism. Furthermore, we present how we have tackled the specificity of NUMA (Non-Uniform Memory Access) allocation policies to encompass both traditional and modern architectures, and proposed a model for our algorithm.

State of the Art

The major problem of virtualization is a weak isolation. Ristenpart et al. [START_REF] Ristenpart | you, get off of my cloud: exploring information leakage in third-party compute clouds[END_REF] discuss multiple approaches to exploit the co-residency in Cloud environments such as Cross-VM performance degradation, Denial of Service (DoS) attacks or stealing cryptographic keys, thus demonstrating the reality of security threats. They have shown the feasibility of collocating their VMs on the same physical machine as business targets in EC2. This work demonstrates that virtualization is far from being sufficient to have a secure environment.

In this section, we focus on the isolation problem of VMs sharing the same hardware and hypervisor. Furthermore, according to our previous definition of isolation, we will not consider performance interference. Indeed, it does not allow information modification or leak even if it is due to improper isolation [START_REF] Varadarajan | Resource-Freeing Attacks: Improve your Cloud Performance (At your Neighbor's Expense)[END_REF].

Microarchitectural Timing Covert Channels

Cloud providers can provide a large range of security mechanisms to prevent unauthorized information flows. But, despite all the effort, there is still a potential risk of data leakage in the Cloud, that is covert channels.

A covert channel is an attack which bypasses the control mechanism using legal means to leak information to unauthorized neighbors. A covert channel breaks the confidentiality property and thus, the isolation property. Therefore, even a perfect control mechanism is useless against covert channels.

Covert channels should not be confused with side channels. A covert channel exists when 2 cooperative entities, let say Trojan and Spy, use a common protocol to communicate or exfiltrate information. For a side channel, only one process, the Spy, collects unwillingly disclosed information. Because the leaking process can be considered as an unintentional Trojan, we argue that side channels are special cases of covert channels. Recent exploits (e.g., Heartblead, Ghost) have shown the easiness of remotely uploading and executing a malicious code. Side and covert channels may exist at any layer i.e., hardware and software. Our approach is dedicated to improve the isolation between VMs. Therefore, we only consider covert channels harmful to VMs i.e., microarchitecturebased covert channels.

As depicted Figure 4.2, side and covert channels may exploit microarchitectural components like caches or CPUs to infer or convey information. In this illustration, two VMs Bob and Mal are collocated on the same host i.e., physical machine. In Figure 4.2a, VM Mal "listens" to the microarchitecture to extract information from VM Bob, this is a side channel. Whereas in A covert storage channel exploits a standard data channel to encode secret information. This problem has been described in 1983 by G. Simmons [START_REF] Simmons | The prisoners' problem and the subliminal channel[END_REF] as the prisoner's problem. Two prisoners, Alice and Bob, are detained in distinct cells. Their goal is to elaborate an escape plan. They can communicate with each other by letters only, conveyed by the warden. But, they have to consider that the warden is free to read the content of the letters, remove (part of) it or even forge new content. Consequently, Alice and Bob have to encode their discussion in an apparently carefree text. This attack is popular for network protocols, for example by using the reserved or unused bits of a frame to convey information. As covert storage channels are not due to hardware components but software design, we will focus mainly on covert timing channels.

A covert timing channel exploits access timings of shared resources. In his work [START_REF]Cache missing for fun and profit[END_REF], Percival took advantage of cache hit and miss to convey "0" and "1" respectively. With collocated VMs sharing multiple resources (hardware and system), virtualization-based environments are conducive for such exploits. Building a covert timing channel in a public commercial Cloud (such as Amazon EC2) has been proven feasible [START_REF] Ristenpart | you, get off of my cloud: exploring information leakage in third-party compute clouds[END_REF][START_REF] Wu | Whispers in the hyper-space: high-speed covert channel attacks in the cloud[END_REF][START_REF] Xu | An exploration of L2 cache covert channels in virtualized environments[END_REF]. A reliable bandwidth of just a hundred bits per second is enough to silently extract hundreds of 1024-bytes private keys, or tens of thousands of credit cards in a day. The DoD guideline [START_REF] Tcsec | Trusted Computer System Evaluation Criteria[END_REF] (TCSEC / Orange Book) characterizes a covert channel by its bitrate and error rate. It suggests that covert channels exceeding a threshold of 0.1 bit per second should be audited and be of concern to security if it performs over 1 bit per second.

In a virtualized environment, covert timing channels can be conducted using some hardware or system components. In Table 4.1, we draw a summary of previous covert timing channels works. For the same component, reported bitrates can differ up to 6 orders of magnitude (e.g., 0.2 bps and 190.4 kbps for L2 cache covert channel) depending on the experimental environment (i.e., setup column). This gap cannot be explained by hardware differences alone (e.g., CPU clock speed, cache size). How the attack is implemented also has a major impact on the bitrate.

Mitigation techniques

Covert channels in multitenant environments pose a real threat with bitrates largely over the 1 bit per second standard threshold. A covert channel is by definition a reliable data channel, therefore reducing the bandwidth, preventing the channel from being reliable (i.e., increasing the error rate) or removing the channel are the basic ideas for mitigation techniques.

We discuss below the mitigation possibilities given 3 perspectives: the tenant, the provider and the hardware manufacturer.

Tenant The tenant has limited possibilities against covert channels. HomeAlone [START_REF] Zhang | HomeAlone: Co-residency detection in the cloud via side-channel analysis[END_REF] is a detection approach to detect unusual L2 cache usage without relying on hardware support nor hypervisor modification. But HomeAlone's oracle is not perfect and the Spy can try to evade the detection. Moreover, according to Wu et al. [START_REF] Wu | Whispers in the hyper-space: high-speed covert channel attacks in the cloud[END_REF], for memory bus covert timing channels, this approach would be subject to high performance overhead and high false positive rate due to non-determinism and higher access latencies. To sum up, a detection approach at the tenant level cannot be generalized and do not apply to yet to discover covert timing channels.

Provider On the other side, the Cloud provider has more latitude to mitigate covert channels. He can use detection techniques at the hypervisor level with lower overhead. Moreover, he can modify the scheduling policy to implement cache partitioning or page coloring to isolate cache/memory accesses [START_REF] Raj | Resource management for isolation enhanced cloud services[END_REF][START_REF] Taesoo | System-Level Protection Against Cache-based Side Channel Attacks in the Cloud[END_REF] at the cost of performance. Others existing preventive approaches are dedicated instances or collocation/anti-collocation placement. In this case, the isolation properties can be modeled as collocation and anti-collocation constraints [START_REF] Caron | Improving users' isolation in IaaS: Virtual machine placement with security constraints[END_REF][START_REF] Jayasinghe | Improving Performance and Availability of Services Hosted on IaaS Clouds with Structural Constraint-aware Virtual Machine Placement[END_REF]. Nevertheless, they require to express the list of tenants with whom each VM is allowed to share resources (or not). Moreover, such measures are costly for the tenant as he pays extra charges for dedicated physical machines as these approaches use coarse grain resource allocation model.

On modern public Clouds such as Amazon EC2 and Microsoft Azure, hardware multithreading called simultaneous multithreading (SMT) is disabled as L1 cache-based covert channels attacks are easy to build. For example, L1 caches that are dedicated to one core are the easiest way to create covert channels between VMs [START_REF]Cache missing for fun and profit[END_REF]. The NoHype concept [START_REF] Keller | NoHype: Virtualized Cloud Infrastructure without the Virtualization[END_REF] consists in removing the virtualization layer while retaining the key features enabled by virtualization. They limit covert channels by enabling one VM per core but as we have shown, other covert channels exist within the microarchitecture components.

Hardware manufacturer A covert channel is based on a faulty implementation. Thus, the hardware design is the initial reason of most covert channels. The solution would be to integrate security concerns when designing hardware components. Needless to say, it will not fix the issues on hardware already in production. Nevertheless, hardware design is out of scope.

Summary Because of the lack of near-future improvement in hardware design and the specificity of detection techniques, we propose a covert channel aware placement solution. Outsourced applications do not have the same level of criticality. For example, a private individual's website is less threatened by covert channels than a banking or government application. Therefore, we consider the tenant to be responsible for specifying an acceptable information leakage risk and then, the Cloud provider has automated procedures to decide whether the tenant's VM should share L1/L2/L3 caches, memory bus, etc. with other VMs. Such solution can be applied to any Cloud and easily enriched with newly discovered covert channel attacks. The placement algorithm has to use a general metric to deduce a value from a given placement/hardware configuration and compare it with the tenant's risk requirement but also to compare two configurations and deduce the more secure one. The following part discusses existing metrics and devises a new metric to tackle practicability issues. Because of the lack of near-future improvement in hardware design and the specificity of detection techniques, we propose a covert channel aware placement solution. Outsourced applications do not have the same level of criticality. For example, a private individual's website is less threatened by covert channels than a banking or government application. Therefore, we consider the tenant to be responsible for specifying an acceptable information leakage risk and then, the Cloud provider has automated procedures to decide whether the tenant's VM should share L1/L2/L3 caches, memory bus, etc. with other VMs. Such solution can be applied to any Cloud and easily enriched with newly discovered covert channel attacks. The placement algorithm has to use a general metric to deduce a value from a given placement/hardware configuration and compare it with the tenant's risk requirement but also to compare two configurations and deduce the more secure one. The following part discusses existing metrics and devises a new metric to tackle practicability issues.

Covert channel aware metric

Due to the recentness of Cloud (and virtualization) covert channel works, the literature is quite poor in covert channel metric propositions. Published in 2012 and after, the reference works are the metrics proposed by Demme J. et al. [START_REF] Demme | Side-channel vulnerability factor: A metric for measuring information leakage[END_REF] and Zhang T. et al. [START_REF] Zhang | Side channel vulnerability metrics: The promise and the pitfalls[END_REF] with respectively the Side channel Vulnerability Factor (SVF) and the Cache Side channel Vulnerability (CSV). Firstly, both metrics are design for side channels and not covert channels, but because side channels and covert channels are intrinsically related, theses metrics cannot be discard based on this sole argument to motive our new information leakage metric.

As illustrated Figure 4.3, SVF and CSV are float values between 0 and 1 reflecting the degree of information leakage an observer can see from an execution. They correlate the oracle execution traces with the leaked execution traces viewed by another process in terms of cache accesses, CPU loads, etc. The approach is thus hardware-independent but the obtained value is application-specific. Indeed, the evaluation is based on the execution of a cryptographic library and it is hard to deduce if a given value would be roughly the same for an arbitrary application. One problematic is to allow a tenant to specify a value as an acceptable risk. Because SVF and CSV are correlation factors, they can be easily used for comparison but except for limit values (0 and 1) it is quite a challenge to give a practical meaning to an intermediate value (e.g., 0.467), even for a knowledgeable tenant.

Therefore, both SVF and CSV are unspecifiable in practice, and thus we must come up with an alternative covert channel aware metric presented thereafter.

Information Leakage Quantitative Metric

We have previously shown that both SVF and CSV metrics are not satisfying. Because the DoD guideline [START_REF] Tcsec | Trusted Computer System Evaluation Criteria[END_REF] (TCSEC / Orange Book) indicates that a covert channel (char-acterized by its bitrate and error rate) over 1 bit per second (bps) should be of concern to security, we use it as a reference value for our metric.

Therefore, we define the Information Leakage Metric as follows:

Definition 18 (Information Leakage Metric). Ratio between the covert channel theoretical bitrate in a noiseless environment and the reference value (1 bps).

Unlike SVF and CSV, our metric characterizes the worst case scenario. In a security context, such scenario corresponds to the maximal bitrate a covert channel can theoretically achieve. Thus, to compute this value, we consider a noiseless environment and a parallel setup (the Trojan and the Spy run on distinct cores). Because our Information Leakage approach is based on a core characteristic (i.e., the bitrate), a value exists for any timing covert channel though it can be complex to compute it.

In the following, we exemplify the approach with a cache-based timing covert channel.

Cache-based Timing Covert channels bitrate in Virtualized Environment

In this part, we detail how a cache-based timing covert channels works using Percival et al. technique [START_REF]Cache missing for fun and profit[END_REF].

The idea is to time the latency of accessing memory addresses. We distinguish two cases, that is, if the accessed data are already in the cache, then the latency is small; else it must be retrieved from the main memory, then the latency is larger. As illustrated in Figure 4.4, the Spy accesses twice a set of cache lines (by accessing memory addresses mapped to it). When the data is in the cache, the latency is under a threshold and so the Spy reads bit "0", otherwise it reads bit "1". Its data are now in the cache.

Similarly, to transmit bit "1", the Trojan accesses the same set of cache lines (by accessing its own memory addresses mapped to it) i.e., he flushes the Spy's data off the cache. To transmit bit "0", the Trojan lets the cache in the same state by doing nothing.

Bandwidth estimation for set-associative cache A set-associative cache is divided in sets of cache lines. As shown in Figure 4.5, a memory address can be split into {TAG, SET, OFFSET} bits where OFFSET is the offset in the cache line, SET the set number and TAG the stored value to compare addresses. In a w-way set-associative cache, w addresses mapped to the same cache line can be stored at the same time, generally based on a LRU replacement policy.

As a result, w addresses must be accessed to fully flush one w-way cache line. Furthermore, virtual to physical address translation rises the problem of addressing uncertainty. Nonetheless, in modern operating systems, the memory space is divided in 4 KB pages and the translation mechanism maps a virtual page to a physical page. Thus, as illustrated in Figure 4.5, the last 12 bits of a memory address remain identical after the translation, leaving unknownsets possible cache sets for one virtual memory address where:

unknownsets " nbsets ˆlinesize pagesize (4.1)

Therefore, to evict a Spy's cache line, the Trojan accesses at least minlines addresses where: minlines " w ˆunknownsets (4.2) Given the total cache size is ttsize " w ˆnbsets ˆlinesize, to read or transmit a single bit the trojan accesses at least:

minlines " ttsize pagesize (4.3)
Finally, we suppose the same probability to transmit bit "0" or bit "1" i.e., P p0q " P p1q " 1{2. Thus, the final time to read or write a bit is:

platency cached `latency f lushed q 2 ˆttsize pagesize (4.4)
Experiment To show the feasibility of building a timing covert channel, we have conducted a proof-of-concept experiment which result is depicted Figure 4.6. We have launched two programs running on distinct cores with a shared L2 cache: a writer (or Trojan) and a reader (or Spy). The upper graph presents the time per access in nanoseconds and the lower graph presents the number of L2 cache misses. All values are obtained from the reader. The green line corresponds to the transmission of only bits 1, the red line to transmissions of only bits 0 and the blue line is an alternation between the two. We have a clear correlation between L2 cache misses and access times suggesting the influence of the former on the latter. In this coarse-grain experiment, the bandwidth is 100 bits per second which is far from the theoretical maximum bitrate of 9.551 Kbps.

Discussion

Previous works on covert timing channels are mainly based on experimental results. To our knowledge, our work is the first attempt to generalize the computation of cache-based covert timing channel bitrate. For this generalization, we consider the time between writing and reading to be null whereas experimental approaches must implement a synchronization mechanism. Indeed, there is a vast range of possibilities for this synchronization between the Trojan and the Spy, and choosing one would alter the quality of our metric. Moreover, this synchronization can be achieved independently from the attack itself. For example, in side channels works, the question is to detect when a cache activity corresponds to a cryptographic computation. If the victim is a web server, a simple solution is to trigger it by accessing a SSL-encrypted web page. Secondly, our information leakage metric can only be based on known covert timing channel attacks, thus it encompasses neither unknown existing attacks nor yet-to-discover attack schemes. However, this metric does not rely on execution traces and as so, it applies to any application and, if properly adapted, any hardware. For example, atomic memory operations are improperly emulated in x86 virtualized environment [START_REF] Wu | Whispers in the hyper-space: high-speed covert channel attacks in the cloud[END_REF]. These atomic operations have been implemented with a big system lock (a lock that freezes all other activities of the system) to keep the memory consistent. Consequently, a memory contention generated by one VM can be seen by another one running on the same physical machine. By observing a contention or its absence, the Trojan and the Spy can transmit respectively bit "1" or "0". A maximum theoretical bandwidth is arguably not the best risk metric i.e., a metric accurately reflecting the dangerousness of timing covert channels. Nevertheless, it can apply to any hardware, be automated and we believe it preserves the scale of dangerousness i.e., a low bitrate should mean a low risk when a high bitrate should mean a high risk. To the best of our knowledge it is the only metric with all discussed features. In the next subsection, we shown how we use this risk metric in our placement algorithm to enforce isolation properties between VMs. And then, in Section 4.2.4, we detail our framework to automate the computation of our information leakage metric.

Information Leakage Aware Placement

This work focuses on the placement of VMs with information leakage constraints specified as isolation properties. What we want to demonstrate is the effectiveness of our approach to ensure isolation and what to consider when doing placement-based security i.e., how to enhance state-of-the-art algorithms to take into account these constraints. In this subsection we present how isolation properties between VMs are satisfied (i.e., enforced) during the placement routine. Moreover, we describe the problem of NUMA allocation and show how we tackle this issue. Finally, we prove the NP-completeness of our placement problem.

Isolation Properties Satisfaction

A placement is the association between a VM and a configuration. We define a configuration as a set of NUMAs and cores. By instantiated VMs, we denote the VMs placed on a physical machine (on a set of NUMAs and cores).

A candidate VM's configuration is valid if both following conditions are met:

1. All properties of the candidate VM are satisfied regarding instantiated VMs.

2. All properties of instantiated VMs are satisfied regarding the candidate VM.

An isolation property of a first VM vm 1 is satisfied regarding a second VM vm 2 if one of the 2 following conditions is met:

1. vm 2 is allowed to transfer information with vm 1 2. the information leakage between their configurations is lower than the one specified by the property (as an acceptable risk).

These two requirements on top of the hardware ones (i.e., CPU, RAM, disk) must be fulfilled to find a suitable configuration. Furthermore, to be able to ensure that all the VMs are respecting their isolation properties (and the ones of the others) during their whole lifetime, it is important to use CPU pinning i.e., to statically associate VMs with cores. Indeed, by not doing so (i.e., if we let a VM changes core during its lifetime or randomly selects one at startup), one of the isolation property could be broken and so the security of the application running inside it as the configuration of the VM would have changed.

Accordingly, our security-aware algorithm must test all configurations for a VM on the physical machines and place it as soon as a configuration is valid. Moreover, the placement routine must update the available resources of the platform. Actually, this update is more complex than it seems due to the way NUMA allocation works. In the following part, we present the NUMA allocation problem and the solution we propose.

The NUMA allocation problem

We must consider real-world microarchitectural allocation schemes to counter real-world microarchitectural attacks (covert channels). Therefore, our proposal is to have a finegrained control over which (microarchitectural) component is shared among multiple VMs to mitigate potential covert channels. With libvirt1 , in addition to the selection of specific cores, we can choose a set of NUMA nodes and one of the 3 available memory allocation policies:

• interleave that allocates memory on a given set of NUMA nodes in a round-robin fashion but falls back to other nodes if the allocation is not possible. In the worst case, any NUMA node can be allocated.

• strict that only allocates memory on a given set of NUMA nodes (or it fails).

• preferred that allocates memory on a given preferred node but falls back to other nodes if the allocation is not possible. In the worst case, any NUMA node can be allocated.

We use the strict policy to have a fine-grained control over memory allocation as we have for CPU cores. Figure 4.7 illustrates how the strict NUMA allocation works. We consider a physical machine composed of 2 NUMA nodes with 2 Gb memory and 2 cores each. A first VM (1 core, 1 Gb memory) is bound to the core c 1 and the closest NUMA node (i.e., the memory banks are directly connected to the core), N uma 1 . A second VM requiring 3 cores is bound to c 2 , c 3 , c 4 which are spread on the 2 NUMA nodes. If this VM requires 2 Gb memory, allocating memory from N uma 2 is enough. But if 3 Gb memory are required, both N uma 1 and N uma 2 are chosen.

In terms of microarchitectural attacks, the information leakage between the 2 VMs is simply the bandwidth leakage between their bound cores and NUMAs. requires more than 2 Gb. The problem is that there is no indication on how much memory will be left on N uma 1 and N uma 2 , a total of 1 Gb memory being free though. As a result, the second VM requiring 1 core and 1 Gb memory is also bound to N uma 1 and N uma 2 . Our solution is to virtually consider the merging of N uma 1 and N uma 2 , that is N uma 1,2 which has a total memory of 4 Gb, 1 Gb being free after the placement of the first VM.

Then, in terms of microarchitectural attacks, the information leakage between the 2 VMs is the bandwidth leakage between {c 1 , c 2 , c 3 , N uma 1 , N uma 2 } and {c 4 , N uma 1 , N uma 2 }. We call ComposedNuma the merging of multiple VNumas where a VNumas is either a real Numa or a ComposedNuma. A VNuma has a name, a total memory mem total , a free memory mem f ree and an internal counter of VMs allocated on it vm insts .

Additionally, we have two references: the list of available Cores and the list of available VNumas. Both refers to components that can be allocated. They consist in respectively:

• The list of Cores not executing any VMs,

• the list of VNuma that are not part of a ComposedNuma. Otherwise (l vnumas is a singleton hence the procedure does not apply), we just update numas available memory. Upon the arrival of a new VM, we suppose a set of Cores and VNumas have been selected according to the information leakage constraints. This selection is simply realized with a First-fit algorithm. In future work, other algorithms such as simulated annealing [START_REF] Kirkpatrick | Optimization by simulated annealing[END_REF] or genetic algorithms [START_REF] Mitchell | An introduction to genetic algorithms[END_REF] could be used providing a way to compare two configurations (i.e., cores and NUMAs) in order to choose the best one. The complete allocation and deallocation procedures are described in Algorithms 4.6 and 4.7.

Our security-aware allocation is not rendering the placement problem less complex. Indeed, VM placement (and any placement problem) is known to be NP-hard and can be abstracted as bin-packing problem [START_REF] Martello | Knapsack problems: algorithms and computer implementations[END_REF]. In the next subsection, we prove that our extension actually increase the complexity of solving the placement problem.

Complexity of our allocation problem

Let an infinity of cores with the VM deployment capacity C. Let a list of virtual machine tvm 1,1 , vm 1,2 , . . . , vm n,n u. We can split this set of virtual machines, in different sub-set: tvm 1,1 , vm 1,2 , . . . , vm 1,n u with a size c n , tvm 2,1 , vm 2,2 u with a size c 2 , and so on. We want pack objects of different volumes (here a sub-set of VMs) into a finite number of bins (here cores) each of volume C in a way that minimizes the number of bins (/cores) used.

We use the binary code to describe the solution and indicate if a VM is on a core or not. Variable x ij is equal to 1 if the VM i is deployed on the core j, and 0 otherwise. Boolean variable y j is equal to 1 if the core is used, 0 otherwise. We try to minimize the number of core used.

min

n ÿ j"1 y j (4.5)
This problem is known as the NP-hard problem called the Bin Packing Problem (BPP). Nevertheless, in our case we have additional constraints due to the security rules. We can consider these constraints like conflicts. The Bin-Packing Problem with Conflicts is called BPPC. It consists in determining the minimal number of identically bins (/cores) needed to store a set of items (VMs) with height is less than the capacity of bins (/cores), where some of these items are incompatible with each other (isolation rules), therefore cannot be packed together in the same bin (/core). The BPPC is a variation of the classical one dimensional BPP which is a combinatorial problem and known also to be NP-hard [START_REF] Coffman | Approximation algorithms for NP-hard problems. chapter Approximation Algorithms for Bin Packing: A Survey[END_REF][START_REF] Maiza | Heuristics for solving the bin-packing problem with conflicts[END_REF]. Finally, our problem is even harder as we do not have 1 dimension (core) but 2 (memory and core). To keep the proof of concept simple, we rely on a first-fit heuristic to solve this BPPC problem.

An Automated Approach

Our approach is a metric-based placement decision. Due to the lack of suitable metric, we have introduced a new information leakage metric measured as a bitrate. Nevertheless, any other sound metric could be substituted. In this subsection, we present our overall automated workflow for VM placement and then discuss how we integrate the concept of metric into our security properties.

Metric-based Placement Decision Workflow

.12 depicts our workflow for placement decision. First, we statically compute the risk metric for each host. In the case of our new information leakage metric, we use two tools: Hwloc [START_REF] Broquedis | hwloc: A generic framework for managing hardware affinities in HPC applications[END_REF] to obtain the hardware topology and Lmbench [START_REF] Mcvoy | lmbench: Portable tools for performance analysis[END_REF] to measure the microarchitectural latencies. Both the topology and latencies are needed to compute information leakage values. A tenant provides his virtualized application model comprising isolation properties with risk metrics. Then, we finally decide the configuration (i.e., NUMAs and cores) for each tenant's VM with the placement procedure previously described.

Scenario: Metric computation

Let's exemplify this workflow. We consider two Grid'5000 [START_REF] Balouek | Adding virtualization capabilities to the Grid'5000 testbed[END_REF] physical machines called Taurus and Genepi. The topology as obtained from Hwloc were depicted respectively in figures 2.13 and 2.12. We recall that Taurus is a NUMA architecture with a shared L3 cache (15 MB) and Genepi is a SMP architecture with a shared L2 cache (6144 KB). Cache latencies measured using lat_mem_rd from the Lmbench benchmarks suite are presented in Figure 4.13. From Taurus latency measures reported in Table 4.2, we can identify 4 steps: 3 cache levels and the main memory (local and remote).

From Genepi latency measures, we can identify 3 steps: 2 cache levels and the main memory.

Finally, using Equation 4. Identically, Genepi L2 cache-based timing covert channel can transmit one bit in 0.5 ˆp6.3ns `130nsq ˆ6144KB{4KB " 104.7µs i.e., 9.551 Kbps bitrate.

Scenario: Tenant specification and Grade

In Section 4.1.3, we have presented our split procedure to obtain typed security properties. In the placement decision, we enforce isolation properties between VMs such as: § ¤ # property IsolationVM ( { VM1 } , { VM2 , VM3 } , grade ) ;

¦ ¥
In Section 2.3.2, we propose a coarse-grain grading system i.e., where grade is an integer. If we directly consider the grade to be our information leakage metric, then a bitrate would be inappropriate, if not senseless, for other types of entities like VNet, Data or Service. Indeed, we require the grade to be generic. Therefore, a solution is to consider a direct mapping between grades and information leakage values. The problem of defining the most relevant grades and mapping is part of our future work.

Automatic Configuration of Security Mechanisms

In addition to having a purely placement-based enforcement of specific security properties (i.e., between VMs), our second complementary solution is the automatic configuration of security mechanisms spread across the infrastructure. This idea is at the core of the Seed4C Project: "seeding" and orchestrating a network of security agents. In this collaborative project, the low-level configuration of security mechanisms comes under our partners and our contribution focuses on the workflow from specification to triggering the low-level configuration.

In the rest of this section, we first present the global architecture of security agents. Then, we detail our solution to integrate security agents into our placement decision.

A Network of Security Agents

All low-level security mechanisms have their own API, language or internal logic. For instance, SELinux policies are composed of deny or allow rules. Similarly, Iptables can reject or accept network packets according to condition rules (e.g., accept if the packet comes from a given IP address). The idea is roughly the same in both cases but their configuration have nothing in common. For this reason, a Security Agent abstracts these low-level mechanisms. A security agent is a process that automatically translates a security property into a configuration of one or more security mechanisms.

A security agent could be placed virtually anywhere it makes sense. As depicted in Figure 4.14, a security agent may be located in the hypervisor to configure mechanisms at the host level, and/or it may be located at the guest level to manage mechanisms within a virtual machine. The two does not bring the same quality of protection. Whether it is within a VM, we must assume the guest kernel is to be trusted otherwise we cannot guarantee that the agent duly enforces the security requirements. On the other hand, the hypervisor is more trustworthy as the end-user cannot directly influence it. However, protecting entities within VMs is much more limited and complex when using mechanisms at the host level i.e., outside VMs. Security agents may also be placed with network controllers to steer the global network configuration (e.g., allocating VLANs and instantiating L3 overlays). In fact, our previously presented placement-based enforcement could be viewed as a security agent dedicated to enforcing specific properties between VMs.

Capabilities and Placement Decision

A security agent may enforce a subset of security properties. This subset depends on the available security mechanisms underneath the agent. For example, an agent is able to enforce the confidentiality between Data or Service entities (e.g., with SELinux) but not for other types of entities. This is related to typed properties except a typed property is first the result of a split procedure and second it is instantiated. Here, the agent has a list of capabilities he knows how to enforce. A capability is to a security property what a function signature is to a function call. In our example, the capability is: .15 depicts our whole placement decision workflow taking into account security agents' capabilities. Security agents can be present at the guest-level i.e., in the VMs of the virtualized application to deploy, and at the host-level i.e., in the hypervisor of some hosts. As illustrated, security agents are not necessarily present in each VM or each host. Each agent has a list of capabilities it can enforce. At the guest-level, this information is attached to the VM image. Indeed, any instance of a VM image have exactly the same mechanisms installed and thus the same list of capabilities. At the host-level, each agent is responsible for publishing its list of capabilities to the placement decision engine. This dynamic approach allows changing hosts' software stack i.e., adding or removing mechanisms (even agents) as needed.

Our decision workflow proceeds as follows. The tenant models its virtualized application and security properties. These properties, after the preprocessing procedure, are sorted into two categories: the capability-based properties with can be enforced by a security agent and the risk-based properties which can only be enforced by selecting correctly hosts and choosing a configuration of NUMAs and cores. Then, a first guest-level solving procedure maps properties to guest-level agents according to their capabilities. After, if some properties are left unsolved, a second host-level solving procedure selects, for each VM, a list of hosts which have the necessary capabilities to solve the VM's properties. Finally, our risk-based placement decision presented in Section 4.2 is applied but with a filtered list of hosts as possiblities. This final step maps each VM to a host and the computed configuration (i.e., NUMAs and cores) as discussed in Section 4.2, but it also maps each VM' properties to the capabilities of their host-level security agents.

Conclusion

In this chapter, we have first shown the preprocessing steps: 1. Implicit to explicit properties: the list of authorized entities can be inferred from the application model to obtain explicit properties.

2. Explicit to singleton properties: a global explicit property can be split into properties with a single secured entity 3. Singleton to typed properties: because mechanisms are specialized, a property can be split into severable properties each one dedicated to a specific type of entity.

Once we obtain typed properties, we have shown two different but complementary methods to enforce them, namely, a placement-based enforcement and the automatic configuration of security mechanisms.

The virtualization cannot provide a strong isolation on shared resources between VMs due to covert channel i.e., leaking unauthorized information by exploiting microarchitectural features. Accordingly, we have first proposed a new information leakage metric to quantify these covert channels, and then an information leakage aware placement algorithm.

The automatic configuration can be achieved with security agents providing capabilities i.e., templates of security properties they can enforce.

In this chapter, we have discussed properties on virtual networks but, due to lack of time, we have not proposed a solution to enforce them. Nevertheless, we could envisioned to tackle this issue as a group membership problem: any VNets (Virtual Networks) with the same properties (and same set of secured/authorized members) can be mapped to the same INet (Infrastructure Network). For instance, VNets without security properties can be mapped to the same public INet. Finally, it would be interesting to prove some equivalences for more complex IF-PLTL formulas.

Chapter 5 Use Case: An Advertising Content Manager for Airports

Through this manuscript, we have presented our user-centric approach to propose a security-aware model and deployment of virtualized applications on virtualization-based infrastructure.

In this chapter, we illustrate our framework on an industrial use case: an Advertising Content Manager service for airports. First, we briefly introduce the Ikusi company and its airport management system. Then, we describe the related virtualized application model and security requirements. In Section 5.3, we detail the different steps of our framework: preprocessing, VM security solving, placement-based enforcement and configuration-based enforcement. For the automatic configuration, we briefly describe the actual architecture of security agents as designed by Bousquet et al. in [START_REF] Bousquet | An autonomous cloud management system for in-depth security[END_REF].

Ikusi Corporation

Ikusi is a corporation offering a broad range of operational management solutions for smart cities, airports, security, mobility (including railways) and health. In particular, this company proposes airport management systems coupled with public information and entertainment systems. In this chapter, our use case focus on the Advertising Content Manager service for airports called Musik.

An airport possesses various spots for advertisements with devices like displays or TV screens. Any advertiser can rent one or more spots to broadcast his advertising campaign. This campaign is designed by an operator using the Musik application. The devices connect to the Musik application to get the content they must broadcast.

As depicted Figure 5.1, the Musik service is a 3-tier application shared between different airports (i.e., Airport1 and Airport2). Any operators or devices (from any airports) access the application by querying a Web Proxy (i.e., tier 1). For instance, an operator from Airport1 can access his advertising web interface by requesting the address https://musik.ikusi.com/airport1/design. Upon receiving this HTTP request, the Web Proxy transfers it to Musik1 App (i.e., tier 2) which returns the web interface. Similarly, a device can query the address https://musik.ikusi.com/airport2/content to obtain the advertising content from Musik2 App. If there is one Musik App per • Proxy, it is the frontend containing the web proxy. A user (i.e., operator or device) queries the proxy which checks the permissions then forward the HTTP request to the proper Musik Application instance.

• Musik_MAD, the Musik application instance for Madrid airport.

• Musik_EAS, the Musik application instance for San Sebastian airport.

• Mysql, the backend containing the database (App_Aodb_database) and an interface presenting the data to the Musik applications (App_Aodb).

The VMs are interconnected with the Intranet VNet and the web proxy is accessible by a user through the Public VNet.

The four VM's resources (i.e., CPU, RAM, Disk) requirements are given in App_Musik containing the Service App_Musik itself plus its executable source code (BinaryExecutable), configuration files (Config), the logs generated by the process (Logs) and some files specific to the instance (File).

Security Policy

The complete use case contains more than 70 properties and it would be too exhaustive to review each one. Instead, we selected four of them to illustrate our approach. These security requirements are the following:

1. An external user is authenticated against the web proxy to determine the airport it belongs to and whether it is a device or an operator.

2. Musik MAD application logs can only be modified by the Musik MAD service.

3. Musik MAD application configuration files can only be read by the Musik MAD service.

4. The whole AirportContentManager framework is isolated from any other tenant in the hosting virtualized infrastructure with at least a medium quality.

From these requirements expressed in natural language, we detail afterwards specific attributes and contexts needed to express the security properties plus the mapping between contexts and real resources we refer to as bindings.

Contexts and Bindings

In this use case, an external user can be either a device or an operator and it belongs to either Madrid or San Sebastian airport. Therefore, we define two new attributes: Role and Airport as follows: § ¤ # attribute Role = ( Device , Operator ) ; # attribute Airport = ( MAD , EAS ) ; Musik Contexts and Bindings The Musik VM is instantiated once per aiport i.e., twice in our case. Nevertheless, as they provide exactly the same service, their security requirements are also the same. As a result, we can optimize the description by defining the contexts and their bindings without specifying which instance they belong to. In the listing below, we give the list of contexts by specifying only the application domain App_Musik. § ¤ # context ctxBinaryMusik = ( Data =" Binary | Executable ") :( AppDomain =" App_Musik ") ; # context ctxConfigMusik = ( Data =" Configuration ") :( AppDomain =" App_Musik ") ; # context ctxFileMusik = ( Data =" File ") :( AppDomain =" App_Musik ") ; # context ctxLogMusik = ( Data =" Log ") :( AppDomain =" App_Musik ") ; # context ctxServiceMusik = ( Service =" App_Musik ") :( AppDomain =" App_Musik ") ; " / opt / dbhook (/.*) ? " ctxFileAODB " / opt / dbhook / dbhook . conf " ctxConfigAODB " / opt / dbhook / jordi . loc " ctxConfigAODB " / opt / dbhook / keys (/.*) ? " ctxKeyAODB " / opt / dbhook / log (/.*) ? " ctxLogAODB " / opt / dbhook / lua (/.*) ? " ctxBinayAODB " / opt / dbhook / pid (/.*) ? " ctxFileAODB " / opt / dbhook / proxydaemon . sh " ctxBinayAODB " / opt / dbhook / proxyrun . sh " ctxBinayAODB " / opt / dbhook / proxystop . sh " ctxBinayAODB " / usr / bin / mysql -proxy " ctxBinayAODB " / etc / rc \. d / init \. d / dbhook " ctxBinayAODB " / usr / lib64 / mysql -proxy / lua / luacall \. so " ctxBinayAODB " / usr / libexec / mysqld " ctxBinaryDB " / etc / my \. cnf " ctxConfigDB " / var / lib / mysql (/.*) ? " ctxFileDB " / usr / bin / mysqld_safe " ctxServiceDB " / usr / libexec / mysqld " ctxServiceDB " / usr / bin / mysql -proxy " ctxServiceAODB ¦ ¥

Listing 5.7: Mysql Bindings Excerpt

Security Properties

After having described some contexts and their bindings, we express the four security requirements as Sam4C security properties. First, we model the requirement "An external user is authenticated against the web proxy to determine the airport it belongs to and whether it is a device or an operator." as an Authentication property where any Clients (Client="*") authenticates against the web proxy service in the proxy VM (ctxProxy:(Service="Web_Proxy")) to obtain a role attribute (Device or Operator) and an airport attribute (MAD or EAS). From this property, we can express the authorized flows depending on the role and the airport. In Section 2.3.2, we introduced our grade as an integer value. But instead of using the full range between 0 and 100, we prefer offering only few levels to the user and have a correspondence between quality levels and grades as detailed in Table 5

Deployment

In this section, we detail the deployment phase of our use case. First we preprocess our security properties to obtain locally enforceable properties. Then, we filter the properties that can be enforced by a guest-level security agent. After, we enforce other properties using our placement-based solution. Finally, we present an internal architecture of security agent and show the configurations enforcing the filtered properties.

Preprocessing

In the four properties we have, only one is eligible to be preprocessed namely: These capabilities matches our three properties. As a result, the Authentication property is mapped to the Proxy VM security agent and the Confidentiality and Integrity properties are mapped to Musik_MAD VM security agent. Suppose the Authentication capability is not present within the Proxy but any other VM (e.g., Musik_MAD), then because the authentication must be performed by the Web_Proxy service which is in Proxy, no solution would have been found and the deployment would have failed. We recall that all these properties have the Medium grade. We arbitrarily define the correspondence between a grade and a covert channel bitrate in Table 5.3.

Placement-based Enforcement

Configuration-based Enforcement

In Section 5.3.2, we have associated the three properties (i.e., Authentication, Confidentiality and Integrity) to guest-level security agents in VMs Proxy and Musik_MAD. After the deployment of the virtualized application described in Section 5.3.3, some security agents receive a set of properties to enforce. In this subsection, we present the security agent architecture as designed by Bousquet et al. in [START_REF] Bousquet | An autonomous cloud management system for in-depth security[END_REF]. Then, we detail the enforcement of the Authentication with PAM and the enforcement of the Confidentiality/Integrity with SELinux. Note that any security agent framework could be used providing it implements the correct interface like in [START_REF] Wailly | Vespa: Multi-layered self-protection for cloud resources[END_REF].

A Security Agent Design

In [START_REF] Bousquet | An autonomous cloud management system for in-depth security[END_REF], a security agent is called a SEE (Secure Element Extended).

As illustrated in Figure 5.8, a security agent has list of security plugins which are individual drivers for each security mechanisms. Each plugin publishes the list of capabilities it can enforce to the capabilities directory. Upon receiving a list of security properties, a plugin selector selects the suitable mechanisms and delegates to the plugin manager the orchestration of properly configuring the security mechanisms through their corresponding plugins.

This architecture can encompass any new mechanism by providing the plugin to drive the configuration of the new mechanism and publish the list of its capabilities.

Authentication with PAM

A Pluggable Authentication Module (PAM) is a mechanism to integrate multiple lowlevel authentication schemes into a high-level application programming interface (API). First, the bindings contain all the necessary information to associate paths to SELinux contexts. For instance, the generation of a SELinux context for ctxLogMusik ((Data="Log"):(AppDomain="App_Musik")) would be:

/opt/musik/log(/.*)?

gen_context(system_u:app_musik_r:log_t,s0) /opt/apache-.*/log(/.*)? gen_context(system_u:app_musik_r:log_t,s0) /opt/devmconn/log(/.*)? gen_context(system_u:app_musik_r:log_t,s0)

Then, the Confidentiality property can be translated in SELinux by allowing read operations (everything is denied by default) as follows:

interface('confidentiality',' gen_require(' type $1; type $2; ') allow $1 $2:file { read_file_perms create_file_perms unlink }; allow $1 $2:lnk_file { read_lnk_file_perms create_lnk_file_perms }; allow $1 $2:dir { search create_dir_perms }; ')

Finally, the application of SELinux confidentiality is the following function call: confidentiality(app_musik_r:log_t, app_musik_r:app_musik_t)

The same process can be realized to enforce the Integrity property by allowing writes operations.

Production Platform Integration

The full deployment implementation is called Sam4C Scheduler. It contains all algorithms and procedures previously presented. Sam4C Scheduler has been integrated in an open source Cloud software platform software called OpenStack. This lighweight integration consists in:

• Replacing the default OpenStack scheduler by Sam4C Scheduler which takes in input Sam4C models.

• Extending the OpenStack database with information leakage informations.

• Extending the Openstack database with the available security agents and their capabilities.

• Extending OpenStack agents with new primitives to add/remove security agents/capabilities.

• Extending OpenStack allocation primitives with the selection of cores and NUMAs.

Given the aforementioned modifications, Sam4C Scheduler can infer the infrastructure model from OpenStack database. Upon receiving a request, Sam4C Scheduler computes the placement and security solutions as previously described, then sends the local security properties to the security agents and provisioned VMs using the new OpenStack primitives.

Conclusion

In this chapter, we have demonstrate the usability of Sam4C to model a real airport management use case. We have detailed each step of our framework from modelization to enforcement. Despite this quite simple application architecture, the quantity of information needed to automatically compute this deployment and enforce its security is huge. For example, defining bindings is time-consuming. Moreover, we recall that we only modeled a small part of the complete airport management framework and only detailed 4 out of 70 security properties for this part. Nevertheless, even if not presented in this manuscript, all the 70 properties have been enforced in practice using several mechanisms.

Chapter 6

Conclusions and Perspectives

The evolution of computing platforms could be viewed as a race between demand i.e., what applications/services need to run efficiently, and supply i.e., what processing power infrastructures are able to offer. Initially in the 1960s, huge computers called mainframes were used to run a vast range of services. At the time, security was a primary concern for the military and secondary for the others. Then, with the sophistication of these applications requiring more resources, services were dispatched and interconnected across multiples machines to form clusters. After, with the continuous growing need of computing and storage resources, grid were designed as a federation of resources operated by multiple organizations. Consequently, it has introduced the novel security issue of concurrent users sharing the same infrastructure. Nowadays, any user of a service like Gmail expects to access the application without delay, from anywhere on earth, at any time and in a responsive and efficient manner. Therefore, new infrastructures have been designed to cope with these issues: Clouds. In such virtualization-based distributed environments, services are deployed on infrastructures providing dynamicity, on-demand resources and abstraction of the physical components for portability. Like Grids, these new virtualization-based infrastructures are shared amongst multiple users/tenants from different organizations from which arise new security issues. Instead of facing external threats mainly, internal threats are now considered as much of a risk. But security is often disregarded due to its complexity, costs and absence of tangible benefits. And when we look at current practices, they mostly rely on multiple independent Access Control methods and do not take into account the propagation of the information that is information flows. But with Access Control, once the information is released from its container, a program may (maliciously or unwillingly) leak the information to an unauthorized entity. Moreover, as most providers offer a security by default of the infrastructure, security issues of hosted applications is left to the user. But the task of configuring the security of an application is complex and error-prone. At the opposite, we believe a user should be able to specify its security without any knowledge of available low-level security mechanisms and should benefit from automatic enforcement methods. In resume, we need a user-centric approach as opposed to provider-centric.

As a solution, we have proposed a specification-driven approach where the security is expressed as properties in a mechanism agnostic language. Our specification-driven approach is materialized as a toolbox called Sam4C (Security-Aware Models for Clouds).

The first part is Sam4C Modeling presented in Chapter 2. We need a simplified repre-sentation (i.e., a model) of the application to be able to deploy it and the list of security properties to enforce them. By following a model-driven engineering methodology, the end-user modelization task is rendered easier with a graphical interface for the virtualized application and a textual language for the security requirements. Our modelization focuses on n-tier applications therefore we have defined a virtualized application as a set of interconnected VMs containing data and services. Following our user-centric philosophy, the security requirements are properties regulating the propagation of information between entities modeled in the application. These properties (e.g., Authentication, Confidentiality, Integrity and Isolation) are mechanism-agnostic: they specify what a secure application is but not how to secure it. As the infrastructure provides the means to enforce the security, we proposed an infrastructure metamodel hosting virtualized applications. This metamodel contains both the description of the distributed infrastructure and the microarchitecture of each physical machine composing it.

If the application part of the model is usually well understood, the exact meaning of the security properties is still fuzzy. Besides, the main issue with existing security languages is the ability to formally guarantee the required property. On the one hand, security policies described in a natural language have quite ambiguous semantics. On the other hand, a formal language or logic provides clear syntax and semantics. Moreover, existing mechanisms are dedicated to secure specific type of entities (e.g., VM, Service, Data, VNet). Therefore, the problem is to have a formal definition of security properties and proven procedures to transform the end-user's global security properties into multiple local properties enforceable by several local mechanisms. For these reasons, we proposed a logic language called IF-PLTL (Information Flow Past Linear Time Logic) in Chapter 3. Our logic is dedicated to controlling the propagation of information i.e., direct and indirect information flows. As these information flows cannot be obtained directly, we have explained their construction from low-level observable events. Security decisions are naturally expressed according to past actions. Accordingly, IF-PLTL is based on the past fragment of LTL with the syntax and semantic detailed in Section 3.5. In addition to using IF-PLTL to transform properties, we have proposed a dynamic monitor that can enforce the full expressivity of IF-PLTL even if its complexity (in time and space) would incur a high overhead in practice.

After having a solid formal basis for our security properties, we must consider their enforcement alongside with the deployment of the application they apply to. If multiple approaches may be envisioned to enforce security properties, we propose two different but complementary solutions in Chapter 4. The first one (described in Section 4.2) is a security-aware placement to enforce security between virtual machines (inter-VM security) which may belong to the same or to different applications. The second (described in Section 4.3) is the configuration of security mechanisms to provide security within applications' virtual machines (intra-VM security). But these approaches can only enforce typed properties obtained after the following preprocessing steps detailed in Section 4.1:

1. Implicit to explicit properties: the list of authorized entities can be inferred from the application model to obtain explicit properties.

2. Explicit to singleton properties: a global explicit property can be split into properties with a single secured entity 3. Singleton to typed properties: because mechanisms are specialized, a property can be split into several properties each one dedicated to a specific type of entity.

All these three procedures are based on proven equivalences thanks to IF-PLTL.

In terms of inter-VM security, the virtualization cannot provide a strong isolation on resources shared between VMs due to covert channels which leak unauthorized information by exploiting microarchitectural features. Accordingly, we have proposed a new information leakage metric to quantify these covert channels, and then integrated this metric into our placement algorithm. The idea is to let the user specify the risk it is willing to face and strictly enforce this constraint by carefully allocating cores and NUMAs for each VM. For intra-VM security, the automatic configuration of mechanisms has been achieved with security agents providing capabilities i.e., templates of security properties they can enforce. Consequently, the problem has been reduced to choosing security agents with the right capabilities.

To illustrate our whole framework, we have presented a real industrial use case: An Advertising Content Manager for Airports in Chapter 5. Using Sam4C Modeling, Ikusi's engineers have modeled their application and security requirements with limited external help i.e., Sam4C seems to be easy-to-use. Each method detailed in each chapter has been exemplified on this use case. In our opinion, this use case demonstrates two general points. First, the task of providing an end-to-end automatic security a real application is not trivial. Many layers from hardware to software code are involved and we are far from providing a precise and complete modelization of the application. But our second point is that it is feasible to do so by relying on formal methods and integrating good practices from domains other than security like model-driven engineering.

Short-Term Perspectives

Our contributions can be extended in several directions. In this section, we present our short-term perspectives.

Modelization The current Sam4C implementation can be improved in several ways.

• First, we can provide automatic analysis tools to verify the validity of the modelization i.e., that all the needed information are specified for a deployment or that the security properties are not contradictory.

• Second, our current metamodel focuses mainly on the IaaS layer with VMs and VNets; it would be interesting to extend our metamodel to the PaaS and SaaS layers by providing the corresponding models and propose a cross-layer security from the hypervisor to application-specific flows.

• Third, we can study new use cases to validate our metamodel or extend it with the necessary features.

• And last but not the least, our current deployment is limited to provisioning VMs with components statically installed in those VMs i.e., we suppose that each VM contains the correct software stack. The full deployment of all components composing this software stack could be automatized as well. To do so, we believe that component-based modeling is a key lead bringing more adaptability, dynamicity and flexibility to our models. An automatic deployment of inner components can facilitate the enforcement of the security. Indeed, without automaticity, the enforcement must be based on the existing architecture which must be accurately specified by the end-user whereas in an automatic process, all these information can be known without requiring the end-user's knowledge.

Logic In our formalization, we have presented a dynamic monitor. It would be interesting to implement it at the system level and evaluate its overhead in practice with a realistic security policy.

Security Enforcement Regarding the enforcement of security, several points can be addressed:

• First, our placement decision is constrained by covert channels. These constraints lead to a deconsolidation of the platform i.e., VMs are more likely to be spread across the infrastructure than be regrouped on the same host. This side effect is in opposition with the economical benefit of maximizing the consolidation i.e., security costs. Therefore, a cost-model for covert channels should be devised to quantify and monetize this impact.

• Then, we have presented the enforcement of properties between VMs and within VMs but we have left aside the enforcement of network properties. We have discussed a potential solution in Section 4.4 and more effort should be put to explore this direction as securing networks is as important as securing VMs.

• Finally, we have briefly discussed the necessity of having a grading system in Section 2.3.2. A short-term contribution would be to effectively propose a user-friendly grading system and assess its suitability by conducting a survey on a panel of users.

Long-Term Perspectives

After having presented our short-term perspectives, we discuss in this section our longterm perspectives.

Modelization We have previously proposed to integrate component-based models in our modelization to automatically deploy the software stack within VMs. Following this idea, component-based models are well known to represent dynamic applications scaling at runtime, for instance by changing the number of instances of a VM delivering a service depending on the load. This approach can be further extended to encompass applications which requires some reconfiguration at runtime, for instance to update a legacy architecture with a more efficient but completely different one. This direction should be explored alongside a dynamically reconfigurable security detailed later.

Logic Our logic formalism can be improve in several ways:

• Thanks to IF-PLTL, we have proved few equivalences specifically for the Confidentiality, Integrity and Isolation properties, but we lack general methods to obtain local properties i.e., methods taking as input any arbitrary IF-PLTL formula.

• Furthermore, to have a complete approach, we should provide the means to ensure the correctness of a security policy i.e., prove that a given theory (policy) is coherent. Indeed, allowing an end-user to deploy an incoherent policy is undesirable.

• Our current monitor is not deadlock-free i.e., a sequence of events can lead to forbidding any future accesses. Consequently, the secured system is overprotected as it does not render any service anymore. The desirable property for a monitor is to preserve the liveness while making decisions. One idea is to detect any events leading to deadlock situation and prevent them.

Security Enforcement As stated before, security has a cost but as demonstrated in this Thesis, a general security is hard to quantify or qualify. We can envision two directions:

• A generic and precise metric or grading system for security. The first milestone is to propose a metric to compare two security configurations i.e., being able to have a partial order on security configurations. Then, the second step is having a metric scale proportional/coherent with the security risk.

• The previous proposition can facilitate the design of a general cost-model associating a price to a given security configuration.

Distributed Security If many works have been conducted on system security, programming language security and network security, fewer achievements have been obtained on what we call distributed security. Current solutions revolve around a more or less centralized security of a distributed system and not a fully distributed security. The closest concept would be decentralized security with is divided into Decentralized Access Control [START_REF] Laganier | Hipernet: a decentralized security infrastructure for large scale grid environments[END_REF] and Decentralized Information Flow Control. In AC, the decentralized component is the delegation authority i.e., the entity delivering roles and permissions, and controls are locally authorized, for instance a distributed/decentralized Public Key Infrastructure [START_REF] Lesueur | An efficient distributed pki for structured p2p networks[END_REF]. In IFC, the major technique is tainting which piggybacks the security policy on each entity. But this technique is efficient only with lightweight piggybacked information and has mostly been applied to a single machine. If we consider a large distributed system with much more entities and conflicting domains, this information grows too and may not scale. Besides, tainting techniques have only been applied only for Confidentiality and Integrity properties. Therefore, we lack scalable methods to control complex information flow properties across a distributed system like Clouds. Generally speaking, the security of each individual components does not ensure the security of the whole. Accordingly, a first can be the design of composable security properties to prove the equivalence between locally enforced properties and a global property of the system. A collaborative security system could also be interesting to explore.

Autonomic Security A very interesting perspective is autonomic security. It can be characterized as a security that can reconfigure itself, recover from intrusions, dynamically adapt the security to the current state of the system. Currently, the closest concept is autonomic networking which includes some considerations on security, for instance by learning from a DDoS network attack to update the firewall rules accordingly. However, the autonomic security has yet to be designed for systems (e.g., OSes).

3. 1

 1 Direct and indirect flows . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 Alice and Bob must not exchange information with each other. . . . . . . 3.3 Monitor Architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.4 Overview of the computation of traces . . . . . . . . . . . . . . . . . . . 3.5 Trace of observable events . . . . . . . . . . . . . . . . . . . . . . . . . . vi 3.6 Trace of functional events . . . . . . . . . . . . . . . . . . . . . . . . . . 3.7 Trace of information flows . . . . . . . . . . . . . . . . . . . . . . . . . . 3.8 Indirect path scenario with Alice and Bob . . . . . . . . . . . . . . . . . . 4.1 Sam4C Model with a security domain of 3 VMs and 2 VNets. . . . . . . 4.2 Microarchitectural Side and Covert Channels . . . . . . . . . . . . . . . . (a) Side Channel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . (b) Covert Channel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3 SVF and CSV workflow . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 1 . 1 :

 11 Figure 1.1: Cloud Stacks and Separation of Duties

Figure 1 . 2 :

 12 Figure 1.2: Non-virtualized and virtualized systems

Figure 1 . 3 :

 13 Figure 1.3: n-tier architecture example

Figure 1 . 4 :

 14 Figure 1.4: Overview of the Thesis

Figure 2 . 1 :

 21 Figure 2.1: Metamodeling hierarchy

Figure 2 . 3 :

 23 Figure 2.3: Root objects of the security-aware virtual distributed system metamodel in UML

Figure 2 . 4 :

 24 Figure 2.4: Virtual Layer Node Components

Figure 2 . 5 :

 25 Figure 2.5: Virtual Network Components

Figure 2 .

 2 Figure 2.6 is our virtual layer metamodel in UML. Any entity (VM, VNet, etc.) inherits from the abstract object Element, they all have a name, and composes the architecture root node.

Figure 2 . 6 :

 26 Figure 2.6: Virtual Layer Metamodel

Figure 2 .

 2 7 depicts an AppDomain called System with an SSH service reading or writing Logs as represented by the green AppLink.

Figure 2 . 7 :

 27 Figure 2.7: System application domain with SSH service accessing Logs data

Figure 2 . 8 :

 28 Figure 2.8: Application Layer Metamodel

Figure 2 . 9 :

 29 Figure 2.9: Infrastructure Layer Metamodel

Figure 2 .

 2 Figure 2.10: SMP architecture principles

Figure 2 . 13 :

 213 Figure 2.13: Intel Xeon E5-2630 Non-Uniform Memory Access topology (Grid'5000 Taurus Node) from Hwloc

Figure 2 .

 2 Figure 2.14: Microarchitecture Metamodel

Figure 2 .

 2 Figure 2.15: Model-to-system workflow

Figure 2 . 17 :

 217 Figure 2.17: Security attributes and contexts metamodel

Figure 2 .

 2 Figure 2.18: Binding metamodel

  [START_REF] Blanc | Mandatory access protection within cloud systems[END_REF] depicts an application with V M 1 connected to a Client and V M 2 through respectively Internet VNet and Intranet VNet. It is natural to assume that a security policy should allow V M 1 to access Internet and Intranet: this information from the model is implicit.

Figure 2 .

 2 Figure 2.19: Virtualized Application Model with 2 VNets, 2 VMs and 1 client.

Figure 3 . 1 :

 31 Figure 3.1: Direct and indirect flows

Figure 3 . 2 :

 32 Figure 3.2: Alice and Bob must not exchange information with each other.

  .3, this process is represented as the Trace Computation box. It receives System Events from the Events Interposition box and produces Information Flow Events. How to implement an Events Interposition mechanism is quickly discussed in Section 3.4.1.

Figure 3 . 3 :

 33 Figure 3.3: Monitor Architecture

Figure 3 . 4 :

 34 Figure 3.4: Overview of the computation of traces

Figure 3 . 5 :

 35 Figure 3.5: Trace of observable events

Figure 3 .

 3 Figure 3.6 is the result of projecting observable events of Figure3.5 into functional events. In this trace, the first observable event (a, begin_read, b) and the third observable event (a, end_read, b) are transformed into a functional event (a, read, b) occurring at every moment between the beginning and the end included.

Figure 3 . 6 :

 36 Figure 3.6: Trace of functional events

•Figure 3 .

 3 Figure 3.7 is the result of projecting functional events in Figure 3.6 into information flows. pa, read, bq and pc, write, bq are substituted by pa ă bq and pc ą bq respectively.

Figure 3 . 7 :

 37 Figure 3.7: Trace of information flows

Figure 3 . 7 (

 37 Page 57) satisfies the property c " a at the second and third moments because of the indirection c ą b and b ą a.

  D satisfying the following properties: (a) Each sort σ P S is mapped to a non empty domain D σ . (b) Each constant symbol c P C of sort σ is mapped to an element c I P D σ . (c) Each function symbol f P F of sorted arity σ 1 ˆ. . . ˆσn Ñ σ is mapped to a function f I : D σ 1 ˆ. . . ˆDσn Ñ D σ . (d) Each predicate symbol p P P of sorted arity σ 1 ˆ. . . ˆσn is mapped to a subset p I Ď D σ 1 ˆ. . . ˆDσn . A FO temporal structure M is composed of a flow of time F, the same domain D and a function A associating every moment of the execution to a FO many-sorted structure previously introduced. Definition 14 (A First-Order Temporal Structure). A FO-temporal Σ IF ´P LT L -structure (or model) is defined by M " F, D, A with:

Figure 3 . 8 :

 38 Figure 3.8: Indirect path scenario with Alice and Bob .

k

  Event reachAlice " Bob Bob " Alice SAT pΨq 1 pAlice ą W orkerAq Alice Ñ tW orkerAu false false true 2 pW orkerA ą AppAq Alice Ñ tW orkerA, AppAu false false true W orkerA Ñ tAppAu 3 pAppA ą F ileq Alice Ñ tW orkerA, AppA, F ileu false false true W orkerA Ñ tAppA, F ileu AppA Ñ tF ileu 4 pF ile ą AppBq Alice Ñ tW orkerA, AppA, F ile, AppBu false false true W orkerA Ñ tAppA, F ile, AppBu AppA Ñ tF ile, AppBu F ile Ñ tAppBu 5 pAppB ą W orkerBq Alice Ñ tW orkerA, AppA, F ile, AppB, W orkerBu false false true W orkerA Ñ tAppA, F ile, AppB, W orkerBu AppA Ñ tF ile, AppB, W orkerBu F ile Ñ tAppB, W orkerBu AppB Ñ tW orkerBu 6 pW orkerB ą Bobq Alice Ñ tW orkerA, AppA, F ile, AppB, W orkerB, Bobu true false false W orkerA Ñ tAppA, F ile, AppB, W orkerB, Bobu AppA Ñ tF ile, AppB, W orkerB, Bobu F ile Ñ tAppB, W orkerB, Bobu AppB Ñ tW orkerB, Bobu Table 3.1: Interpretation and satisfaction of the isolation between A and B.

  Figure 4.1 depicts a security domain Dom comprising 3 VMs i.e., VM1 to VM3 and one VNet (Virtual Network) Intranet.

Figure 4 . 1 :

 41 Figure 4.1: Sam4C Model with a security domain of 3 VMs and 2 VNets.

Algorithm

Algorithm 4 . 2

 42 Singleton Split Procedure Variables: P " pP rop, S, A, gq if |S| " 1 then return tP u P Set " H for all x P S do P Set " P Set Y pP rop, txu, A Y S ´txu, gq return P Set Let us apply Algorithm 4.2 to the scenario inFigure 4.1. If we consider the following (explicit) property in input: § ¤ # property Isolation ( { VM2 , VM3 , Intranet } ,{ VM1 } ) ; ¦ ¥ Then, the result of this singleton splitting procedure is: § ¤ # property Isolation ( { VM2 } ,{ Intranet , VM3 , VM1 } ) ; # property Isolation ( { VM3 } ,{ Intranet , VM1 , VM2 } ) ; # property Isolation ( { Intranet } ,{ VM3 , VM1 , VM2 } ) ; ¦ ¥

Figure 4 . 1 .

 41 If we consider our previous singleton properties in input: § ¤ # property Isolation ( { VM1 } , { Public , Intranet , VM2 , VM3 } ) ; # property Isolation ( { VM2 } ,{ Intranet , VM3 , VM1 } ) ; # property Isolation ( { VM3 } ,{ Intranet , VM1 , VM2 } ) ; # property Isolation ( { Intranet } ,{ VM3 , VM1 , VM2 } ) ; ¦ ¥

Figure 4 .

 4 2b, VM Mal receives information from a Trojan represented by a square in VM Bob.

Figure 4 . 2 :

 42 Figure 4.2: Microarchitectural Side and Covert Channels

Figure 4 . 3 :

 43 Figure 4.3: SVF and CSV workflow

Figure 4 . 4 :

 44 Figure 4.4: Cached-based timing covert channel transmitting "10".

Figure 4 . 5 :

 45 Figure 4.5: Memory address cache line and page mapping.

Figure 4 . 6 :

 46 Figure 4.6: Timing Cached-based Covert Channel on Intel Xeon E5420 QC.

Figure 4 .

 4 8 illustrates our proposal to deal with the memory segmentation. The first VM (3 cores and 3 Gb of memory) is bound on both N uma 1 and N uma 2 because it

Figure 4 . 7 :

 47 Figure 4.7: Strict memory allocation policy for 2 VMs (1 core then 3 cores).

Figure 4 . 8 :

 48 Figure 4.8: Strict memory allocation policy for 2 VMs (3 cores then 1 core).

  Metamodel for NUMA allocation Figure4.9 is an extension of our previous metamodel described in Figure2.14 (Page 35) to encompass the NUMA allocation scheme.

Figure 4 . 9 :

 49 Figure 4.9: Microarchitecture Metamodel with Virtual NUMAs.

Figure 4 .

 4 Figure 4.11: NUMA Structure Model with 3 VMs sequentially removed.

Algorithm

Figure 4 .

 4 Figure 4.12: Metric-based Placement Decision Workflow.

Figure 4 . 13 :

 413 Figure 4.13: Taurus (with NUMAs) and Genepi memory read latencies.

Figure 4 . 14 :

 414 Figure 4.14: Security Agents (SA) Location

Figure 4

 4 Figure 4.15 depicts our whole placement decision workflow taking into account security agents' capabilities. Security agents can be present at the guest-level i.e., in the VMs of the virtualized application to deploy, and at the host-level i.e., in the hypervisor of some hosts. As illustrated, security agents are not necessarily present in each VM or each host. Each agent has a list of capabilities it can enforce. At the guest-level, this information is attached to the VM image. Indeed, any instance of a VM image have exactly the same mechanisms installed and thus the same list of capabilities. At the host-level, each agent is responsible for publishing its list of capabilities to the placement decision engine. This dynamic approach allows changing hosts' software stack i.e., adding or removing mechanisms (even agents) as needed.Our decision workflow proceeds as follows. The tenant models its virtualized application and security properties. These properties, after the preprocessing procedure, are sorted into two categories: the capability-based properties with can be enforced by a security agent and the risk-based properties which can only be enforced by selecting correctly hosts and choosing a configuration of NUMAs and cores. Then, a first guest-level solving procedure maps properties to guest-level agents according to their capabilities. After, if some properties are left unsolved, a second host-level solving procedure selects, for each VM, a list of hosts which have the necessary capabilities to solve the VM's properties. Finally, our risk-based placement decision presented in Section 4.2 is applied but with a filtered list of hosts as possiblities. This final step maps each VM to a host and the computed configuration (i.e., NUMAs and cores) as discussed in Section 4.2, but it also maps each VM' properties to the capabilities of their host-level security agents.

Figure 4 . 15 :

 415 Figure 4.15: Complete Placement Decision Workflow.

Figure 5 . 2 :

 52 Figure 5.2: Screenshot of the Ikusi use case from Sam4C

Figure 5 . 3 :

 53 Figure 5.3: Sam4C Model of Ikusi Use Case

  § ¤ # context ctxAodbDB = { AirportContentManager . Mysql . App_Aodb_database } ; # context ctxBinaryDB = ctxAodbDB :( Data =" BinaryExecutable ") ; # context ctxConfigDB = ctxAodbDB :( Data =" Config ) ; # context ctxFileDB = ctxAodbDB :( Data =" File ) ; # context ctxServiceDB = ctxAodbDB :( Service =" App_Aodb_database ) ; # context ctxAodb = { AirportContentManager . Mysql . App_Aodb } ; # context ctxBinayAODB = ctxAodbDB :( Data =" BinaryExecutable ) ; # context ctxConfigAODB = ctxAodbDB :( Data =" Config ) ; # context ctxKeyAODB = ctxAodbDB :( Data =" Key ) ; # context ctxLogAODB = ctxAodbDB :( Data =" Log ) ; # context ctxFileAODB = ctxAodbDB :( Data =" File ) ; # context ctxServiceAODB = ctxAodbDB :( Service =" App_Aodb ) ; ¦ ¥ Listing 5.6: Mysql Contexts Excerpt Then, the Mysql bindings are the following: § ¤

Listing 5 . 8 :Listing 5 . 9 :

 5859 § ¤ # property Authentication (( Client ="*") , ctxProxy :( Service =" Web_Proxy ") , [ ( Role =" Device | Operator ") :( Airport =" MAD | EAS ") ] ) ; ¦ ¥ Ikusi Authentication Property Our second and third requirements, namely "Musik MAD application logs can only be modified by the Musik MAD service." and "Musik MAD application configuration files can only be read by the Musik MAD service.", are respectively an Integrity and a Confidentiality properties. Previously, we have defined Musik contexts without attaching a particular VM. Therefore, in the following listing, we specialize our contexts with the VM Musik_App by writing (VM="Musik_MAD"):ctx. § ¤ # property Integrity (( VM =" Musik_MAD ") : ctxLogMusik , ( VM =" Musik_MAD ") : ctxServiceMusik ) ; # property Confidentiality (( VM =" Musik_MAD ") : ctxConfigMusik , ( VM =" Musik_MAD ") : ctxServiceMusik ) ; ¦ ¥ Ikusi Integrity and Confidentiality PropertiesFinally, the fourth requirement "The whole AirportContentManager framework is isolated from any other tenant in the hosting virtualized infrastructure with at least a medium quality." is simply expressed using an implicit property as: § ¤ # property Isolation ( { AirportContentManager } , MEDIUM ) ;

  Our security-aware placement algorithm must enforce the four following properties: § ¤ # property IsolationVM ( { Musik_MAD } ,{ Proxy , Mysql , Musik_EAS } ) ; # property IsolationVM ( { Mysql } ,{ Proxy , Musik_MAD , Musik_EAS } ) ; # property IsolationVM ( { Musik_EAS } ,{ Proxy , Musik_MAD , Mysql } ) ; # property IsolationVM ( { Proxy } ,{ Musik_MAD , Mysql , Musik_EAS } ) ; ¦ ¥ Listing 5.15: Ikusi Typed IsolationVM Properties

  required) and Musik_MAD (2 cores, 6 GB memory required) are provisioned on the local cores of N uma1 i.e., no cache is shared with Other. As a result, we obtain the infrastructure depicted Figure 5.5.

Figure 5 . 5 :

 55 Figure 5.5: Infrastructure State after placing Proxy and Musik_MAD.

Figure 5 . 6 :

 56 Figure 5.6: Taurus1 Final State.

Figure 5 . 7 :

 57 Figure 5.7: Taurus2 Final State.

Figure 5 . 8 :Listing 5 . 16 :

 58516 Figure 5.8: Security Agent Architecture.

Figure 5 . 9 :Listing 5 . 17 :

 59517 Figure 5.9: LDAP tree structure.

  3.1 Logic 101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.1.1 Syllogistic or Classical Logic . . . . . . . . . . . . . . . . . . . . . 3.1.2 Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . 3.1.3 Predicate or First-Order Logic . . . . . . . . . . . . . . . . . . . . 3.1.4 Modal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.1.5 Verification of Logics . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 State of the Art . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2.1 Information Flow Control properties . . . . . . . . . . . . . . . . 3.2.2 Logic-based Policies . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.3 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.4 System Model: Traces Acquisition . . . . . . . . . . . . . . . . . . . . . . 3.4.1 Traces with Observable Events . . . . . . . . . . . . . . . . . . . 3.4.2 Traces with Functional Events . . . . . . . . . . . . . . . . . . . . 3.4.3 Traces with Information Flows . . . . . . . . . . . . . . . . . . . . 3.4.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.5 Security Properties: Information Flow Past Linear Time Logic . . . . . . Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Security Deployment for Virtualized Distributed Systems 4.1 Preprocessing of Security Requirements . . . . . . . . . . . . . . . . . . . 4.1.1 Equivalence for Confidentiality, Integrity and Isolation . . . . . . 4.1.2 Implicit to Explicit Properties . . . . . . . . . . . . . . . . . . . . 4.1.3 Model-based Property Split . . . . . . . . . . . . . . . . . . . . . 4.1.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2 Placement-based Security . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.1 State of the Art . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.2 Information Leakage Quantitative Metric . . . . . . . . . . . . . . 4.2.3 Information Leakage Aware Placement . . . . . . . . . . . . . . . 4.2.4 An Automated Approach . . . . . . . . . . . . . . . . . . . . . . . 4.3 Automatic Configuration of Security Mechanisms . . . . . . . . . . . . . Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Cloud Stacks and Separation of Duties . . . . . . . . . . . . . . . . . . . 1.2 Non-virtualized and virtualized systems . . . . . . . . . . . . . . . . . . 1.3 n-tier architecture example . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4 Overview of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1 Metamodeling hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Integration of GMF and Xtext with EMF . . . . . . . . . . . . . . . . . 2.3 Root objects of the security-aware virtual distributed system metamodel in UML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.4 Virtual Layer Node Components . . . . . . . . . . . . . . . . . . . . . . . Virtual Network Components . . . . . . . . . . . . . . . . . . . . . . . . 2.6 Virtual Layer Metamodel . . . . . . . . . . . . . . . . . . . . . . . . . . 2.7 System application domain with SSH service accessing Logs data . . . . 2.8 Application Layer Metamodel . . . . . . . . . . . . . . . . . . . . . . . . 2.9 Infrastructure Layer Metamodel . . . . . . . . . . . . . . . . . . . . . . 2.10 SMP architecture principles . . . . . . . . . . . . . . . . . . . . . . . . . 2.11 NUMA architecture principles . . . . . . . . . . . . . . . . . . . . . . . . 2.12 Intel Xeon E5420 QC Uniform Memory Access topology (Grid'5000 Genepi Node) from Hwloc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.13 Intel Xeon E5-2630 Non-Uniform Memory Access topology (Grid'5000 Taurus Node) from Hwloc . . . . . . . . . . . . . . . . . . . . . . . . . . 2.14 Microarchitecture Metamodel . . . . . . . . . . . . . . . . . . . . . . . . 2.15 Model-to-system workflow . . . . . . . . . . . . . . . . . . . . . . . . . . 2.16 Model of a SSH service in a System application domain inside VM1 virtual machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.17 Security attributes and contexts metamodel . . . . . . . . . . . . . . . . 2.18 Binding metamodel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.19 Virtualized Application Model with 2 VNets, 2 VMs and 1 client. . . . .

	List of Figures
	1.1

3.5.1 Temporal Many-Sorted Logic with Information Flow . . . . . . . 3.5.2 IF-PLTL Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.5.3 IF-PLTL Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 3.6 Dynamic Monitoring . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.6.1 Memory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.6.2 Monitoring Algorithm . . . . . . . . . . . . . . . . . . . . . . . . 3.6.3 Complexity Analysis . . . . . . . . . . . . . . . . . . . . . . . . . 3.7 3.7.1 Isolation Policy . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.7.2 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.8 4.3.1 A Network of Security Agents . . . . . . . . . . . . . . . . . . . . 4.3.2 Capabilities and Placement Decision . . . . . . . . . . . . . . . . 4.4 (a) VM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . (b) Client . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . (c) Security Domain . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.5

  pM, kq |ù pa « bq iff pa « bq P I k p«q pM, kq |ù pa ą bq iff pa ą bq P I k pąq pM, kq |ù pa P sq iff pa P sq P I k pPq pM, kq |ù pa " bq iff pM, kq |ù pa ą bq or kq |ù ϕ pM, kq |ù ϕ 1 ^ϕ2 iff pM, kq |ù ϕ 1 and pM, kq |ù ϕ 2 pM, kq |ù D σ xϕpxq iff pM, kq |ù ϕrx I {xs for some x I P D σ pM, kq |ù Y ϕ iff 0 ă k and pM, k ´1q |ù ϕ pM, kq |ù ϕ 1 Sϕ 2 iff Di, p0 ď i ď kq,

		$
		' & pM, kq |ù pc ą bq
		Di, p0 ď i ď kq, D ctx c,	and
		' % pM, iq |ù pa " cq
	pM, kq |ù ϕ	iff pM, $
		' & pM, iq |ù ϕ 2
		and
		'
		%

The satisfaction relation (or truth-relation) pM, kq |ù ϕ between a model (structure) M and a formula ϕ at the moment k is defined as follows: @j, pi ă j ď kq, pM, jq |ù ϕ 1

Satisfiability

As previously explained, the existence of a future state is unsatisfiable for a dynamic trace (constructed as events occur). Here, we make two general observations: Observation 1. In the general case, a model M at moment k can satisfy a theory T (set of closed formulas), but not at moment k `1. pM, kq |ù T ùñ pM, k `1q |ù T Observation 2. In the general case, a model M would not satisfy a theory T at moment k, but could at moment k `1. pM, kq |ù T ùñ pM, k `1q |ù T

  val pre , Ψ upon event px ą yq do reach

new Ð ADDREACH(reach pre , x ą y) INIT(val new ) for all ϕ P subf(Ψ) do {Monitored subformulas ordered by depth-inverse} val new rϕs Ð COMPUTEVAL(ϕ, val pre , val new ) if SAT(Ψ, val new ) then UPDATE(reach new , val new ) ACCEPTpx ą yq else REFUSEpx ą yq

  4.1 Implicit to Explicit Procedure Input: P implicit : set of implicit properties to extend.

	From our example depicted Figure 4.1, the result of Algorithm 4.1 is:
	§	¤
	# property Isolation ( { VM2 , VM3 , Intranet } ,{ VM1 } ) ;
	# property Isolation ( { VM1 } ,{ Public , VM2 , Intranet , VM3 } ) ;

Variables: P Ð H for all p i " pT, S, gq P P implicit do S border Ð listBorder(S) S internal Ð S ´Sborder P Ð P Y pT, S internal , S border , gq for all x P S border do A neighbors Ð listNeighbors(x) P Ð P Y pT, txu, S internal Y A neighbors Y S border ´txu, gq return P ¦ ¥

3

  Typed Split Procedure Variables: P " pP rop, S, A, gq P Set typed " H for all type P tvm, vnetu do A typed " tx | x P A ^x P typeu P Set typed " P Set typed Y pP rop type , S, A typed , gq return P Set typed Let us apply Algorithm 4.3 to the scenario in

Table 4 .

 4 1: Covert timing channels summary for Cloud environments

	Paper Component	Bitrate	Error Rate	Setup	Access Pattern	Error Correction
	[97]	L1	3.2 Mbps ă25% Lab	Parallel (SMT) No
		L2	800 kbps	ă25% Lab	Parallel (SMT) No
	[120]	SMT/FU	500 kbps	NC	Lab	Parallel (SMT) NC
		Speculation	200 kbps	NA	Lab	Sequential	Noiseless
	[124]	L2	262.47 bps NA	Lab	Sequential	Noiseless
		L2	3.75 bps	8.59% EC2	Sequential	DF
	[123]	Memory bus 746.8 bps	0.09% Lab	Parallel	FEC
		Memory bus 107.9 bps	0.75% EC2	Parallel	FEC
		L2	190.4 kbps NC	Lab	Parallel	NC
	[93]	CPU	0.49 bps	NA	Lab	Sequential	Noiseless
	[122]	Xen	174.98 bps 2%	Lab	Sequential	No
		Shared-Mem
	[103]	Memory bus 0.006 bps	NC	EC2	NC	NC
		Hard disk	0.0005 bps NC	EC2	NC	NC
		L2	0.2 bps	NC	EC2	Sequential	DF

NA: do Not Apply; NC: Not Communicated; FEC: Forward Error Correction; DF: Differential Coding.

  4.6 Allocation Procedure Input: n: Node, v: VM, l numas : List of VNumas , l cores :List of Cores Precondition: l numas ą 0 {A VM must have some memory} Variables: vn: VNuma {Remove cores from availability list} n.cores available Ð n.cores available ´lcores q {Compose numas if needed and remove sub-numas from availability list} if |l numas | ą 1 then vn Ð composeNuma(n, l numas ); else vn Ð getFirst(l numas ) {There is only 1 numa in l numas } {Substract VM's required memory} vn.mem f ree ´" v.mem required {Increment VM instances} vn.vm insts `" 1 {Substract VM's required disk space} n.disk´" v.disk required {Substract VM's required disk space} n.disk´" v.disk required instantiateVM(v, l cores , vn) Algorithm 4.7 Deallocation Procedure Input: n: Node, v: VM, vn: VNuma , l cores :List of Cores Variables: vn: VNuma {Decrement VM instances} vn.vm insts ´" 1 {Add cores back to availability list} n.cores available Ð n.cores available Y l cores q {Add back VM's required memory} vn.mem f ree `" v.mem required {Propagate newly free memory to parent NUMAs} VNuma vn parent Ð vn while pvn parent Ð vn parent .parentq ‰ Hq do vn parent .mem f ree `" v.mem required

	{Decompose if possible}
	decomposeNuma(n, vn);
	{Add vack VM's required disk space}
	n.disk`" v.disk required

Table 4 .

 4 4, Taurus L3 cache-based timing covert channel can transmit one bit in 0.5 ˆp17ns `108nsq ˆ15M B{4KB " 240.0µs i.e., 4.167 Kbps bitrate on 3: Genepi latency measurements local NUMA, and 0.5 ˆp17ns `184.5nsq ˆ15M B{4KB " 386.9µs i.e., 2.585 Kbps bitrate on remote NUMA.

	Component	Block size	latency
	L1 cache	1 B to 32 KB	1.43 ns
	L2 cache	32 KB to 256 KB	4.3 ns
	L3 cache	256 KB to 15 MB	17.0 ns
	Local NUMA	-	108 ns
	Remote NUMA	-	184.5 ns
	Table 4.2: Taurus latency measurements
	Component	Block size	latency
	L1 cache	1 B to 32 KB	1.2 ns
	L2 cache	32 KB to 256 KB	6.3 ns
	Main Memory 256 KB to 15 MB 130.0 ns

Table 5

 5

	.1.

Table 5 .

 5

1: Ikusi VMs Resource Requirements

Each VM contains one or two Application Domains grouping coherent sets of processes and files. For instance, Musik_MAD has an application domain

  Proxy Contexts and Bindings For the web proxy VM, we create the alias ctxProxy for the application domain App_Proxy. Then, we can simply create a context for the binary source code (ctxBinaryWeb) as being the Data element BinaryExecutable in ctxProxy. § ¤These abstract contexts can be associated with "real" component of the system. This association is called binding. For instance, ctxConfigWeb represents two real files namely /etc/httpd/conf/httpd.conf and /etc/httpd/conf.d/ssl.conf.

	¦	¥
	Listing 5.1: Ikusi Specific Attributes
	# context ctxProxy = { AirportContentManager . Proxy . App_Proxy } ;
	# context ctxBinaryWeb = ctxProxy :( Data =" BinaryExecutable ") ;
	# context ctxConfigWeb = ctxProxy :( Data =" Config ") ; ¦	¥
	Listing 5.2: Proxy Contexts Excerpt
	§	¤
	" / usr / sbin / httpd " ctxBinaryWeb
	" / etc / httpd / conf / httpd . conf " ctxConfigWeb
	" / etc / httpd / conf . d / ssl . conf " ctxConfigWeb ¦	¥
	Listing 5.3: Proxy Bindings Excerpt

  Listing 5.4: Musik Contexts ExcerptThe following listing contains the corresponding bindings. A binding can be expressed as a regular expression. For instance, "/opt/musik(/.*)?" designates the directory /opt/musik and all files or subdirectories inside. § ¤ Mysql Contexts and Bindings For Mysql VM, we proceed exactly as before by defining two aliases ctxAodbDB and ctxAodb for the two application domains respectively the database and the interface.

	" / opt / musik (/.*) ? "	ctxFileMusik
	" / opt / musik / properties (/.*) ? " ctxConfigMusik
	" / opt / musik / musik . lic " ctxConfigMusik
	" / opt / musik / rsc (/.*) ? " ctxConfigMusik
	" / opt / musik / log (/.*) ? "	ctxLogMusik
	" / opt / musik / webapps / musik . war " ctxBinaryMusik
	" / opt / apache -.*/ conf / Catalina / localhost (/.*) ? " ctxConfigMusik
	" / opt / apache -.*(/.*) ? " ctxFileMusik
	" / opt / apache -.*/ bin (/.*) ? " ctxBinaryMusik
	" / opt / apache -.*/ lib (/.*) ? " ctxBinaryMusik
	" / opt / apache -.*/ webapps /*. war " ctxBinaryMusik
	" / opt / apache -.*/ conf (/.*) ? " ctxConfigMusik
	" / opt / apache -.*/ log (/.*) ? " ctxLogMusik
	" / opt / devmconn (/.*) ? "	ctxFileMusik
	" / opt / devmconn / bin (/.*) ? " ctxBinaryMusik
	" / opt / devmconn / lib (/.*) ? " ctxBinaryMusik
	" / opt / devmconn / log (/.*) ? " ctxLogMusik
	" / opt / devmconn / conf (/.*) ? " ctxConfigMusik
	" / opt / devmconn / properties (/.*) ? " ctxConfigMusik
	" / opt / ffmpeg (/.*) ? "	ctxFileMusik
	" / opt / ffmpeg / ffmpeg "	ctxBinaryMusik
	" / opt / jre .*(/.*) ? "	ctxFileMusik
	" / opt / jre .*/ bin (/.*) ? " ctxBinaryMusik
	" / opt / jre .*/ lib (/.*) ? " ctxBinaryMusik
	" / etc / rc \. d / init \. d / activemq "	ctxBinaryMusik
	" / etc / rc \. d / init \. d / tomcat "	ctxBinaryMusik
	" / etc / rc \. d / init \. d / devmconn "	ctxBinaryMusik
	" / opt / jre1 .7.0 _60 / bin / java " ctxServiceMusik ¦	¥
	Listing 5.5: Musik Bindings Excerpt

¦ ¥

Table 5 .

 5 .2. We use indiscrim-2: Correspondence between Quality Levels and Grades inately the quality level of grade i.e., Isolation({AirportContentManager}, MEDIUM) and Isolation({AirportContentManager}, 40) are the same property.

	Quality Level Grade
	Low	20
	Medium	40
	High	60
	Very High	100

  Listing 5.11: Ikusi Implit Isolation PropertyThe three other properties secure entities within VMs and thus splitting them is not necessary. For the sake of simplicity, we shorten AirportContentManager.Entity into Entity and, as grades are preserved through split procedures, each one of the following Isolation properties has implicitly the grade Medium.First, Algorithm 4.1 (Page 80) extends our implicit Isolation property into the two following explicit properties: § ¤ Except for our Isolation properties, the three others (i.e., Authentication, Confidentiality and Integrity) may be mapped to a guest-level security agent. In our model, the Proxy and Musik_MAD VMs have the following capabilities:

	# property IsolationVNet ( { Musik_EAS } ,{ Intranet } ) ;
	# property IsolationVM ( { Musik_EAS } ,{ Proxy , Musik_MAD , Mysql } ) ;
	# property IsolationVNet ( { Intranet } ) ;
	# property IsolationVM ( { Intranet } ,{ Proxy , Musik_MAD , Mysql ,
		Musik_EAS } ) ;
	# property IsolationVNet ( { Proxy } ,{ Public , Intranet } ) ;
	§ # property IsolationVM ( { Proxy } ,{ Musik_MAD , Mysql , Musik_EAS } ) ; ¦ ¦ # property Isolation ( { AirportContentManager } , MEDIUM ) ; Listing 5.14: Ikusi Typed Isolation Properties	¥ ¤ ¥
	5.3.2 VM Security Solving
	# property Isolation ( { Musik_MAD , Mysql , Musik_EAS , Intranet } ,{ Proxy } ) ; Proxy:
	# property Isolation ( { Proxy } ,{ Public , Musik_MAD , Mysql , Musik_EAS , Authentication(Client, Service, Role:Airport)
		Intranet } ) ; Confidentiality(Service, Client)
		Confidentiality(Data, Client)
	Musik_MAD:
		Confidentiality(Data, Service)
		Integrity(Data, Service)
	Then, Algorithm 4.2 (Page 81) transforms our global explicit properties into local
	properties i.e., one property per secured entity: §	¤
	# property Isolation ( { Musik_MAD } ,{ Proxy , Mysql , Musik_EAS , Intranet
	} ) ;
	# property Isolation ( { Mysql } ,{ Musik_MAD , Proxy , Musik_EAS , Intranet
	} ) ;
	# property Isolation ( { Musik_EAS } ,{ Musik_MAD , Proxy , Mysql , Intranet
	} ) ;
	# property Isolation ( { Intranet } ,{ Musik_MAD , Proxy , Mysql , Musik_EAS
	} ) ;
	# property Isolation ( { Proxy } ,{ Musik_MAD , Mysql , Musik_EAS , Public ,
	¦	Intranet } ) ;	¥
		Listing 5.13: Ikusi Singleton Explicit Isolation Properties
	Finally, Algorithm 4.3 (Page 82) split the previous local properties into typed proper-
	ties: §		¤
	# property IsolationVNet ( { Musik_MAD } ,{ Intranet } ) ;
	# property IsolationVM ( { Musik_MAD } ,{ Proxy , Mysql , Musik_EAS } ) ;
	# property IsolationVNet ( { Mysql } ,{ Intranet } ) ;
	# property IsolationVM ( { Mysql } ,{ Proxy , Musik_MAD , Musik_EAS } ) ;

¦ ¥

Listing 5.12: Ikusi Explicit Isolation Properties

The first explicit property states that Proxy is authorized to exchange information only with Musik_MAD, Mysql, Musik_EAS and Intranet. The second states that any VMs or VNets (in this model) are authorized to exchange information with Proxy.

http://www.infosecbuddy.com/download-cloud-security-report/

http://opensource.com/business/14/7/docker-security-selinux

http://www.ikusi.com/en/fids-musik-public-information-system-advertising-content-manager

http://www.eclipse.org/

https://www.openstack.org/

SOAP is a protocol based on XML for exchanging structured information.

A VM image is a virtual copy of a physical hard disk drive. It contains complete contents and data structure of a hard disk.

An instance is a running VM obtained by executing a VM image.

https://www.oasis-open.org/committees/tosca/

http://www.open-mpi.org/projects/hwloc/

http://www.netfilter.org/

The arity of a symbol is the number of "parameters" it takes

The API for managing the virtualization layer on Linux: http://libvirt.org/

Availability and Fault-tolerance In this Thesis, we have deliberately ignored the Availability property of the CIA triad as it comes under the concept of fault-tolerance. A denial of service is a common attack which violates the Availability but neither the Confidentiality nor the Integrity. Yet, it is a threat any security administrator must cope with. In our opinion, security and fault-tolerance should be more integrated. Indeed, a byzantine fault (in the fault-tolerance domain) can be seen as a malicious user. Therefore, the study of byzantines may help designed more robust security systems.

Acces Control

IF-PLTL a read b b ą a a write b a ą b no-read-up Gpp@h P Highqp@l P Lowq ph ą lqq no-write-down confidentiality(S, A) p@x P Sqp@yqpx ą yq Ñ py P S ^y P Aq integrity(S, A) p@x P Sqp@yqpx ă yq Ñ py P S ^y P Aq Figure 4.10 depicts the composition phase of our NUMA algorithm with 3 sequentially instantiated VMs. First, vm 1 is allocated onto N uma 1 (1 Gb required for 2 Gb available). Then, vm 2 requires 3.5 Gb and we consider N uma 2 and N uma 3 to be chosen. As a result, a ComposedNUMA N uma 2,3 is created with a total of 4 Gb and 0.5 Gb available after the instantiation of vm 2 . At this step, there is 3.5 Gb of memory available spread between N uma 1 (1 Gb), N uma 2,3 (0.5 Gb) and N uma 4 (2 Gb). Finally, vm 3 which requires 3.5 Gb is instantiated. A ComposedNUMA, N uma 1,2,3,4 is created for a total of 8 Gb, 3.5 Gb free before the instantiation of vm 3 and none after. Despite not having any VM referencing it, N uma 2,3 is not removed as it still has a parent (N uma 1,2,3,4 ). But when vm 3 is terminated, N uma 1,2,3,4 is neither referenced by any VM nor it has any parent, leading to its removal. The same applies to N uma 2,3 after removing N uma 1,2,3,4 . At this step, N uma 1 , N uma 2 , N uma 3 , N uma 4 can be directly allocated again. The termination of vm 1 returns the physical machine to its initial state.

Allocation Algorithm Now that we have given our composition and decomposition procedure for NUMAs, we detail our VM allocation and deallocation procedure. airport, all useful data are stored in a common Database (i.e., tier 3) framework called AODB (Airport Operational Database). In the rest of this chapter, we present the Sam4C model of this Advertising Content Manager use case including a meaningful excerpt of the security policy. Then, we detail the successive steps of our approach: preprocessing, deployment and the enforcement of the required security properties using both the placement and the configuration of mechanisms.

Modeling

In this section, we present the modelization of the airport use case using the Sam4C Modeling tool. A screenshot of the use case model in Sam4C is depicted Figure 5.2. The left part contains the virtualized application model with the tool palette to graphically manipule the model. The right part contains the security policy with the definition of attributes, contexts and properties. The circled upper button triggers the deployment of the model by sending it to Sam4C Scheduler using its IP address.

In this section, we first detail the virtualized application model and then discuss few security properties.

Virtualized Application Model

The Sam4C Model of the Advertising Content Manager service is depicted Figure 5.3. It is worth noting that the modelization has been done by Ikusi with limited help from our side i.e., Sam4C seems to be easy to use. Two airports are considered namely MAD (for Madrid) and EAS (for San Sebastian). A Security Domain AirportContentManager contains the 3-tier application which is composed of 4 VMs: As depicted in Figure 5.4, inially i.e., before deploying the Ikusi use case, Taurus1 node already executes the VM Other on core c1 using 8 GB of memory in N uma0 without enforcing any particular security properties.