Accountability allows to assign legal responsibility to an entity. It is the basis for many contracts, obligations or regulations, either for digital services or not. In our previous work we studied the Abstract Accountability Language for expressing accountability [BGRS15,RSDO16] with a logical focus. We demonstrate the AccLab tool support over a set of policies from the Hope University in Liverpool governing the use of their IT systems and computer resources. These policies are representative of terms of use and other agreements, being really part of the University management, under control of the University Council. Moreover, this application context is more familiar to the general public than other domains, such as nancial or health care services. One important task is to analyze and interpret these policies which are written in a natural, sometimes legal style. Of course, during this analysis we found many ambiguities, omissions, inconsistencies and other problems, but our purpose is to demonstrate that a part of it can be formalized and automatically veri ed. This paper presents the laptop user agreement policy and discussed its speci cation with our tool support.
The policy of interest is a set of seven texts from [Uni17] related to IT concerns and data protection. We will focus here on the laptop agreement. The laptop agreement is rather short (10 clauses), included below.
In accepting the use of a University laptop, I agree to the following conditions: 1. I understand that I am solely responsible for the laptop whilst in my possession 2. I shall only use the laptop for University related purposes. 3. I shall keep the laptop in good working order and will notify I.T. Services of any defect or malfunction during my use. 4. I shall not install and / or download any unauthorized software and / or applications 5. I shall not allow the laptop to be used by an unknown or unauthorized person.
I assume the responsibility for the actions of others while using the laptop. 6. I shall abide by the University Acceptable Use, Information Security and Portable Data Device security policies as published on the I.T. Services Website 7. Any work saved on the laptop will be deleted prior to the machine's return 8. If the laptop is lost, stolen or damaged, the incident must be reported to the
University Secretary's O ce within 24 hours 9. If the lost, stolen or damaged laptop and / or accessories is determined to be caused by negligence or intentional misuse, I shall assume the full nancial responsibility for repair costs or fair market value of the laptop. 10. I am aware that any breach of these policies may render me liable to disciplinary action under the University's procedures
In the remainder of this paper we will go through the exercise of formalizing and verifying this policy. 2.1
AAL Our policies are written with the Abstract Accountability Language (AAL) and we will comment the main constructions. In our approach, we consider that an accountability clause should express three things: a usage, an audit and a rectication. The usage expression describes access control, obligations, privacy concerns, usage controls, and more generally an expected behavior. In the course of the design of AAL we reviewed several related languages, and our requirements are aligned with several points raised by [BMB10]. Expressiveness is ensured by negation, unrestricted set of actions, type hierarchies, conditions and policy templates. We also advocate for a readable language with succinct unambiguous semantics. In this context we introduce notions of permission, interdiction and obligation, but we do not have the exact concepts of deontic logic since we want to get our approach free from paradoxes and we aim at reusing classic logic with its tool support. Point to point communications with messages passing, used by many related work, is a good abstraction, simple and exible. The audit and recti cation expressions are similar to usage expression but dedicated to auditing, punishment and remediation. The audit expression de nes a speci c audit event which triggers the auditing steps. The recti cation expression denotes actions that are done in case of usage violations. For instance, to punish the guilty party and to compensate the victim agent. We follow [Sch99,Mul00] which argue that punishments and sanctions are parts of accountability. AAL allows to de ne types with union, intersection, inclusion and negation to help in modeling data and roles. An action or a service call is represented as a message sender.action[receiver](parameters). The language enables predicates (pre xed by @) and if Type is a type, @Type denotes its associated unary predicate. Authorizations are denoted by the PERMIT and DENY keywords pre xing an action or an expression. The language provides Boolean operators, rst-order quanti ers and linear temporal operators. We need to de ne policies and to reuse them thus we implement a notion of template (introduced by TEMPLATE) which improves readability and structuration. A template enables to name a policy with parameters (called with @template) but it also supports higher-order de nitions helpful in de ning common schemas of accountability or usage. 2.2
As we can see in the policy from Section 2, sentences are often vague but sometimes they contain more precise information. It is the case in other policies like the data protection, data portable or information security policies. Thus we did a rst reading of all the policies to extract some elements about the information system. From that, we conclude that the \I" is referring to a student or a sta of the university (named here resp) which is explicitly de ned as of type EligibleUser in the IT usage policy. In fact another kind of person (AllPerson) appears in clause 5 which obliged us to reconsider clause 2 with a di erent meaning as other persons may use the laptop assigned to resp.
As a rst simple example the clause 10 above states that \disciplinary action under the University's procedures" may take place in case of breach. This de nes the policy recti cation and we represent it as an abstract action in Listing 1.1 with a simple policy with a typed parameter. LHU is a constant denoting the University representative lawyer, it may be a ctitious or a real person.
TEMPLATE LHURectificationPolicy (resp:AllPerson)
(IF (@EligibleUser(@arg(resp))) THEN {LHU.disciplinaryAction[@arg(resp)]()})) In the laptop policy there is no more information about recti cation and nothing about audit. This last can be reduced to auditor.audit[LHU](). As in the case of recti cation once we have more details, the template construction allows to re ne these de nitions. A large section of the laptop policy describes in fact information about permissions, prohibitions, obligations and some conditions. Most of this usage policy will be described by a template named laptopUA, see Listing 1.2. Only our interpretation of few clauses is given but this policy covers clauses 1 to 9. The rst line says that if a person is permitted to use a laptop then he is an eligible user and this laptop was assigned to him. We also assume that the eligible user should bring back his assigned laptop in the future to the university secretary.
TEMPLATE laptopUA(resp:AllPerson)( (FORALL laptop:Laptop FORALL p:Purpose (IF (PERMIT @arg(resp).use[laptop](p))
THEN {@EligibleUser(@arg(resp)) AND @assigned(@arg(resp), laptop)})) AND (FORALL laptop:Laptop FORALL p:Purpose (IF (@EligibleUser(@arg(resp)) AND @assigned(@arg(resp), laptop))
THEN {SOMETIME (@arg(resp).bringBack[LHUsecretary]())})) AND ...) They are many things which are left implicit, are wrong or skipped in natural language policies. One important bene t is that problems and omissions appear during the speci cation phase or will be detected by the veri cation tools.
The laptop clause 2 is simple, however, it interacts with the clause 5 which leaves open the use of the laptop by a known and authorized person, maybe a colleague. But in fact we do not have information about which kind of person is permitted and for what kind of purposes. Other technical problems occur with the clause 5, 7 and 8: they need explanations, as we will see later. Finally, the overall structure of the laptop accountability policy is as in Listing 1.3. The accountability policy has two parts, the rst is related to all clauses except clause 7 which is related to the second part.
The ACCOUNT and ACCUNTIL templates de ne accountability schemas. Let us describe the most classic which is quite similar to the one used in our previous papers, see Listing 1.4.
TEMPLATE ACCOUNT(UE:Template, RE:Template) ( ALWAYS (auditor.audit[LHU]() AND (IF (NOT(@arg(UE)))
THEN {ALWAYS (IF (auditor.audit[LHU]()) THEN {@arg(RE)})}))) This template assumes that the audit is simple and at each instant (in linear time) if the usage (@arg(UE)) is not satis ed then recti cation (@arg(RE)) applies in case of an audit. The ACCUNTIL will be discussed later. Note that for clause 7 we diverge from the original text and we choose a weaker recti cation to illustrate the language exibility. 3
Formal speci cations are bene cial but they are really more e ective if we have tool support and preferably some automated veri cation means. Thus we develop AccLab for Accountability Laboratory to experiment the speci cation, veri cation and monitoring of accountability policies. AccLab is compound from a set of tools which are: The component editor, the AAL editor and its veri cation, and the monitoring tools. The last release of AccLab is version 2.2 which was released on July 23, 2017 on github (https://github.com/hkff/AccLab) under GPL3 license. The AccLab IDE is a web interface that provides a component diagram editor and tools to work with the AAL language. The backend is written in Python3 and the front-end in JavaScript based on dockspawn (http://www.dockspawn.com) which is a web based dock layout engine released under MIT license. For veri cation purposes AccLab is interacting with the TSPASS tool ([LH10]), a prover for rst-order linear temporal logic (FOTL). The implementation is still in progress we will give an overview of its main current features. Some features like the full type constructions and the template are not fully operational thus we mix the use of AccLab and the TSPASS prover with some manual manipulations to process our example.
To manage more easily the AAL language a dedicated editor has been implemented. This editor is directed by the syntax and highlights the language keywords. There are syntactic checking but also semantic controls for type checking and the consistency of the declared services. A panel in the editor arranges a set of tools providing assistance in writing by the use of dedicated templates, for instance generating type declarations, accountability clauses or speci c privacy expressions. This panel also contains few veri cation tools mainly the conict checking with localization and the compliance checking. AccLab translates the AAL language into FOTL and the checking tools use the connection with TSPASS and its satis ability algorithm. In case of unsatis ability we implemented a mean to isolate the minimal core unsat. The tool provides macro calls which are useful in automating some complex tasks related to the translation to FOTL and the interaction with TSPASS.
One idea behind AccLab is to see accountability in action, and one way to achieve that is to be able to run simulations. AccLab includes a simulation module that allows it to monitor agents in a system and to observe accountability in action. We also proposed a tool called AccMon which reuses the above monitoring principles and provides means to monitor accountability policies in the context of a real system. 4
This is an ongoing work but from now on we formalize several parts. One important task was to built and partly invent the information system and to get it consistent. 4.1
The basic accountability scheme for a given usage is expressed simply as (UE OR RE), or equivalently IF (NOT UE) THEN RE, where UE is the usage expression and RE the recti cation expression. However, often we need quanti ers, for instance to identify the responsible user. We also consider time and our choice was to consider linear time as it seems su cient in many cases. Thus we write formulas like ALWAYS FORALL resp:Any IF (NOT UE(resp)) THEN RE(resp), or FORALL resp:Any ALWAYS IF (NOT UE(resp)) THEN RE(resp). These are two distinct schemas, the rst implies the second but the reverse is false (it is related to the Barcan formula).
Note that the above scheme allows to de ne rst order accountability, that is the user is responsible and will be subject to recti cation in case of a violation. But it is possible to de ne second order accountability, that is the processor or implementer is responsible to enforce IF (NOT UE) THEN RE and in case of violation it is recti ed with RE2. In this case, the schema will be (UE OR RE OR RE2), and more generally higher-order responsibility is de ned as (UE OR RE OR ... OR REn). Templates are useful here to capture relevant accountability schemas. 4.2
We consider to have a full speci cation of the laptop agreement but it evolved since our rst speci cation. We prove the satis ability with most of the types and actions declarations and we also prove that violation of every clause will result in a recti cation of the responsible person. As a general comment it is always possible to represent any kind of information but without semantics it remains purely syntactic. Of course aligning the syntax between di erent policies is a non obvious requirement. In our work we elaborate a rich information model resulting from the analyzing of most of the 7 policies. We have a type hierarchy with nearly 50 types and 50 relations, a set of 40 actions and more than 40 predicates and constants. This is a critical task because there is more or less nothing in the texts and sometimes they have some aws. An important part is to add some behaviours to link together actions and predicates. Except type relations the action and predicate the behaviour is still poor but may be enriched later with the analysis of other policies.
The overall structure of the laptop policy has been given in Listing 1.3. We succeed in proving the satis ability of the clauses and taking into account some user behaviours. The FOTL formula generation takes around 3s, the prover generates a total of around 1000 conjunctive normal forms in less than one second. We express several di erent user behaviours, for instance (see Listing 1.5) once a user signs the policy he gets an assigned laptop and accept the policy until he leaves.
FORALL res:AllPerson FORALL laptop:Laptop
ALWAYS (IF (resp.signed[LaptopAccountabilityPolicy]())
THEN {(@assigned(resp, laptop) AND @template(LaptopAccountabilityPolicy, resp))
UNTIL (resp.leave[LHU]())}) Indeed, the interaction between the proper user behaviour and the policy is a critical point for semantic reasons but it also brings some di culties about quanti ers. The above formula is not monodic (this is a constraint for decidability of satis ability) and we reformulate it with the laptop quanti er inside the accountability policy rather than in the user behaviour.
With the laptop clause 7 there is a technical point to discuss. The simplest formulation is to use an UNTIL operator, however this is more tricky to align with our ACCOUNT accountability clause which is based on a ALWAYS pattern. One solution is to use the principles of the separated normal form, for instance from [Fis11]. We can rewrite this expression as an ALWAYS clause without the need of the UNTIL operator. However, the result is not intuitive and only understandable by specialists of linear logic. We implement another solution that is to de ne a separate accountability clause based on a di erent pattern. This pattern is ACCUNTIL = (A UNTIL B) | (A AND NOT B) UNTIL NOT (A OR B). The second term of this pattern represents a part of the negation of the rst, and then the case where recti cation should happen. This pattern is not equivalent to the A UNTIL B OR NOT (A UNTIL B) scheme, but the di erence is on the negative part. This di erence is an in nite trace which is not really monitorable thus it can be discarded. Nevertheless, this behaviour introduces new quanti ers and the satis ability process does not terminate. We reconsider it and succeed with a weaker speci cation (see Listing 1.6) and additional behaviour for the delete action.
FORALL laptop:Laptop IF (@assigned(resp, laptop) AND resp.bringBack[LHUsecretary](laptop))
THEN {@deletedSavedWork(resp)}
The clause 8 introduces a notion of real time with \before 1 day", while we have a construction for that we choose to replace it with a NEXT construction. In fact there are only three such references in all the 7 policies. But during the veri cation step we realize that it is not su cient because: It is acceptable that the user reports immediately and this is not acceptable that he reports after two states. Furthermore the ALWAYS pattern is not correct since the recti cation may occur before the violation will be e ectively realized. Thus, as for clause 7, a separate accountability pattern can be used, see Listing 2.
FORALL laptop:Laptop (IF (@EligibleUser(resp) AND @assigned(resp, laptop)
AND (@lost(laptop) OR @damaged(laptop) OR @stolen(laptop))) THEN {(resp.report[LHUsecretary](problem)
OR (NEXT (resp.report[LHUsecretary](problem))))}) Another important point to note is related to clause 5 which states that \I assume the responsibility for the actions of others while using the laptop". The \I" is represented by resp in our usage policy and appears at the level of the accountability policy, see Listing 1.3. From that we can verify that if another user did a breach with the laptop assigned to resp then recti cation is e ectively applied to the responsible person. These veri cations where successfully done, however, not without some technical di culties. 4.3
This is an ongoing work, as we need to complete our information model, to formalize other policies and at least to verify their consistency. The current natural language policies have many drawbacks: lack of precision, redundancies, ambiguities etc, unsurprisingly. Regarding accountability there are some information about monitoring and really few details about the remediation, compensation and punishment parts. One important task before any formalization of the policies is to build a consistent information model with su cient relevant details about data and behaviour.
There are ambiguities about the status of some statements and our language's strength in clarifying them. For instance, in several policies (laptop, IT usage) there are sentences related to the fact that a person will sign and accept a policy. If we consider it as a part of the accountable usage it will say that to not sign is a breach which is not sensible. Thus it should be part of the proper user behavior, it is free to sign, and if he signs he will accept the responsibilities included in the policy. As we have seen, this impacts the structure of the speci cation but also brings some di cult points regarding the interaction between quanti ers and modal operators.
The use of FOTL or linear temporal logic often simpli es the speci cation and there is only few references to precise dates or dense time in the policies. However, there are several subtleties in writing formulas with both quanti ers and temporal operators. FOTL is quite expressive but the bottleneck is the tool support, there is only one, TSPASS, which is now not maintained. Another problem is that it relies on the monodic constraint which is constraining for the behaviour speci cation. Improvements are possible here but need important theoretical and implementation e orts. Another point is the use of the standard semantics based on in nite traces which is not suitable for real monitoring. The alternative is a translation into pure FOL, the drawback is the explicit management of time parameters. These additional parameters may compromise the decidability of satis ability but this logic has been intensively studied and a complete map of the decidable fragments exists. An adaptation of our language and its tool support is perfectly possible and it seems a sensible future perspective.