Shukun Tokas

Olaf Owe

A Formal Framework for Consent Management

Keywords: GDPR, Data Protection, Privacy Policies, Policy Compliance, Tagging, Runtime Enforcement, Consent Management

The aim of this work is to design a formal framework for consent management in line with EU's General Data Protection Regulation (GDPR). To make a general solution, we consider a high-level modeling language for distributed service-oriented systems, building on the paradigm of active objects. Our framework provides a general solution for data subjects to observe and change their privacy settings and to be informed about all personal data stored about them. The solution consists of a set of predefined types for privacy related concepts, a formalization of policy compliance, a set of interfaces that forms the basis of interaction with external users for consent management, a set of classes that is used in interaction with the runtime system, and a runtime system enforcing the consented policies.

Introduction

In response to the emerging privacy concerns, the European Union (EU) has approved the General Data Protection Regulation (GDPR) [START_REF]Regulation (GDPR)[END_REF] to strengthen and impose data protection rules across the EU. This regulation requires controllers that process personal data of individuals within EU and EEA, to process personal information in a "lawful, fair, and transparent manner". Article 6 and Article 9 of the regulation [START_REF]Regulation (GDPR)[END_REF] provide the criteria for lawful processing, such as consent, fulfillment of contractual obligation, compliance with a legal obligation etc. The regulation (including several other data protection laws) recognises consent as one of the lawful principles for legitimate processing, and Article 7 sets out the conditions for the processing personal data when relying on consent.

A data subject's consent reflects his/her agreements in terms of the processing of personal data. The regulation indicates that the consent must specifically be given for the particular purpose of processing. It is also indicated in Recital 43 that the data subject should be given a free choice to accept or deny consent for specific purposes, rather than having one consent for several purposes. In particular our focus is on processing of personal data when consent is the legal ground, i.e., processing is valid only if a data subject has given consent for the specific purpose, otherwise processing of the personal data should cease. Moreover, this can be extended to incorporate other applicable legal grounds, such as vital interest, legitimate interest etc, but a discussion on this will be out of scope of this work.

Furthermore, Article 15 of the regulation prescribes that the data subject has Right of Access, which requires the data controllers to provide the data subject with his/her personal data, the purposes of processing, the legal basis for doing so, and other relevant information (see Article 15 [START_REF]Regulation (GDPR)[END_REF]). WP29 recommends controllers to introduce tools, such as a privacy dashboards through which the data subject can be informed and engaged regarding the processing of their personal data [START_REF]Guidelines on Consent under Regulation[END_REF]. The regulation also introduces an obligation for data controllers to demonstrate compliance, i.e., accountability (see Article 5 [START_REF]Guidelines on Consent under Regulation[END_REF] [START_REF]Regulation (GDPR)[END_REF]). These requirements are likely to pose substantial administrative burden. This work is an attempt to design a pragmatic solution to address these requirements, using a formal approach. In particular, our framework covers certain aspects of privacy principles (Article 5), lawfulness of processing (Article 6), privacy by design (Article 25) and data subject access request (Article 15). Due to the nature of these requirements and space constraints, we cover these requirements partially.

The privacy requirements in the data protection regulations are defined informally, therefore, to avoid ambiguity the policy language equipped with a formal semantics is essential [START_REF] Owe | Formal methods as a link between software code and legal rules[END_REF]. It is essential that the policy terminology establishes a clear link between the law and the program artifacts. For this, we let privacy policies and consent specifications be expressed in terms of several predefined names, reflecting standard terminology (allowing names to be added as needed). It is necessary that the policy terminology used towards the data subject is simple but with a formal connection to the underlying programming elements. We have previously studied static aspects of privacy policies and static checking of policy compliance from a formal point of view, a brief overview is given in [START_REF] Tokas | Language-based mechanisms for privacy by design[END_REF].

The aim of this work is to design a formal framework for consent management where a data subject can change his/her privacy settings through predefined interfaces, which could be part of a library system. The data subjects are seen as external system users without knowledge of the underlying program. Data subjects may interact with the system at runtime through a user-friendly interface (e.g. a privacy dashboard), to view current privacy settings and update these settings. To make a general solution, we consider a high-level modeling language for distributed service-oriented systems, building on the paradigm of active objects [START_REF] Nierstrasz | A tour of Hybrid -a language for programming with active objects[END_REF][START_REF] Johnsen | An asynchronous communication model for distributed concurrent objects[END_REF]. The method for protecting access to personal data in this setting comprises of: tagging the data with (subject, purpose) pairs; associating a purpose to each method accessing personal data; storing consented policies of a subject in a subject object; deriving an effective policy for the access from the executing method and data tags; and comparing the effective policy with the current consented policies to determine if it is a valid operation.

The main contribution of this research is a framework that consists of: (i) a policy specification language; (ii) a formalization of runtime policy compliance; (iii) predefined interfaces and classes for consent management; (iv) a run-time system for dynamic checking of privacy compliance, with built-in generation of runtime privacy tags when new personal data is created. We prove a notion of runtime compliance with respect to the consented policies. BNF syntax definition of the policy language. I ranges over interface names, R over purpose names, and P over principal names. A principal is given by an object or an interface (representing all objects of that interface). Superscripts * and + denote general and non-empty repetition, respectively.

Paper Outline. The rest of the paper is structured as follows. Section 2 presents the policy and consent specification language, a formalization of policy compliance, and the core language. Section 3 introduces the functionality for consent management. Section 4 presents tag generation, dynamic checking and an operational semantics. Section 5 discusses related work, and Section 6 concludes the paper and discusses future work.

Language Setting

In order to formalize the management and processing of personal information, we introduce basic notions for privacy policies and consent in Section 2.1, and introduce a small language for interface and class definitions in Section 2.2.

Policy and Consent Specification

Privacy policies are often described in natural language statements. To verify formally that the program satisfies the privacy specification, the desired notions of privacy need to be expressed explicitly. To formalize such policies, we define a policy specification language. In our setting, a privacy policy is a statement that expresses permitted use of the personal information by the declared program entities. In particular, a policy is given by triples that put restrictions on what principals can access the personal data for specific purposes and access-rights. That being the case, a policy p is given by a triple (P, R, A), where:

i) P describes a principle that can access personal information and is given by an object representing a principal, or by an interface (representing all objects supporting that interface). Interfaces are organized in an open-ended inheritance hierarchy, letting I < J denote that principal I is a subinterface of J and letting o < I if object o supports I. We let ≤ denote the transitive and reflexive extension of <. As an example, Specialist < Doctor < HealthWorker ii) The purpose name R describe the specific purpose for which personal data can be used. Such purpose names are organized in an open-ended directed acyclic graph, reflecting specialization. For instance, the declaration purpose treatm, health_care where treatm < health_care policy pDoc = (Doctor, treatm, rincr) // general policy consent pos(pDoc) = (Doctor, health_care, write) // general positive consent consent neg(pMyDoc) = (Dr.Hansen, treatm, f ull) // specific negative consent Fig. 2. Sample purpose and policy definitions. Here Dr. Hansen is a principal object.

purpose spl_treatm, treatm where spl_treatm < treatm makes spl_treatm more specialized purpose than treatm. If data is collected for the purpose of spl_treatm then it cannot be used for treatm. However, if it is collected for the purpose of treatm then it can be used for spl_treatm. We let ≤ denote the transitive and reflexive extension of <, and let the predefined purpose all be the least specialized purpose.

iii) Access rights A describe the permitted operations on personal data, and are given by a lattice, with full and no as top and bottom and with a partial ordering A : read gives read access, write gives write access (without including read access), incr allows addition of new information but neither read nor write is included. The join of read and incr is abbreviated rincr, the join of write and incr is abbreviated wincr, while the join of read and write is full.

The language syntax for policies is summarized in Fig. 1, where [ ] is used as meta-parenthesis, and superscripts * and + denote general and non-empty repetition, respectively. Sample policies are given in Fig. 2.

Definition 1 (Policy Compliance). Policy compliance, , is defined by

(P , R , A ) (P, R, A) P ≤ P ∧ R ≤ R ∧ A A A
Thus, a policy p complies with p if it has the same or smaller interface, the same or more specialized purpose, and the same or weaker access rights. In order to deal with both addition and removal of policies, we organize the policies in a list of negative and positive policies, such that the newest and most significant policy is last in the list. A positive consent has the form pos(p), where p is a policy triple, meaning that access to personal data requiring p is allowed. A negative consent has the form neg(p), meaning that access to personal data requiring p is forbidden. The disjoint union of these two forms is captured by the type Consent. Consented policies are organized in a Consent list. We define compliance of policies with respect to such a list L by: p = false p (L; pos(p )) = if p p then true else p L p (L; neg(p )) = if p p then false else p L where _; _ denotes list append. Thus positive or negative policies later in the list (capturing newer ones) override policies earlier in the list (capturing older ones) with smaller policy triples. This gives a simple way to upgrade and downgrade consent, and with a uniform treatment of negative as well as positive consent.

A High-Level Language for Active Objects

In the setting of active objects, the objects are autonomous and execute in parallel, communicating by so-called asynchronous method invocations. Objectlocal data structure is defined by data types. Classes are defined by an imperative language while data types and associated functions are defined by a functional language. We assume interface abstraction, i.e., remote field access is illegal and an object can only be accessed though an interface. This allows us to focus on major challenges of modern architectures, without the complications of low-level language constructs related to the shared-variable concurrency model. A strongly typed language for active objects based on [START_REF] Johnsen | An asynchronous communication model for distributed concurrent objects[END_REF] is given in Fig. 3. The programs we consider are defined by a sequence of declarations of interfaces (containing method declarations), classes (containing class parameters, fields, methods and class constructors), and data type definitions. Class parameters are like fields, but with read-only access. A subclass inherits class parameters, fields, and methods (and the class constructor) unless redefined. A method m may have a cointerface Co given by the with clause, with Co, restricting callers to objects supporting interface Co (this is checked statically and allows type-correct call backs). Each method dealing with personal data must have an associated purpose, given at the end of the method definition (:: R), if any, otherwise the one declared for the method in the interface, if any, or otherwise the one declared for the interface. Methods may declare local variables and end with a return statement. We include standard statements such as skip, assignment (:=), object creation (new), if-and while-statements, and we allow blocking calls (v := o.m(e)) where o is the callee and e is the list of actual parameters, and asynchronous calls o!m(e) and broadcasts I!m(e) to all objects of interface I. The incremental update v :+ e extends a list v with one or more elements e.

We consider pure expressions, including products (e 1 , e 2 , . . .), lists, and function applications f (e) where f may be a defined function or a constructor function (including ";" for lists and constants such as nil, void, 0, 1, 2, etc.). A value is a variable-free expression with only constructor functions, such as the list nil; 1; 2; 3.

Consent Management

The policy settings of each data subject may change dynamically during runtime in interaction with the external users. In order to handle this, we define a runtime system where personal data values are tagged with specification of data subjects and processing purposes The runtime system will check that every access to personal data complies with the consented policies. Since there could be a huge amount of personal information in a distributed system, it is essential that the information in the tags is minimized. Our framework includes a general solution for subjects to observe and change their privacy settings. We chose to let the information about the consented policies be stored separately from the tags. The tags are generated by the runtime system as explained in detail in Section 4.1.

The consented policy may change dynamically, in contrast to the information in the tags, which do not change. By combining the core information in the tags with the dynamically changing consent information, we are able to keep the information in the tags relatively small.

We let interface Principal correspond to a system user, be it a person, an organization, or other identifiable actor. Interface PrivacySettings (Fig. 4) defines methods for accessing and resetting consented policies by the data subject, while the subinterface Subject (Fig. 5) defines methods for consent management including functionality for requesting and updating policy settings. For each data subject there is an associated object (i.e., the subject object) supporting PrivacySettings and Subject, and this object is used to manage the privacy settings and policies in interaction with an external user (for instance through an app on a mobile phone). The subject object will contain the consented policies and is used when personal data about the data subject is accessed, in order to check compliance with the consented policies as explained in the operational semantics. In addition, it is used to manage the collection of personal data from sensitive objects. Thus the class SUBJECT, supporting interface Subject, deals with handling of consented policies and collection of personal data.

The interface PrivacySettings specifies the interface for updating consent (Fig. 4). It includes methods for adding and removing consent by the user such that after successful addition/removal of a policy p, that policy (or a smaller) allows/denies access to personal data. There is also functionality for an user to check her current policy settings, through method seeMyPolicies, which returns all policies of that user.

Class PRIVACYSETTINGS in Fig. 6 implements PrivacySettings by storing the consented policies in a field variable consented, which is a Consent list (i.e., list of consented policies). The add operation addP olicy(p) adds pos(p) at the end of the consented list (unless p consented holds already), and the remove operation remP olicy(p) adds neg(p) at the end of the list (unless p consented gives false, in which case it is redundant). The consent list of a subject S can be initialized with some initial policies, including (S, all, rincr) for self access.

One may also remove redundant consented policies in the list when new ones are added, using the following strategy: A positive policy pos(p) occurring in a list L is redundant in the list if p L holds where L is the list with this occurrence removed. Similarly, a negative policy neg(p) occurring in L is redundant if p L gives false. In these cases L can replaced by L in order to simplify future compliance tests by limiting the size of the consented list.

Data Collection from Sensitive Objects to Data Subjects

In order to restrict processing of personal information, we define an interface Sensitive, which will be the superinterface of all objects handling personal data. The interfaces Subject and Sensitive in Fig. 5 define the functionality for collection of personal information for subjects and define consent management. Class SUBJECT in Fig. 7 gives an implementation. A call to the method collectMyData on a subject object from the corresponding user will start a process to collect all personal information about the subject. The broadcast Sensitive!requestMySensitiveData() sends a requestMySensitiveData message to all objects implementing Sensitive. A sensitive object may receive a request-MySensitiveData request from a subject object (caller) and will then react by collecting the personal data tagged with the subject and send it back to the subject object through the method receiveMySensitiveData. This data is then collected incrementally and stored in a (tagged) list, mydata, which can be accessed by the corresponding user using seeMyData or seeData. This class may be used as superclass of objects supporting Subject. The method requestMySen-sitiveData is provided by, and implemented in, the runtime system as explained in Section 4.2.

Interface Subject has all as declared purpose, and all methods in the interface and class inherit this purpose. The access to personal information in SUBJECT complies with the general policy (S, all, rincr) for a subject object S.

Runtime System

The operational semantics of the considered language is given in Fig. 9. Data values are tagged with set of pairs of subject and purpose. A runtime configuration of an active object system is captured by a multiset of objects and messages (using blank-space as the binary multiset union constructor). Each object o is responsible for executing all method calls to o as well as self-calls. An object has at most one active process, reflecting the remaining part of a method execution. Objects have the form o : ob(δ, s) where o is the object identity, δ is the current object state, and s is a sequence of statements ending with a return, representing the remaining part of the active process, or idle when there is no active process. The state of an object δ is given by a twin mapping from variable names to tagged values, written (α|β), where α is the state of the field variables w and class parameters z (including

v := e] abbreviates if v in β then (α | β[v → (α|β)[e]]) else (α[v → (α|β)[e]] | β).
In addition, the operational semantics defines the system variables pcs and nextFut, which appear in the state of each object (in α). The "program counter stack" pcs is used for storing the stack of tags on the conditions corresponding to the nesting of enclosing if/while statements, and nextFut is used for generating unique identities for calls. Furthermore, the self reference this is handled as an implicit class parameter, while myfuture and caller appear as implicit method parameters, holding the identity of a call and its caller, respectively.

Example. Consider some personal health data with the tag {(Alice, treatm)}, and assume the consented policies (. . . ; pos(Doctor, treatm, f ull)) in object Alice. A Doctor can then read the data since there is a matching positive policy with at least read access where Doctor is the principal and the purpose of the current method is treatm or less. However, for the consented list (. . . ; pos(Doctor, treatm, f ull); neg(Bob, treatm, read)), where Bob is a doctor object, read access will be denied due to the presence of negative policy.

Runtime Tagging of Values

The runtime checking uses two special notions: The current purpose, denoted R current , is the purpose of the enclosing method, which we assume is statically specified, as in [START_REF] Tokas | Language-based mechanisms for privacy by design[END_REF]. (Alternatively one could take the purpose defined in some other way, for instance by data-flow graphs as in [START_REF] Basin | On purpose and by necessity: compliance under the GDPR[END_REF].) Secondly, we define the current principal, denoted P current , as the first principal object found by following the dynamic call chain from a method as illustrated in Fig. 8 (ignoring non-principals such as objA).

The runtime evaluation of an expression e gives a tagged value c of form d l with a tag l. In a method execution the evaluation of an expression e in a state δ and with policy context pcs is denoted where the data value is evaluated (as explained in the next subsection) ignoring tags, resulting in a ground term, i.e., a term d with only constructor functions (g), and where the tag is given by the tag function defined below: For tagged data values, the tag function is given by tag(d l ) = l, and for untagged values it is given by:

tag() = f latten(δ[pcs]) tag(g(S)) = {(S, R current )}∪ tag() tag(g(c)) = tag(c), otherwise tag(d l , c) = l ∪ tag(c) tag(S, c) = {(S, R current )} ∪ tag(c) tag(d, c) = tag(d) ∪ tag(c), otherwise
Note that the tag includes flatten(δ[pcs]), defined as the union of all tags in the stack pcs. An untagged product (..., S, ...) will also include the tag (S, R current ). A pair (S, S ) will be tagged with {(S, R current ), (S , R current ), f latten(δ[pcs])}. An untagged constructor value g(S, c) is tagged like the product (S, c). When a subject S occurs as an argument to a constructor term or product, the pair (S, R current ) is added to the tag set. Note that g(S), (S, S ), (S, c), and (c, S) include (S, R current ) in the tag set, but S and (S) do not, as a product must have at least two arguments. A tag (S, R) is redundant in a tag set l, and may be removed, if there is another tag (S, R ) in l such that R < R . Non-personal data will have an empty tag set. Policies are considered non-personal.

Runtime Checking of Privacy Compliance

The runtime system keeps track of the current consented policy list for each subject, specifying the policies for accessing personal data concerning the subject. In the runtime system there is a mapping from subjects to policy lists M : Subject → P olicyList given by M[S] == S.consented where each consented is maintained by the runtime system. Note that even though remote field access is not possible within the program syntax, this restriction does not apply to the runtime system.

The evaluation of expressions, ∆[e], is done depth-first, left-to-right. Thus

∆[f (e)] is [f (∆e]), ∆[if b then e else e ] is ∆[e] if ∆[b] is true and ∆[e ] if ∆[b]
∆[v] = δ[v], if ∀(S, R) ∈ tag(δ[v]) : (P current , R, read) M[S] ∆[v] = error, otherwise
In the first line, the tag is defined by the tag function in Section 4.1. A policy (S, all, rincr) is initially added to the consented list of each subject object S, to allow the data subject to read and increment his/her own data.

For write access, we define a modified state update function ∆[v := c] so that it includes the appropriate checks for assignments, and similarly for incremental assignments. Note that there is no check on local variables since they form the local work space, i.e., a method has always write access to the local variables. Implementation of method requestMySensitiveData is provided by the runtime system by making the call caller!receiveMySensitiveData(tl) where tl is given by ∆[w]/caller, i.e., the tagged values of fields with caller in the tag.

∆[x := c] = δ[x := c], ∆[w := c] = δ[w := c], if ∀(S, R) ∈ tag(c) : (P current , R, write) M[S] ∆[w := c] = δ[w := error], otherwise
Runtime Overhead. We have given a solution for compliance checking by a runtime system formulated at a high-level of abstraction. We here discuss the overhead in tagging and checking with this solution, and how it can be reduced. By combining the core information in the tags with the dynamically changing consent information, we are able to keep the information in the tags relatively small, and moreover the tags are not changed when the consent is changed, which is a crucial property. Thus the main overhead is in accessing the consented list for the subjects in the tag. Note that the updates on each consent list is atomic, so there is no need for critical regions nor object synchronization at the runtime level. Thus a compliance check made by one object will not slow down the other objects. This processing can easily be made more efficient by letting each principal pull a copy of a subject's consent setting when needed. However, as this could lead to outdated consent information, one could use a version number for each subject's consent list, and let a principal check that it has the latest version before applying its local copy of a consent list. A further method of reducing overhead, would be to re-represent each consent list by means of a mapping (from principal and purpose of a given subject to access right) thereby the list traversal is reduced to direct look-up. This method has a cost whenever a consent list is updated. A further discussion is beyond the scope of this paper.

Operational Rules

Each rule in the operational semantics deals with only one object o, and possibly messages, reflecting the nature of concurrent distributed active objects, The semantics in Fig. 9 formalizes the notion of idleness, and generation of objects and messages, including a rule (no-query) for garbage collection of unused reply messages. Generation of identities for objects and method calls is handled by underlying semantic functions and implicit attributes.

The operational semantics uses an additional query statement, get u, for dealing with the termination of call statements. A synchronous call is treated as an asynchronous call followed by a get query. The query get u is blocking while waiting for the method response with identity u.

Assignment is handled by updating the state, requiring that there is read access to any personal data (using ∆). An if-statement requires read access to personal data in the condition and the resulting tag set l is pushed on the policy stack pcs, ensuring that all evaluations in the taken branch implicitly includes l in the tag set. A while loop is handled by expanding while b do s od to if b then s; while b do s od fi upon execution of the while-statement. Void methods return the value void. We assume all methods end in a return statement, including class constructors, which end in return void (although omitted in the examples). An assignment of the form v : + e is treated as an atomic operation at runtime. (When lists are implemented by linked lists, this operation can be executed by a single pointer assignment, since the value of e is not affected by other objects.) Semantically, v : + e is the same as v := v + e, and we do not show a special rule for it. This means that a consent update can also be considered atomic. Furthermore, we assume that initial values given to fields or local variables are expanded to assignments, as described earlier.

For simplicity, rules for broadcasting (similar to that for asynchronous calls) and local synchronous calls (i.e., queries on local calls) are omitted, since such calls do not pose additional privacy challenges. In the current semantics, a query on a local call will lead to deadlock. The handling of local queries would require addition of a stack in the object state in order to be able to push and pop unfinished local method frames, for instance as in [START_REF] Johnsen | An asynchronous communication model for distributed concurrent objects[END_REF].

The theorem below ensures that every access to a data subject's personal information will comply with the consented policy.

Theorem 1 (Runtime compliance). After a policy is successfully removed, all further variable accesses that need this policy will fail by giving a runtime error until the policy, or a stronger one, is added again.

Proof. Consider an object state δ where (S, R) ∈ tag (δ[v]). Let policy p denote (P current , R, read). We must prove that a runtime look-up of v in such a state gives error after a policy p such that p p is removed from the consented list of S and before a policy p such that p p is added to the consented list of S.

Every variable look-up is made through one of the operational rules, by means of δ or ∆. By inspection of these rules, we observe that all program variables are evaluated by ∆ apart from caller and this in rule Return, but here the pcs stack is empty (since a return statement occurs last in a body), so evaluation by δ in this case is the same as by ∆. It remains to show the theorem for variable access through ∆, and for an access to v we must show that p M [S].

By induction on the length of the execution we show that ∆ [v] gives error between the successful removal of

Related Work

This paper focuses on the intersection between compliance formalization and programming languages. This line of work is relatively recent, featuring several threads of active research such as policy specification, policy enforcement, monitoring, privacy by design, language-based privacy, and role-based access control.

The work presented in [START_REF] Métayer | A formal privacy management framework[END_REF] provides a privacy management framework for the definition of privacy agents (such as subject, controller) acting as representatives of individuals. These privacy agents play a specific role as "representative" or "proxy" of the user in order to manage personal data and ensure privacycompliant interactions among agents. We share with [START_REF] Métayer | A formal privacy management framework[END_REF] the objective of privacy compliant interactions, but we use an integrated style, i.e., including compliance checks within objects and actors accessing personal data. In addition, we use the same policy language for different actors and consented policies are maintained in subject objects. Cunche et al. [START_REF] Morel | A generic information and consent framework for the IoT[END_REF] present a generic information and consent framework for IoT that allows the data subject to express privacy requirements as well as receive the information and associated privacy policy. The privacy policies for subjects and controllers are based on the PILOT semantics [START_REF] Pardo | Analysis of privacy policies to enhance informed consent[END_REF]. Privacy policies in [START_REF] Pardo | Analysis of privacy policies to enhance informed consent[END_REF] are more expressive than ours as they also encapsulate contextual information, but the semantics of policy compliance is not discussed in particular. We define fewer privacy requirements and focus on compliance formalization. The approach followed in [START_REF] Morel | A generic information and consent framework for the IoT[END_REF] makes use of dedicated privacy agents, while we integrate the compliance checks in actor objects.

Sen et al. [START_REF] Sen | Bootstrapping privacy compliance in big data systems[END_REF] demonstrate techniques for compliance checking in big data systems. Privacy policies are specified using a policy specification language, LEGALEASE, where policies can be expressed using allow and deny clauses to permit and prohibit access. Policies can be expressed using nested allow-deny rules. Policy clauses use data store, purpose, role, and data type attributes to specify information flow restrictions. Then, a data inventory tool GROK maps data types in code to high-level policy concepts, and the compliance checking then reduces to a form of information flow analysis. This is similar to our approach in [START_REF] Tokas | Language-based mechanisms for privacy by design[END_REF] where we associate policy with the types carrying sensitive information, but the difference is that the type-policy mapping is integrated in the language. The policy specification language in [START_REF] Sen | Bootstrapping privacy compliance in big data systems[END_REF] has some similarities with our work: the semantics of policies is compositional and policies are expressed as lists of positive and negative policies. However, for the sake of simplicity, we do not consider nested-policies. All information flow restrictions (policy attributes) are encoded as a lattice in [START_REF] Sen | Bootstrapping privacy compliance in big data systems[END_REF], while in our setting that is not the case. However, in [START_REF] Sen | Bootstrapping privacy compliance in big data systems[END_REF] the concept lattice does not seem to distinguish with information about other subjects, which we do and in addition we can generate tags at runtime when new information (involving a subject or personal information) is created.

Yang et al. [START_REF] Yang | Preventing information leaks with policy-agnostic programming[END_REF] propose a policy-agnostic programming model. Sensitive data values are associated with policies and then the programmer may implement the rest of the program in a policy agnostic manner. The language's [START_REF] Yang | A language for automatically enforcing privacy policies[END_REF] runtime system enforces these policies to ensure that only policy compliant values are used in computations. In contrast, we use generalized polices for each subject (including purpose) and minimize the information in the tags.

Other examples of language-based approaches relying on information-flow control include the role-based approach in [START_REF] Myers | Protecting privacy using the decentralized label model[END_REF] and the purpose-based approach in [START_REF] Hayati | Language-based enforcement of privacy policies[END_REF]. Myers and Liskov present a model of decentralized information flow labels, where principals and labels are the essentials of the model [START_REF] Myers | Protecting privacy using the decentralized label model[END_REF]. Principals are the entities that own, update and release (to other principals) information. A label is a set of owner: reader policy pairs, where owner is the data owner (i.e., subject in our approach), and reader is the principal that has read access to this data. Programs and data are annotated with such labels, and information flow restrictions are enforced by type checking. For an access to be valid, all the policy requirements of the label should be enforced, which holds in our approach as all the tags must comply with the consented policies. There are no generalized policies, and the tags will take more space than in our case. In [START_REF] Hayati | Language-based enforcement of privacy policies[END_REF], Hayati and Abadi describe an approach to model and verify aspects of privacy policies in the Jif (Java Information Flow) programming language. Data collected for a specific purpose is annotated with Jif principals and then the methods needed for a specific purpose are also annotated with Jif principals. Explicitly declaring purposes for data and methods ensures that the labeled data will be used only by the methods with connected purposes. However, this representation of purpose is not sufficient to guarantee that principals will perform actions compliant with the declared purpose. In contrast, this can be checked at runtime in our approach.

Basin et al. [START_REF] Basin | On purpose and by necessity: compliance under the GDPR[END_REF] propose an approach that relates a purpose with a business process and use formal models of inter-process communication to demonstrate GDPR compliance. Process collection is modeled as data-flow graphs which depict the data collected and the data used by the processes. Then these processes are associated with a data purpose and are used to algorithmically generate data purpose statements, i.e., specifying which data is used for which purpose and detect violation of data minimization. A main challenge tackled by this work is to automatically generate compliant privacy policies from the model. We share with this work an explicit specification of purpose. In [START_REF] Basin | On purpose and by necessity: compliance under the GDPR[END_REF], a purpose is associated with a process, while in our approach a method accessing personal information is tagged with a purpose and personal data is tagged with sets of (subject, purpose) pairs. This tagging is useful in generating privacy policies to check compliance.

Conclusion

We propose a consent management framework that allows a data subject to communicate and update consent policies to the controller and to view all personal data about her in the system along with the purposes for which they are used. We have considered a core language for distributed active object systems and formalized the notion of policy compliance and given an operational semantics for the considered programming language. The runtime system ensures that every access to personal data complies with the currently consented polices.

We have illustrated the feasibility of formalizing GDPR specific privacy requirements, including privacy by design by providing explicit specifications of purpose and policy constructs; lawfulness and transparency of processing based on consented purposes; data subject access request by providing predefined interfaces and classes to assist in providing the data subject with the personal data and purposes for which it is being processed.

Our framework includes a general solution for subjects to observe and change their privacy settings and for subjects to be informed about all personal data stored about them. The solution consists of a set of predefined types for privacy related concepts and a set of interfaces that forms the basis for interaction with external users, a set of classes that is used in interaction with the runtime system, and runtime checking of all access to personal data to ensure that it complies with the current privacy settings. The same framework can be reused for another language, as long as the assumption of interface abstraction is respected and as long as the purpose of any method handling personal data is identified.

Future Work: The framework can be extended to accommodate for other legal bases by having separate policy lists for each legal basis, and a logic to chose from these bases as required. More information can be included in the tags for a richer compliance check, for instance, the data creator can be recorded as the current principal of the method instance creating the data. More information can be included in the policy specification, for example restrictions on temporal validity, data collectors, and data creators. Furthermore, we could add cases of non-personal tag information as exceptions to the generated tags, for instance to deal with encryption. We can easily add more fine-grained methods for selection of policies/personal data in the interfaces/classes for privacy settings and data collection (from sensitive objects), for instance using purpose and principal to limit the selection.

AFig. 1 .

 1 Fig.1. BNF syntax definition of the policy language. I ranges over interface names, R over purpose names, and P over principal names. A principal is given by an object or an interface (representing all objects of that interface). Superscripts * and + denote general and non-empty repetition, respectively.

Fig. 3 .Fig. 4 .

 34 Fig.3. BNF syntax of the core language, extended with purpose specifications (::R). A field is denoted w, a local variable x, a method parameter y, a class parameter z, type names N , expressions e, and expression lists e. The brackets in [T ] and [T ] are ground symbols. Function symbols f range over pre-/programmer-defined functions/constructors with prefix/mixfix notation.

Fig. 5 .

 5 Fig. 5. Interface Declarations for Sensitive Objects and Data Subjects.

Fig. 7 .Fig. 8 .

 78 Fig. 7. The implementation of Subject.

  is false, and for a value c, ∆[c] is c. (Here b is a boolean expression.) For a defined function f , ∆[f (c)] is obtained by the definition of f replacing the formal parameters by the actual values c. We let the evaluation of a variable v have a built-in compliance check of read access:

  This definition is lifted to expressions e, letting ∆[x := e] denote ∆[x := ∆[e]]. Similarly, ∆[v : + c ] requires (P current , R, incr) M[S]for (S, R) ∈ tag(c). Non-personal data can be accessed without restrictions since the tag is empty.

Fig. 9 .

 9 Fig. 9. Operational rules defining small-step semantics with privacy tags. Unique future identities are ensured by functions initialF ut, parameterized with the parent, and next.

  p and addition of p to M[S]. A successful removal must perform the atomic operation consented : + neg(p ) in S. Right afterwards, neg(p ) is the last element in M[S] and therefore ∆[v] gives error. If a consent neg(p ) is added, p M[S] remains false. If a consent pos(p ) is added, we may assume that p p (otherwise p can be used as p and there is nothing to prove) and by the induction hypothesis p M[S] remains false.

  The implementation of privacy settings and policy changes.

	class PRIVACYSETTINGS (User user) implements PrivacySettings {
	List[Consent] consented; // the current privacy policies
	with User
	op PolicyList seeMyPolicies()
	{return (if caller = user then consented else nil fi)}
	op Bool addPolicy(Policy p) { // add a new policy (return false if redundant)
	Bool ok := (caller = user); if ok then
	if p consented then ok := false
	else consented :+ pos(p) fi fi; return ok } // incremental update
	op Bool remPolicy(Policy p){ // add a negative policy (return false if redundant)
	Bool ok := (caller=user); if ok then
	if p consented then consented :+ neg(p)// incremental update
	else ok := false fi fi; return ok }
	...}
	Fig. 6.


Eleni Bila

Simon Doherty

Brijesh Dongol

John Derrick

Gerhard Schellhorn

Heike Wehrheim

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory

Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency. So far, this has lead to the design of a number of persistent concurrent data structures, built to satisfy an associated notion of correctness: durable linearizability. In this paper, we transfer the principle of durable concurrent correctness to the area of software transactional memory (STM). Software transactional memory algorithms allow for concurrent access to shared state. Like linearizability for concurrent data structures, opacity is the established notion of correctness for STMs. First, we provide a novel definition of durable opacity extending opacity to handle crashes and recovery in the context of NVM. Second, we develop a durably opaque version of an existing STM algorithm, namely the Transactional Mutex Lock (TML). Third, we design a proof technique for durable opacity based on refinement between TML and an operational characterisation of durable opacity by adapting the TMS2 specification. Finally, we apply this proof technique to show that the durable version of TML is indeed durably opaque. The correctness proof is mechanized within Isabelle.

Introduction

Recent technological advances indicate that future architectures will employ some form of non-volatile memory (NVM) that retains its contents after a system crash (e.g., power outage). NVM is intended to be used as an intermediate layer between traditional volatile memory (VM) and secondary storage, and has the potential to vastly improve system speed and stability. Software that uses NVM has the potential to be more robust; in case of a crash, a system state before the crash may be recovered using contents from NVM, as opposed to being restarted from secondary storage. However, because the same data is stored in both a volatile and non-volatile manner, and because NVM is updated at a slower rate than VM, recovery to a consistent state may not always be possible. This is particularly true for concurrent systems, where coping with NVM requires introduction of additional synchronisation instructions into a program. This observation has led to the design of the first persistent concurrent programming abstractions, so far mainly concurrent data structures. Together with these, the associated notion of correctness, i.e., linearizability [START_REF] Herlihy | Linearizability: A correctness condition for concurrent objects[END_REF], has been transferred to NVM. This resulted in the novel concept of durable linearizability [START_REF] Izraelevitz | Linearizability of persistent memory objects under a full-system-crash failure model[END_REF]. A first proof technique for showing durable linearizability of concurrent data structures has been proposed by Derrick et al. [START_REF] Derrick | Verifying correctness of persistent concurrent data structures[END_REF].

Besides concurrent data structures, software transactional memory (STM) is the most important synchronization mechanism supporting concurrent access to shared state. STMs provide an illusion of atomicity in concurrent programs. The analogy of STM is with database transactions, which perform a series of accesses/updates to shared data (via read and write operations) atomically in an all-or-nothing manner. Similarly with an STM, if a transaction commits, all its operations succeed, and in the aborting case, all its operations fail. The now (mainly) agreed upon correctness criterion for STMs is opacity [START_REF] Guerraoui | Principles of Transactional Memory[END_REF]. Opacity requires all transactions (including aborting ones) to agree on a single sequential history of committed transactions and the outcome of transactions has to coincide with this history.

In this paper, we transfer STM and opacity to the novel field of non-volatile memory. This entails a number of steps. First, the correctness criterion of opacity has to be adapted to cope with crashes in system executions. Second, STM algorithms have to be extended to deal with the coexistence of volatile and non-volatile memory during execution and need to be equipped with recovery operations. Third, proof techniques for opacity need to be re-investigated to make them usable for durable opacity. In this paper, we provide contributions to all three steps.

-For the first step, we define durable opacity out of opacity in the same way that durable linearizability has been defined based on linearizability. Durable opacity requires the executions of STMs to be opaque even if they are interspersed with crashes. This guarantees that the shared state remains consistent. -We exemplify the second step by extending the Transactional Mutex Lock (TML) of Dalessandro et al. [START_REF] Dalessandro | Transactional mutex locks[END_REF] to durable TML (DTML). To this end, TML needs to be equipped with a recovery operation and special statements to guarantee consistency in case of crashes. We do so by extending TML with a logging mechanism which allows to flush written, but volatile values to NVM during recovery. -For the third step, we build on a proof technique for opacity based on refinement between IO-automata. This technique uses the automaton TMS2 [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF] which has been shown to implement opacity [START_REF] Lesani | Putting opacity in its place[END_REF] using the PVS interactive theorem prover. This automaton gives us a formal specification, which can be used as the abstract level in a proof of refinement. Furthermore, the IO-automaton framework is part of the standard Isabelle distribution. For use as a proof technique for durable opacity, TMS2 is extended with a crash operation (mimicing system crashes and their effect on memory) to yield DTMS2. The automaton DTMS2 is then proven to only have durably opaque executions. Thereby we obtain an operational characterisation of durable opacity.

invocations possible matching responses invt(TMBegin) rest(TMBegin(ok)) invt(TMCommit) rest(TMCommit(ok)), rest(TMCommit(abort)) invt(TMRd(x)) rest(TMRd(v)), rest(TMRd(abort)) invt(TMWr(x, v)) rest(TMWr(ok)), rest(TMWr(abort)) Table 1. Events appearing in the histories of TML, where t ∈ T is a transaction identifier, x ∈ L is a location, and v ∈ V a value Finally, we bring all three steps together and apply our proof technique to show that durable TML is indeed durably opaque. This proof has been mechanized in the interactive prover Isabelle [START_REF] Nipkow | Isabelle/HOL -A Proof Assistant for Higher-Order Logic[END_REF]. Our mechanized proof proceeds by encoding DTMS2 and DTML as IO-automata within Isabelle, then proving the existence of a forward simulation, which in turn has been shown to ensure trace refinement of IO-automata [START_REF] Lynch | Forward and backward simulations[END_REF], and hence guarantees durable opacity of DTML.

Transactional Memory and Opacity

Software Transactional Memory (STM) provides programmers with an easy-to-use synchronisation mechanism for concurrent access to shared data, whereby blocks of code may be treated as transactions that execute with an illusion of atomicity. STMs usually provide a number of operations to programmers: operations to start (TMBegin) and commit a transaction (TMCommit), and operations to read and write shared data (TMRd, TMWr). These operations can be called (invoked) from within a client program (possibly with some arguments, e.g., the variable to be read) and then will return with a response. Except for operations that start transactions, all other operations might potentially respond with abort, thereby aborting the whole transaction.

A widely accepted correctness condition for STMs that encapsulates transactional phenomena is opacity [START_REF] Guerraoui | On the correctness of transactional memory[END_REF][START_REF] Guerraoui | Principles of Transactional Memory[END_REF], which requires all transactions, including aborting transactions to agree on a single sequential global ordering of transactions. Moreover, no transactional read returns a value that is inconsistent with the global ordering.

Histories

As standard in the literature, opacity is defined on the histories of an implementation. Histories are sequences of events that record all interactions between the implementation and its clients. An event is either an invocation (inv) or a response (res) of a transactional operation. For the TML implementation, possible invocation and matching response events are given in Table 1, where we assume T is a set of transaction identifiers, L a set of addresses (or locations) mapped to values from a set V.

The type Mem = L → V describes the possible states of the shared memory. We assume that initially all addresses hold the value 0 ∈ V.

We use the following notation on histories: for a history h, h t is the projection onto the events of transaction t only and h[i..j] the subsequence of h from h(i) to h(j) inclusive. For a response event e, we let rval(e) denote the value returned by e; for instance rval(TMBegin(ok)) = ok. If e is not a response event, then we let rval(e) = ⊥.

We are interested in three different types of histories [2]. At the concrete level the TML implementation produces histories where the events are interleaved. At the abstract level we are interested in sequential histories, which are ones where there is no interleaving at any level -transactions are atomic: a transaction completes before the next transaction starts. As part of the proof of opacity we use an intermediate specification which has alternating histories, in which transactions may be interleaved but operations (e.g., reads, writes) are not interleaved.

A history h is alternating if h = or is an alternating sequence of invocation and matching response events starting with an invocation. For the rest of this paper, we assume each process invokes at most one operation at a time, and hence, assume that h t is alternating for any history h and transaction t. Note that this does not necessarily mean h is alternating itself. Opacity is defined for well-formed histories, which formalises the allowable interaction between an STM implementation and its clients. For every t, h t = s 0 , . . . , s m of a well-formed history is an alternating history such that s 0 = inv t (TMBegin), for all 0 < i < m, event s i = inv t (TMBegin) and rval(s i ) ∈ {commit, abort}. Note that by definition, well-formedness disallows transaction identifiers from being reused. We say t is committed if rval(s m ) = commit and aborted if rval(s m ) = abort. In these cases, the transaction t is completed, otherwise t is live. A history is well-formed if it consists of transactions only and there is at most one live transaction per process.

Opacity

Opacity [START_REF] Guerraoui | On the correctness of transactional memory[END_REF][START_REF] Guerraoui | Principles of Transactional Memory[END_REF] compares concurrent histories generated by an STM implementation to sequential histories and can be seen as a strengthening of serializability to accommodate aborted transactions. Below, we first formalise the sequential history semantics, then consider opaque histories.

Sequential history semantics.

A sequential history has to ensure that the behaviour is meaningful with respect to the reads and writes of the transactions.

Definition 1 (Valid history)

. Let h = ev 0 , . . . , ev 2n-1 be a sequence of alternating invocation and matching response events starting with an invocation and ending with a response.

We say h is valid if there exists a sequence of states σ 0 , . . . , σ n such that σ 0 (l) = 0 for all l ∈ L, and for all i such that 0 ≤ i < n and t ∈ T:

The point of TM is that the effect of the writes only takes place if the transaction commits. Writes in a transaction that abort do not affect the memory. However, all reads, including those executed by aborted transactions, must be consistent with previously committed writes. Therefore, only some histories of an object reflect ones that could be produced by a TM. We call these the legal histories, and they are defined as follows.

Definition 2 (Legal histories). Let hs be a non-interleaved history and i an index of hs. Let hs be the projection of hs[0..(i -1)] onto all events of committed transactions plus the events of the transaction to which hs(i) belongs. Then we say hs is legal at i whenever hs is valid. We say hs is legal iff it is legal at each index i. This allows us to define sequentiality for a single history, which we lift to the level of specifications.

Definition 3 (Sequential history). A well-formed history hs is sequential if it is noninterleaved and legal. We denote by S the set of all possible well-formed sequential histories.

Opaque histories. Opacity is defined by matching a concurrent history to a sequential history such that (a) both histories consist of the same events, and (b) the real-time order of transactions is preserved. For (b), the real-time order on transactions t 1 and t 2 in a history h is defined as t 1 ≺ h t 2 if t 1 is a completed transaction and the last event of t 1 in h occurs before the first event of t 2 .

A given concrete history may be incomplete, i.e., it may contain pending operations, represented by invocations that do not have matching responses. Some of these pending operations may have taken effect, and others may not. The corresponding sequential history however must decide: either by adding a suitable matching response event for the pending invocation (the effect has taken place), or by removing the pending invocation (no effect yet). Therefore, we define a function complete(h) that constructs all possible completions of h by appending matching responses for some pending invocations and removing all the other pending invocations. This is similar to the treatment of completions in the formalisation of linearizability [START_REF] Herlihy | Linearizability: A correctness condition for concurrent objects[END_REF]. The sequential history then must have the same events as those of one of the results returned by complete(h).

Definition 4 (Opaque history).

A history h is end-to-end opaque iff for some hc ∈ complete(h), there exists a sequential history hs ∈ S such that for all t ∈ T, hc t = hs t and ≺ hc ⊆≺ hs . A history h is opaque iff each prefix h of h is end-to-end opaque; a set of histories H is opaque iff each h ∈ H is opaque; and an STM implementation is opaque iff its set of histories is opaque.

STMs over Persistent Memory

We now consider STMs over a non-volatile memory model comprising two layers: a volatile store, whose contents are wiped clean when a system crashes (e.g., due to power loss), and a persistent store, whose state is preserved after a crash and available for use upon reboot. During normal program execution, contents of the volatile store may be transferred to the persistent store by the system. The main idea behind programs for this memory model is to include a recovery procedure that executes over the persistent store and resets the system into a consistent (safe) state. To achieve this, a programmer can control transfer of information from volatile to persistent store using a FLUSH(a) operation, ensuring that the information in address a is saved in the persistent store.

For STMs, we introduce a new notion of consistency: durable opacity which we define in Section 3.1. Durable opacity extends opacity [START_REF] Guerraoui | On the correctness of transactional memory[END_REF][START_REF] Guerraoui | Principles of Transactional Memory[END_REF] in exactly the same way that durable linearizability [START_REF] Izraelevitz | Linearizability of persistent memory objects under a full-system-crash failure model[END_REF] extends linearizability [START_REF] Herlihy | Linearizability: A correctness condition for concurrent objects[END_REF], namely a history that contains crashes is durably opaque precisely when the same history with crashes removed is opaque. We present an example STM implementation that satisfies durable opacity in Section 3.2, extending Dalessandro et al.'s Transactional Mutex Lock [START_REF] Dalessandro | Norec: streamlining STM by abolishing ownership records[END_REF].

Durable Opacity

Durable opacity is a correctness condition that is defined over histories that record the invocation and response events of operations executed on the transactional memory like opacity. Unlike opacity, durably opaque histories record system crash events, thus may take the form:

H = h 0 c 1 h 1 c 2 ...h n-1 c n h n ,
where each h i is a history (containing no crash events) and c i is the ith crash event. Following Izraelevitz et al. [START_REF] Izraelevitz | Linearizability of persistent memory objects under a full-system-crash failure model[END_REF], for a history h, we let ops(h) denote h restricted to non-crash events, thus for H above, ops(H) = h 0 h 1 . . . h n-1 h n , which contains no crash events. We call the subhistory h i the i-th era of h.

The definition of a well-formed history is now updated to include crash events. A history is durably well-formed iff ops(h) is well formed and every transaction identifier appears in at most one era. Thus, we assume that when a crash occurs, all running transactions are aborted.

Definition 5 (Durably opaque history).

A history h is durably opaque iff it is durably well-formed and ops(h) is opaque.

Example: Durable Transactional Mutex Lock

We now develop a durably opaque STM: a persistent memory version of the Transactional Mutex Lock (TML) [START_REF] Dalessandro | Transactional mutex locks[END_REF], as given in Fig. 1. TML adopts a strict policy for transactional synchronisation: as soon as one transaction has successfully written to a variable, all other transactions running concurrently will be aborted when they invoke another read or write operation. To enforce this policy, TML uses a global counter glb (initially 0) and local variable loc, which is used to store a copy of glb. Variable glb records whether there is a live writing transaction, i.e., a transaction that has started, has not yet ended nor aborted, and has executed (or is executing) a write operation. More precisely, glb is odd if there is a live writing transaction, and even otherwise. Initially, we have no live writing transaction and thus glb is 0 (and hence even).

A second distinguishing feature of TML is that it performs writes in an eager manner, i.e., it updates shared memory during the write operation 5 . This is potentially problematic in a persistent memory context since writes that have completed may not be committed if a crash occurs prior to executing the commit operation. That is, writes of uncommitted transactions should not be seen by any transactions that start after a crash occurs. Our implementation makes use of an undo log mapping addresses to their persistent memory values prior to executing the first write operation for that address. Logged values are made persistent before the address is overwritten. Thus, if a crash occurs prior to a transaction committing, it is possible to recover the transaction to a safe state by undoing uncommitted transactional writes.

Operation TMBegin copies the value of glb into its local variable loc and checks whether glb is even. If so, the transaction is started, and otherwise, the process attempts to start again by rereading glb. A TMRead operation succeeds as long as glb equals loc (meaning no writes have occurred since the transaction began), otherwise it aborts the current transaction. The first execution of TMWrite attempts to increment glb using a cas (compare-and-swap), which atomically compares the first and second parameters, and sets the first parameter to the third if the comparison succeeds. If the cas attempt fails, a write by another transaction must have occured, and hence, the current transaction aborts. Otherwise loc is incremented (making its value odd) and the write is performed. Note that because loc becomes odd after the first successful write, all successive writes that are part of the same transaction will perform the write directly after testing loc at line W1. Further note that if the cas succeeds, glb becomes odd, which prevents other transactions from starting, and causes all concurrent live transactions still wanting to read or write to abort. Thus a writing transaction that successfully updates glb effectively locks shared memory. Operation TMEnd checks to see if a write has occurred by testing whether loc is odd. If the test succeeds, glb is set to loc+1. At line E2, loc is guaranteed to be equal to glb, and therefore this update has the effect of incrementing glb to an even value, allowing other transactions to begin.

Our implementation uses a durably linearizable [START_REF] Derrick | Verifying correctness of persistent concurrent data structures[END_REF][START_REF] Izraelevitz | Linearizability of persistent memory objects under a full-system-crash failure model[END_REF] set or map data structure log, such as the one described by Zuriel et al. [START_REF] Zuriel | Efficient lock-free durable sets[END_REF]. A durably linearizable operation is guaranteed to take effect in persistent memory prior to the operation returning. In Fig. 1, we use use operations pinsert(), pempty() and pdelete() to stress that these operations are durably linearizable.

Our durable TML algorithm (DTML) makes the following adaptations to TML. Note the the operations build on a model of a crash that resets volatile memory to persistent memory.

-Within a write operation writing to address addr, prior to modifying the value at addr, we record the existing address-value pair in log, provided that addr does not already appear in the undo log (lines W4 and W5). After updating the value (which updates the value of addr in the volatile store), the update is flushed to persistent memory prior to the write operation returning (line W7). -We introduce a recovery operation that checks for a non-empty log and transfers the logged values to persistent memory, undoing any writes that have completed (but not committed) before the crash occurred. Since a crash could occur during recovery, we transfer values from the undo log to persistent memory one at a time. -In the commit operation, we note that we distinguish a committing transaction as one with an odd value for loc. For a writing transaction, the log must be cleared by setting it to the empty log (line E2). Note that this is the point at which a writ-

Proving Durable Opacity

Previous works [1,2,[START_REF] Doherty | Proving opacity of a pessimistic STM[END_REF][START_REF] Dongol | Verifying linearisability: A comparative survey[END_REF] have considered proofs of opacity using the operational TMS2 specification [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF], which has been shown to guarantee opacity [START_REF] Lesani | Putting opacity in its place[END_REF]. The proofs show refinement of the implementation against the TMS2 specification using either forward or backward simulation. For durable opacity, we use a similar proof strategy. In Section 4.3, we develop the DTMS2 operational specification, a durable version of the TMS2 specification, that we prove satisfies durable opacity. Then, in Section 5, we establish a simulation between DTML and DTMS2.

Background: IOA, Refinement and Simulation

We use Input/Output Automata (IOA) [START_REF] Lynch | Hierarchical correctness proofs for distributed algorithms[END_REF] to model both the implementation, DTML, and the specification, DTMS2.

Definition 6. An Input/Output Automaton (IOA) is a labeled transition system A with a set of states states(A), a set of actions acts(A), a set of start states start(A) ⊆ states(A), and a transition relation trans(A) ⊆ states(A) × acts(A) × states(A) (so that the actions label the transitions).

The set acts(A) is partitioned into input actions input(A), output actions output(A) and internal actions internal(A). The internal actions represent events of the system that are not visible to the external environment. The input and output actions are externally visible, representing the automaton's interactions with its environment. Thus, we define the set of external actions, external(A) = input(A) ∪ output(A). We write s a -→ A s iff (s, a, s ) ∈ trans(A).

An execution of an IOA A is a sequence σ = s 0 a 0 s 1 a 1 s 2 . . . s n a n s n+1 of alternating states and actions, such that s 0 ∈ start(A) and for all states s i , s i ai -→ A s i+1 . A reachable state of A is a state appearing in an execution of A. An invariant of A is any superset of the reachable states of A (equivalently, any predicate satisfied by all reachable states of A). A trace of A is any sequence of (external) actions obtained by projecting the external actions of any execution of A. The set of traces of A, denoted traces(A), represents A's externally visible behaviour.

For automata C and A, we say that C is a refinement of A iff traces(C) ⊆ traces(A). We show that C is a refinement of A by proving the existence of a forward simulation, which enables one to check step correspondence between the transitions of C and those of A. The definition of forward simulation we use is adapted from that of Lynch and Vaandrager [START_REF] Lynch | Forward and backward simulations[END_REF]. Forward simulation is sound in the sense that if there is a forward simulation between A and C, then C refines A [START_REF] Lynch | Forward and backward simulations[END_REF][START_REF] Müller | I/O Automata and beyond: Temporal logic and abstraction in Isabelle[END_REF].

IOA for DTML

We now provide the IOA model of DTML. The state of DTML (Fig. 1) comprises global (shared) variables glb ∈ IN (modelling glb in volatile memory); log ∈ L → V, where → denotes a partial function (modelling log in persistent memory); the volatile memory store vstore ∈ L → V; and the persistent memory store pstore ∈ L → V. We also use the following transaction-local variables: the program counter pc ∈ T → PC, loc ∈ T → IN, the input address addr ∈ T → V, the input value val ∈ T → V. We also make use of an auxiliary variable writer whose value is either the transaction id of the current writing transaction (if one exists), or None (if no writing transaction is currently running). Execution of the program is modelled by defining an IOA transition for each atomic step of Fig. 1, using the values of pc t (for transaction t) to model control flow. Each action that starts a new operation or returns from a completed operation is an external action. The crash action is also external. All other actions (including flush and recovery) are internal actions.

To model system behaviours (crash, system flush and recovery), we reserve a special transaction id syst. A crash and system flush is always enabled, and hence can always be selected for execution. Recovery steps are enabled after a crash has taken place and are only executed by syst. The effect of a flush is to copy the value of the address being flushed from vstore to pstore. Note that a flush can also be executed at specific program locations. In DTML, a flush of addr occurs at lines W7 and C5. The effect of a crash is to perform the following:

set the volatile store to the persistent store (since the volatile store is lost), set the program counters of all in-flight transactions (i.e., transactions that have started but not yet completed) to aborted to ensure that these transaction identifiers are not reused after the system is rebooted, and set the status of syst to C1 to model that a recovery is now in progress. In our model, it is possible for a system to crash during recovery. However, no new transaction may start until after the recovery process has completed.

IOA for DTMS2

In this section, we describe the DTMS2 specification, an operational model that ensures durable opacity, which is based on TMS2 [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF]. TMS2 itself has been shown to strictly imply opacity [START_REF] Lesani | Putting opacity in its place[END_REF], and hence has been widely used as an intermediate specification in the verification of transactional memory implementations [1,2,[START_REF] Derrick | Verifying opacity of a transactional mutex lock[END_REF][START_REF] Doherty | Proving opacity of a pessimistic STM[END_REF].

We let f ⊕ g denote functional override of f by g, e.g.,

f ⊕ {x → u, y → v} = λ k. if k = x then u elseif k = y then v else f (k).
Formally, DTMS2 is specified by the IOA in Fig. 2, which describes the required ordering constraints, memory semantics and prefix properties. We assume a set L of locations and a set V of values. Thus, a memory is modelled by a function of type L → V. A key feature of DTMS2 (like TMS2) is that it keeps track of a sequence of memory states, one for each committed writing transaction. This makes it simpler to determine whether reads are consistent with previously committed write operations. Each committing transaction containing at least one write adds a new memory version to the end of the memory sequence. However, unlike TMS2, following [START_REF] Derrick | Verifying correctness of persistent concurrent data structures[END_REF], the memory state is considered to be the persistent memory state. Interestingly, the volatile memory state need not be modelled.

The state space of DTMS2 has several components. The first, mems is the sequence of memory states. For each transaction t there is a program counter variable pc t , which ranges over a set of program counter values, which are used to ensure that each transaction is well-formed, and to ensure that each transactional operation takes effect between its invocation and response. There is also a a begin index variable beginIdx t , that is set to the index of the most recent memory version when the transaction begins. This variable is critical to ensuring the real-time ordering property between transactions. Finally, there is a read set, rdSet t , and a write set, wrSet t , which record the values that the transaction has read and written during its execution, respectively.

The read set is used to determine whether the values that have been read by the transaction are consistent with the same version of memory (using validIdx). The write set, on the other hand, is required because writes in DTMS2 are modelled using deferred update semantics: writes are recorded in the transaction's write set, but are not published to any shared state until the transaction commits.

The crash action models both a crash and a recovery. We require that it is executed by the system thread syst. It sets the program counter of every in-flight transaction to aborted, which prevents these transactions from performing any further actions in the era following the crash (for the generated history). Note that since transaction identifiers are not reused, the program counters of completed transactions need not be set to any special value (e.g., crashed) as with durable linearizability [START_REF] Derrick | Verifying correctness of persistent concurrent data structures[END_REF]. Moreover, after restarting, it must not be possible for any new transaction to interact with memory states prior to the crash. We therefore reset the memory sequence to be a singleton sequence containing the last memory state prior to the crash.

The following theorem ensures that DTMS2 can be used as an intermediate specification in our proof method. We provide a proof sketch below. The full proof may be found in the appendix of [START_REF] Bila | Defining and verifying durable opacity: Correctness for persistent software transactional memory[END_REF].

Theorem 1. Each trace of DTMS2 is durably opaque. Proof (Sketch). First we recall that TMS2 is exactly the same as the automaton in Fig. 2, but without a crash operation. The proof proceeds by showing that for any history h ∈ traces(DTMS2), we have that ops(h) ∈ traces(TMS2). Then since ops(h) is opaque, we have that h is durably opaque. We establish a formal relationship between h and ops(h) by establishing a weak simulation between DTMS2 and TMS2 such that {ops(h) | h ∈ traces(DTMS2)} ⊆ traces(TMS2). The simulation is weak since the external crash action in DTMS2 has no matching counterpart in TMS2.

The simulation relation we use captures the following. Any transaction t of DTMS2 that is aborted due to a crash will set pc t to aborted without executing resp t (abort). This difference can easily be compensated by the simulation relation. A second difference is that mems is reset to last(mems) in DTMS2 when a crash occurs, and hence there is a mismatch between mems in DTMS2 and in TMS2. Let ds be a state of DTMS2 and as a state of TMS2. To compensate for the difference between ds.mems and as.mems, we introduce an auxiliary variable "allMems" to ds that records memories corresponding to all committed writing transactions in DTMS2. We have the property that ds.mems of DTMS2 is a suffix of ds.allMems and that ds.allMems = as.mems.

Durable Opacity of DTML

We now describe the simulation relation used in the Isabelle proof. 6Our simulation relation is divided into two relations: a global relation globalRel, and a transactional relation txnRel. The global relation describes how the shared states of the two automata are related, and the transaction relation specifies the relationship between the state of each transaction in the concrete automaton, and that of the transaction in the abstract automaton. The simulation relation itself is then given by: simRel(cs, as) = globalRel(cs, as) ∧ ∀ t ∈ T • txnRel(cs, as, t)

We first describe globalRel, which assumes the following auxiliary definitions where cs is the concrete state (of DTML) and as is the abstract state (of DTMS2). These definitions are used to compensate for the fact that the commit of a writing transaction in the DTML algorithm takes effect (i.e., linearizes) at line E2 when the log is set to empty.

writes(cs, as) = if cs.writer = t ∧ pc t = E3 then as.wrSet t else ∅ logical glb(cs) = if cs.writer = t ∧ pc t = E3 then cs.glb + 1 else cs.glb write count(cs) = logical glb(cs) 2

Function writes(cs, as) returns the (abstract) write set of the writing transaction. This is the write set of the writing transaction, t, in the abstract state as provided t hasn't already linearized its commit operation, and is the empty set otherwise. Function logical glb(cs) compensates for a lagging value of glb after a writing transaction's commit operation is linearized. Namely, it returns the glb incremented by 1 if a writer is already at E3. Finally, write count(cs) is used to determine the number of committed writing transactions in cs since the most recent crash since cs.glb is initially 0 and reset to 0 by the recovery operation, and moreover, cs.glb is incremented twice by each writing transaction: once at line W2 and again at line E2 when the writing transaction commits. Relation globalRel comprises three main parts. We assume a program counter value RecIdle which is true for pc syst iff syst is not executing the recovery procedure. globalRel(cs, as) = (pc syst = RecIdle ⇒ cs.vstore = (last(as.mems) ⊕ writes(cs, as)) ∧

(1) write count(cs) + 1 = length(as.mems))) ∧

(2) (cs.vstore ⊕ cs.log) = last(mems(as)) ∧

(3) ∀ t.t = syst ∧ cs.pc t = NotStarted ⇒ as.pc t = NotStarted (4)

Conditions ( 1) and ( 2) assume that a recovery procedure is not in progress. By (1), the concrete volatile store is the last memory in as.mems overwritten with the write set of an in-flight writing transaction that has not linearized its commit operation. By (2), the number of memories recorded in the abstract state (since the last crash) is equal to write count(cs) + 1. By (3), the last abstract (persistent) store can by calculated from cs.vstore by overriding it with the mappings in log. Note that this is equivalent to undoing all uncommitted transactional writes. Finally, (4) ensures that every identifier for a transaction that has not started at the concrete level also has not started at the abstract level.

We turn now to txnRel. Its specification is very similar to the specification of txnRel in the proof of TML [START_REF] Derrick | Mechanized proofs of opacity: a comparison of two techniques[END_REF]. Therefore, we only provide a brief sketch below; an interested reader may consult [START_REF] Derrick | Mechanized proofs of opacity: a comparison of two techniques[END_REF] for further details. Part of txnRel maps concrete program counters to their abstract counterparts, which enables steps of the concrete program to be matched with abstract steps. For example, concrete pc values W1, W2, . . . , W6 correspond to abstract pc value doWrite(cs.addr t , cs.val t ), whereas W7 corresponds to writeResp, indicating that, in our proof, execution of line W6 corresponds to the execution of an abstract DoWrite t (cs.addr t , cs.val t ) operation. Moreover, as in the proof of TML [START_REF] Derrick | Mechanized proofs of opacity: a comparison of two techniques[END_REF], a set of assertions are introduced to establish as.validIdx(t, write count(cs)) for all inflight transactions t, which ensures that each transactional read and write is valid with respect to some memory snapshot.

Relation txnRel must also provide enough information to enable linearization of a commit operation against the correct abstract step. Note that DTMS2 distinguishes between read-only and writing transactions by checking emptiness of the write set of the committing transaction. To handle this, we exploit the fact that in DTML, writing transactions have an odd loc value if the cas at line W2 is successful and loc is incremented at W3, indicating that a writing transaction is in progress.

Finally, txnRel must ensure that the recovery operation is such that the volatile store matches the last abstract store in mems prior to the crash. To achieve this, we require that length(as.mems) = 1 when syst is executing the recovery procedure, and the volatile store for the address being flushed at C3 matches the abstract state before the crash, i.e., cs.vstore(cs.addr t ) = ((as.mems)(0))(cs.addr t ). Since the recovery loop only terminates after the log is emptied, this ensures that the concrete memory state is consistent with the abstract memory prior to executing any transactions after a crash has occurred.

In order to prove that our simulation relation is maintained by each step of the algorithm, we must use certain invariants of the DTML model. These invariants are similar to the corresponding invariants used in a proof of the original TML algorithm for the conventional volatile RAM model (see [START_REF] Derrick | Mechanized proofs of opacity: a comparison of two techniques[END_REF] for details). For example, our invariants imply that there is at most one writing transaction, and there is no such transaction when glb is even. The main additional invariant that we use for DTML constrains the possible differences between volatile and persistent memory: volatile and persistent memory are identical except for any location that has been written by a writer or by the recovery procedure but not yet flushed. This simple invariant combined with the global relation is enough to prove that the memory state after each crash is correct. Our DTML invariants have been verified in Isabelle, and can be found in the Isabelle files.

Related Work

Although there is existing research on extending the definition of linearizability to durable systems, there is comparatively less work on extending other notions of transactional memory correctness such as, but not limited to, opacity to durable systems. Various systems attempt to achieve atomic durability, transform general objects to persistent objects and provide a secure interface of persistent memory. The above goals usually require the use of logging which can be software or hardware based. Raad et al have proposed a notion of durable serialisability under relaxed memory [START_REF] Raad | Weak persistency semantics from the ground up: formalising the persistency semantics of armv8 and transactional models[END_REF], but this model does not handle aborted transactions.

ATLAS [START_REF] Chakrabarti | Atlas: Leveraging locks for non-volatile memory consistency[END_REF] is a software system that provides durability semantics for NVRAM with lock-base multithreaded code. The system ensures that the outermost critical sections, which are protected by one or more mutexes, are failure-atomic by identifying Failure Atomic Sections (FASEs). These sections ensure that, if at least one update that occurs to a persistent location inside a FASE is durable, then all the updates inside the session are durable. Furthermore, like DTML, ATLAS keeps an persistent undo log, that tracks the synchronisation operations and persistent stores, and allows the recovery of rollback FASEs that were interrupted by crashes.

Koburn et al. [START_REF] Coburn | Nvheaps: making persistent objects fast and safe with next-generation, non-volatile memories[END_REF] integrate persistent objects into conventional programs, and furthermore seek to prevent safety bugs that occur in predominantly persistent memory models, such as multiple frees, pointer errors, and locking errors. This is done by implementing NV-heaps, an interface to the NVRAM based on ACID transactions that guarantees safety and provides reasoning about the order in which changes to the data structures should become permanent. NV-heaps only handle updates to persistent memory inside transactions and critical sections. Other systems based on persistent ACID transactions include Mnemosyne [START_REF] Volos | Mnemosyne: Lightweight persistent memory[END_REF], Stasis [START_REF] Sears | Stasis: flexible transactional storage[END_REF] and BerkeleyDB [START_REF] Olson | Berkeley db[END_REF].

Ben-David et al. [START_REF] Ben-David | Delay-free concurrency on faulty persistent memory[END_REF] developed a system that can transform programs that consist of read, write and CAS operations in shared memory, to persistent memory. The system aims to create concurrent algorithms that guarantee consistency after a fault. This is done by introducing checkpoints, which record the current state of the execution and from which the execution can be continued after a crash. Two consecutive checkpoints form a capsule, and if a crash occurs inside a capsule, program execution is continued from the previous capsule boundary. We have not applied this technique to develop DTML, but it would be interesting to develop and optimise capsules in an STM context.

Mnemosyne [START_REF] Volos | Mnemosyne: Lightweight persistent memory[END_REF] provides a low-level interface to persistent memory with highlevel transactions based on TinySTM [START_REF] Felber | Dynamic performance tuning of word-based software transactional memory[END_REF] and a redo log that is purposely chosen to reduce ordering constraints. The log is flushed at the commit of each transaction. As a result, the memory locations that are written to by the transaction remain unmodified until commit. Each read operation checks whether data has been modified and if so, returns the buffered value instead of the value from the memory. The size of the log increases proportionally to the size of the transaction, potentially making the checking time consuming.

Hardware based durable transactional memory has also been proposed [START_REF] Joshi | Dhtm: Durable hardware transactional memory[END_REF] with hardware support for redo logging [START_REF] Joshi | Atom: Atomic durability in non-volatile memory through hardware logging[END_REF]. Other indicative hardware systems help implement atomic durability either by performing accelerated ordering or by performing the logging operation are [START_REF] Lu | Loose-ordering consistency for persistent memory[END_REF][START_REF] Nalli | An analysis of persistent memory use with whisper[END_REF].

Conclusions

In this paper we have defined durable opacity, a new correctness condition for STMs, inspired by durable linearizability [START_REF] Izraelevitz | Linearizability of persistent memory objects under a full-system-crash failure model[END_REF] for concurrent objects. The condition assumes a history with crashes such that in-flight transactions are aborted (i.e., do not continue) after a crash takes place, and simply requires that the history satisfies opacity [START_REF] Guerraoui | On the correctness of transactional memory[END_REF][START_REF] Guerraoui | Principles of Transactional Memory[END_REF] after the crashes are removed. This is a strong notion of correctness but ensures safety for STMs in the same way that durable linearizability [START_REF] Izraelevitz | Linearizability of persistent memory objects under a full-system-crash failure model[END_REF] ensures safety for concurrent objects. It is already known that TMS1 [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF], which is a weaker condition than opacity [START_REF] Lesani | Putting opacity in its place[END_REF] is sufficient for contextual refinement [START_REF] Attiya | Safety of live transactions in transactional memory: TMS is necessary and sufficient[END_REF]; therefore we conjecture that durable opacity can provide similar guarantees in a non-volatile context. For concurrent objects, more relaxed notions such as buffered durable linearizability [START_REF] Izraelevitz | Linearizability of persistent memory objects under a full-system-crash failure model[END_REF] have also been proposed, which requires causally related operations to be committed in order, but real-time order need not be maintained. Such notions could also be considered in a transactional memory setting [START_REF] Dongol | Transactions in relaxed memory architectures[END_REF], but the precise specification of such a condition lies outside the scope of this paper.

To verify durable opacity, we have developed DTMS2, an operational characterisation that extends the TMS2 specification with a crash operation. We establish that all traces of DTMS2 are durably opaque, which makes it possible to prove durable opacity by showing refinement between an implementation and DTMS2. We develop a durably opaque example implementation, DTML, which extends TML [START_REF] Dalessandro | Transactional mutex locks[END_REF] with a persistent undo log, and associated modifications such as the introduction of a recovery operation. Finally, we prove durable opacity of DTML by establishing a refinement between it and DTMS2. This proof has been fully mechanised in Isabelle.

Our focus has been on the formalisation of durable opacity and the development of an example algorithm and verification technique. Future work will consider alternative implementations of the algorithm, e.g., using a persistent set [START_REF] Zuriel | Efficient lock-free durable sets[END_REF], or thread-local undo logs [START_REF] Izraelevitz | Failure-atomic persistent memory updates via justdo logging[END_REF]. develop and implement a logging mechanism based on undo and redo log properties named JUSTDO logging. This mechanism aims to reduce the memory size of log entries while preserving data integrity after crash occurrences. Unlike optimistic transactions [START_REF] Chakrabarti | Atlas: Leveraging locks for non-volatile memory consistency[END_REF], JUSTDO logging resumes the execution of interrupted FASEs to their last store instruction, and then executes them until completion. A small log is maintained for each thread, that records its most recent store within a FASE, simplifying the log management and reduce the memory requirements. Future work will also consider weakly consistent memory models building on existing works integrating persistency semantics with hardware memory models [START_REF] Raad | Weak persistency semantics from the ground up: formalising the persistency semantics of armv8 and transactional models[END_REF][START_REF] Raad | Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model[END_REF].

Fig. 1 .

 1 Fig. 1. A durable Transactional Mutex Lock (DTML). Initially: glb = 0, log = emptyLog(). Line numbers for return statements are omitted and we use *addr for the value of addr

Definition 7 .

 7 A forward simulation from a concrete IOA C to an abstract IOA A is a relation R ⊆ states(C) × states(A) such that each of the following holds. Initialisation. ∀ cs ∈ start(C). ∃as ∈ start(A). R(cs, as) External step correspondence. ∀ cs ∈ reach(C), as ∈ reach(A), a ∈ external(C), cs ∈ states(C). R(cs, as) ∧ cs a -→ C cs ⇒ ∃as ∈ states(A). R(cs , as ) ∧ as a -→ A as Internal step correspondence. ∀ cs ∈ reach(C), as ∈ reach(A), a ∈ internal(C), cs ∈ states(C). R(cs, as) ∧ cs a -→ C cs ⇒ R(cs , as) ∨ ∃a ∈ internal(A), as ∈ states(A). R(cs , as ) ∧ as a -→ A as

This is in contrast to lazy implementations that defer transactional writes until the commit operation is executed (e.g.,[START_REF] Dalessandro | Norec: streamlining STM by abolishing ownership records[END_REF][START_REF] Dice | Transactional locking II[END_REF]).

All Isabelle theory files related to this proof may be downloaded from[START_REF] Bila | Defining and verifying durable opacity: Correctness for persistent software transactional memory[END_REF].

Bila and Dongol are supported by VeTSS project "Persistent Safety and Security". Dongol is supported by EPSRC grants EP/R019045/2 and EP/R032556/1. Derrick and Doherty are supported by EPSRC grant EP/R032351/1. Wehrheim is supported by DFG grant WE2290/12-1.

State variables: mems : seq(L → V), initially satisfying dom mems = {0} and initMem(mems(0)) pct : PCVal, for each t ∈ T, initially pct = notStarted for all t ∈ T beginIdxt : IN for each t ∈ T, unconstrained initially rdSett : L → V, initially empty for all t ∈ T wrSett : L → V, initially empty for all t ∈ T

where validIdx(t, n) = beginIdxt ≤ n < len(mems) ∧ rdSett ⊆ mems(n) Fig. 2. The state space and transition relation of DTMS2, which extends TMS2 with a crash event