Walid Benghabrit
email: walid.benghabrit@imt-atlantique.fr

Hervé Grall
email: herve.grall@imt-atlantique.fr

Jean-Claude Royer

Anderson Santana De Oliveira
email: anderson.santana.de.oliveira@sap.com

Jean-Claude Royer

J-C Royer

A S De Oliveira

The Abstract Accountability Language: its Syntax, Semantics and Tools

Keywords: Accountability, Formal specification, First-order temporal logic, Semantics, Tool support, Verification

come   L'archive ouverte pluridisciplinaire

Introduction

Demonstrating accountability is the main goal for organizations that need to comply with corporate policies and regulations. This involves defining control objectives and controls that span across organizational units, outsourced service providers, roles, and event technological infrastructures. The concept of accountability draws the central elements for many regulations, let us mention the European Union's General Data Protection Regulation (EU GDPR) [START_REF] Regulation | European Parliament and of the Council of 27[END_REF], the Health Insurance Portability and Accountability Act (HIPAA) [START_REF]104th Congress Public Law 191[END_REF] and the Corporate and Auditing Accountability and Responsibility Act (also known as SOx) [3], to cite a few. Given its importance, it is paramount to understand under which conditions accountability can be met. In the digital era, the question involves controlling usage of information flows across organizational boundaries. Defining roles and accountability for the multiple actors handling data is not straightforward. The very first step is modelling organizational processes, their agents, and the interplay between the obligations they must execute in the processes, the authorizations, and the remediation actions in case of failures. Although the topic of accountability for distributed critical systems has gained importance over the years, there are few frameworks to help analyzing whether suitable properties apply to a given context today. Reviewing the related work in formal accountability we observe a lack of concrete languages and tools to specify and experiment with accountability policies.

We are interested in concrete approaches for reasoning about accountability for a diverse set of applications (cloud computing, mobile, etc.) where models are defined in a formal language with precise semantics that can be verified by tools, such as theorem provers, SAT solvers and model checkers. We focus on accountability policies for computer based systems, where events can be unambiguously observed and asserted. We consider out of the scope of our work typically human moral dilemmas, or determining whether force majeure conditions were met that justify not fulfilling an obligation (mostly external to the system in question), or yet determining if an excuse is valid. These questions require human judgment, and very frequently some sort of human mediator. In this work we explore the spectrum of automatable, reproducible and enforceable accountability rules.

In previous work [START_REF] Benghabrit | Accountability for Abstract Component Design[END_REF][START_REF] Benghabrit | volume 512 of Communications in Computer and Information Science, chapter From Regulatory Obligations to Enforceable Accountability Policies in the Cloud[END_REF][START_REF] Benghabrit | Abstract accountability language: Translation, compliance and application[END_REF][START_REF] Royer | Aal and static conflict detection in policy[END_REF] we introduced the Abstract Accountability Language (AAL) which is a declarative policy specification language based in First-Order and linear Temporal Logic, featuring constructs supporting role definitions, delegations, obligations, and usage control rules. Besides setting its syntax and semantics, in these papers we showed how AAL is used to check compliance with regulations, how to find inconsistencies in policies using static analysis, and a practical verification approach supported by a state of the art automatic prover.

The current paper brings new contributions to some important aspects for accountability management: expressiveness and tool support. We provide an expressive language covering the three dimensions of [START_REF] Schedler | Self-Restraining State: Power and Accountability in New Democracies, chapter Conceptualiazing Accountability[END_REF]: information, justification and punishment. Information is achieved via formal declarative statements comprising various privacy features, temporal modalities, audit and rectification aspects. Justifications are realized thanks to our verification principles which allow checking for contract compliance and to query contracts using property verification. Punishment can be made explicit in the accountability contract and enforced thanks to a monitoring mechanism. Furthermore, we introduce policy templates, generic specifications useful in determining the expected behaviour for an abstract policy. This mechanism is very useful, since often accountability is challenged in outsourcing chains. The paper also overviews the AccLab tool support, our dedicated application allowing a component based description, the edition, verification and monitoring of accountability policies.

The remainder of the paper is structured as follows. Section 2 presents the core AAL grammar, usage examples to express accountability and the translational semantics. The next section is devoted to verification principles covering consistency, compliance, and property verification. Section 4 describes our AccLab tool support. We present the state of the art in computer science and accountability in Section 5 focusing on formal models and verification. The reader being up on accountability may skip this section and directly go to Section 6 which compares AAL and AccLab with related work and discuss some limits. A last section summarizes our findings and describes future perspectives.

Abstract Accountability Language

This section introduces our AAL language, its semantics and accountability expressiveness through various examples. In our approach, we consider that an accountability clause should express three things: a usage, an audit and a rectification. The usage expression describes access control, obligations, privacy concerns, usage controls, and more generally an expected behavior. The audit and rectification expressions are similar to usage expression but dedicated to auditing, punishment and remediation. The audit expression defines a specific audit event which triggers the auditing steps. The rectification expression denotes actions that are done in case of usage violations. For instance, to punish the guilty party and to compensate the victim agent. We follow [START_REF] Schedler | Self-Restraining State: Power and Accountability in New Democracies, chapter Conceptualiazing Accountability[END_REF][START_REF] Mulgan | accountability': An ever-expanding concept[END_REF] which argue that punishments and sanctions are parts of accountability.

AAL Grammar

We present in Listing 1 the core AAL syntax, more details and extensions can be found in [START_REF] Benghabrit | Accountability Laboratory[END_REF]. An AAL program declares a set of types, agents, data and services which define the context. Usage expressions denote access control, privacy, or other actions and properties relevant to this context. The usage expression, ActionExp , is the most general construction but we also provide a dedicated accountability clause (the CLAUSE construction) and templates to assist users in defining accountability. The main AAL notion is an action or a service call represented as a message sender.action[receiver](parameters). Authorizations are denoted by the PERMIT and DENY keywords prefixing an action or an expression. The language provides Boolean operators, first-order quantifiers and linear temporal operators. This is a simplified grammar and it has syntactic constraints about typechecking ensuring the consistency of the provided and data useful for data privacy expressions. The usage expression states a permission and a prohibition related to some purposes for the KardioMon agent. It expresses that in any state for any D:Data if the owner is Kim and the purpose is research or statistics then KardioMon is allowed to process D. Else KardioMon is denied to process the data from Kim. This also defines a simple behavioral obligation for KardioMon: In any state each data processing should be followed by a notification to a data controller. We consider internal actions (like process) and binary actions (like notify) which represent a communication from a client (the required side) to a server (the provided side). The prefix @ declares a predicate, and an action without receiver as in KardioMon.process(D, purpose) is an internal action. In [START_REF] Royer | Aal and static conflict detection in policy[END_REF] we show that AAL subsumes XACML, the de facto standard for security language, on several points, namely its pure logical semantics and expressiveness regarding privacy concerns and data transfer. The language supports a type system with Boolean operators, hierarchies for actions, users, resources and roles. AAL allows discrete linear time and duration. It enables complex dependencies between authorizations and obligations, thus making possible the writing of various protocols. In addition to covering many classic characteristics needed for security it provides new features for expressing accountability policies.

Accountability Expressiveness

As previously explained an accountability clause (CLAUSE) is compound from three expressions which are usage, audit and rectification (see Listing 3). Audit and rectification are optional expressions with the same syntax as usage expressions. The usage expression defines two permissions for the KardioMon agent and a simple send action. The audit is triggered as soon as the data subject alert the auditor. The rectification is a simple punishment with compensation to the data subject. The informal meaning of a clause is: Always the usage is satisfied or if violated and if an audit occurs a rectification will be done.

This meaning addresses security but also unanticipated behaviors violating the usage expression. This view is compliant with [START_REF] Etalle | A posteriori compliance control[END_REF] and governs both preventive security and deterrence. It is simpler to write for end users and also it provides several intuitive properties we will see later.

Nevertheless, usage phrases are expressive and thanks to the uninterpreted (abstract) use of actions and predicates we are able to define many more controls (see Listing 4). Here, we write a more complex accountability example using only a unique usage expression with more precise descriptions of violations and rectifications. The usage defines an authorization to process and a prohibition to send data from Kim. If Kim does not give consent to processing then, in case KardioMon processes a data, he will be denied to process data forever. Finally, if the data processor sends a Kim data he is punished and Kim is compensated. Following this example many variations can be considered for the audit time, for the data to be audited and the auditing mechanism. A punishment example is described in Listing 5, where Kim.do() is a denied action. The punishment has three cumulative steps, the two first oblige Kim to pay in case of misconduct. The last step prohibits login for Kim in case of a third violation. In Listing 6 we have another example denoting permissions, logging in case of modify and send actions, audit, punishment and compensation. The first part of the example shows a generalized authorization. Alice has the permission to modify and send any data, however she is denied to modify a data and then send it to Bob. Such a prohibition is an information which can be checked for consistency but also it can be violated and we should detect and rectify it. The second part of the example illustrates an explicit logging and audit in case of the violation. An external observer is assumed to log these critical actions and to detect the violations. Listing 7 makes explicit the violation expression, EXISTS S:Data Bob.send[Alice](S), which is assumed to be disjoint from the usage expression. It also extends the accountability clause in specifying a link between a judgment identifying culprits and victims, and the rectification. The behavior of this example is: always the usage is satisfied or else it is satisfied until a violation occurs and in case of audit there is punishment of culprits and compensation of victims. )))))

We limit the complexity of the sub-expressions for readability, which is a critical problem. To mitigate it we propose to use templates in Section 2.6.

Semantics

In this subsection we sketch the translation process from AAL to FOTL, giving semantics to it. Additional details can be found in [START_REF] Benghabrit | Abstract accountability language: Translation, compliance and application[END_REF]. Here, we concentrate on the main principles and two extensions: general authorizations and templates.

There are two cases for the translation:

1. The first case is to translate each usage expression in FOTL, and this applies to a clause without its optional audit and rectification expressions. 2. The second case is relevant for CLAUSE with its two optional sub-expressions. In this case we built a new temporal sentence with the three expressions, then an interpretation of this sentence is made. More generally, this is the process used by the template construction.

First-Order Temporal Logic

FOTL extends both first-order logic (allowing predicates and quantifiers) and propositional linear temporal logic (allowing temporal modalities). FOTL formulas are built from variables V , constants C and predicates with a fixed arity P i . If P i is a predicate symbol and (e j ) are variables or constants then P i (e j ) is an atom (A). In the grammar of Listing 8 one can recognize Boolean operators (not, and, or, =>), temporal operators (next, until, always, sometime) and quantifiers (forall, exists). Note that we use lower case letters for these operators to make more clear the distinction with AAL.

Listing 8 FOTL grammar

F ::= C + A + (not F) + (F and F) + (F or F) + (F => F) + (forall V F) + (exists V F) + (always F) + (sometime F) + (next F) + (F until F)
The semantics of FOTL is based on models which are infinite sequences, indexed by naturals, of first order structures (a non empty domain and an interpretation of the atomic predicates). Such a model will be called a trace as usual in linear temporal logic.

Expression Translation

The function [_]: AAL → FOTL represents the translation from an AAL expression to a FOTL one. Types, predicates, actions, attributes are all translated into predicates. Boolean operators are convenient to express logical relations like type union or disjunction. Agents and data instances are defined as constants. The translation of these declarations leads to a logical context prefixed with an always modality. Interpretation of Boolean, quantifiers and temporal operators are straightforward in FOTL. The PERMIT and DENY modalities generate new opposite events and a new context property which states that processing an action implies it is permitted. The extended grammar supports few additional facilities to express time in actions, limited equality and a past temporal operators. We also provide translations for these features. This translation needs some care in managing existential and universal quantifiers, and in adding the logical sentences capturing equality, dates, and authorizations.

Accountability Clause Interpretation

The accountability clause with its three expressions is an ease to write accountability and its translation is more elaborated. Our accountability clause is defined in Listing 9, AE the audit expression is assumed to generate atomic audit events. The informal clause meaning is as follows: audit is running and at each instant either usage is satisfied or it is violated and then if an audit event occurs there will be rectification.

Listing 9 Accountability clause interpretation [ALWAYS AE AND ALWAYS (UE OR ((NOT UE) AND (ALWAYS audit => RE)))]

Listing 9 provides our default interpretation for accountability. As soon as a violation of the usage is done and if an audit event occurs later then rectification applies. Figure 1 illustrates the linear traces with a violation and rectification. Let UE a usage expression, a violation can be formally defined as an expression verifying (VE => NOT UE). Note that there is no hypothesis on RE and it could allow one rectification only, one each time, only one in the future or stands forever in the future. However, this clause is restricted because we dot not make explicit logging or auditing actions and parameter passing between the three parts is limited to constants.

General Authorizations

We define a general means to describe complex permissions, not only covering the case of atomic expressions as in many previous work. There are many cases, in protocols, for instance where we want to specify some permissions for individual actions but in the same time to prohibit few chaining of these actions. For instance, in our Listing 6 we permit modify and send actions, but we do not want to chain a data modification and a send action. In our interpretation we have a sub-world for the authorizations and another one for the "real" actions. The distinction is made by generating new events associated to each permitted sequences of actions. The connection between both worlds is done by generating context rules like always (expression => permit(expression)).

The function permit copies the expression and uniquely

UE UE UE NOT UE audit RE audit
Fig. 1 A trace with a violation and rectification tagged each actions, thus putting it in the world of permissions. We extend our initial semantics in the following manner: i) DENY is rewritten as NOT PERMIT, ii) for the construction PERMIT expression, without nested authorization, the expression is copied thanks to the function permit, iii) we add the clauses linking an expression with its permission, and iv) we enrich the context with rules to link permissions for complex expressions with action permissions. The translation of expressions [START_REF] Regulation | European Parliament and of the Council of 27[END_REF] and [START_REF]104th Congress Public Law 191[END_REF] of Listing 6 appears in Listing 10 (but without the data type translations). This example captures that chaining modify and send requires the permission to do it but there is a conflict with the negative permission. However it does not prohibit to do the modify or send actions as far it concerns distinct data. Another useful feature for the user is the ability to set different interpretation modes. For instance, the MODE: STRICT generates (always (action <=> permit (action))) for the case at hand, it provides a context where, in addition to the default mode, if an action is permitted its negation cannot be performed. We also add MODE: => which allows to relate permissions for complex usage expressions with action permissions as in the above example. The default mode corresponds to <=> denoting that a permission for a complex expression is equivalent to the expression of its atomic permissions. One remaining point is to find an efficient implementation of the general authorization feature. We are investigating a solution based on a unique normal forms for FOTL expressions. Dependencies between formal parameters are permitted if they are not circular. Furthermore, we will show in Section 3.3 that this instantiation can be automatically verified. As the previous accountability clause, this template enjoys few properties described in Listing 17 and 18.

We expect to enrich this initial set of templates, the challenges are: i) to get a catalogue of accountability practices with a precise while informal description and ii) to formalize them in AAL and to prove their expected properties.

Verification and Tool Principles

The goal of this section is to introduce the principles behind the AccLab tool support. We focus here on software engineering activities related to policy verification. The objectives of verification are various, comprising: To prove some expected properties, to detect undesirable situations, or to eliminate redundancies. A redundancy is defined, in our context, as a policy P for a policy set R, satisfying R => P is valid. It can be checked using the prover back-end, but it is not a critical problem since it does not entail the system logic. Furthermore, we claim that it is practically uncommon in complex accountability policies with linear time and quantifiers. Thus we consider that the conflict detection question is really more critical, and formal policy compliance is an important requirement in regulations. From the related papers we can classify the properties of interest as internal properties or specific properties. Internal properties are related to the system and independent from the business domain like consistency, completeness, simplification, conciseness, and so on. Specific properties are depending on the business domain, several classes are relevant in our context. We consider specific properties related to privacy or security concerns but also some proper accountability properties.

To perform verification we rely on the temporal resolution procedure presented in [START_REF] Ludwig | Implementing a fair monodic temporal logic prover[END_REF]. This procedure has been implemented in a theorem prover (TSPASS [START_REF] Ludwig | Tspass[END_REF]), which we have integrated into our specification and verification environment, the AccLab tool. The decision procedure behind the prover addresses the so-called monodic fragment [START_REF] Hodkinson | Decidable fragment of first-order temporal logics[END_REF][START_REF] Degtyarev | Monodic temporal resolution[END_REF]. The monodic condition states that any temporal sub-formula has, at most, one free variable. This is a constraint which is satisfied in our examples. It allows to mix, in a non trivial way, linear temporal logic and first-order logic, thus providing expressiveness. Regarding efficiency, the temporal resolution behind TSPASS has a non elementary complexity. Nevertheless, there are three papers which demonstrate the ability of this tool to solve real examples [START_REF] Fernández-Gago | First-order temporal verification in practice[END_REF][START_REF] Ludwig | Implementing a fair monodic temporal logic prover[END_REF][START_REF] Schuppan | Evaluating LTL satisfiability solvers[END_REF]. The latter shows in fact that TSPASS is competitive with model-checkers and SAT solvers. In addition [START_REF] Benghabrit | Checking Accountability with a Prover[END_REF][START_REF] Benghabrit | Abstract accountability language: Translation, compliance and application[END_REF] study several non trivial examples with temporal operators and unbounded data with acceptable performances. In the rest we focus on three activities: conflict management, checking compliance and proving accountability properties.

Conflict Management

Conflict management consists of three activities: detection, localization (that is, finding the conflicting rules, or more generally finding the unsatisfiable core in the policy set) and conflict resolution, this is a key issue. There are various techniques, the most common principle is to check for pairs of incompatible rules. But this is not generally a correct approach since it can forget some conflicts. A more general way is to look for conflicts between any number of rules. It is still weak, inefficient and enforces a too strict writing style. In a context where we do not have rule, like with AAL, the correct approach is to rely on satisfiability or logical consistency and to use a solver, prover or modelchecker. This is the approach we use with AAL, the TSPASS prover allows us to check for the satisfiability of a set of policies. However, the drawback is that localization becomes less obvious than looking for pair of rules. But we reused the masking principle suggested in [START_REF] Viktor Schuppan | Towards a notion of unsatisfiable and unrealizable cores for LTL[END_REF], which is intuitive and simple to implement. We consider that resolution is a manual activity in charge of the specifier.

Writing inconsistent specifications is rather common, one example is our Listing 4 where we can find a problem as soon we add the fact that Kim owns some private data. Indeed there is a conflict between the permission and the prohibition to process by KardioMon.

Listing 15 shows the result provided by our tool and the solution is to remove the permission for KardioMon to always process.

Policy Compliance

In accountability contracts, compliance covers different meanings. A common idea, as in [START_REF] Khandelwal | Analyzing the AIR language: A semantic web (production) rule language[END_REF][START_REF] Butin | Strong Accountability: Beyond Vague Promises[END_REF], is to check if a given real situation or execution trace is compliant or according to the contract. This is often the basis of the audit and detection mechanisms. We called it testing compliance and while this kind of compliance can be tested with our tool we are rather concerned with contract compliance. The goal of the contract compliance is to ensure that the provider's contractual terms satisfy or ensure the client's requirements. Thus it is much more complex than testing compliance since it is about proving that a policy is "stronger" than another one. In propositional logic it could be as simple as the implication of Provided => Required. In the FOTL framework the semantics is linear trace based and the previous intuition is also correct in the sense that the traces satisfying the provider clauses are included in those satisfying the client expectations. More sophisticated semantics exist, but this one provides an intuitive and simple interpretation which is suitable for end-users. Thus compliance between two expressions relies on the validity of the logical implication, that is the validity of R => (Provided => Required). For instance, Listing 16 presents a provider policy which ensures the clause in Listing 3. While this example seems rather simple, a tool is convenient in establishing the compliance, here in less than one second.

The CLAUSE construction of Listing 11 enjoys an interesting property: The contract compliance between two accountability clauses can be established with more natural (monotonic/covariant) conditions (see Listing 17). Where AE, UE, RE, are respectively, the audit, usage, and rectification expressions and p (respectively r ) is the server (or provided) side (respectively the client/required side). We also demonstrate that this provides a more efficient way to check for compliance by splitting the formula in three shorter verification parts. For instance, in [START_REF] Benghabrit | Abstract accountability language: Translation, compliance and application[END_REF] we show an example of accountability compliance, with more than 1200 identifiers, which does not finish before 10000s with the global compliance formula. Using the above criterion it succeeds in less than 1400s. The use of additional heuristics can reduce the proving time down to 4s.

Specific Property Verification

Verification of properties needs the manual translation of the property into AAL and then the use of the prover. As previously explained the principle is to check the validity of R => Property. The prover, with the monodic restriction, enables us to automatically prove data properties as well as safety and liveness properties. In the following, we will give various examples of properties but related to specific privacy or accountability concerns.

We can prove dependent conflict properties as in [START_REF] Montangero | Logic-based conflict detection for distributed policies[END_REF][START_REF] Wu | An extensible intra access control policy conflict detection algorithm[END_REF], for example: But our conflict detection based on logical consistency is more general and safer. Other properties are related to reachability. For instance [START_REF] Scott | Efficient policy analysis for administrative role based access control[END_REF] in the context of administrative RBAC and with specific algorithms, studies how an initial system can reach a specific state. Defining the initial system and the expected final state this problem can be solved using property verification. Time, discrete or with dates, is useful in expressing the state change progression. A related example is the verification of purpose: does an agent performing an action is processing it according to the required purpose? There are several dedicated articles ( [START_REF] Sun | Privacy preserving access control policy and algorithms for conflicting problems[END_REF][START_REF] Carl Tschantz | Purpose restrictions on information use[END_REF]) on this subject but none with a property verification view. Since doing an action is constrained by its permission in the generated logical context, a simple schema for this property in AAL is ALWAYS FORALL D:Data PERMIT KardioMon.processing(D, purpose).

Controlling data disclosure is the main concern of data privacy. In this case we are interested in situations where a piece of data reaches an authorized or non authorized agent. This can also be viewed as a reachability case but with emphasis on agent locations, with or without specific behavior for the agents. In [START_REF] Benghabrit | Abstract accountability language: Translation, compliance and application[END_REF] we show a related verification in the context of an healthcare system.

We also automatically prove several original accountability related properties. It is possible to automatically prove the natural criterion in Listing 17. We also prove three other properties which appear in Listing 18. The first states that it exists a simple and sufficient audit condition to catch all the violations. The second is an equivalent formulation of the accountability clause interpretation of Listing 9. This clause says that either, in any state, the usages are correct or it is correct until a violation occurs then rectification happens in case of an audit. It is common that contracts are presented as a conjunction of policies. The third property expresses that such a complex accountability contract can be split in several sub-contracts and its verification implies the verification of its sub-contracts. The equivalence is possible for property 3) if the usage expressions are equivalent. These properties are rather intuitive or desirable but also improve efficiency in verification.

Other examples of properties and proofs are: i) a compliance criterion for the extended accountability template of Listing 13, however the compliance is covariant on all the parameters but contravariant on the audit expression, ii) the equivalent formulation for the ex-tended template with the condition that ALWAYS (VE => NOT UE), and iii) the decomposition property is also valid for the extended template in case of conjunction of policies.

A last usage of verification is relevant to the extended accountability template (from Listings 13 and 14) and its instantiation (Listing 7). Listing 19 shows the equivalence between both expressions and it can be proved in about two seconds. More precisely, with the set of expressions in Listing 14, we can prove that the example in Listing 7 is an instantiation of the extended template of Listing 13. This listing has three parts: i) the parameter instantiation and the conditions of the template, ii) the instantiated example coming from Listing 7, and iii) the template as in Listing 13. This expression is difficult to read but it is only for specialists of formal specifications which are in charge of defining the templates with their conditions and properties. The listing above illustrates the steps performed by the specialist to validate a new template. It starts from one or more concrete examples of accountability policy, it manually write the conditions and the template, next the specifier tries to automatically prove the expected instantiation.

plate and its sub-expressions. Assistance could be improved by a dedicated graphic user interface. However, we claim that templates provide assistance specifically in case of complex regulations with several sub-contracts. Each sub-contracting has to formalize its proper part of the contract, maybe still using some templates. Afterwards the primary data processor should check the conditions of the template and then automatically apply it to the sub-contracts.

The AccLab Tool Support

In this section we sketch the main features of the Ac-cLab tool support which represents a step in defining an end to end accountability framework from specification to implementation. AccLab is compound from a set of tools which are: The component editor, the AAL editor and its verifications, and the monitoring tools. The last release of AccLab is version 2.1 which was released on November 23, 2016 on GitHub (https: //github.com/hkff/AccLab) under GPL3 license. The AccLab IDE is a web interface that provides a component diagram editor and tools to work with the AAL language. The back-end is written in Python3 and the front-end in JavaScript based on dockspawn (http: //www.dockspawn.com) which is a web based dock layout engine released under MIT license. For verification purposes AccLab is interacting with the TSPASS tool. The implementation is still in progress we will give an overview of its main current features.

System Specification

We consider accountability by design that is going from specification to implementation of accountability. The starting point of the accountability process is a component diagram in the UML style which describes the application architecture. The method was described in [START_REF] Benghabrit | Accountability for Abstract Component Design[END_REF] and allows the user to define in a graphic way the different agents and their required, provided and internal services. The diagram is enriched with textual annotations for services types and with accountability clauses associated to services and agents. To manage more easily the AAL language a dedicated editor has been implemented. This editor is directed by the syntax and highlights the language keywords. There are syntactic checks but also semantic controls for type checking and consistency of the declared services.

Verification Tools

A panel in the editor arranges a set of tools providing assistance in writing by the use of dedicated templates, for instance generating type declarations, accountability clauses or specific privacy expressions. This panel also contains few verification tools mainly the conflict checking with localization and the compliance checking. Figure 2 shows the graphical interface of AccLab, the AAL editor and its tool panel. Both checking tools use Fig. 2 AccLab screenshot the connection with TSPASS and its satisfiability algorithm as explained in the previous section. This panel assists in generating macro calls which are useful in automating some complex tasks related to the translation to FOTL and the interaction with TSPASS.

Accountability in Action

One idea behind AccLab is to see accountability in action, one way to achieve that is to be able to run simulations. AccLab includes a simulation module that allows it to simulate agents in a system and to observe accountability in action. Each agent is wrapped in a reference monitor which acts as a proxy and intercepts all incoming and out-going messages of an agent. Reference monitors communicate with each other via a component that simulates the network. The agents are asynchronous and use asynchronous communications, and they exchange monitoring information when communicate with each others. The policy is monitored using an engine based on the rewriting technique [START_REF] Rosu | Rewriting-based techniques for runtime verification[END_REF][START_REF] Bauer | Runtime verification for ltl and tltl[END_REF][START_REF] Scheffel | Three-valued asynchronous distributed runtime verification[END_REF][START_REF] Bauer | The ins and outs of first-order runtime verification[END_REF] and the monitors use distributed monitoring techniques [START_REF] Sen | Efficient decentralized monitoring of safety in distributed systems[END_REF]. [START_REF] Sen | Efficient decentralized monitoring of safety in distributed systems[END_REF] proposes local monitoring for distributed systems but limited to past formulae only. We reuse and extend this work focusing on future formulae and we use knowledge vectors (extending vector clocks) to update local monitors knowledge. Sub-monitors are generated for each formula that describes non local actions in each agent. We extended the progression function to deal with knowledge vectors that are exchanged between agents during communications and containing the evaluation of sub-monitors.

Real Monitoring

We introduce the AccMon tool which implements the aforementioned principles, allowing for monitoring accountability policies in the context of real systems. The tool is build over the Django, an open-source web application framework in Python, relying on the modelview-controller pattern. AccMon allows to specify policies that are applicable to network traffic, web application code and other components via plug-ins. AccMon acts as a middleware in the Django framework. It intercepts and logs client's HTTP requests, server's requests processing and responses. On the web application side, the developer can configure the framework to intercept function/method calls and databases access. The properties to be monitored with the tool are defined in a variant of AAL with interpreted predicates. The tool receives log events via its RESTful API. AccMon can act as a daemon and interconnecting a variety of external tools.

In the following, we present a broad review of related works in Section 5. Experts in these areas will rather focus on Section 6, where we compare our work with similar initiatives in the field of computer science.

Formal Models for Accountability in Computer Science

Accountability is a complex and broad notion which has been discussed in several domains: economy, laws and regulations, ethics, privacy, education, public services, and much more. The term has recently evolved and gained much interest as analyzed in [START_REF] Mulgan | accountability': An ever-expanding concept[END_REF]. However, there is not a clear agreement on its characteristics [START_REF] Schedler | Self-Restraining State: Power and Accountability in New Democracies, chapter Conceptualiazing Accountability[END_REF] and how to make it computer understandable if possible. This is the main reason why we restrict our study to accountability in computer science. The notion of accountability crosscuts several domains of computer science: digital forensics, computer security, distributed systems in general (grid and cloud computing, the Internet and network applications) and natural language processing. The notion of accountability has been the subject of several surveys in computer science [START_REF] Daniel | Information accountability[END_REF][START_REF] Lin | Accountability computing for e-society[END_REF][START_REF] Xiao | A survey of accountability in computer networks and distributed systems[END_REF][START_REF]Managing Privacy through Accountability[END_REF]. We will here focus only on a set of papers related to computer science and accountability, focusing on formal models, specifications and verification. There are only few references in computer science which considers a general and interdisciplinary view of accountability, see [START_REF] Daniel | Information accountability[END_REF][START_REF] Le | Formal methods as a link between software code and legal rules[END_REF][START_REF] Pearson | An interdisciplinary approach to accountability for future internet service provision[END_REF]. Most of the papers, due to the complexity of the concept, only address some properties or specific mechanisms related to accountability. The preventive controls used by classical information technology security are not sufficient to achieve accountability. Accountability performs a posteriori control and it requires several mechanisms: information transparency, secure logging, checking misbehavior and responsibilities, then proceeding to penalties and compensation. There are already some proposals for frameworks integrating these aspects [START_REF] Pearson | An interdisciplinary approach to accountability for future internet service provision[END_REF][START_REF] Butin | Strong Accountability: Beyond Vague Promises[END_REF] and formal models or logic for accountability [START_REF] Cederquist | An audit logic for accountability[END_REF][START_REF] Jagadeesan | Towards a theory of accountability and audit[END_REF][START_REF] Kusters | Accountability: definition and relationship to verifiability[END_REF][START_REF] Feigenbaum | Towards a formal model of accountability[END_REF][START_REF] Feigenbaum | Open vs. closed systems for accountability[END_REF]. Recently Butin et al. advocate for strong accountability in [START_REF] Butin | Strong Accountability: Beyond Vague Promises[END_REF]. The authors put forward strong accountability as a set of precise legal obligations supported by an effective software tool set. They demonstrate that the state of the art in term of technology is sufficient to ensure the notion of accountability by design. In the rest of this section we summarize some formal work around accountability since it is more closely related to our current work. There are also several interesting applications of the notion of accountability in concrete domains. Among them [START_REF] Chun | Decentralized trust management and accountability in federated systems[END_REF][START_REF] Haeberlen | Accountable virtual machines[END_REF][START_REF] Sundareswaran | Ensuring distributed accountability for data sharing in the cloud[END_REF][START_REF] Ryan | Towards achieving accountability, auditability and trust in cloud computing[END_REF][START_REF] Pearson | Accountability in cloud service provision ecosystems[END_REF][START_REF] Datta | Privacy through Accountability: A Computer Science Perspective[END_REF]. These approaches are dedicated to specific applications and use techniques that are not fully relevant to our abstract and formal context. We group the references of interest in three coarse parts: logical models, theories, and formal verification aspects.

Logical Models

These are logical models often with delegation. In [START_REF] Crispo | Reasoning about Accountability within Delegation[END_REF] authors consider accountability transfer during right delegations. The basis of accountability is for a participant to prove a statement to a third party. This paper provides a rich logical model for communication protocols with authentication, a participant can formally prove some statements, is trusted on some statements or can exercise some rights. [START_REF] Corin | A Logic for Auditing Accountability in Decentralized Systems[END_REF] focuses on distributing digital assets while preserving some privacy properties. The authors define a formal model to express usage policies and to enforce them. This is a logical model with agent creation, exchanging and redistributing data and assuming that an authority observes evidences of these actions. The associated proof system is based on predicate logic enriched with inference rules for communication, data and policy creation and delegation. The context of [START_REF] Cederquist | An audit logic for accountability[END_REF] is data privacy in a distributed system. The formal model allows to define accountability policies as extensions of First-Order-Logic (FOL) with special constructions for data ownership and right delegation but without negation. A terminating proof system for accountability is defined and implemented in the Twelf prover. The paper from Etalle and Winsborough [START_REF] Etalle | A posteriori compliance control[END_REF] discusses the weaknesses of preventive security face to unanticipated situations occurring in collaborative environments. The authors argue that an approach based on deterrence is complementary and forms "a second line of defence". They define APPLE, a logical framework for a posteriori policy enforcement based on three critical components: logging, auditing, and accountability. The concept of sticky policy is used, it is a conjunction of few specific first-order predicates describing the owner and the permission to modify or distribute a document and to modify or refine a policy. An inference system can audit logs and proves that a user performed action in compliance with the sticky policy. A formal framework for privacy relying on accountability is proposed in [START_REF] Le | A Formal Privacy Management Framework[END_REF]. The author considers privacy in modern pervasive systems and specifically the disclosure of privacy information. The author defines the SIMPL privacy language allowing features related to data disclosure. The semantics of agents is based on traces on which a notion of compliance is defined. The model of computation uses the notion of sticky policy and two global properties. These properties express that if a value is in the space of an agent, either the owner directly sent it to the agent, or the sticky policy enabled this agent to receive this value.

Theories

These are references focusing on abstract properties of audit, accountability and agent behaviours. In [START_REF] Jagadeesan | Towards a theory of accountability and audit[END_REF] the authors state that the accountability approach to security lacks general foundations for models and programming. They propose a theoretical operational model for accountability in a distributed system with definitions of honest agent, auditor, and responsiveness. This allows them to discuss the power of the auditor and the constraints placed on agents and on the communication infrastructure. The model is based on point to point communications providing integrity and authenticity guarantees. The behavior of agents is expressed via process algebra and discrete time. They use a game-based method, linear temporal logic and model-checking to check accountability properties. This model explores the trade offs between the honest principals, the communication network, the audit protocol and proposes five abstract properties about agent guilty blamed by the auditor. In [START_REF] Kusters | Accountability: definition and relationship to verifiability[END_REF] new definitions for accountability and verifiability are proposed and shown to be connected together. They provide two interpretations: A symbolic one in the Dolev-Yao style and a computational one with a cryptographic model. The authors demonstrate the applicability of their approach analyzing several cryptographic protocols. The authors of [START_REF] Feigenbaum | Towards a formal model of accountability[END_REF] claim to provide a more general and more widely applicable definition of accountability. They explain that existing approaches have been mainly preventive which is inadequate since it is generally impossible to, a priori, differentiate an honest user from an attacker. A posteriori or corrective approach is being more suitable to accountability. They provide a formal model of accountability based on event traces and utility functions taking into account anonymous agents, automatic and mediated enforcement of accountability.

Formal Verification

The work discussed in this section is related to concrete approaches targeting verification means for specific domains. Note that [START_REF] Cederquist | An audit logic for accountability[END_REF] suggests a limited tool support. AIR [START_REF] Khandelwal | Analyzing the AIR language: A semantic web (production) rule language[END_REF] (Accountability in RDF) is a rulebased language for the semantic Web and supports rule nesting, and explanation of inferences. AIR supports a non-monotonic negation and rules ordering counts. The semantics is based on defining the translation of an AIR-program to a semantically equivalent stratified Logic Program. It employs a RETE based forwardchaining approach to compute the AIR-closure and allows closed-world reasoning. The language does allow neither permissions nor features for rectifications. The accountability views of AIR is only covering explanations and justifications needed for the audit task. [START_REF] Zou | A formal service contract model for accountable saaS and cloud services[END_REF] provides a formal service contract for accountable SaaS services. The authors, after analyzing some business contract languages, identify few requirements, a major one for them is language decidability. They propose a formal model, called OWL-SC, and a representation of the contracts based on ontology and mixes two languages OWL-DL and SWLR. They also present a translation of these contracts into the formalism of colored Petri nets. This allows to check properties and to reason on the contracts with CPN-tools. [START_REF] Zou | Modeling accountable cloud services[END_REF] proposes a formal model for service composition with accountability, which is called Accountable Cloud Service (ACS). The language enables the expression of deontic constructions: obligatory, permissible, and prohibited actions as well as rules for remediation. The semantics is based on dynamic logic extended with deontic and accountability constructions but the authors claim to remove any paradox using the Dynamic Logic. ACS provides a notation for modeling service collaboration based on BPMN 2.0 and proposes an Obligation Flow Diagram as a method for conflict resolution and verification. ACS allows the specification of accountability contracts in a machine understandable style but does not yet pave the way for a tool support.

AAL and AccLab Discussion

We introduce our general approach for accountability in [START_REF] Benghabrit | volume 512 of Communications in Computer and Information Science, chapter From Regulatory Obligations to Enforceable Accountability Policies in the Cloud[END_REF] with the idea to focus on enforcement by synthesizing an XACML [START_REF]eXtensible Access Control Markup Language (XACML) Version 3.0[END_REF] extension. [START_REF] Benghabrit | Accountability for Abstract Component Design[END_REF] presents a component-based approach to specify accountability in a system and a model-checking based verification approach. We switch to a more abstract approach using the First-Order linear Temporal Logic and the TSPASS prover in [START_REF] Benghabrit | Checking Accountability with a Prover[END_REF][START_REF] Benghabrit | Abstract accountability language: Translation, compliance and application[END_REF]. In [START_REF] Royer | Aal and static conflict detection in policy[END_REF] we demonstrate that AAL is suitable for several kinds of security and privacy concerns. We also analyze the problem of conflict detection in policy sets, exhibit weaknesses of most of the current proposals and justify the choice to rely on logical consistency. A real accountability policy example is discussed in [START_REF] Benghabrit | Towards the specification of natural language accountability policies with acclab: The laptop policy use case[END_REF] as well as lessons learnt from its formal specification with our language. The current paper summarizes our previous work but adds a bundle of related work and comparisons. We also discuss more precisely how to write accountability expressions and some limits of the current formalism. We provide new unique features: the generalized authorizations and the accountability templates. We also expose the verification principles, behind our tool like conflict detection, and compliance. The Ac-cLab tool description and its monitoring facilities were also never published.

Comparison with Related Work

[53] proposes a formal model for service composition with accountability, which is called Accountable Cloud Service. The logic is not a classic one and is mixed with BPMN notations, the drawback is that neither a decision algorithm nor a tool support are described. Another close work is [START_REF] Cederquist | An audit logic for accountability[END_REF] which defines a policy language based on FOL with policy disclosure allowing delegation responsibility. The main difference is that we consider policies already defined and assigned, without a native delegation mechanism. But note that the same compliance relation is valid in both contexts. It also proposes a concrete tool support with the Twelf proof checker but AAL adds linear temporal features and Ac-cLab automated proofs. [START_REF] Etalle | A posteriori compliance control[END_REF] is another formal model for accountability, AAL is more abstract because we do not assume specific component like trust management and dedicated predicates for refinement or transfer. There are only two previously existing tools [START_REF] Zou | A formal service contract model for accountable saaS and cloud services[END_REF][START_REF] Khandelwal | Analyzing the AIR language: A semantic web (production) rule language[END_REF]. On one hand, the language proposed by [START_REF] Zou | A formal service contract model for accountable saaS and cloud services[END_REF] is limited to ontology, without specific feature for audit or rectification and targeted to monitoring. On the other hand [START_REF] Khandelwal | Analyzing the AIR language: A semantic web (production) rule language[END_REF] focuses on explanations of inferences. Our approach is unique on two sides: the language and its tool support. Regarding AAL its unrivalled features are its FOTL foundation with an accountability clause, general authorizations and templates. AccLab has the following noteworthy characteristics: an expressive language covering most of the security and accountability needs as well as formal compliance, conflict checking and monitoring support.

Aside the previous accountability articles there is other related work which crosscuts our approach. Accountability like security is expressed by policies thus many works done in the policy domain are related to our. Our work, especially the usage expression part is related to privacy and security languages like: [START_REF] Deyoung | Experiences in the logical specification of the HIPAA and GLBA privacy laws[END_REF][START_REF] Moritz | A practical generic privacy language[END_REF][START_REF] Piolle | Representing privacy regulations with deontico-temporal operators[END_REF][START_REF] Datta | Understanding and protecting privacy: Formal semantics and principled audit mechanisms[END_REF]]. In addition to specific accountability features (audit and rectification) our work has the following characteristics. As demonstrated in [START_REF] Royer | Aal and static conflict detection in policy[END_REF] the language provides negation, even for obligation, access control and privacy concerns thus covering many needs. We rely on the FOTL framework with the monodic constraint, this is related to [START_REF] Deyoung | Experiences in the logical specification of the HIPAA and GLBA privacy laws[END_REF], but without the burden of fix points. While [START_REF] Datta | Understanding and protecting privacy: Formal semantics and principled audit mechanisms[END_REF] present a FOL approach for privacy and accountability enforcement but without explicit linear temporal operators.

Regarding policy verification we think that [START_REF] Halpern | Using firstorder logic to reason about policies[END_REF][START_REF] Montangero | Logic-based conflict detection for distributed policies[END_REF][START_REF] Craven | Expressive policy analysis with enhanced system dynamicity[END_REF][START_REF] Cau | Verification and enforcement of access control policies[END_REF] are the most related, all are limited to usual security policies. [START_REF] Halpern | Using firstorder logic to reason about policies[END_REF] is only access control in the FOL context, [START_REF] Montangero | Logic-based conflict detection for distributed policies[END_REF] focuses on location properties without tool support, and [START_REF] Craven | Expressive policy analysis with enhanced system dynamicity[END_REF] uses FOL with event calculus and a verification prototype restricted to finite domains. While [START_REF] Cau | Verification and enforcement of access control policies[END_REF] defines a rich policy language in Fusion logic and uses model-checking.

Enforcement of accountability has been done in a specific and concrete way in [START_REF] Azraoui | A-PPL: an accountability policy language[END_REF] with an extension of XACML. However, A-PPL (An Accountability Policy Language) is not a flexible approach since it operates with few dedicated constructions. It also inherits various limitations from its XACML ancestor. A more abstract vision of enforcement is proposed by monitoring or runtime verification [START_REF] Goodloe | Monitoring distributed real-time systems: A survey and future directions[END_REF]. Our monitoring approach is rather close to the following papers [START_REF] Sen | Efficient decentralized monitoring of safety in distributed systems[END_REF][START_REF] Rosu | Rewriting-based techniques for runtime verification[END_REF][START_REF] Bauer | The ins and outs of first-order runtime verification[END_REF]. In fact we mix the use of rewriting temporal expressions, the temporal and first-order approach, localization and monitoring distributed systems.

Open Questions and Limits

In the previous sections, we have seen several ways to express accountability with AAL. Regarding the three dimensions of accountability from [START_REF] Schedler | Self-Restraining State: Power and Accountability in New Democracies, chapter Conceptualiazing Accountability[END_REF], i) we have information as formal contract which can be checked for compliance, ii) justification is provided by querying the formal contract using property verification, and iii) punishment is made explicit in the contract and enforced by monitoring.

It is possible to embed models like [START_REF] Crispo | Reasoning about Accountability within Delegation[END_REF][START_REF] Corin | A Logic for Auditing Accountability in Decentralized Systems[END_REF][START_REF] Cederquist | An audit logic for accountability[END_REF][START_REF] Etalle | A posteriori compliance control[END_REF][START_REF] Le | A Formal Privacy Management Framework[END_REF] as they are based on predicate calculus, first-order inference rules and linear traces. The model in [START_REF] Zou | Modeling accountable cloud services[END_REF] uses a dynamic deontic logic based on FOL and a discrete temporal operator. The definition of the accountability clause is rather limited and specific, because it considers accountability related to one atomic action. In AAL we keep a classic logic with its tool support. We have orthogonal notions of permission, and action but not the exact obligation of deontic logic. Paradoxes of deontic logic seem difficult, if possible, to remove [START_REF] Albert | Dynamic deontic logic and its paradoxes[END_REF]. Another set of related work is focusing on properties for audit and accountability [START_REF] Jagadeesan | Towards a theory of accountability and audit[END_REF][START_REF] Feigenbaum | Towards a formal model of accountability[END_REF][START_REF] Kusters | Accountability: definition and relationship to verifiability[END_REF]. These are more challenging or impossible to fully encode without strongly restricting expressiveness since they are based on utility functions or probabilistic approaches.

We aim at integrating other notions of accountability, those defined outside computer science, as in [START_REF] Schedler | Self-Restraining State: Power and Accountability in New Democracies, chapter Conceptualiazing Accountability[END_REF][START_REF] Mulgan | accountability': An ever-expanding concept[END_REF]. However, one first limitation is that these are complex notions and there is no clear agreement on precise and operational definitions of accountability characteristics. The second point is that some characteristics (for instance, moral dilemma or force majeure) are specific of human behaviors and cannot be modelled or are out of the scope of automation. Many works consider that true accountability cannot be completely automatic and humans (an auditor, a judge, etc) should be involved in the process. This is still according to [START_REF] Schedler | Self-Restraining State: Power and Accountability in New Democracies, chapter Conceptualiazing Accountability[END_REF]: "Given that the notion of accountability is not built on the illusion that power is subject to full control ...". A fully automated solution would be equivalent to a preventive security solution, all violation cases and countermeasures are known and decided in advance. In our approach human behavior is defined by actions connected to a virtual agent (as in [START_REF] Le | A Formal Privacy Management Framework[END_REF]) under the control of the real human, thus it will be transparent here.

Other difficult notions are linked to deontic concepts, like the contrary to duty. Finally, there are some concepts like complicity, valid excuse, group accountability, grades of accountability which are totally or partly machine understandable. The main barrier for us is to obtain an agreement or at least sufficiently precise definitions for these concepts in order to model them. There are also expressiveness and decidability issues in accountability policies. However many progresses have been done recently in satisfiability modulo theories and we could expect new results in automated verification of FOTL.

Conclusion and Perspectives

Accountability is a complex concept that becomes more important in the digital society, as an effect of the raising privacy concerns in ubiquitous systems. We advocate a privacy by design approach, addressing accountability requirements starting from specification towards their implementation in software systems. We provide a flexible and expressive domain agnostic language, where one can handle distinct usages and definitions for the term accountability. Accountability interpretation and its operational management are slightly varying in the related work, even from a formal perspective. This lead us naturally to the development of the accountability laboratory, supported by its verification principles and concrete tools for policy verification and monitoring. The existing related work is rather limited to theoretical models without tool support. Tools support for some dedicated applications and domains are proposed in [START_REF] Khandelwal | Analyzing the AIR language: A semantic web (production) rule language[END_REF][START_REF] Zou | A formal service contract model for accountable saaS and cloud services[END_REF]. However, a wider perspective with concrete language and enforcement tools was lacking. In this paper we demonstrate that this objective is perfectly attainable and our proposal is aligned with the three Schedler dimensions [START_REF] Schedler | Self-Restraining State: Power and Accountability in New Democracies, chapter Conceptualiazing Accountability[END_REF]. We provide the AAL language with semantics based on FOTL, we demonstrate its expressiveness and flexibility concerning accountability policies. Apart from its expressiveness AAL provides a notion of general authorizations and a convenient notion of templates to assisting in writing policies. We study verification means for internal and specific properties and we propose conflict detection, and policy compliance. Finally, these ideas have been implemented in our Ac-cLab tool support and it provides accountability writing, consistency checking, compliance verification, and runtime monitoring.

In the near future, we intend to improve the language and its tool support. In fact one challenge is the integration of more computation primitives in FOTL. We also expect to relax the monodic constraint. For instance, (always forall X,Y pred(X, Y)) => forall X,Y always pred(X, Y)) is a valid property. While the conclusion of the right-hand side is not monodic, it can be proved with the left-hand side. With respect to performance, in [START_REF] Benghabrit | Abstract accountability language: Translation, compliance and application[END_REF] we defined some heuristics to reduce execution time and we expect to rationalize them. One important topic, which is actually not discussed in this paper, is the link between the global view promoted by AAL and the local view needed for distributed agents. Still, there are some decidability issues but results exist with the session type theory [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF].

Listing 4 A

 4 usage expression with accountability // some authorizations (ALWAYS FORALL D:Data (D.owner==Kim) => (PERMIT KardioMon.process(D) AND FORALL X:Subject DENY KardioMon.send[X](D))) AND // illegal processing and rectifying (FORALL D:Data ((NOT Kim.giveConsent[KardioMon]("Agreed")) UNTIL ((KardioMon.process(D) AND (D.owner==Kim) AND NEXT (ALWAYS (FORALL D:Data DENY KardioMon.process(D))))))) AND // illegal sending then punishing and compensating (ALWAYS ((SOMETIME EXISTS D:Data X:Subject (KardioMon.send[X](D) AND (D.owner==Kim) AND (X!=Kim))) => (Auditor.punish[KardioMon]() AND Auditor.compensate[Kim](tenEuros))))

Listing 10 FOTL translation part of Listing 6 /

 106 / from expression [1] always forall X, D (modify(X, D) => P1_modify(X, D)) and always forall X, Y, D (send(X, Y, D) => P2_send(X, Y, D)) and always forall Z, D ((relatives(Kim, Alice) and owner(Kim, D)) <=> (P1_modify(Alice, D) and P2_send(Alice, Z, D))) and // from expression [2] not exists D sometime (P3_modify(Alice, D) and sometime P3_send(Alice, Bob, D)) and // link between expression and permission always ((exists D sometime (modify(Alice, D) and sometime send(Alice, Bob, D))) => (exists D sometime (P3_modify(Alice, D) and sometime P3_send(Alice, Bob, D)))) and // link between complex and atomic permissions always ((exists D sometime (P3_modify(Alice, D) and sometime P3_send(Alice, Bob, D))) => (exists D sometime (P1_modify(Alice, D) and sometime P2_send(Alice, Bob, D))))

Listing 14

 14 Parameters instantiation AUDIT = Auditor.audit() AE = (Kim.notify[Auditor]() => AUDIT) UE = FORALL D:Data (PERMIT Kim.send[Bob](D) AND DENY Bob.send[Alice](D)) VE = EXISTS S:Data Bob.send[Alice](S) JE = (VE => ((@guilty(Bob) UNTIL Auditor.enforced[Bob]()) AND (@victim(Kim) UNTIL Auditor.enforced[Kim]()))) RE = (FORALL A:Agent (@guilty(A) => Auditor.punish[A]())) AND (FORALL A:Agent (@victim(A) => Auditor.compensate[A]()))

Listing 16 A

 16 provider compliant policy CLAUSE ListingProvider ( (FORALL D:Data S,K,M,A:Agent ((D.owner==S) AND (PERMIT K.usage(D)) AND PERMIT K.send[M](D) AND K.send[M](D) AND K.notify[A]())) AUDITING (FORALL P,A:Agent (P.notify[A]() OR P.alert[A]()) => A.audit()) IF_VIOLATED_THEN (FORALL M:Money (auditor.punish[KardioMon](M) AND (NEXT (KardioMon.give[auditor](M))) AND auditor.transfer[Kim](M))) )

  SOMETIME EXISTS D:data NOT (PERMIT Kim.input[Hospital](D) AND DENY Kim.input[Hospital](D)).

Listing 18

 18 Accountability properties // 1) validity of the sufficient audit condition (ALWAYS AE => (ALWAYS SOMETIME AUDIT)) => (CLAUSE(AUDIT, AE, UE, RE) => (ALWAYS ((NOT UE) => (SOMETIME RE)))) // 2) an equivalent formulation of CLAUSE(AUDIT, AE, UE, RE) ((ALWAYS (AE AND UE)) OR (ALWAYS AE AND (UE UNTIL ((NOT UE) AND (ALWAYS AUDIT => RE))))) // 3) decomposition of a complex contract CLAUSE(AUDIT, AE1 AND AE2, UE1 AND UE2, RE1 AND RE2) => CLAUSE(AUDIT, AE1, UE1, RE1) AND CLAUSE(AUDIT, AE2, UE2, RE2)

  Listing 13 describes a template for an extension of our accountability clause. Our example of Listing 7 is an instantiation of the template in Listing 13. This template makes explicit several new parameters: the VE violation expression and the JE the judgment expression, and two conditions. The first condition states that UE and VE are disjoint. The second condition links the judgment expression JE with the violation VE and should identify culprits or victims. The qualification with predicates @guilty and remains until enforcement by the agent A. The parameter instantiation for Listing 7 appears in Listing 14.

	Listing 13 Extended template	2.6 Accountability Templates
	extended(AUDIT, AE, UE, VE, JE, RE) = // application conditions	We go further in assisting privacy and security officers
	(ALWAYS (VE => NOT UE)) AND (ALWAYS ((JE AND VE) => ((EXISTS A:Agent (@guilty(A) UNTIL Auditor.enforced(A)))	in writing policies with the help of dedicated templates. A template, or a behavioral pattern, is a function which
	OR (EXISTS A:Agent (@victim(A) UNTIL Auditor.enforced(A)))) )) => // template	transforms several AAL expressions into a more com-plex AAL sentence expressing a specific security prac-
	(ALWAYS (JE AND AE) AND ((ALWAYS UE) OR (UE UNTIL (VE AND (ALWAYS (AUDIT => RE))))))	tice. The interpretation uses the translation function [ ]
		and applies it to the template instantiation with some
	That means, replacing the template parameters (List-	parameters. It is quite straightforward to write few tem-
	ing 13) with these values (Listing 14) we should get	plates for authorizations, data retention, data transfer,
	the original accountability expression (Listing 7) or an	transfer of ownership or permission. More complex tem-
	equivalent expression.	plates concern accountability. For instance, the tem-
		plate associated to the previous accountability clause is
		defined as in Listing 11.
		Listing 12 Punishment templates
		// VE: violation expression
		// P1 ... Pn : punishment expressions
		// END: last deactivate the possibility of violation
		// first exclusive punishment template
		punish1(VE, P1, ... Pn, END) = (ALWAYS (END => NOT VE)) =>
		((ALWAYS NOT VE) OR
		(SOMETIME (VE AND NEXT ((ALWAYS NOT VE) AND (SOMETIME P1))))
		OR ... OR
		(SOMETIME (VE AND ... AND
		NEXT ((ALWAYS NOT VE) AND (SOMETIME END)) ... ))
		// second cumulative punishment template
		// same hypotheses as above
		punish2(VE, P1, ... Pn, END) = (ALWAYS (END => NOT VE)) =>
		(ALWAYS (VE => SOMETIME P1)) AND
		...
		(ALWAYS ((VE AND ... NEXT SOMETIME VE) => SOMETIME END))

Listing 11 Accountability clause template clause(AUDIT, AE, UE, RE) = ALWAYS AE AND ALWAYS (UE OR ((NOT UE) AND (ALWAYS AUDIT => RE)))

Templates abstracting two punishment variations appear in Listing 12. The first template enables exactly one punishment in case of a violation (VE). It triggers the i th punishment in case of i successive violations. While the second one generalizes the Listings 5 and accumulates the punishments for every sequence of violations. That is, if an execution trace contains i (i ≤ n) successive violations then punishment actions are performed from 1 to i.

  Listing[START_REF] Degtyarev | Monodic temporal resolution[END_REF] Conflicting example // The example is unsatisfiable, there is a conflict // with the following expressions PERMIT KardioMon.process[KardioMon](D) EXISTS private:Data (private.owner == Kim) NEXT ALWAYS FORALL D:Data (DENY KardioMon.process[KardioMon](D))

Privacy officers are mainly concerned by choosing and filling the templates. In case of standard and simple regulation the privacy officer selects the right tem-


Hervé Jourde
email: herve.jourde@um2.fr

Christelle Batiot-Guilhe

Vincent Bailly-Comte

Cristina Bicalho

Mathieu Blanc

Valérie Borrell Estupina

Christophe Bouvier

Jean-François F Boyer

Philippe Brunet

Mathieu Coustau

V Borrell

M Cousteau

C Dieulin

E Gayrard

V Guinot

F Hernandez

L Kong

A Siou

A Johannet

V Leonardi

N Mazzilli

P Marchand

N Patris

S Pistre

J L Seidel

J D Taupin

S Van- Exter

The MEDYCYSS observatory, a Multi scalE observatory of flooD dYnamiCs and hYdrodynamicS in karSt (Mediterranean border Southern France)

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

The MEDYCYSS observatory, a Multi scalE observatory of flooD dYnamiCs and hYdrodynamicS in karSt (Mediterranean border Southern France)

Introduction

The number of damages related to flood has been increasing during the last years in the Mediterranean regions [START_REF] Fleury | Modelling the hydrologic functions of a karst aquifer under active water management -the Lez spring[END_REF]. In these regions, most floodprone streams and rivers flow on karstic rocks which are typical of the carbonates terrains of the Mediterranean circumference. Besides flood hazard, extreme rainfall events are also associated with the risk of groundwater resource contamination. Groundwater contamination can be related either to surface flow or groundwater flow because of the significant karst-river interactions. In all cases, a better assessment of these dynamics is a major stake for preserving the groundwater supply safety within the hydrosystem as groundwater management of these karsts is strongly dependent on the knowledge of their hydrodynamics. Moreover, because of the increased demand for water, the importance and awareness of karst aquifers in Mediterranean regions has grown.

For a better assessment of karst water resource, conceptual models are generally proposed to characterize the relationships between the recharge and the discharge at the outlets of the systems, based on hydrodynamics, hydrochemistry or isotopic studies (Bicalho et al., 2011 a,b,c;Fleury, 2010;Mazzilli, 2011;[START_REF] Estupina | Un modèle pluie-débit pour la prévision des crues sur un bassin karstique. Cas du bassin du Lez[END_REF]Kong A Siou et al., 2011 c ;Coustau et al., 2011;[START_REF] Bailly-Comte | Influence of karst aquifers on flood genesis and propagation in an ephemeral Mediterranean River: A semi-distributed conceptual model of the Coulazou River (Southern France)[END_REF]. The quantification (on the basis of long term time series) of these rechargedischarge relationships is a key parameter to estimate the sustainable yield of aquifers and assess the impacts of climatic and anthropogenic changes on the long term groundwater resources. However, an important limit of these approaches is related to the fact that it does not take into account the heterogeneity and the complexity of the transfers within each compartment (soil, epikarst/perched aquifer, unsaturated zone, saturated zone) of the karst aquifer. It is thus crucial to characterize and then consider these transfers in distributed models that account for each compartment.

Therefore, various experimental sites have been constructed to better understand these transfer processes. On these pilot sites, the challenges are i) to better characterize the karst/river interactions for the risk assessment of floods and water resource contamination; ii) to discriminate and quantify the distribution of the hydric fluxes (rapid and slow transfers) between the surface and the spring; iii) to quantify the water storage variation with time and understand the role of the unsaturated zone on the long term storage of the aquifer; and iv) to quantify the recharge as a function of field and climatic parameters, as it is a key variable for the assessment and management of groundwater resources.

Experimental sites of the MEDYCYSS Observatory

The MEDYCYSS observatory (Fig. 1) comprises three main watersheds where karst/river interactions occur: the Lez, the Mosson and the Coulazou river catchments. The major objectives of MEDYCYSS are:

-The observation and characterisation at local and regional scale of groundwater hydrodynamics in karst watersheds, under climatic and anthropogenic forcing; -The observation and characterisation of the rapid hydrological processes during extreme flood events in Mediterranean watersheds, where interactions occurs between the river network and the karst aquifer; -The observation and characterisation of groundwater resource contamination hazard, based on the coupled hydrochemistry /hydrodynamic monitoring; -The assessment of the links between karst evolution over time (geology and geomorphology) and its current hydrodynamic behaviour. -The characterisation and coupled modelling of the groundwater and surface water hydrodynamics in karst watersheds; -The characterisation and modelling of the global change impact on the recharge/discharge relationships over long time period. Long term time series (more than 40 years) of rain, water table level and discharge exist on the three experimental sites, which is a major asset for long term modelling and the characterization of global change impact on the long term groundwater resource.

Karst watersheds of the Coulazou and Mosson rivers

Since 2004, the experimental site of the Coulazou River allowed to study the modality of surface floods genesis [START_REF] Jourde | Dynamics and contribution of karst groundwater to surface flow during Mediterranean flood[END_REF]) and transfer (Bailly-Comte et al. 2008[START_REF] Bailly-Comte | Conceptualization and classification of groundwatersurface water hydrodynamic interactions in karst watersheds: Case of the karst watershed of the Coulazou River (Southern France)[END_REF]) in karst terrains, at the scale of a well monitored small catchment. This site comprises a karst catchment, the Causse d'Aumelas, which is a Jurassic calcareous plateau crossed by the intermittent Coulazou River. This area is a binary karst system developed within the calcareous Jurassic plateau, in contact with an Oligocene impermeable basin in the North and a Miocene impermeable basin in the South.

In order to better understand the groundwater contribution to flash floods in the Coulazou river the water table in the karst aquifer is monitored in various locations (wells, karstic network, permanent and temporary springs), as well as the Coulazou river discharge at the entry and the exit of the karst system.

More than 15 karstic events, which can function alternately as sinkholes or springs, have been observed in this hydrosystem. In order to understand the interactions between surface water and groundwater, hydrodynamic monitoring is enriched with various chemical tracers monitoring (Major and trace elements, TOC: Total Organic Carbon, stable isotopes of water and Carbon) on springs, boreholes, swallow holes, and on the Coulazou river. This "multiparameters" approach allows identifying the various types of water that contribute to flow, but also flow inversions between the karst system and the river. The understanding of these specific links between surface water and groundwater are fundamental to estimate the vulnerability of the aquifer and to protect water resources in this Mediterranean context [START_REF] Batiot | Sink holessprings study to underline flow inversion in a Mediterranean karst system partly supplied by an intermittent river (Causse d'Aumelas, southeastern France)[END_REF][START_REF] Selles | Influence des relations karst/rivière sur la restitution plurimodale d'un traçage artificiel : Cas du Causse d'Aumelas[END_REF]. Moreover, a regular monitoring (twice a month during two hydrological cycles) of CO2 and 222 Rn allowed explaining the temporal variability of these elements [START_REF] Batiot | Seasonal variations of CO2 and Radon 222 in a Mediterranean Cavity (Causse d'Aumelas, SE France)[END_REF].

One of the major interest of this site is that, from upstream to downstream, the watershed evolution is characteristic of many Mediterranean rivers like Cèze, Hérault, Vidourle or Gardon in southern France, i.e: i) an upstream impervious watershed; ii) an intermediate watershed where karst/river interactions occur, with consequences on floods but also on groundwater contamination; iii) a downstream watershed in a alluvial plain, where flood hazard is generally more important.

This system thus constitutes a local scale experimental site to study karst/river interactions before focusing on larger systems where flood hazards have larger human and economic consequences.

On this site, some important experimental results characteristics of most Mediterranean karst watersheds and concerning hydrodynamics, groundwater/surface water interactions and transport have been highlighted:

-A hydrodynamic analysis coupled with a hydrological modelling showed that groundwater contribution from the karst to surface flood can reach one third of the total flood volume, and increase the flood peak discharge by a factor of two [START_REF] Jourde | Dynamics and contribution of karst groundwater to surface flow during Mediterranean flood[END_REF]. -Times series analysis in time (correlation) and frequency (power spectral density) domains coupled with recession curves analysis showed that: o karst groundwater flows may either attenuate or amplify the rapid surface flow transfers depending on the initial state (groundwater level) of the system (Bailly-Comte et al., 2008a, b).

o the initial groundwater level may be used to forecast the type of hydraulic connection between the river and the saturated zone during flood. This level is found to be also controlled by the limited discharge capacity of karst conduits. A conceptual model of karst/river interactions during flood has been proposed [START_REF] Bailly-Comte | Conceptualization and classification of groundwatersurface water hydrodynamic interactions in karst watersheds: Case of the karst watershed of the Coulazou River (Southern France)[END_REF]. o water exchange between matrix and conduits control the spring hydrograph (Bailly-Comte et al., 2010) -A dye tracing experiment conducted in a small but highly transient tracing system interacting with the Coulazou River has shown that plurimodal tracer breakthrough curves only result from surface water/groundwater interactions, each flood pulse of the sinking stream inducing a tracer pulse at the outlet with low dilution and dispersion [START_REF] Selles | Influence des relations karst/rivière sur la restitution plurimodale d'un traçage artificiel : Cas du Causse d'Aumelas[END_REF].

Karst watershed of the Lez river

The hydrological and hydrogeological catchments of the Lez River (North-West of the city of Montpellier) are remarkable as regards both their vulnerability to pollutions or flood hazards, and the active management of the groundwater resource. The objectives of the hydrodynamics monitoring are: (i) a better understanding of flash floods and contaminant transfers during extreme rain events, (ii) the characterization of the recharge and the transfer processes within each compartment of the karst system. To improve the understanding of the groundwater origins and its circulation dynamics within this karst system, regular sampling for hydrochemical and isotopical analysis is also carried out on the main springs and wells of the karst system. The application of a multi-tracer approach based on major ions, trace elements, isotopes and emerging tracers, helped determining water origins, water mixing proportions and levels of anthropogenic contaminations. Those results also allowed proposing a conceptual model of groundwater circulation for this aquifer [START_REF] Batiot-Guilhe | Characterisation of underground flows in karstic aquifers by studying DOM fluorescence. Example of two Mediterranean systems (Lez and Causse d'Aumelas[END_REF][START_REF] Bicalho | Hydrogeological functioning of a complex Mediterranean karst system by multivariable tracing[END_REF][START_REF] Bicalho | Investigation of Groundwater dynamics in a Mediterranean karst system by using multiple geochemical tracers[END_REF]Bicalho et al. submitted). High flow rate pumping (up to 6000 m 3 /h) performed at the Lez spring for Montpellier water supply allows investigating the hydrodynamic properties of the karst aquifer at a regional scale. Besides, a small experimental site (Terrieu site) with 18 boreholes and 3 wells on a 500 m 2 area allows the characterisation of the hydrodynamic properties of the karst aquifer at a local scale (pumping up to 60 m 3 /h). This configuration allows identifying the hydrodynamic behaviour of the karst system at nested observation scale and thus characterizing the scale effects in the assessment of hydrodynamic properties from pumping test analysis at local and regional scales [START_REF] Jazayeri | Influence of observation scale on the hydrodynamic analysis of well tests in a fractured reservoir. Case of the Lez karst system[END_REF]. Recent works focused on the karst drainage network development as a function of the hydrological, geodynamical and structural changes over time [START_REF] Leonardi | Eléments de Genèse des karsts péri-méditerranéens : Impact de la tectonique sur l'évolution des drains karstiques (Karsts Nord-Montpelliérains)[END_REF] Recent studies also allowed proposing new results regarding hydrological modelling in karst watershed. For example, a distributed parsimonious eventbased rainfall-runoff model was developed and applied on the Lez watershed upstream Montpellier (Coustau et al., 2011). On one hand, the model produces very satisfactory flash flood simulations, and on the other hand, its initialization is relatively easy thanks to a powerful relationship between the initial condition of the model and either the Hu2 index from the Meteo-France SIM model (soil humidity), or the piezometric levels. The interpretation of the model suggests that groundwater does not affect the first peaks of the flood, but can strongly impact subsequent peaks in the case of a multi-storm event. Because this kind of model is based on a limited amount of readily available data, it could be a crucial tool for flash floods real-time forecasting.

An original methodology based on neural networks was also developed to better understand the hydrodynamical behaviour of karst (Kong A Siou et al., 2011 a,b,c). A dedicated architecture allows to describe the recharge of the system according to its geological heterogeneity. This model allows refining knowledge on the behaviour and the delimitation of its alimentation basin (Kong A Siou et al., 2011 c). Global modelling based on reservoir model that takes into account flow through both the saturated zone and the unsaturated infiltration zone was developed to characterize the functioning of this aquifer under active water management [START_REF] Fleury | Modelling the hydrologic functions of a karst aquifer under active water management -the Lez spring[END_REF][START_REF] Mazzilli | Hydrological modelling of a karst aquifer under active groundwater management using a parsimonious conceptual model H2Karst[END_REF] The Lez hydrosystem was also studied to assess the role of karst in flood dynamics, with a specific focus on the consequences of the active management of the groundwater resource, which offers some new insights in the integrated water resource/flood management on these hydrosystems with a high karstic component [START_REF] Jourde | Optimization of the generalization capability for rainfall-runoff modeling by neural networks: The case of the Lez aquifer (southern France)[END_REF]

Conclusion and perspectives in terms of modelling and observation strategies

Flow modelling in karst hydrosystems implies various approaches to capture the spatio-temporal complexity of the studied site. Indeed groundwater hydrodynamics differs from surface water hydrodynamics, which involve referring to different conceptual models. Furthermore, depending on the considered temporal scale, the dominant processes within the hydrosystem will not be the same. For example, at the temporal scale of a flash flood, the processes will notably differ from the processes at the scale of one or more hydrological cycles.

The distributed measurement of humidity and evapotranspiration, together with piezometric monitoring in different compartments of the hydrosystems will enhance both hydrological modelling for flash floods forecasting and recharge estimation for hydrogeological modeling and water resource evolution with time.

Developing a multi-tracer approach based on major and trace elements and emerging tracers (isotopes, Rare Earth Elements, fluorescence of Dissolved Organic Matter), a better characterisation of the water origins, water mixing and of potential anthropogenic contaminations has been achieved [START_REF] Batiot-Guilhe | Characterisation of underground flows in karstic aquifers by studying DOM fluorescence. Example of two Mediterranean systems (Lez and Causse d'Aumelas[END_REF][START_REF] Bicalho | Hydrogeological functioning of a complex Mediterranean karst system by multivariable tracing[END_REF][START_REF] Bicalho | Investigation of Groundwater dynamics in a Mediterranean karst system by using multiple geochemical tracers[END_REF]Bicalho et al. submitted). The hydrochemical monitoring already shows that the chemical signatures vary all along the hydrological cycle but also during a flood event. This change will enhance a better understanding of the various processes occurring in different compartments of the karst system.

It will be useful to distinguish different types of pedological and landscape units, where infiltration and evapotranspiration will be determined. Defining a mean soil permeability and evapotranspiration for each units and characterizing the variability of these parameters within one unit will be possible. Based on these results, a GIS analysis taking into account landscape use, pedology and geology, will facilitate the drawing of a map with these distributed parameters.

The different perspectives in terms of modelling and observation strategies can be listed as follows:

-Couple distinct models for the integrated and distributed simulation of the hydrological, hydrogeological and hydraulic processes in karst hydrosystems at different time scales (flood event, hydrological cycle) . -Analyse the sensitivity and assess the uncertainty of the hydrological and hydrogeological models with regards to the main parameters (e.g. contrast between the hydrodynamic parameters of the different compartments, initial state of the system, soil humidity, recharge), -Discriminate and quantify the distribution of the hydric fluxes (rapid and slow transfers) in each compartment of the hydrosystem. -Characterize the transfer within each subsystem and develop distributed models taking into account the transfer within each compartment of the hydrosystem. -Quantify the water storage variation with time and understand the role of the unsaturated zone on the long term storage of the aquifer. -Quantify the recharge, which is a key variable for the assessment and management of groundwater resources in karsts -Quantify the recharge-discharge relationships to estimate the sustainable yield of aquifers and determine the impacts of climatic change on the long term groundwater resources. -Quantify the impact of anthropogenic forcing (pumping, active management) on the global water balance and hydrodynamic behaviour of the karst system.

Fig. 1 :

 1 Fig.1: Hydrogeological and hydrological contexts of the MEDYCYSS observatory (44°0 0'N, 4°00'E -43°17'N 3° 26'E)