Context-aware security: Linguistic mechanisms and static analysis

1. Introduction

If you are in an airport for a little while and you want to have just a quick look at your mailbox, you would like to connect without bothering with all the details of the wireless connection, yet you would like to do that in a secure manner. A hosting environment and an application programmed in an adaptive fashion will transparently connect you to the available server. So, you never need to change your settings and capabilities, nor to worry about the new context and the resources it provides you. Instead you are likely to be worried about malicious activities that the hosting environment may carry on, and vice versa. Nevertheless, adaptivity amplifies the difficulties of security provisioning, because these two features are tightly interwoven. Their combination requires addressing two aspects. First, security may reduce adaptivity, because it adds further constraints on the possible actions of software. Second, new highly dynamic security mechanisms are needed to scale up to adaptive software.

These are the problems we address here from a linguistic point of view, in particular within a static analysis approach. To analyse such highly dynamic applications with a standard technique one has to take care of all the contexts that will be visited. This is computationally expensive and may even be unfeasible, because new contexts may appear later on, e.g. a new wireless network at the airport. We propose a technique that addresses these difficulties by splitting the analysis in two parts. The first collects at compile time information about the behaviour of the application regardless of the running context, while the second specialises this information at load time when the context is fully known.

Context and adaptivity. As intuitively anticipated above, today’s software systems are expected to operate every time and everywhere. They have to cope with changing environments, and never compromise their intended behaviour and their non-functional requirements, typically security or quality of service. Therefore, languages need effective mechanisms to sense the changes in the operational environment in which the application is plugged in, i.e. the context, and to properly adapt to changes, with little or no user involvement. At the same time, these mechanisms must maintain the functional and non-functional properties of applications after the adaptation steps.

The context is a key notion for adaptive software. Typically, a context includes different kinds of computationally accessible information coming from both outside (e.g. sensor values, available devices, code libraries offered by the environment), and from inside the application boundaries (e.g. its private resources, user profiles, etc.). There have been many different proposals to support dynamic adjustments and tuning of programs inside programming languages, e.g. [38,39,42,45,64,66,67]. However, they do not neatly separate the working environment from the application as done, e.g. in Context Oriented Programming (COP) [20]. The COP linguistic paradigm explicitly deals with contexts and provides programming adaptation mechanisms to support dynamic changes of behaviour, in reaction to changes in the context. In this paradigm software adaptation is programmed through behavioural variations, chunks of code that can be automatically selected depending on the current context hosting the application, so to dynamically modify its execution.

Security and contexts. Security is a major concern in context-aware systems, as witnessed by the interest risen in the business world [44], because an activity can be carried on safely in one operating environment and become weak in another. This implies that one has to determine which information in the environment is relevant for the security of the application. Also, it is important to constantly tune the security policies accordingly to the changes of the relevant part of the environment. New security techniques are therefore in order, that have to both scale up and maintain the ability of software to adapt as much as possible. These two interrelated aspects have already been studied in the literature [14,68] that presents two ways of addressing it: securing context-aware systems and context-aware security.

Securing context-aware systems aims at rethinking the standard notions of confidentiality, integrity and availability [58] and at developing techniques for guaranteeing them in adaptive applications [68]. The main challenge is to understand how to get secure and trusted context information. Contexts may indeed contain sensible data of the working environment (e.g. information about surrounding digital entities) that should be protected from unauthorised access and modification, in order to grant confidentiality and integrity. Also, one has to protect applications from portions of the context that may misbehave and forge deceptive data.

Context-aware security is dually concerned with the use of context information (identity, location, time and date, device type, reputation and so on) to dynamically improve and drive security decisions. Contextual information helps to overcome the “one-size-fits-all” security solutions. These now become more flexible because they can take into account the different situations in which a user is operating. For example, consider the usual no flash photography policy in museums. While a standard security policy never allows people to use flash, a context-aware security one does not allow flashing only inside particular rooms – in other words, the last policy has a scope. Similarly, a company might allow a user to access a database from the office, but deny access if the user attempts to from home, without an explicit authorisation. Accordingly, controlling and enforcing security need not to be placed everywhere, but only where needed, depending on the context that makes specific actions risky.

Yet, there is no unifying concept of security, because the two aspects above are often tackled separately. Indeed, mechanisms have been implemented at different levels of the infrastructure, in the middleware [60] or in the interaction protocols [29]. These mechanisms mostly address access control, often from a software engineering viewpoint [56]. Also, particular attention is being paid on the ways contextual policies are defined [48]. Ours is a first step towards developing a uniform and formal treatment of security and adaptation.

Our proposal. We study security within a linguistic approach to adaptivity, and we propose techniques for analysing and enforcing secure behaviour of adaptive applications since the early stages of software development. To investigate these issues, we chose the COP paradigm because it provides us with a neat framework, where contexts and applications are clearly defined and identified, even though strictly intertwined. Consequently, this separation reduces the complexity of the security analysis by first considering the application in isolation, and then by tailoring the obtained results to the running context.

Here we extend ML CoDa , a core of ML with COP features, recently proposed in [21–23]. It has two tightly integrated components: a declarative constituent for programming the context and a functional one for computing. The bipartite structure of ML CoDa  reflects the separation of concerns between the specific abstractions for describing a context and those used for programming applications [61]. The context in ML CoDa  is a knowledge base implemented as a (stratified, with negation) Datalog program [43,55]. Applications inspect the contents of a context by simply querying it, in spite of possibly complex deductions required. Programming adaptation is specified through behavioural variations, a sort of pattern matching with Datalog goals as selectors. The behavioural variation to be run is selected by the dispatching mechanism that inspects the actual context and makes the right choices. Note that the choice depends on both the application code and the “open” context, unknown at development time. If no alternative is viable, then a functional failure occurs as the application cannot adapt to the current context. We address context-aware security issues, in particular for defining and enforcing access control policies, by exploiting ML CoDa  features. Our policies are expressed in Datalog, and are checked and enforced by just querying goals. In this regard, our version of Datalog is an asset because many logical languages for defining access control policies compile in it, e.g. [12,26,41]. In addition, it is powerful enough to express all relational algebras, it is fully decidable, and it guarantees polynomial response time [27]. There are two kinds of policies separately imposed by the context and by the applications. A single reference monitor enforces both at run time, aborting the execution when a security violation is about to occur.

More in detail, the designer of the context can define a context policy to protect some sensible entities hosted therein, e.g. specific devices or confidential data. The reference monitor prevents then an application running in that context from altering the values of the protected entities. Context policies are enforced along the execution of the application within the current context. Actually, the reference monitor is not required to stepwise supervise the execution of the controlled application, rather it only intervenes when an assertion concerning a protected entity changes in the context.

Instead, application policies are defined by the designer of the application, to protect its own resources and data. Following [9], we extend the original ML CoDa  with the construct ψ [ e ] , called policy framing, where ψ is one of such policies and e is an expression within the application itself. The intuition is that the policy ψ has to be enforced stepwise during the execution of e, which is therefore its scope; when e is reduced to a value, the policy is no longer active. For example, suppose e is sending some confidential data. Then a policy can check whether all the recording devices in the context are off, so this sort of de-classification is not risky. When the transmission is completed, a recorder can be safely switched on, if the rest of the application does not care about. Of course, application policies can be nested, and are to be all obeyed by an expression occurring within the (nested) scope of their framing.

Observe that context and application policies have a different nature, mainly because they are defined by separate designers, in a completely independent manner. Actually, context policies are most likely unknown to the application developer at design and implementation time, and similarly for the application policies that are unknown to the context manager.

The execution model underlying our proposal assumes that the context is the interface between an application and the system running it. Applications interact with the system through a predefined set of APIs that provide handles to resources and operations on them. The system and the application do not trust each other, and may act maliciously. For instance, the first can alter some parts of the context inserting specific assertions so forcing the application to select a particular behavioural variation. The system can then falsify these assertions to drive the application in an unsafe state. The application developer can design and enforce a policy to protect sensible data against these malicious changes. In turn, the application can modify the context arbitrarily by driving the system in a vulnerable state, and context policies prevent these attacks. As a matter of fact, our policies specify the acceptable runs with respect to access control, so they are safety policies.

Here we do not address how code is protected against hostile modifications, and for that we assume our execution model to rely on known techniques, e.g. obfuscation [16]. A key point of our proposal is the instrumentation of the application code by inserting invocations to a reference monitor, and the resulting machinery is assumed to be suitably protected.

We aim at detecting policy violations (non-functional failures) as early as possible, so we conservatively extend the static approach of [22,23,28], briefly summarised below. It takes care of failures in adaptation to the current context (functional failures), dealing with the fact that applications operate in an “open” environment. Indeed, the actual value and even the presence of some elements in the current context are only known when the application is linked with it at run time. The first phase of our static analysis is based on a type and effect system that, at compile time, computes a safe over-approximation of the application behaviour, namely the effect. Then the effect is used at load time to verify that the resources required by the application are available in the actual context, and in its future modifications. To do that, the effect of the application is suitably combined with the effect of the APIs provided by the context that are computed by the same type and effect system. If an application passes this analysis, then no functional failure can arise at run time.

Our extensions are as follows. First, we record in the approximations the operations that modify the context, namely tell and retract , together with the scope of the policy framings in which they occur. The collected information is then used by our extended load time analysis. It requires building a graph, which safely approximates which contexts the application will pass through, while running. We also label the edges of the graph with (pointers to) the tell / retract operations in the code, exploiting the approximation. Before launching the execution, we detect the risky actions, i.e. those that might violate a reachable context or an active application policy. Now, we can call our reference monitor to guard the risky actions only, and leave it switched off for the remaining ones. Note that our two-phase analysis is similar to enforcing invariants over global data [52], which are however completely known at compile time. In our case instead the context is not available until run time, so an analysis at compile time would require predicting all the possible contexts an application will interact with – this is clearly overwhelming, or even unfeasible at all.

The detection of risky actions mentioned above drives code instrumentation, so to build applications that are prevented from violating security policies at run time. In a sense, the reference monitor is incorporated within the instrumented application, only using constructs of ML CoDa  itself. Actually, the monitor is implemented by inserting in the source code of the application e a call to a suitable procedure (essentially a behavioural variation) for each occurrence of a tell / retract occurring in e. This form of instrumentation is not standard, as it does not operate on the object code, rather it is mechanically done at implementation time. Given a specific action and a set of policies, this procedure will obviously check whether the first obeys all the elements of its second argument. At load time, the information about which actions are risky and which policies can be violated by them is then used to link the actual and the formal parameters of the procedure. Indeed, the reference monitor is never called on those actions that the static analysis has safely predicted not to affect security.

Structure of the paper. The next section introduces ML CoDa  and our proposal, with the help of an example, along with an intuitive presentation of the various components of our two-phase static analysis, and the way security is dynamically imposed and enforced. The syntax and the operational semantics of our extension of ML CoDa  are in Section 3, and its type and effect system in Section 4. Section 5 presents the load time analysis, the results of which are used in Section 6 to describe our way of instrumenting applications. The conclusion summarises our results, discusses some future work, and briefly surveys related approaches. The proofs of the theorems establishing the correctness of our proposal are in the Appendices.

A preliminary version of some technical parts of this paper appeared in [11], that only considered context policies, and consequently had simpler definitions of the dynamic semantics, of the static analysis, and of the code instrumentation.

2. A guided tour of our proposal through an enterprise mobility scenario

We illustrate our proposal by considering a scenario of enterprise mobility, a typical example of ubiquitous and flexible computing: a mobile application used for accessing to some databases of a company through a tablet. For further details about the language and other applicative scenarios see [21,23].

We first intuitively introduce ML CoDa , focussing on its logical aspects, used to inquire and update the context, and on our extensions to ML, used to program adaptation in a functional way. In particular, we will emphasise on how an application installs itself in a context (Section 2.1) and how the main adaptation feature, namely behavioural variation, is resolved through the dispatching mechanism (Section 2.2). In Section 2.3 we will add to our example both a context and an application policy, and discuss why at run time two different techniques are required for enforcing each of them. Then in Section 2.4, we exemplify two different ways an application may fail, either because it cannot adapt to the hosting context (functional failure) or because it or the context attempt to violate a policy (non-functional failure). We also describe the two-phase static analysis we are proposing for detecting both kinds of failures and for efficiently controlling policies at run time. The first phase occurs at compile time and determines a sound abstraction of the behaviour of applications. The second phase analyses this abstraction at load time and provides us with the basis for instrumenting the code and for defining an adaptive reference monitor, that is only called on need. We conclude this intuitive presentation of our main contributions by briefly looking at some classical access control policies that show the expressivity of ML CoDa .

2.1. Context description and updates

As anticipated, the context in ML CoDa  is a knowledge base implemented as a (stratified, with negation) Datalog program [43,55]. To retrieve the state of a resource, programs simply query the context, in spite of the possibly complex deductions required to solve the corresponding goal; the context is changed by using the standard tell / retract constructs.

In our example, the usage of the tablet depends on the current location and on the profile of who is using it. For simplicity, we suppose that the tablet is able to recognise three locations each providing access to the network: (i) office, (ii) home, and (iii) public spots. Information on the current location can be retrieved by querying the context, described by a set of Datalog clauses. In our case, the user’s location is described by the following clauses (for clarity, Datalog variables will be capital letters, while constants will be lower case identifiers):

Assuming a mechanism that connects the tablet to a specific network, the predicate wifi_connected identifies the current operating environment by the network name. In particular, the tablet results to be in the office (the predicate location(office) holds) when connected to the network in either the west or east wing of the building.

The company employees can perform different actions depending on their profiles. We assume to have three of them: (i) vendor, (ii) system administrator, (iii) admin staff. The profile of a user is represented in the context by the binary fact profile (e.g. profile(Jane,vendor)). As expected, the user profile enables different applications and features: for example, vendors can access a database of customers, but not the company balance of payments; while a member of the staff can access both.

Furthermore, the context represents the resources currently available and manages the access to them in a declarative manner. Below we discuss some examples of different kinds of resources.

In the code snippet below, the first case returns a handle for accessing the contents of a digital archive that is stored in the office server, the second for the archive in a public server:

Of course, also physical or hybrid resources can be represented using Datalog, as the following typical situation arising in the Internet of Things [57]. Suppose that employees can remotely control the thermostat of their office room R, through the handle S, e.g. for checking whether their own is on or off.

In ML CoDa  there are two manners for dynamically updating a context. The first exploits the API provided by the system, e.g. a function disconnect for closing the connection with a specific network. The second one is more explicit: a programmer can use the Datalog primitive constructs tell and retract that add and remove facts. In our example, a system administrator can change the profile of an employee, e.g. moving Bob to the vending department, as follows:

2.2. Behavioural adaptation

The ML CoDa  code in Fig. 1 implements a simple application which accesses a database and performs a query to retrieve data about customers. The labels of the expressions tell , retract , and psi are not part of the code, and will be mechanically added for supporting the static analysis; they will be discussed later on and are to be ignored for the time being. The behaviour of the application depends on the location and on the profile of the user: when inside the office, the user can directly connect to and query the database. Otherwise, the communication exploits a proxy which allows getting the database handle.

OPEN IN VIEWER

Fig. 1.

A simple ML CoDa  application.

A first example of specific ML CoDa  construct, namely context-dependent binding, is at line 2 where the name for the office archive is taken from the context and bound to the variable db_name. The idea is to implement a simple form of adaptivity of data because the actual value is extracted from the current context, only known at run time. As a matter of fact, the value of db_name depends on the location of the user as prescribed by the definition of office_archive. The retrieved value is then used by open_db to open a connection to the database.

The core of the snippet above is the behavioural variation (lines 3–18) bound to records that downloads the table of customers. Behavioural variations change the program flow in accordance to the current context. Syntactically, they are similar to pattern matching, where Datalog goals replace patterns and variables can additionally occur: a behavioural variation is a list G 1 . e 1 , … , G n . e n where the expressions e i are guarded by Datalog goals G i . In the code above, there are two alternatives, starting at lines 4 and 9 respectively. The selection between them depends on the location and on the capabilities of the current employee. To be more precise, behavioural variations are a sort of functional abstractions and their application triggers a specific dispatching mechanism that inspects the context and selects the expression e i guarded by the first goal G i satisfied. If no guards are satisfied, the computation gets stuck, as the application behaviour is undefined in that specific context: the application cannot adapt to it and a functional failure occurs.

In our example, the application behaves differently depending on the current location of the vendor, as intuitively shown in Fig. 2. If the vendor is inside the office, he can directly access customers data connecting to db1; when outside, he has to first connect to the company proxy, then he can access db2 through a secure channel; otherwise the application raises an error because running in an unexpected context. Note that every resource available to the application, is only accessible through a handle provided by the context and only manipulated through system functions provided by the API.

If the second case is selected, the IP address of an available proxy is retrieved by the predicate proxy that binds the corresponding handle to the variable ip. Then the application calls the API function connect to establish a communication through chan. By exploiting this channel the application gets a handle to the database (through the API function get_db at line 13) in order to obtain the required data. Accessing and releasing the relevant database is notified by updating the context through the tell and retract actions at lines 5, 12 and 8, 18, respectively. Note that the third argument of crypto_query at line 15 is a lambda expression (in a sugared syntax) that invokes another API function select-from (as common, we assume that the cryptographic primitives are supplied by the system). Other resources and APIs occur in the snippet above: the database connection channel c at line 6, the cryptographic key k at line 10, and open_db at line 6, query at line 7, decrypt at line 16.

The code lines 15 and 16 are within the scope of the application policy psi, discussed in the next section. It guards the execution of the calls to crypto_query and decrypt: intuitively the policy psi guarantees the compatibility of the cryptographic key k and of the channel c.

OPEN IN VIEWER

Fig. 2.

A flow chart intuitively describing the function main.

2.3. Security policies

We now discuss how the context protects itself against misuses by applications and symmetrically how applications constrain the usage of their data and resources. For that, ML CoDa  provides two kinds of security policies: context and application policies. As a matter of fact, policies predicate on the context, so they are easily expressed in Datalog and enforced by the deductive machinery of ML CoDa . As anticipated, the enforcement of a context policy ω is done by a reference monitor that checks the validity of ω right before every context change, i.e. before executing each tell / retract . Checking whether an application policy ψ is obeyed by a context has to be done continuously by the reference monitor, actually before and after each reduction step. Below we describe some examples of both kinds of policies.

Since the boundaries between personal and business space and time are blurred, the company adopts security policies to limit certain functionalities such as access to data from outside the office. In this scenario, the employees have different access rights: the vendors, among which Jane and Bob, can access the databases from both inside and outside the office, and the following facts specify which databases Bob and Jane can access, whereas the predicate allows an administrator to grant permissions:

A context policy that controls how vendors access the database db2 from outside the office follows

Pictorially, the dotted circles in Fig. 2 (blue in the pdf) represent that every modification of the context requires checking the policy omega.

As an example, if Jane is outside the office, no violation occurs. Instead, if Bob attempts to access the database from outside and has no delegation from the administrator, the policy omega is infringed at line 12. Of course policies can take into account any other kind of contextual information. One may e.g. constrain less the accesses of a vendor if he is using a corporate tablet whose running operating system is trusted. Also, a policy can prohibit vendors from accessing any databases during the week-ends.

As intuitively introduced above, the application policy psi regulates the usage of cryptographic keys and communication channels. We assume that the application has its own private key k, stored in the application context. The communication infrastructure offers channels supporting different cryptographic protocols. The application is designed in such a way that the key used is compatible with the protocol sec_protocol associated with the channel c returned by the call get_db(chan). Context information is therefore used for choosing the suitable cryptographic protocol for the communication [40]. For simplicity, here compatibility means that the protocol can use keys of a certain length, following the context-agile encryption technique of [59]. Formally

Note that an application policy cannot be rendered by a behavioural variation, because its guards are only checked when it is applied. Instead, the goal corresponding to the check of an application policy is queried by the reference monitor at each execution step. Assume in our simple example above that the protocol used to communicate and the channel c are compatible, but that the API crypto_query selects another protocol which is not compatible. Consequently, psi holds when entering the policy framing and a behavioural variation replacing line 14 will succeed at that execution point. However, a security violation occurs thereafter, because the case of the behavioural variation has been already selected. Instead our mechanism for application policy detects the violation: psi is indeed enforced step-wise along the execution of the API functions crypto_query (and decrypt) as intuitively shown by the dotted rectangle in Fig. 2 (purple in the pdf).

2.4. Failures, static analysis and instrumentation

An application fails to adapt to a context (functional failure), when it has not been designed for the actual hosting context, e.g. because a missing facility was assumed to be present. In our example, this happens when a vendor attempts to access the database from home. A functional failure is reflected by a failure of the dispatching mechanism that causes the computation to get stuck. As a matter of fact, adaptive applications are prone to a new class of run time errors that are hard to catch, since the running contexts are unpredictable.

Another kind of failure happens when an application does not manipulate resources as expected (non-functional failure) and causes a violation of a policy. As said above, in our example Bob infringes the context policy omega when attempting to access the database db2 if not delegated to. Another example is the violation of the application psi occurring when the key k is too short for the protocol associated with the channel c in lines 14–17.

To avoid functional failures and to optimise policy enforcement, we extend the two-phase static analysis of ML CoDa  [22,23]. This analysis consists of (i) a type and effect system, and (ii) a control-flow analysis. It checks whether an application will be able to adapt to its execution contexts, and detects which contexts possibly violate the required policies.

In more detail, at compile time, we associate a type and an effect with an expression e. The type is (almost) standard, and the effect is an over-approximation of the actual run time behaviour of e, called history expression. The effect abstractly represents the changes and the queries performed on the context during its evaluation. The second phase occurs at load time and exploits the history expression to build a graph describing how the context may evolve during the execution.

For example, the history expression associated by the type system with the behavioural variation records is the following: H records = ask G 1 . tell F 1 l 1 · H open _ db · H query · retract F 1 l 2 ⊗ ask G 2 . H connect · tell F 2 l 3 · H get _ db · ψ l 4 [ H crypto _ query · H decrypt ] · retract F 2 l 5 ⊗ fail . In H records the symbol · abstracts sequential composition; ψ represents the application policy psi; ask G 1 . ⋯ ⊗ ask G 2 . ⋯ ⊗ fail is the abstract counterpart of the behavioural variation records, where ⊗ sequentially composes the pair of effects associated with a guard and its expression; goals G 1 and G 2 represent the goals at lines 4 and 9, respectively; facts F 1 and F 2 are accessing(db1) and accessing(db2).

History expressions are labelled (for the sake of readability, we just show the relevant ones in H records ). These labels enable us to link the abstract actions in histories to the corresponding actions of the code, that we assume labelled by the compiler. For instance, the tell F 1 l 1 in H records corresponds to the tell at line 5 in records, which is labelled by 1; the ψ l 4 is similarly linked to the policy framing with label 4. All the correspondences are { l 1 ↦ 1 , l 2 ↦ 2 , l 3 ↦ 3 , l 4 ↦ 4 , l 5 ↦ 5 } (the abstract labels that do not annotate tell / retract actions or policies have no counterpart; also, the correspondence needs not to be injective as it happens in this example).

At load time, the virtual machine of ML CoDa  performs two steps: linking and verification. The first step resolves the system names, and constructs the initial context C, by combining the one of the application with the system context that includes information on the current state, e.g. available resources and their usage constraints. The linking step also checks the logical consistency of the context C. The verification first checks whether no functional failure occurs, i.e. whether the application adapts to all evolutions of C that may occur at run time. If this is the case, the application will not be run. Then, the analysis looks for the points in the code where non-functional failures can occur, i.e. when the application may act against the policies established by the system that loads the program, and vice versa. This information is used to drive the activation of a run time monitor by need.

To perform our analysis conveniently and efficiently, we build a graph G describing the possible evolutions of the initial context C, through a control flow analysis of the history expression H. The nodes of G over-approximate the contexts arising at run time and its edges carry (the labels of) the actions which change the context. A distinguished aspect of our analysis is that it depends on the initial context C, right because our application may behave correctly in one context and fail in another, so this analysis can only be done at load time.

Back to our example, we consider three cases depending on different initial contexts, depicted in Fig. 3, where for the sake of brevity we collapsed parts of the graph as a single edge labelled by the relevant history expression. The first initial context C home records that the vendor is at home (predicate wifi_connected(myplace) holds). Since no case of the behavioural variation records can be selected because the application is not designed to work in that context. No guards are satisfied, and the dispatching mechanism fails. A pictorial representation of this functional failure is in Fig. 3: the failure node ⋇ (red in the pdf) is reachable from the initial one. Suppose now that in the context C Bob the predicate current_usr(Bob) holds. The tell F 2 l 3 is risky because it may violate the context policy omega (actually it does), therefore the corresponding action, labelled by 3 in the code, must be blocked. For achieving this, it suffices switching on the run time monitor, right before executing this operation. Another potential non-functional failure arises when the cryptographic key and the protocol are not compatible (the application policy psi is violated). This is shown in Fig. 3 assuming as done above that the crypto_query may cause the violation. Again the correspondence between the label l 4 in the history expression and the label 4 in the code indicates that the run time monitor has to be switched on when entering the scope of the policy psi and switched off when leaving it. Of course, if in context C 1 one proves that the cryptographic key and the protocol agree, there is no potential non-functional failure and the application runs without any monitoring.

OPEN IN VIEWER

Fig. 3.

Three evolution graphs showing a functional failure (assuming that wifi_connected(myplace) holds in C home ) and two policy violations. The context policy omega is not obeyed because the user in C Bob is Bob; the application policy psi is violated because the key is not compatible with the protocol. The dotted edges will be cut off by the run time monitor.

2.5. Other examples of security policies

We conclude the intuitive presentation of our proposal with a few examples showing how Datalog expresses other policies and how we manage them. In particular, we consider below delegation, dynamic activation and deactivation of policies, and a way of controlling which data in a context a user is allowed to access.

Imagine that the company allows a vendor to delegate another vendor to access the data of a particular customer without resorting to the system administrator as done above. Such a delegation is represented in the context as the fact grant_permission(user1, user2) meaning that the employee user2 can operate in place of the employee user1. So a tell of this fact suffices to activate the delegation. Of course, the delegation is better constrained by the following policy that forbids a member of the staff to delegate a vendor and vice versa:

In order to dynamically activate or deactivate context policies, we require that their definition includes a fact, that acts as an activation flag. If this fact holds in the current context, then the corresponding policy is active, otherwise it is not. So the context manager can activate/deactivate a policy by simply changing the value of the corresponding flag. For example, take the policy omega above regulating the accesses to the database db2 from the outside. Its dynamic version is the following where policy_flag is the activation flag:

We can also express policies that control which parts of the context an application is allowed to modify, by suitably guarding the facts to be protected by a context policy. For example, the following one bans the users blacklisted from retracting a specific fact F. The first case of omega3 requires that the fact F always holds in a context where the current user is blacklisted. Any attempt to remove F leads to a violation of the policy, while this is not the case if the user is allowed to retract F.

Suppose that the cryptographic algorithm used by crypto_query and decrypt are energy consuming. The following policy protects our application to run short of battery, when it wraps lines 15 and 16:

3. ML CoDa

Below, we survey the syntax and the semantics of ML CoDa , along with some small examples to illustrate its peculiar constructs; for more details see [23].

Syntax.  ML CoDa  consists of two components: Datalog with negation to describe the context, and a core ML extended with COP features. The Datalog part is standard: a program is a set of facts and clauses.

Let Var (ranged over by x , y , … ), Const (ranged over by c , n , … ) and Predicate (ranged over by P , … ) be a set of variables, of basic constants and of predicate symbols, respectively. The syntax is x ∈ Var c ∈ Const P ∈ Predicate ω , ψ ∈ Policies u : : = x ∣ c u ∈ Term A : : = P ( u 1 , … , u n ) A ∈ Atom L : : = A ∣ ¬ A L ∈ Literal cla : : = A ← B . cla ∈ Clause B : : = ϵ ∣ L , B B ∈ ClauseBody F : : = A ← ϵ F ∈ Fact G : : = ← L 1 , … , L n . G ∈ Goals

As usual in Datalog, a term is a variable x or a constant c; an atom A is a predicate symbol P applied to a list of terms; a literal is a positive or a negative atom; a clause is composed by a head, i.e. an atom, and a body, i.e. a possibly empty sequence of literals; a fact is a clause with an empty body and a goal is a clause with empty head. We let goals be ranged over by G, with the intuition that it occurs in a behavioural variation. Context and application policies are ranged over by ω and ψ, respectively. As expected, a policy is obeyed if and only if the corresponding goal holds. For simplicity, we assume that there is a unique context policy Ω (referred in the code as Omega), resulting from the conjunction of all the relevant policies.

In the following, we assume that each Datalog program is safe and stratified [18] (our world is closed, so we can deal with negation). As anticipated in the Introduction, our version of Datalog can express all relational algebras, is fully decidable, and guarantees polynomial response time [27]. Also, many logical languages for defining access control policies follow this stratified-negation-model, e.g. [12,26,41].

The functional part inherits most of the ML constructs. In addition to the usual ones, our values include Datalog facts F and behavioural variations. Moreover, we introduce the set x ˜ ∈ DynVar of parameters, i.e. variables that assume values depending on the properties of the running context, while x , f ∈ Var are identifiers for standard variables and functions, with the proviso that Var ∩ DynVar = ∅ . The syntax of ML CoDa  is below. Va : : = G . e ∣ G . e , Va Variations v : : = Values c ∣ λ f x . e ∣ ML-like Values ( x ) { Va } ∣ Behavioural Variations F Facts e : : = Expressions v ∣ x ∣ e 1 e 2 ∣ let x = e 1 in e 2 ∣ if e 1 then e 2 else e 3 ∣ ML-like Expressions x ˜ ∣ Parameters dlet x ˜ = e 1 when G in e 2 ∣ Context-dependent Binding tell ( e 1 ) l ∣ retract ( e 1 ) l ∣ Context update e 1 ∪ e 2 ∣ Append Operator # ( e 1 , e 2 ) ∣ Variation Application ψ l [ e ] Policy Framing To facilitate our static analysis (see Section 5) we associate each tell / retract and each policy ψ with a different label l ∈ Lab C ; labels do not affect the dynamic semantics, which is defined below.

Standard expressions are evaluated in the usual way. Very briefly, a variable x evaluates to the value it is bound. Both expressions in an application are to be evaluated to values v 1 and v 2 , and if v 1 = λ f x . e , the evaluation goes on by substituting v 1 for all the (free) occurrences of f in e and v 2 for those of x. The evaluation of a let is that of e 2 where all the (free) occurrences of x have been replaced by the value of e 1 . Conditionals evaluate as expected.

The COP-oriented constructs of ML CoDa  include behavioural variations ( x ) { Va } , each consisting of a variation Va , i.e. a list G 1 . e 1 , … , G n . e n of expressions e i guarded by Datalog goals G i (x free in  e i ). At run time, the first goal G i satisfied by the context selects the expression e i to run (dispatching). For instance, in Section 2, we declared the behavioural variation records, that returns information on customers, by accessing to different databases depending on the vendor’s location.

Context-dependent binding is the mechanism to declare variables whose values depend on the context. The dlet construct implements the context-dependent binding of a parameter x ˜ to a variation Va . Note that context-dependent binding is designed for expressing adaptability of data, while behavioural variations express adaptability of control flow.

The tell and retract constructs assert and retract facts in the context, provided that no violation of security occurs.

The append operator e 1 ∪ e 2 concatenates behavioural variations, so allowing dynamic composition.

A behavioural variation # ( e 1 , e 2 ) applies e 1 to its argument e 2 . To do so, the dispatching mechanism is triggered to query the context and to select from e 1 the expression to run, if any.

Furthermore, we use the construct ψ l [ e ] , called policy framing, to guarantee that the context obeys the policy expressed by ψ while running e. With this construct programmers can protect their application from a possible misuse of the running context C. We require ψ to be true in C until e completes its execution, and then the scope of the policy framing is left and the policy de-activated. Also, policy framings can be nested, with the intuition that an expression enclosed in many of them is executed only if the running context obeys them all. The (context) policies ω are instead imposed by the context, to protect its sensible data and devices from a misuse of an application, during its entire evaluation. We will formalise later on how both kinds of policies will be enforced. We presented some examples in the previous section: omega is the (part of) context policy that only allows vendors with explicit authorisation to access the database db2; omega3 controls which parts of the context an application is allowed to modify.

Semantics. The Datalog component has the standard top-down semantics [18]. Given a context C ∈ Context and a goal G, we let C ⊨ G with θ mean that the goal G, under a ground substitution θ, is satisfied in the context C.

The SOS semantics of ML CoDa  is defined for expressions with no free variables, but possibly with free parameters, thus allowing for openness. To this aim, we have an environment ρ, i.e. a function mapping parameters to variations DynVar → Va . A transition ρ ⊢ C , e → C ′ , e ′ represents a single evaluation step. It says that under the environment ρ the expression e is evaluated in the context C and reduces to e ′ changing C to C ′ . The initial configuration is ρ 0 ⊢ C , e p , where ρ 0 contains the bindings for all system parameters, and C results from joining the predicates and facts of the system and of the application e p .

OPEN IN VIEWER

Fig. 4.

The reduction rules for the ML-like constructs of ML CoDa .

OPEN IN VIEWER

Fig. 5.

The reduction rules for the constructs of ML CoDa  concerning adaptation and policies.

Figures 4 and 5 show the inductive definitions of the reduction rules for ML CoDa : we briefly comment below on those for our new constructs.

The rules (Dlet1) and (Dlet2) for the construct dlet , and the rule (Par) for parameters implement our context-dependent binding. For brevity, we assume here that e 1 contains no parameters. The rule (Dlet1) extends the environment ρ by appending G . e 1 in front of the existent binding for x ˜ . Then, e 2 is evaluated under the updated environment. Note that the dlet does not evaluate e 1 , but only records it in the environment in a sort of call-by-name style. The rule (Dlet2) is standard: the whole dlet reduces to the value to which e 2 reduces.

The (Par) rule looks for the variation Va bound to x ˜ in ρ. Then, the dispatching mechanism selects the expression to which x ˜ reduces. The dispatching mechanism is implemented by the partial function dsp , defined as follows dsp ( C , ( G . e , Va ) ) = ( e , θ ) if C ⊨ G with θ , dsp ( C , Va ) otherwise . It inspects a variation from left to right looking for the first goal G satisfied by C, under a substitution θ. If this search succeeds, the dispatching mechanism returns the corresponding expression e and θ. Then, x ˜ reduces to e θ , i.e. to e, whose variables are bound by θ. Instead, if the dispatching fails because no goal holds, the computation gets stuck, because the program cannot adapt to the current context.

As an example of context-dependent binding, consider the simple conditional expression if x ˜ = F 2 then 42 else 51 , in an environment ρ that binds the parameter x ˜ to e ′ = G 1 . F 5 , G 2 . F 2 and in a context C that satisfies the goal G 2 , but not G 1 : ρ ⊢ C , if x ˜ = F 2 then 42 else 51 → C , if F 2 = F 2 then 42 else 51 → C , 42 , where we first retrieve the binding for x ˜ (recall it is e ′ ), with dsp ( C , e ′ ) = ( F 2 , θ ) , for a suitable substitution θ. Since facts are values, we can bind them to parameters and test their equivalence by a conditional expression.

The application of the behavioural variation # ( e 1 , e 2 ) evaluates the subexpressions until e 1 reduces to ( x ) { Va } and e 2 to a value v. Then, the rule (VaApp3) invokes the dispatching mechanism to select the relevant expression e from which the computation proceeds after v is substituted for x. Also in this case the computation gets stuck, if the dispatching mechanism fails. As an a example, consider the behavioural variation ( x ) { G 1 . c 1 , G 2 . x } and apply it to the constant c 2 in a context C that satisfies the goal G 2 , but not the goal G 1 . Since dsp ( C , ( x ) { G 1 . c 1 , G 2 . x } ) = ( x , θ ) for some substitution θ, we get: ρ ⊢ C , # ( ( x ) { G 1 . c 1 , G 2 . x } , c 2 ) → C , c 2 .

The rules (Tell1, Tell2) update the context by asserting a fact, that is a value of ML CoDa ; similarly (Retract1, Retract2) retract a fact (note that labels are immaterial here, and will only be used in the static analysis). The new context C ′ , obtained from C by adding/removing F, is checked against the security policy Ω (recall that we assume to join all the context policies in the single one Ω). In this way we prevent the application from damaging the context, as exemplified below. We can easily reuse our dispatching machinery above: we implement the check as a call to the function dsp where the first argument is C ′ and the second one is Ω . ( ) , the trivial variation with goal Ω. If this call produces a result, then the evaluation yields the unit value and the new context C ′ .

The following example shows the reduction of a retract in a context C = { F 3 , F 4 , F 5 } , under a context policy Ω requiring that the fact F 4 always holds. Let f = λ x . if e 1 then F 5 else F 4 and evaluate retract f ( ) ℓ . If e 1 evaluates to false (without changing the context), the context eventually produced violates the policy in hand, dsp ( C \ { F 4 } , Ω . ( ) ) fails, and therefore the evaluation gets stuck: ρ ⊢ C , retract f ( ) ℓ → ∗ C , retract F 4 ℓ ↛ , where ↛ means that no transition goes out from C , retract F 4 ℓ . If, instead, e 1 reduces to true , there is no policy violation and the evaluation reduces to unit : ρ ⊢ C , retract f ( ) ℓ → ∗ C , retract F 5 ℓ → { F 3 , F 4 } , ( ) . The rules for e 1 ∪ e 2 sequentially evaluate e 1 and e 2 until they reduce to behavioural variations (rules (Append1, 2)). Then, they are concatenated together by renaming bound variables to avoid name captures (rule (Append3)). The policy ψ of the application e is also enforced along its evaluation when asserting or retracting a fact by rule (Frame1). Before performing one of these actions, the ψ has to be shown true in the context C, and the changes made on the context must preserve ψ true, i.e. C ′ ⊨ ψ . This check is implemented at run time through a call to the dispatching mechanism, as suggested in the comment to the rules for tell / retract . The rule (Frame2) simply discards the framing, so it de-activates the policy ψ as soon as a value is produced.

Back to the example of Section 2, assume that Jane wants to access the database from outside the office, then we have the following computation ( → + indicates a non empty computation): ρ ⊢ C , #(records, customers) → + C ′ , psi 4 [e] → + C ″ , psi 4 [decrypt(k,data)] , where e is the code at lines 15 and 16. From the first to the second configuration the dispatching mechanism queries the context C and selects the second case of records. From the third to the fourth configuration the connection to the database is established and the data are retrieved. The framing construct checks the policy psi at each step of this computation.

Note that imposing a context policy ω to an application e could be intuitively implemented by wrapping its whole code within the framing ω [ e ] , at load time. However, monitoring context and application policies is done differently, and separation of concerns and efficiency reasons strongly suggest us keeping them apart.

We now associate an ML CoDa  expression with a type, an abstraction called history expression, and a function called the labelling environment. During the verification phase, the virtual machine uses the history expression to ensure that the dispatching mechanism will always succeed at run time. The labelling environment helps in selecting which portions of the code may lead to violations of the security policies, and in instrumenting the code with suitable calls to a run time monitor. First, we briefly present History Expressions and labelling environments, and then the rules of our type and effect system.

4.1. History expressions

A history expression is a term of a simple process algebra that soundly abstracts program behaviour [10,63]. Here, they over-approximate the sequence of actions that an application may perform over the context at run time, i.e. asserting/retracting facts and asking if a goal holds. History expressions also record the application policies that are to be enforced. We assume that a history expression is uniquely labelled on a given set of Lab H . Labels will be used to link static actions in histories to the corresponding dynamic actions inside the code; we feel free to omit them when immaterial. The syntax of History Expressions is as follows: H ∋ H : : = ∍ ∣ ϵ l ∣ h l ∣ ( μ h . H ) l ∣ tell F l ∣ retract F l ∣ ( H 1 + H 2 ) l ∣ ( H 1 · H 2 ) l ∣ ψ l [ H ] ∣ Δ , Δ : : = ( ask G . H ⊗ Δ ) l ∣ fail l .

The empty history expression abstracts programs that do not interact with the context. For technical reasons, we syntactically distinguish when the empty history expression comes from the syntax ( ϵ l ), and when it is instead obtained by reduction in the semantics (∍ that is unlabelled). With μ h . H we represent possibly recursive functions, where h is the recursion variable; the “atomic” history expressions tell F and retract F are for the analogous constructs of ML CoDa ; the non-deterministic sum H 1 + H 2 abstracts if - then - else ; the concatenation H 1 · H 2 is for sequences of actions that arise, e.g. while evaluating applications; the history expression ψ l [ H ] is the abstract version of the security framing; Δ mimics our dispatching mechanism, where Δ is an abstract variation, defined as a list of history expressions, each element H i of which is guarded by an ask G i . For instance, the history expression H records intuitively introduced in Section 2 abstracts the behavioural variation records in Fig. 1.

OPEN IN VIEWER

Fig. 6.

Semantics of History Expressions.

Given a context C, the behaviour of a history expression H is formalised by the transition system inductively defined in Fig. 6. A transition C , H → C ′ , H ′ means that H reduces to H ′ in the context C and yields the context C ′ . Most rules are similar to the ones of [10]: below we only comment on those dealing with the context and with the policy framings. The rules for Δ scan the abstract variation and look for the first goal G satisfied in the current context; if this search succeeds, the whole history expression reduces to the history expression H guarded by G; otherwise the search continues on the rest of Δ. If no goal is satisfiable, the stuck configuration C , fail is reached, meaning that the dispatching mechanism fails.

An action tell F reduces to ∍ and yields a context C ′ , where the fact F has just been added; similarly for the action retract F . Differently from what we do in the semantic rules, here we do not consider the possibility of a violation of a context policy ω: a history expression approximates how the application would behave in the absence of any kind of check imposed by the context.

The rules for policy framings are much alike those of the dynamic semantics: a non-empty history expression H can transform into H ′ , provided that in both the starting context C and in the next one C ′ the policy ψ holds; when ∍ is reached, the policy framing is left.

Labelling environment. We assume as given the function μ : Lab H → H that recovers a construct in a given history expression H ∈ H from a label l ∈ Lab H . Using μ, we can link the occurrences of tell , retract and ψ in a history expression to the corresponding operations in an expression e (labelled on Lab C , see Section 3), while type-checking e. This correspondence is recorded in the auxiliary labelling environment introduced below. It will later on help in instrumenting the code.

Definition 4.1 (Labelling environment).

A labelling environment is a (partial) function Λ : Lab H → Lab C , defined only if μ ( l ) ∈ { tell ( F ) , retract ( F ) , ψ } .

We shall write ⊥ for the function undefined everywhere.

As anticipated in Section 2, the labelling environment { l 1 ↦ 1 , l 2 ↦ 2 , l 3 ↦ 3 , l 4 ↦ 4 , l 5 ↦ 5 } puts in correspondence the labels of the history expression H records with those in the code snippet in Fig. 1. Note that labelling environments need not to be injective.

4.2. Typing rules

We assume that each Datalog predicate has a fixed arity and a type (see e.g. [51]). From here onwards, we also assume that there exists a Datalog typing function γ that, given a goal G, returns a list of pairs (x, type-of-x), for all variables x ∈ G .

The rules of our type and effect system have:

the usual environment Γ : : = ∅ ∣ Γ , x : τ , binding the variables of an expression; ∅ denotes the empty environment, and Γ , x : τ denotes an environment having a binding for the variable x (x not in the domain of Γ). A standard assumption is to have an initial environment containing the signatures of the APIs;

a further environment K : : = ∅ ∣ K , ( x ˜ , τ , Δ , Λ ) , that maps a parameter x ˜ to a triple consisting of a (i) type, (ii) an abstract variation Δ, used to solve the binding for x ˜ at run time, and (iii) a labelling environment Λ that links the tell , retract and ψ occurring in Δ to the corresponding operations in an expression e; K , ( x ˜ , τ , Δ , Λ ) denotes an environment with a binding for the parameter x ˜ ( x ˜ not in the domain of K).

Our typing judgements have the form Γ ; K ⊢ e : τ ⊳ H ; Λ and express that in the environments Γ and K the expression e has type τ, effect H and yields a labelling environment Λ.

Our types are either basic τ c ∈ { int , bool , unit , … } for constants and variables, or functional types for functions and behavioural variations, or types for facts: τ : : = τ c ∣ τ 1 → K ∣ H ; Λ τ 2 ∣ τ 1 ⟹ K ∣ Δ ; Λ τ 2 ∣ fact ϕ , ϕ ∈ ℘ ( Fact ) .

Some types are annotated for analysis reasons. In fact ϕ , the set ϕ contains the facts that an expression can be reduced to at run time (see the semantics rules (Tell2) and (Retract2)).

In the type τ 1 → K ∣ H ; Λ τ 2 associated with a function f, the environment K stores the types and the abstract variations of the parameters occurring inside the body of f, and represents a precondition needed to apply it. The history expression H is the latent effect of f, i.e. the sequence of actions that may be performed over the context during the function evaluation. The labelling environment Λ links (some of) the labels of H to those occurring in the body of f.

Similarly, the behavioural variation bv = ( x ) { Va } has type τ 1 ⟹ K ∣ Δ ; Λ τ 2 , where K is a precondition for applying bv ; Δ is an abstract variation, that represents the information used at run time by the dispatching mechanism to apply bv ; and Λ is as above.

We now introduce four partial orderings ⊑ H , ⊑ Δ , ⊑ K , ⊑ Λ on H, Δ, K and Λ, respectively, and we often omit the indexes when no ambiguity may arise. Below the symbol ⊎ stands for disjoint union, the type ordering ⩽ is defined in Fig. 7, and we assume that fail ⊗ Δ = Δ , so Δ ′ ⊗ Δ will have a single trailing fail . H 1 ⊑ H H 2 ⟺ ∃ H 3 such that H 2 = H 1 + H 3 , Δ 1 ⊑ Δ Δ 2 ⟺ ∃ Δ 3 such that Δ 2 = Δ 1 ⊗ Δ 3 , K 1 ⊑ K K 2 ⟺ ( ( x ˜ , τ 1 , Δ 1 , Λ 1 ) ∈ K 1 K 1 ⊑ K K 2 ⟺ ⟹ ( x ˜ , τ 2 , Δ 2 , Λ 2 ) ∈ K 2 and τ 1 ⩽ τ 2 and Δ 1 ⊑ Δ Δ 2 and Λ 1 ⊑ Λ Λ 2 ) , Λ 1 ⊑ Λ Λ 2 ⟺ ∃ Λ 3 such that dom ( Λ 3 ) ∩ dom ( Λ 1 ) = ∅ and Λ 2 = Λ 1 ⊎ Λ 3 .

OPEN IN VIEWER

Fig. 7.

The subtyping relation.

The rules of our type and effect system inherited from ML are displayed in Fig. 8, while the others are introduced in Figs 9 and 10.

OPEN IN VIEWER

Fig. 8.

Typing rules for ML-like constructs of ML CoDa .

OPEN IN VIEWER

Fig. 9.

Typing rules for context updates.

ML-inherited rules. We briefly comment on the most relevant rules in Fig. 8. In the rules (Tconst), (Tvar) and (Tabs) the labelling environment is empty. The rule (Tif) is standard, apart from the resulting labelling environment that is the (disjoint) union of those of the components e i . Same for (Tlet) and for (Tapp) where the labelling environment of the latent effect is also considered. Note that in the conclusion of (Tapp), the precondition of the latent effect of e must be included in the environment K to guarantee that all parameters will be duly bounded. The rule (Tabs) is standard, except for the way the environments K and Λ are handled. As usual, the actual effect guessed in the premise becomes latent in the conclusion of the rule, while the effect and the labelling environment become empty; note that in the premise the guessed parameter environment is the one used for typing e, while the guessed effect H and the guessed labelling environment Λ are those of e.

Context rules. The rules for the constructs that handle the context are in Fig. 9. A few comments follow. The rule (Tfact) gives a fact F type fact annotated with { F } and the empty effect. The rule (Ttell) asserts that the expression tell ( e ) has type unit , provided that the type of e is fact ϕ . The overall effect is obtained by combining the effect of e with the non-deterministic summation of tell F , where F is any of the facts in the type of e. The current labelling environment is extended with links from the elements of ϕ to the label of tell ( e ) . Similarly for (Tretract). In rule (Tvariation) we determine the type for each subexpression e i under K ′ , and the environment Γ, extended by the type of x and of the variables y → i occurring in the goal G i (recall that the Datalog typing function γ returns a list of pairs (z, type-of-z) for all variables z of G i ). Note that all subexpressions e i have the same type τ 2 , but of course they have different effects and labelling environments. We also require that the abstract variation Δ results from concatenating ask G i with the effect computed for e i . The arrow in the type of the behavioural variation is annotated by K ′ , Δ and by the union of all the labelling environments Λ i . Consider e.g. the behavioural variation bv 1 = ( x ) { G 1 . e 1 , G 2 . e 2 } . Assume that the two cases of this behavioural variation have type τ and effects H 1 and H 2 , respectively, under the environment Γ , x : int (goals have no variables) and the guessed environment K ′ . Hence, the type of bv 1 will be int ⟹ K ′ ∣ Δ τ with Δ = ask G 1 . H 1 ⊗ ask G 2 . H 2 ⊗ fail , while the effect will be empty.

OPEN IN VIEWER

Fig. 10.

Typing rules for adaptation and security.

Rules for adaptation and security. In Fig. 10 we list the rules dealing with adaptation and security. The rule (Tsub) allows us to freely enlarge types and effects by applying the subtyping and subeffecting rules (and the orderings on them). Also the labelling environment can be enlarged, and it is required to be defined on all the labels of the (larger) history expression H ( Lab ( H ) ). The rule (Tdvar) associates x ˜ with the triple stored in the environment K. The rule (Tdlet) requires that e 1 has type τ 1 in the environment Γ extended with the types for the variables y → of the goal G. Also, e 2 has to type-check in an environment K, extended with the information for parameter x ˜ . The type and the effect for the overall dlet expression are the same as e 2 , while the labelling environment is the union of those of e 1 , e 2 and of the one coming from x ˜ . The rule (Tappend) asserts that two expressions e 1 , e 2 with the same type τ, except for the abstract variations Δ 1 , Δ 2 in their annotations, and effects H 1 and H 2 , are combined into e 1 ∪ e 2 with type τ, and concatenated annotations and effects. The rule (Tvapp) type-checks behavioural variation applications and reveals the role of preconditions. As expected, e 1 is a behavioural variation with parameter of type τ 1 and e 2 with type τ 1 . We get a type if the environment K ′ , which acts as a precondition, is included in K according to ⊑. The type of the behavioural variation application is that of the result of e 1 , and the effect is obtained by concatenating the ones of e 1 and e 2 with the history expression Δ, occurring in the annotation of the type of e 1 . The overall labelling environment results from joining those of the subexpressions and of the latent effect.

Finally, in the single rule for the security framing (Tframe), the effect computed for e is wrapped with the policy ψ, and the labelling environment is the union of that of e with a link from the occurrence of ψ in the history expression to the corresponding one in the code.

5. Load time analysis

Our execution model for ML CoDa  extends the one in [23]: the compiler1

Technically, we compute G through a static analysis, specified in terms of Flow Logic [54]. To ease the formal development, we assume below that all the bound variables occurring in a history expression are distinct. So it is straightforward to define, by structural induction, a function K mapping a variable h l to the history expression ( μ h . H 1 l 1 ) l 2 that introduces it.

The static approximation is represented by a quadruple ( Σ ∘ , Σ ∙ , Ψ ∘ , Ψ ∙ ) , called estimate for H, with Σ ∘ , Σ ∙ : Lab H → ℘ ( Context ∪ { ⋇ } ) and Ψ ∘ , Ψ ∙ : Lab H → ℘ ( Policies ) , where ⋇ is the distinguished “failure” context representing a dispatching failure. For each label l we define the following four sets:

the pre-ctx Σ ∘ ( l ) and the post-ctx Σ ∙ ( l ) , containing the contexts possibly arising before and after evaluating H l , respectively;

The notion of acceptability has been used in [22,23] to check whether the history expression H, hence the expression e it is an abstraction of, will never fail in a given initial context C (made of the system and the application contexts) because the dispatching mechanism does not succeed. Here, we also detect which actions, if any, may violate the security policies in force.

In the following we introduce into two parts (shown in Figs 11 and 12, respectively) the set of inference rules that validate the correctness of a given estimate E = ( Σ ∘ , Σ ∙ , Ψ ∘ , Ψ ∙ ) . As expected, the checks in the clauses mimic the semantic evolution of the history expression in a given context, by modelling the semantic preconditions and the consequences of the possible reductions.

OPEN IN VIEWER

Fig. 11.

Specification of the analysis for History Expressions associated with standard ML expressions.

OPEN IN VIEWER

Fig. 12.

Specification of the analysis for History Expressions for adaptation and security.

Rules for the standard construct. The rules for the history expressions that abstract standard ML expressions are in Fig. 11. The rule (Aeps) says that the estimate E is acceptable for the “syntactic” ϵ l if the pre-sets are included in the corresponding post-sets.

The rules (Aseq1) and (Aseq2) handle the sequential composition of history expressions. The first rule states that ( Σ ∘ , Σ ∙ , Ψ ∘ , Ψ ∙ ) is acceptable for H = ( H 1 l 1 · H 2 l 2 ) l if it is valid for both H 1 and H 2 . Moreover, the pre-ctx of H 1 must include the pre-ctx of H and the pre-ctx of H 2 includes the post-ctx of H 1 ; finally the post-ctx of H includes that of H 2 . Just the same condition is required for the pre- and post-pol. The second rule states that E is acceptable for H = ( ∍ · H 1 l 2 ) l if it is acceptable for H 1 and the pre-ctx (pre-pol, respectively) of H 1 includes that of H, while the post-ctx (post-pol, resp.) of H includes that of H 1 .

By the rule (Asum), E is acceptable for H = ( H 1 l 1 + H 2 l 2 ) l if it is valid for each H 1 and H 2 ; the pre-ctx of H is included in the pre-sets of H 1 and H 2 ; the post-ctx of H includes those of H 1 and H 2 ; and the same inclusions hold between the pre- and the post-pol.

By the rule (Arec), E is acceptable for H = ( μ h . H 1 l 1 ) l if it is valid for H 1 l 1 , the pre-ctx (pre-pol, resp.) of H 1 includes that of H; and the post-ctx (post-pol, resp.) of H includes that of H 1 .

Finally, the rule (Avar) says that ( Σ ∘ , Σ ∙ , Ψ ∘ , Ψ ∙ ) is an acceptable estimate for a variable h l if the pre-ctx (pre-pol, resp.) of the history expression introducing h, namely K ( h ) , is included in that of h l , and the post-ctx (post-pol, resp.) of h l includes that of K ( h ) .

Rules for adaptation and security. We now introduce and discuss the rules for adaptation and security, displayed in Fig. 12.

The rule (Anil) says that every pair of functions is an acceptable estimate for the “semantic” empty history expression ∍ (the empty history expression reached after a successful execution).

In the rule (Atell), we check whether the context C is in the pre-ctx, and C ∪ { F } is in the post-set, while the pre-pol have to be included in the post-pol; similarly for (Aretract), where C ∖ { F } should be in the post-set.

The rules (Aask1) and (Aask2) handle the abstract dispatching mechanism. The first states that E is acceptable for H = ( ask G . H 1 l 1 ⊗ Δ l 2 ) l , provided that, for all C in the pre-ctx of H, if the goal G succeeds in C then the pre-ctx of H 1 includes that of H and the post-ctx of H includes that of H 1 . Otherwise, the pre-ctx of Δ l 2 must include the pre-ctx of H and the post-ctx of Δ l 2 is included in that of H. The rule (Aask2) requires ⋇ to be in the post-ctx of fail l . Note that this implies that the dispatching mechanism may fail at run time. Needless to say, in both rules the same inclusions must hold between the pre- and the post-pol.

Finally, through the rule (Aframe) we say that E is acceptable for H ′ = ψ l [ H l ′ ] if it is such for H l ′ ; if the pre-ctx (pre-pol, resp.) of H ′ is included in the pre-ctx (pre-pol, resp.) of H l ′ ; if the post-ctx of H ′ includes that of H l ′ ; if additionally the policy ψ belongs to the pre-pol of H ′ and the post-pol of H ′ without ψ (recall that the framing is left) is included in the post-pol of H l ′ . In other words, all the policies that have to be enforced before entering the policy framing for ψ are still active when the framing is left, and furthermore ψ is in force entering the framing and is de-activated when leaving it.

Semantic properties. We now formalise the notion of valid estimate for a history expression, plugged in a context; we prove that there always exists a minimal valid analysis estimate; and that a valid estimate is correct with respect to the operational semantics of history expressions. Valid estimates then soundly approximate the behaviour of history expressions.

It is easy to partially order the set of analysis estimates by set inclusion, component-wise, and to prove that they are a Moore family. Since such families contain a least element (as well as a greatest one), there always exists a least choice of ( Σ ∘ , Σ ∙ , Ψ ∘ , Ψ ∙ ) that is acceptable. The existence of a least estimate is stated below.

The next theorem guarantees that the analysis estimates are preserved under execution steps.

Viability of history expressions. We now define when a history expression H is viable for an initial context C, i.e. when it passes the verification phase at load time, following [22,23]. Actually, a viable H never evaluates to fail, and the expression the behaviour of which it abstracts will never get stuck, because the dispatching mechanism fails.

Note that if the minimal valid estimate satisfies the requirement above, then no other valid estimate will violate it, because of the Moore family property.

Intuitively, the nodes of G are sets of contexts reachable from C by running H, and we label them with the policies of the application that are to be enforced. An edge between two nodes C 1 and C 2 says that C 2 is obtained from C 1 , through an action tell or retract , a reference to which is recorded in the edge label. Note in passing that the graph is a compact and easy way to manipulate representation of the information computed by the analysis, and that it paves the ways for more involved verification mechanisms. For example, one could check CTL formulas on it, where the atomic propositions are Datalog goals. Consider again the history expressions H p and H p ′ and their evolution graphs G p and G ′ p in Figs 13 and 14. In G p , from the initial context C there is an edge labelled { 1 } to C ∪ { F 1 } , because of tell F 1 1 , and there is an edge labelled { 5 } to the C ∖ F 8 , because of retract F 8 5 . Of course, all the nodes are labelled by ∅, since no policy occurs in H p . A simple reachability algorithm suffices in showing H p viable for C (even less, as ⋇ does no occur in G p ). Instead, ⋇ is a reachable node of G ′ p showing H p ′ not viable. In addition, in H p ′ there are two application policies, and so the nodes of the graph G ′ p are labelled with those that must be checked there, in particular { F 1 , F 2 , F 5 , F 8 } is labelled by { ψ 0 , ψ 1 } . It is now equally simple showing that the action retract F 2 2 has to be blocked, since { F 1 , F 5 , F 8 } ⊭ ψ 0 .