Paragon – Practical programming with information flow control

2.1. High-level policy

Suppose we have a program which deals with two actors, a vendor and a customer. The program has access to the vendor’s secret data – a software activation key – which should not be permitted to flow to the customer unless the customer has paid for the software. To model the payment act we have a special boolean flag called a lock. Let us call this particular lock “Paid”.

The Paid lock, and locks in general, is used solely to specify when information may flow from storage locations to actors. The lock is a special variable in the sense that the only interaction between the program and the lock is via some instructions to open or close the lock; it can be seen as an abstraction of the program’s security-relevant state. In the case of our example program we would need to associate the opening of the Paid lock with the actual confirmation of payment in the code.

The idea is then that security policies are associated with information containers in a program. In the case of a variable holding a software key, the policy would then be expressed as:

the data may flow to the vendor,

If at some later point the lock was closed again, perhaps because the customer’s access to the software key was only for a limited period of time, the data should no longer be accessible to the customer (though they would not be required to forget what they have already learned).

Some paragon declarations, including this policy, are given in Fig. 1. In the following section we will explain the specifics of the Paragon policy language, returning to this example along the way.

OPEN IN VIEWER

Fig. 1.

Policies for a Software Key (single customer, single key).

Note that what we have described here is an information flow policy specification mechanism – it allows the programmer to specify a flow policy in a program, and get guarantees that the program correctly conforms to the policy as stated. We make no attempts to address the issue of whether the policy itself is correctly stated, i.e., that the opening and closing of locks is done in the right places, and that data is labelled with the proper policies. As we shall see though, the combination of the policy language and Java’s encapsulation gives us further guarantees that help address these latter issues; we return to this in Section 3.

Policies are used to label information containers in order to specify information flow constraints on the data they contain. The subject of these policies are known as actors, and a policy consists of a set of clauses, each of which names an actor and specifies the conditions under which information may flow to that actor. The information flow conditions are special predicates called locks. In this section we describe each of these policy language components, and sketch how policies can be compared according to how liberal they are.2

Actors. The subjects of Paragon policies are the information-flow relevant entities, which we refer to as actors. An actor could represent a user, a resource, a system component, an information source or sink, etc.; any entity that is involved in some information-flow concern. Note that we deliberately do not use the term principal, used in many other systems [33,42] to denote information-flow relevant entities. We consider actors to be a more primitive notion than principals; a system using the notion of principals could use (one or more) actors to represent them, but actors can also be used more liberally to denote e.g. files or resources, entities that are typically owned by principals, but rarely modelled as principals in their own right. This discussion is related to the notion of information recipients, to which we return in Section 2.3. In the software key example of Fig. 1 the actors are the vendor and the customer.

In Paragon, actors are represented by objects. As a further example, the code fragment below creates regular instances of some User and File classes, where alice and f1 can play a dual role; both as program variables, and as actors in Paragon policies:

There are no special native Paragon classes to use as actors; any object created from any class can be used in this fashion, and User and File here are merely examples of user-defined (or standard Java) classes. For our actors vendor and customer, we do not expect the need for them to play a dual role; hence we could simply use objects of type Object to represent them.

Policies. A policy is used to annotate information containers in the program (fields, local variables), and specifies to which actors the information in those containers is allowed to flow. The KeySeller class from the figure, for example, declares three strings, each annotated by a policy (the question mark prefix indicates that this is a policy on data read from the respective variables).

A Paragon policy itself consists of a set of clauses, each specifying one particular actor, or one group of actors of a particular type: the head of the clause. In the software key example, the vendorData policy is intended for data for the vendor’s eyes only. It consists of a single clause vendor: signifying in this case a single actor. In contrast, the policy p2 in the example below states that information may flow to any (actor with type) file:

Since every actor is an object, there is a globally most permissive policy, namely { Object o: }, and a least restrictive Paragon policy, namely the policy with no clauses (written {:}). The type policy is a primitive type of Paragon.3

A policy may have multiple clauses. The policy customerData is an example of this which represents the policy for data that can always flow to both the vendor and the customer. A similar example is the following policy p2:

Here data can flow to both actor alice and actor bob.

It is important to note here the difference in interpretation between information flowing “to an actor”, and information flowing to (the fields and methods of) the object which is used to represent the actor. The possible confusion arises since objects serve double-duty, both as ordinary Java objects, and as actor identifiers. The statement that some information may flow to some actor, say vendor, has a priori nothing to do with the object identified by the reference vendor. The statement that some particular piece of information “may flow to vendor” is equivalent to saying that the policy of said information is consistent with assigning the information to a sink (e.g. field or variable, method parameter, out-going channel) with the basic policy { vendor: } – such as the vendorNotes field of the KeySeller class. We return to the question of sensible policy design in Section 2.3.

Flow locks. A clause may have a body that constrains the states in which the information may flow to the actors specified in the head. These constraints come in the form of flow locks which represent the policy-relevant state of the system. In the example, the second clause of payData – the policy used to annotate the software key – says that the flow to customer is conditional on the Paid lock (defined at line 2) being open.

This is an example of a simple lock. The power of Paralocks comes from the fact that a lock may have parameters representing actors. We illustrate this with a simple generalisation of the software key example. In this scenario there are potentially multiple customers. Each customer can access the software key if that specific customer has paid for it. Figure 2 contains policy definitions for this case.

OPEN IN VIEWER

Fig. 2.

Policies for a Software Key (multiple customers, single key).

Note that Fig. 2 (line 3) illustrates the more general form of flow lock which consists of a typed predicate – a lock family – and a list of actors forming the arguments to that predicate. In this example we model multiple customers by introducing a customer class. Instances of this class will be the representatives of actual customers. The policy customerData can flow to any actor x who is an instance of Customer. This policy is suitable for generic customer data such as product information, but not data for a specific customer such as billing address. The policy payData would be used to label a software key; it says that the information can flow to the vendor, and any customer who had paid, where we would model the successful payment by a given customer x by opening the Paid(x) lock.

Let us consider a further example involving binary locks. The following code defines two families of locks, one for modelling the ownership of files, and another for the organisational hierarchy among users:

Individual locks in the family can be addressed by specifying the actor arguments of the correct type, e.g. Owns(f1, alice) or ActsFor(alice, bob). Viewing the lock families as predicates, opening or closing a lock corresponds to changing the value of that predicate for the specified arguments to true or false respectively.

Apart from using concrete actors, policies can quantify over the arguments to lock families:

The policy p3 expresses that information can flow to any file owned by Alice, while the policy p4 states that u ranges over users, and that information having this policy may flow to any file f for which f is owned by some u such that u acts for alice. Note that variables that are mentioned in the head of a clause (in this case f) are universally quantified, whereas those declared in parentheses before the head (in this case u) are existentially quantified.

The policy lattice. As mentioned above, there exist both a least restrictive policy, { Object o: }, which permits flows to any actor, and a most restrictive one {:}, which permits flows to no actors. In fact the “more restrictive than” relation between policies enjoys a rich structure, namely that it forms a lattice, a structure who’s significance for information flow security was recognised in seminal work by Denning [18]. Let p and q denote policies. Let us write p ⊑ q to denote the property that q is more restrictive than p. The precise semantics of this relation is not given in detail here (see [50]), but intuitively it means that policy p allows flows to every actor that q allows, and in that case never requires more locks to be open.

In the examples of both Figs 1 and 2, respectively, we have customerData ⊑ payData ⊑ vendorData This relation is the key to checking whether the movement of information with policy p 1 to a container with policy p 2 is safe – namely we must have p 1 ⊑ p 2 . For example, if k is an instance of the KeySeller class, then the following assignment would be invalid:

since the policy of customerId is customerData which is not less than the policy of vendorNotes.

But what if we combine information with policy p 1 and information with policy p 2 ? To come up with a policy which safely describes the result, we need a policy q such that p 1 ⊑ q and p 2 ⊑ q , and in order to be useful we want such a q to be as small as possible. The key property of a lattice is that there exists a least upper bound (also known as a join operator), written p 1 ⊔ p 2 , which is the smallest policy that is at least as big as both of its arguments. The fact that the policies form a lattice means that p 1 ⊔ p 2 always exists for any p 1 and p 2 . As an example, the following assignment is valid:

since the least upper bound of the policy of vendorNotes and customerId is vendorData.

The least upper bound operator has a lower-bound dual, the greatest lower bound or meet operator, ⊓, which will also be useful.

Interfacing with Paragon. To integrate the policy language into a host language, we need (i) a way to associate policies with data, and (ii) a way to interface with the lock state. In Paragon we allow policies to be attached to data sources and sinks, through the use of modifiers. We saw an example of this in the declaration of the fields of the KeySeller class:

We discuss policy annotations and their consequences in more detail in Section 4.2.

To work with the lock state, we allow locks to be directly manipulated using the special statements open L and close L respectively, for some lock L (see Section 4.5 for a more thorough discussion).

Before we dig into the raw mechanical aspects of policies; their syntax and semantics, as well as their effect on what flows are allowed (Section 4), we reflect on the process of designing policy annotations and placing them on various program elements. In general the question of how to develop and use policy annotations depends on what overall system policy should be enforced, and thus cannot be answered in the abstract. However, some basic principles and patterns are common to all policy design and specification.

Out-going channels. As noted earlier, the statement that “some information may flow to a” is equivalent to saying that its policy agrees with assigning that information to a sink (e.g. field or variable, method parameter, out-going channel) annotated with the basic policy { a: }.

The first step of policy design is thus typically to consider the outward-bound end-points of the system, and assign policies to them, indicating who can be expected to gain access to the information after it leaves the system through that end-point. In the following, we will refer to such actors as information recipients. Consider for example a call to System.out.println(...). Assuming a system whose information recipients are users represented by type User, a potential policy to assign to the parameter of this method is { User u: }. In other words, information written to System.out is expected to be visible to any user.

Depending on the specific scenario, this may or may not be a reasonable expectation. For instance, in a setting where the end users communicate remotely with the system, information printed to System.out is likely not available to any such user.

The choice of how to represent the information recipients is a natural corollary to the question of what policies to put on end-points. Are there more than one sort of recipient to whom information may flow? If so, the different sorts of recipients should typically be modelled using different types. Does the system need to identify many different individual recipients of the same type (e.g. the User type), or would a role or abstract security level (e.g. high and low) be sufficient? Are there already suitable types for objects in the system that can be reused as actor representations, or should a separate, dedicated actor object type be introduced? The answers to all these questions will naturally vary depending on the particular system at hand, but they should all be asked (and answered) at this point in the design.

Integrity and confidentiality. An interesting aspect of the choice of representation for information recipients is the classic duality between confidentiality and integrity, exhibited by most systems that include both components [7,8,34,42]. In Paragon this duality does not manifest – instead, Paragon always asks the basic question: under what circumstances may certain information flow to some actor. Paragon is agnostic as to whether the restrictions on flows arise due to concerns for confidentiality or integrity. For an information recipient to whom flows should be restricted for both integrity and confidentiality reasons, a useful and powerful pattern in Paragon is to model that recipient as a pair of actors; one for each kind of restriction. An out-going channel for flows to recipient a is then annotated with a policy that allows flows to both actors, e.g. { a_conf: ; a_int: }.

There are several benefits to using this pattern. Firstly, by giving the different kinds of actors different object types, Paragon will know when joining policies to keep the different concerns from becoming mixed up. This potentially makes complex policies, formed when combining information from several sources, easier to read and understand. Secondly, this split also easily allows for also having (channels to) recipients that care about only one kind of concern but not the other. For example, the recipient a may have one channel on which only trusted information is allowed, with policy {a_conf: ; a_int:}, and a separate channel on which untrusted information is also allowed, with the simpler policy {a_conf:}. This “trick” can in principle be employed to effect a separation between e.g. two different confidentiality concerns as well.

Input sources. Once the decisions have been made regarding recipients, the policies on information input sources to the system should be crafted with those different recipients in mind. If any part of some information from an input source should ever be allowed to influence information flowing to some recipient, the actor(s) representing that recipient must appear as the head(s) of some clause(s) in the policy assigned to that input source. If not, Paragon will never, under any circumstances, allow such a flow. No catch-all, Alexandrian declassification operator exists that would allow adding potential recipients at a later point.

For each actor representing some (aspect of a) recipient, the restrictions that limit the information’s flow to that actor are then added. This amounts to identifying the security-relevant events of the system; modelling these using appropriate lock families; and deciding how they interact with the actors in the system. There are many different patterns for expressing restrictions on flows through locks, e.g. declassification, access control, temporal restrictions, relationships, etc. We showcase these patterns in the examples in next section. At this point, more kinds of actors can be introduced; actors that are not active recipients of information and therefore never appear as heads of clauses. These extra actors typically represent e.g. specific information sources, resources, or schemes. We show a few examples of such actors in the later sections: the Post objects in the social network in Section 3.3, and the Encryption schemes used in JPMail, discussed in Section 6.

Internal entities. What remains in the process of building Paragon code is to assign policies to internal entities, i.e. fields or methods that are neither input or output channels. The policies to assign typically follow from the use of those entities, and the flows to and from sinks and sources. Both read and write effects should be specified. This is usually less of a design task and more a question of calculation and specification.

Special care should be taken when assigning policies to channels that allow information to temporarily leave the system, such as writing to a file or a database. Those policies should be assigned to allow neither backdoor channels (e.g. information written to a file read by a recipient through means outside the system) nor laundering (information is read back into the system with a less restrictive policy than it had when it was written).

In the next section we now proceed to show a series of examples, showcasing both the various language features (discussed more formally in Section 4), and the design principles presented here.

3.1. Simple declassification

Our first example is the classic information flow idiom of a two-level confidentiality lattice with a simple declassification mechanism, showing succinctly how class encapsulation gives us the possibility to encode a policy scheme as a library. The interface of this scheme consists of three elements: policies for data that is secret (“high”) and public4

OPEN IN VIEWER

Fig. 3.

Simple declassification.

We define the policy low as the least restrictive policy, for data that anyone can see: {Object x:}. Policies in Paragon are first class values of the primitive type policy . For a policy to be used as a variable annotation, we require that policy to be marked final , i.e. immutable. This ensures that the policies remain consistent throughout the program.

High data may be made visible to low observers through declassification. We represent this with a condition (lock) Declassify. Unlike policies, locks are not first class values in Paragon, and cannot for instance be stored in variables. Locks are always implicitly static , to avoid aliasing problems (see Section 4.5 for further explanation).

The policy high is now simply the specification that data may be made visible to a low observer when the lock is open: {Object x: Declassify}. The act of declassification then becomes a simple matter of taking data with policy high and, in a context where Declassify is open, re-annotating it with policy low. Such re-annotations typically happen at assignments, but can also happen at e.g. the return of a method. This is exactly what the method declassify does.

There are several interesting things to note about this method declaration. First, it shows the use of policy annotations as modifiers on variables and methods. Here we see that the formal parameter x has a modifier ? high, stating that an argument to the method should have a policy no more restrictive than this. The method itself has a modifier ? low, the return policy, i.e. the effective policy on data returned by the method.

The body of the method consists of a single statement: a scoped open statement. As suggested above, returning from a method causes a re-annotation of the returned data to the declared return policy of the method. Here the re-annotation is valid since it appears in a context where Declassify is open.

Finally, we note that this method is now the only way to declassify data from high to low, since the Declassify lock is declared to be private to this class. Our library can thus have a simple, consistent interface through the use of standard encapsulation techniques.

The library exposes only the basic building blocks to the application programmer: the primitive policies low and high which can be used to label data, and a declassification method. The compiler statically checks that information in user code flows according to the policy, and encapsulation of the Declassify lock ensures that the declassification method is the only way that high data can be relabelled as low.

For an example use of the Declass library, consider the code fragment below:

To further demonstrate the modularity, we could easily extend our library with the notion of data that may never be declassified:

Data annotated with policy top can never be the argument to declassify, since that method’s parameter is stated to be no more restrictive than high.

Our next example is a small application, which has been used as an example in several earlier papers [2,10,11]: a server for running online sealed-bid auctions. We want to model the following information flow properties:

The class Bidder in Fig. 4 represents bidders in the system, and instances of this class double as actors; these are the information recipients. The bid placed by a bidder b should be visible only to b while the auction is running, and be released to all other bidders when the auction is complete and b placed the winning bid. Additionally, the process of determining the winner of the auction must by necessity reveal some information about the bids of all bidders (namely that they were no higher than the winning bid); we thus treat this process as a trusted operation (one we take extra care to get right) following the declassification pattern from the previous example. This is all modelled by annotating the field bid with the policy bidpol. Note that the lock family declaration for HasBid (and Winner defined in Fig. 5) explicitly states the actor type it is parameterised over, providing the additional guarantee to the system that a lock in this family cannot be opened for an actor that is not an instance of the Bidder class.

OPEN IN VIEWER

Fig. 4.

Sealed-bid auctions – Bidder and Channel class.

OPEN IN VIEWER

Fig. 5.

Sealed-bid auctions – Auction class.

We note that the policy here, unlike those used in the previous simple examples, is not marked as static . This is required in order to use the this keyword to refer to instances of Bidder in the definition of the policy, effectively giving each instance a distinct bid policy.

Each Bidder instance is associated with a channel, chan, for communication with the actual bidder. The class Channel uses type parameters to be generic in the policies on the data sent and received (see Section 4.7 for more details).

Note that the out-going put method for the channel for bidder b is annotated with the simple policy { b: }, as suggested in Section 2.3. On the other hand, the policy on the get method will be instantiated to the more complex bidpol (specialised to b), to account for all the different recipients of the information.

When the bidder supplies a bid as requested, by a call to the method getBid, we signal this by opening the corresponding HasBid lock. If the bidder fails to supply a bid, an exception is thrown.

Two things are worth noting here. The first is the modifier + HasBid( this ), which signals to the type checker that calling this method will open that lock, assuming the method call terminates normally. If it instead terminates with an exception, we make no such guarantees. HasBid is exported as readonly , meaning it can only be opened or closed within this class, which ensures that a correctly terminating call to getBid is the only way this lock can be opened (see Section 4.5). The second thing to note is the write effect modifier on the declared exception. Roughly speaking, this policy denotes the level at which it will be possible to observe that the function has terminated with this exception. Java does not normally allow modifiers on declared exceptions – they are an addition in Paragon (see Section 4.6).

Running the auction now consists of four phases: Getting the bids from all the bidders, determining the winner, reporting the results, and handing out the spoils. The implementation of these actions in the class Auction is displayed in Fig. 5.

We first declare a policy allBidders as the part of the policy on bids that is not specific to a particular bidder. That is, information under this policy may flow to any bidder at the end of the auction, and may be used in the trusted context of determining the winner.

The first phase, method collectBids, simply loops over all bidders, gets the bid of each, catching exceptions along the way. The only thing to note here is that the contents of the set bidders must be observable by all the bidders, due to the write effect of getBid. The same is true for the overall write effect of this method – every bidder can observe that the method has been called, so the only sensible write effect policy is bottom, i.e. the policy { Object x: }.

In the next phase, method determineWinner, we look at all the collected bids, determine the winner among them, and declare the auction closed. The method is guaranteed to open the AuctionClosed lock, as signalled by the appropriate modifier.

The local variable winner must have policy allBidders for the above code to be type correct. We don’t need to explicitly annotate it with that policy though – Paragon performs inference of policies for local variables (see Section 4.3).

Also noteworthy is that the assignment to winner does not affect the write effect (side effect) of this method, since winner is only available locally within the body of the method, so changes to it will not be visible from outside a call to the method.

For explicit flows – such as assignments – the current lock state is taken into account; for implicit flows – such as conditionals – it is not. It is for that reason that we need the isHigher variable. The motivation for this choice is that the implicit flow happens at the assignment to winner, not at the branching point. Locks might have been opened or closed in between which would give us awkward semantics if we consider the lock state for this check as well. Hence, if the outcome of a conditional expression has to be declassified this must be done explicitly via an auxiliary variable. Since this is a very common pattern, we could readily consider a pre-processing step that would transform any inlined conditional expression into a version with a direct flow into a local variable, as in the example here. We stress however that this would be a matter of syntactic convenience, and would not change the fundamental semantics.

Next we want to notify the bidders about the winning bid, calling the method reportResult. By virtue of the type arguments (see Section 4.7) of the Channel class, the method put can only accept data with policy (no more restrictive than) {b:}, where b is the currently iterated bidder. To be allowed to send winBid, with policy allBidders, on this channel, we must know that we are in a context where the two locks mentioned in that policy are truly open. The modifier ~ AuctionClosed declares that this method expects that lock to be open whenever it is called (Section 4.5 discusses lock state modifiers). Calling it in a context where that lock is not guaranteed to be open is a type error, and consequently the body of the method may assume that the lock is indeed open. For the second lock, we rely on so called runtime querying (see Section 4.5) for the status, through an if statement. If the condition of the if is a lock, the type checker can assume that this lock is open when checking the then-branch. Thus the re-annotation of winBid is correctly allowed.

Leaving the implementation of sendSpoils to the imagination, the method run ties all the phases together. We note that the re-annotation of winner.bid is allowed when using it as the argument to reportResult, since we know that Winner(winner) is guaranteed to be open.

Next we present the scenario of a simple social network, illustrating the three generations of information-flow control policies described in the introduction. In the network, users can befriend each other and share messages in the form of posts that can be read by their friends. The scenario contains two information flow policies that we want Paragon to enforce.

OPEN IN VIEWER

Fig. 6.

A simple social network application written in Paragon.

First, posts can only be read by a direct friend of the poster or, if the poster so indicates, by friends of friends of the poster. A user can decide, per post, whether it should be shared with friends-of-friends or not. Paragon should thus enforce that the network properly checks the friendship relations before allowing a user to read a post.

Second, to prevent injection or scripting attacks, a message should be properly sanitised before it is stored in the network. That is, we want to enforce the policy that all posted messages first pass through a sanitising function.

The Paragon implementation of this network is shown in Fig. 6. Some policy annotations are omitted in the implementation, since Paragon provides default policies in these cases. For example, all fields that do not specify a read effect automatically get the least restrictive policy {Object x:} (see Section 4.3).

The relevant information recipient actors in this scenario are the users, modelled by reusing the User type. To establish the first policy we define the Friend lock family to model friendships. Similarly we create a lock family FoFriend to model friend-of-friend relations. The FoFriend lock family has an explicit lock property stating a condition for when locks in this family are implicitly open (see Section 4.5). Since the User class never explicitly opens or closes the FoFriend lock and exports it as readonly we know that it models a purely derived property of the Friend lock family, and thus one that will evolve correctly as the friendship status changes over time. The Friend lock family also has lock properties; here we use the common shorthands symmetric and reflexive (see Section 4.5).

With the lock families in place we can now create the desired policy as messagePol, which we use for the read-effect on a post’s content stored in message. We assume that the correct Friend instances are opened elsewhere in the program. Turning sharing with friends-of-friends on per post is handled in the post method by opening the ShareFoF lock for that post.

As an effect of calling this method the array posts is changed (among others). Any observer that may notice this change (i.e. of level {Object x:} and above) may thus notice that this method has been called. To prevent this method from being called in a context where these side-effects result in implicit flows, we are required to annotate the method with the corresponding write effect.

The user’s receive method sends the user the provided information, therefore arguments to this method should be allowed to flow to that user. This is the relevant end-point of the system, as proposed in Section 2.3. All combined, we get Paragon’s enforcement ensuring that the policy-relevant state is properly checked before sharing a post with another user.

Leveraging Java’s encapsulation mechanism we are able to provide the ingredients for the sanitisation policy entirely as a separate library. Following the pattern shown in the declassification example (Section 3.1), the lock Sanitising is private to the class, meaning that no code outside the class is able to open, close or even mention the lock. Therefore, any data labelled with the unsanitised policy cannot lose its Sanitising constraint, other than by actually sanitising the data by calling the exported sanitise method. With this library we can thus easily enforce our second policy by labelling each newly incoming message as unsanitised.

The example demonstrates the three different generations of information-flow control policies and how Paragon models them:

As per traditional non-interference, some flows are never allowed in the network. For example, Paragon enforces that a posted message can only flow to users in the network, and not to any other channel. We see an example of the exceptional information declassification pattern in the sanitiser library: the sanitise function serves as a declassifier, deliberately allowing the provided argument to flow to more actors. Finally, the Friend locks exemplify third-generation information-flow policies. Here, there is no explicit declassification of information. Instead, flows are allowed or not depending on the state of the system – in this case the state of the social network and the relationship between user actors.

Our last example is an encoding of an information flow idiom in which permitted flows are specified using lexically scoped declarations, reminiscent of the work by Boudol and Almeida Matos [2]. The basic idea is a language mechanism that allows flows between security levels inside a lexically enclosed scope:

In this example, within the scope of the enclosed block information owned by (or that could flow to) security level x may also flow to level y. While this is a somewhat obscure example, it succinctly showcases two powerful features of Paragon – type methods and type parameters – which allow us to define complex policy schemes encapsulated as libraries. The Paragon encoding and encapsulation of this mechanism is shown in Fig. 7.

OPEN IN VIEWER

Fig. 7.

Encoding and encapsulating Lexically Scoped Flows in Paragon.

Encoding. To encode the scheme we first introduce the binary lock family Flow, where each lock in the family represents a flow relation between its two arguments of some unspecified class Level. Since the relation of flows between levels is intended to be transitive and reflexive, we annotate the lock family with the respective Paragon short-hands for these lock properties.

With this lock family we can easily encode the flow mechanism using the scoped open statements, so e.g. flow (x to y){ ... } would be encoded as open Flow(x,y){ ... }.

Lastly we need to encode the policy annotations used with this scheme. Given data of some security level, this data should be allowed to flow to other levels as well when the proper flows are enabled. Thus data with security level l can be correctly annotated with policy { Level x : Flow(l, x)} (which through reflexivity of Flow includes l).

The three components we have defined here – the Flow lock family, the encoding of the flow statement, and the encodings of policies – is all we require to express the idiom.

Encapsulation. The second step is the encapsulation, making the lock family read-only and exporting only two things: a way to construct consistent policies, and a method representing the flow construct.

To encapsulate the construction of policies we export the typemethod pol which given a security level returns the corresponding policy (see Section 4.4). Thus, data with security level s can now be annotated with the policy ? pol(s). The Paragon type checker replaces the annotation by the result of interpreting the method during type checking.

The flow construct should take the code to run as an argument, but our host language Java does not support first class statements or procedures. The standard Java approach is to wrap the code to pass as a method of an anonymous object implementing a declared interface, and then pass the whole object as argument to the flow method.5

The levels from and to state for which levels to enable the flow. Thanks to the ~ Flow(from, to) modifier on the code in the FlowBlock, the code can depend on this lock being open, enabling flows from level from to level to in the body as intended.

To allow arbitrary side effects in the code block the interface receives an additional policy type argument w describing this write effect.

Finally, we wish to nest multiple flow calls, requiring some context sensitivity on the opened locks. The last type parameter is therefore a set of locks ls which allows us to specify the context in which a flow method is invoked. By adding the ~ ls modifier the inner code can now also depend on these locks being open.

With these definitions of pol, flow and the auxiliary interface FlowBlock we have achieved a proper encapsulation, ensuring that the library is used consistently. As an example on how to use the library, Fig. 8 displays two nested scoped flows side-by-side with their Paragon encoding, assuming variables xData and zData of security levels x and z respectively. This encoding is unfortunately far more verbose than the mechanism we are encoding – but note that the extra noise comes mostly from Java not having first class statements. Paragon also allows type arguments to be omitted in many cases, relying on inference to supply them. We could have done so in this example, but include them for (verbose) clarity.

OPEN IN VIEWER

Fig. 8.

Using Lexically Scoped Flows in Paragon.

4.1. Information flows and policies

The various flows of information that need to be controlled in Paragon are essentially the same as the ones occurring in Java. As is common in information-flow analysis we make a distinction between direct and indirect information flows.

Direct flows. The typical direct flow is an assignment, where information flows directly from one location to another. Direct flows also happen at method calls (arguments flow to parameters), returns (the returned value flows back to the caller) and exception throws (an exception value flows to its enclosing catch clause).

As an example, let x be a variable with the policy {File f:Owns(f, alice)} (can flow to file f if it is owned by alice) and y a variable with the policy {f1:} in the assignment y = x;. Whether or not the assignment will be flagged as an error by the Paragon compiler depends on the lock state in which the direct flow occurs. If the Owns(f1,alice) lock cannot statically be determined to be open the compiler raises an error, since the information stored in x, according to its policy, should only flow into file f1 when the file is owned by Alice, whereas information held in y can always flow to f1. In other words, the assignment constitutes an insecure information flow because it moves information to a place where it becomes visible to more actors, and/or in more states, than its policy declares. If, however, the lock is determined to be open, i.e. declaring that alice owns f1, the assignment occurs in a state where f1 can already read the information in x, and so the program compiles successfully. Section 4.5 described the lock state analysis in more detail.

Indirect flows. An indirect flow is one where the effect of evaluating one term reveals information about a completely different term that was evaluated previously. The typical indirect flow is a side-effect happening in a branch that reveals which branch was chosen, which in turn reveals the value of the conditional expression that was branched on. Indirect flows also arise from other control flow constructions (including loops and exceptions), and field updates or instance method-calls (possibly revealing the object they belonged to).

Due to the delayed nature of these information flows, the lock state in effect at the time of the indirect flow might be different to that in effect at the point at which it is revealed. Therefore, indirect flows are handled conservatively, by not allowing the lock state to affect which of these flows are considered secure.

4.2. Policy annotations

When integrating the policy language into Java, the two core design issues are (i) how policies are to be associated to data, and (ii) how the lock state is specified, updated, and queried.

In Paragon every information container (field, variable, parameter, lock) has a policy detailing how the information contained therein may be used. Every outgoing (or incoming) channel similarly has a policy specifying what it means to have information leave (or enter) the system through that channel. Further, every expression has an effective policy which is (an upper bound on) the conjunction of all policies on all containers whose contents affect its resulting value – we refer to this as the expression’s read effect.

Paragon separates policies from base (Java) types syntactically by having all policy annotations as modifiers. Examples of ordinary Java modifiers are static and final , and Paragon modifiers syntactically appear in the same positions as their Java cousins. A modifier ? pol denotes a policy on an information container, and the read effect of accessing that container. When used on a method we refer to it as the return policy, as it is the read effect on the value returned by the method. Using modifiers for policies allows for a clean separation of concerns, allowing us to analyse base types and policies separately.

Similarly, every expression (and statement) has a write effect, which is (a lower bound on) the disjunction of all policies on all containers whose contents are modified by the expression. Write effects allow us to control implicit information flows, by limiting the contexts in which expressions with side-effects may occur. A modifier ! pol denotes a write effect, and is typically used to annotate methods.

4.3. Policy inference and defaults

To reduce the burden on the programmer to put in policy annotations, Paragon attempts to either infer, or supply useful defaults for, policies on variables, fields and functions. The policy defaulting and inference mechanisms, the latter based on work by Rehof and Mogensen [38], are very heavily influenced by those used in Jif [34]. We describe them in this section for the sake of completeness.

Policy defaults. For fields, omitting the policy annotation is interpreted as having no information flow concerns for that field. Hence, the default policy for fields is simply the most liberal policy, { Object o: }.

Methods have policies both on their parameters and on their return value (if any). Omitting the policy annotation on a parameter makes the method parametric in the policy of the corresponding argument. Paragon supplies a special construct policyof (p) to refer to the policy of the argument supplied as parameter p, either in policies within the method’s body, on other parameters, or in the method’s return policy.

For the return policy, the default assumption is that the returned value depends on all the arguments given to the method, so the default return policy is the conjunction (join) of the policies on all parameters.

As a typical example of a policy-parametric method, consider Math.abs(...) from the standard libraries, which returns the absolute value of a number. The returned value depends directly on the supplied argument, regardless of the policy on that argument, and can reasonably be assigned the same policy. In this case, neither the parameter nor the return value need explicit policy annotations.

The default write effect for a method is {:}, i.e. the most restrictive policy (top), meaning that the method performs no side effects that would be visible to any actor at any time. Note that the write effect of a method is always checked, not inferred.

Policy inference. Local variables serve a common role as temporary information containers. Omitting the policy annotation on such a variable is interpreted as the programmer not caring what policy it has, so long as that policy does not violate any information flow concerns specified elsewhere. Paragon therefore tries to infer policies for local variables such that all information flows that involve them are deemed safe by the type checker. We discuss the technical details of policy inference in Section 5.

4.4. Policy expressions

So far we have seen many examples of literal policies, that is, policies constructed directly using clauses of actors and locks. Policies can also be constructed programmatically in various ways. They can be used as values at runtime, and can be dynamically hoisted to the type level to be used in modifiers. To ensure consistency across e.g. several calls to the same method, only final fields or variables may be used in the construction of policy modifiers. Again this decision is directly influenced by the same behaviour in Jif.

Policy operators. Policies can be created by combining other policies using the overloaded operators for join ( * ) and meet ( + ). The policy resulting from a join is the least restrictive policy that is still at least as restrictive as both of the operands. Phrased differently, the policy p1 * p2 allows all flows allowed by bothp1 and p2. Conversely, the policy resulting from the expression p1 + p2 allows any flow allowed by eitherp1orp2, which simply amounts to the union of all clauses from both operands.

Type methods. To allow for the creation of complex policies in libraries, we must allow policies to be generated by methods, which forces our policy analysis to also analyse the behaviour of method calls. To avoid a situation where the precision of the analysis appears unintuitive and ad-hoc to the programmer, we allow programmers to explicitly mark which methods the analysis should take into account with the modifier typemethod – a method to be interpreted during type checking.

A more formally correct name would perhaps be type functions, since these methods must be both pure, i.e. have no side-effects, and deterministic. By deterministic we mean that the end result may only depend on values known statically when the method is called. That includes the method’s arguments, as well as certain static fields; specifically, for a field to be usable in a type method, it must be static and final, have a primitive type, have the least restrictive policy (i.e. bottom) applied to it, and have a simple initialiser that is itself pure and deterministic. These constraints are checked by our compiler for methods marked as type methods.

Runtime policies. Some policies for information simply cannot be known statically during type checking. They may be read from files or database entries, or constructed to model the UNIX privileges for a file, or based on other external and dynamic conditions.

To handle such runtime policies, the analysis must approximate upper and lower bounds for all policies based on what information is available for them. To improve precision, we need ways to relate policies that are not known statically to other (static or runtime) policies, to improve precision. We let our policy analysis be guided by inequality constraints between policies appearing as the condition in if statements and conditional cond ? e1:e2 expressions. As an example, consider the following code:

Here we assume that polA and polB are not statically known, but due to the inequality constraint, we can still allow the assignment in the branch.

This problem has been studied by Zheng and Myers in the context of Jif [57], and the solution presented here closely follows theirs.

4.5. Lock state analysis

Manipulation of the lock state is done programmatically through the use of the Paragon-specific statements open and close . The compiler performs a lock state analysis which conservatively approximates the set of locks guaranteed to be open at any given program point.

Paragon also provides a lexically scoped version of the open statement. This scoped open keeps the specified lock open for the extent of its body; in other words, it opens the specified lock at the start (if it was not already open), closes it when done (unless it was already open at the start), and rules out any (non-scoped) opens or closes of that lock throughout the body.

Runtime lock queries. Locks in Paragon are not first class. They cannot be stored in variables, nor can they be passed as arguments to methods. The only way to manipulate the status of a lock is via open and close statements. However, the status of a lock may be queried at runtime. A lock can be used syntactically as an expression of type boolean , with the value true if the lock is currently open. For expressions appearing as the condition of an if , while or do loop, or as the first operand of the ternary conditional operator ?:, the policy type checker analyses what locks are known to be open or closed when the condition is true, respectively false, and includes that knowledge when checking the respective branches. In a setting with concurrency, such assumptions cannot be made; Paragon as of yet does not support concurrency.

Lock state modifiers. To facilitate modularity, Paragon introduces three modifiers, used on methods and constructors, to specify their interaction with the lock state:

The opens and closes modifiers are also used to annotate each exception type thrown by a method, to signal to the analysis what changes to the lock state can be assumed if the method terminates by throwing an exception of that type.

Lock properties. A lock can be declared to have properties. A property specifies conditions under which some locks are implicitly open. For example, we might want to express that the acts-for relation defined in Section 2.2 is transitive and reflexive. This requirement can be stated at the point of declaration as follows:

These clauses look similar to those of policies, however the heads here represent locks that are implicitly open, while in policies they represent information recipients. We follow the Java tradition of forcing variables to be declared before they are mentioned, even though the types could easily be inferred in this example. This is not always the case though; specifically, we could have rules that declare some locks to be implicitly opened for actors that are members of a specific subclass.

Transitivity and reflexivity properties (as well as symmetry) are a common pattern, so Paragon provides syntactic sugar for these:

Since lock properties must be attached to the declaration of a lock, they are a modest restriction of the Recursive Paralocks, discussed in [11]. However it turns out that this restriction make the policy operations decidable, and the policy comparison operation specified in [11] becomes complete (as opposed to just being sound). Full details are given in [50].

Actors and aliasing. Together with locks, actors, represented by object references, play a crucial role in the typing of Paragon code. Locks determine what flows are allowed at what points, and locks are often parameterised by actors. The typeability of some code may depend on a given lock, with some given actor arguments, being open. Formally, the type checker treats actors as singleton types [4].

However, the possibility of aliases complicates things. If some code opens lock L(a) and then closes lock L(b), is the first lock still open? Clearly that depends on whether or not a and b are two different actors.

We discuss the technical aspects of alias analysis in more detail in Section 5. For the purpose of language presentation we note that, like with runtime lock queries guiding lock state analysis, or runtime inequality constraints on policies help increase precision, we let conditions involving tests on reference (in-)equality help make our alias analysis more precise.

Modifiers on lock families. Since locks may be queried at runtime, they are information containers, and, like other containers of information, need policies to dictate how that information may flow. The policy on a lock family becomes the read effect of a lock query expression, as well as the write effect of any open or close statements manipulating it. A lock family can also be annotated with an expects modifier, which restricts the lock states in which it may be manipulated.

To avoid further issues with aliasing of locks, all locks are static; there is only ever one version of a lock family, not one per instance of the class in which it is declared. This restriction is without loss of generality, since the behaviour of having one lock family per instance can be achieved by giving the lock family one more parameter of the appropriate type, and use the instances as arguments. Thus, instead of o.L(...) we get L(o,...). This way, the analysis needs only be concerned with potential aliases of actors.

A lock may be exported as readonly . This means that it may be mentioned in policy declarations, in lockstate modifiers on methods and constructors, and in lock queries, but not opened or closed outside the scope of the defining class. Note that the same effect could be had through the use of a dedicated class-private lock combined with clever use of an expects modifier. This is a very common pattern, however, and we introduce the readonly modifier as a shorthand that also conveys the intention more clearly.

4.6. Exceptions and indirect control flow

The static policy type system in Paragon tracks two kinds of information flows: direct flows arising from assignments, and indirect flows arising from control flow. It makes no attempt to track flows arising from termination – it is termination insensitive. If exceptions could not be caught, an exception would be the same as (premature) termination, which means we would not need to care about them. However, the catch mechanism makes exceptions rather a kind of control flow primitive, needing special attention.

All exceptions in Paragon must be checked, i.e. declared to be thrown by methods that may terminate with such exceptions. This implies the need for analyses that can rule out the possibility of exceptions, in particular for null pointers, to avoid a massive blow-up in the number of potential exceptions that must be declared. Paragon adds the modifier notnull for fields, variables and method parameters that may never be null, to aid the null-pointer analysis.

A caught exception is in essence a jump, where control is passed from the throw point to a catch block. Such a jump may be noticeable by anyone who can notice the catch block being executed, or the statements in the normal control flow past the throw point. To avoid unintended flows, all such statements are constrained by the context in which the throw appears. We refer to this as the exception’s area of influence.

Since an exception might not be caught locally, the area of influence is not a local property in general. To handle this modularly we let methods that throw exceptions declare the write effects of those exceptions as modifiers on the exception types in the method’s throws clause. This declared write effect serves as an approximation of the context where the throw appears. It is thus both used as the effective write effect of the throw statement itself, to ensure that it is not used in even more restrictive contexts, as well as a bound on the write effects of all statements in the area of influence. Constraining subsequent statements in this way is reminiscent of the way termination sensitivity is typically achieved for information flow type systems. Indeed, the constraints we introduce here will stop termination leaks caused by uncaught exceptions. To achieve full termination sensitivity however, we would also need to disallow “low” effects to follow potentially non-terminating “high” loops. We choose not to do so though, for two reasons. First, the mechanisms needed to perform the required analysis would be pervasive and heavy-weight (all methods would need the equivalent of a termination effect). Second, since every loop in the program would be like a potentially thrown exception that can never be caught, putting large constraints on subsequent statements, it would significantly reduce the class of type-correct programs.

Since uncaught exceptions are effectively premature exit points from a method, the opens and closes modifiers pertaining to a normal exit do not apply when entering a catch block. Hence we let the declared exceptions also take opens and closes modifiers, specifying the lock state that will be in effect at the start of a corresponding catch block.

For the cases where a thrown exception is caught locally, before ever reaching the top level of a function, there will be no need for approximations via declared policy or lockstate modifiers. Instead, all the necessary information can be computed locally.

Interestingly, several other control flow mechanisms in Java can be treated as special cases of exceptions for purposes of policy inference: return , break and continue . These are simpler to handle than exceptions, since their area of influence is always contained locally.

4.7. Type parameters

Java, since the introduction of “Generics” in Java 5.0, allows types and methods to be parameterised by types, giving Java parametric polymorphism. Paragon introduces several new entities – actors, policies and locks – that affect typing in various ways. It is natural to extend the polymorphism to also include these aspects. To ensure that the different entities are handled correctly, we need a kind system to signal which kind of entity we expect for a given parameter.

A typical use of a policy type parameter can be seen for a collection, e.g. java.util.Stack. In vanilla Java, collections are parameterised over the base type E of the elements, e.g. Stack<E>. This is then reflected in the signatures of methods: push will take an argument of type E, while pop returns an value of that same type.

In Paragon, those same elements have both a type E and a policy P, declared Stack<E, policy  P>. Note the use of policy as a kind annotation. Now push will expect an argument of type E and with policy P, and pop returns an element with that same type and policy.

Arrays are a special case of collections, and the same pattern is repeated with elements having a common policy. The syntax differs slightly; we write int []<P> for an array with elements of type int and policy P. The pattern can be repeated for higher dimensions, e.g. int []<P>[]<Q> is an array of arrays where the ( int ) elements of the innermost arrays are subject to policy P, while those inner arrays themselves are subject to policy Q. Paragon puts no restriction on the relationship between P and Q, however, the read effect of reading an element from an inner array will be the join of the policies on each of the outer levels down to the level read from. This means inner policies that are less restrictive than outer policies are in effect pointless.

In Paragon, ordinary reference types have the implicit kind type. Type parameters of kind type need not be annotated, like in vanilla Java. For the Paragon-specific entities we introduce kind annotations, as seen in the example above, to separate them from each other and from ordinary types. Since actors are modelled by objects, we use an actor’s reference type as its kind. For policies we can simply reuse their type as kinds as well.

We can do the same for locks though we typically want to parameterise over not just single locks, but rather sets of locks. To avoid introducing new keywords, we reuse the syntax for arrays for this purpose, i.e. the kind annotation on parameters taking sets of locks is lock []. For an example of parameterising over the lock state, see Section 3.4.

With Generics, the Java type checker tries to infer type arguments where none are provided. Paragon does the same for missing type arguments, with a slight generalisation – we allow partial type argument lists, which are assumed to instantiate the type parameters of the method or constructor from left to right.

5.1. Overview of phases

Phase 1: Type checking. The first phase roughly corresponds to ordinary Java type checking, albeit with some additions for Paragon-specific constructs. Particularly, we must assure that arguments to locks are type correct, and that policy expressions used in modifiers are indeed of type policy . This phase also checks that potential (runtime) exceptions are properly handled, which includes performing a notnull analysis. Our current notnull analysis is based on the work by Müller and Summers [45], and is described in more detail in [56]. Finally, typemethods are checked to conform to the restrictions placed on them as discussed in Section 4.4.

The important thing to note here is that the checking of ordinary Java type correctness is largely unaffected by the addition of information flow policies, and can be performed prior to the analysis of information flow.

Phase 2: Policy type evaluation. Locks, policies, and objects all play a dual role, both as type-level and value-level entities. In this phase the values of each of these entities are statically approximated. For locks we ensure that, whenever a lock is queried, the information in the query is propagated to the respective branch (or loop body).

For fields and variables holding actors, i.e. object references, approximating their runtime values means performing an alias analysis. Our present analysis is simple but has performed well enough in practice. However, work is in progress to improve its precision by adapting the work by Whaley and Rinard [54].

Since policies can be used as values at runtime, and dynamically hoisted to the type level, our analysis needs to approximate policies as singleton types, similar to the analysis of actors. For each field or variable storing a policy, and for each policy expression appearing in a modifier, we thus calculate upper and lower bounds on the policy held by that variable at runtime.

Further, we need ways to relate policies that are not known statically to other (static or dynamic) policies, to improve precision. Similar to runtime lock queries, we thus let our policy analysis be guided by inequality constraints between policies appearing as the condition in if statements and conditional ?: expressions. This problem has been studied by Zheng and Myers in the context of Jif [57], and our solution closely follows theirs.

Phase 3: Lock state evaluation. The next phase approximates the lock state, i.e. a static (under-)approximation of the set of locks that will always be open at each program point. This amounts to a dataflow analysis over the control flow graph, to properly capture the influence of method calls and exceptions, and to handle loops. Each program point where a direct flow takes place is annotated with the lock state in effect at that point. Direct flows are limited to the following four language constructs: assignments, method calls (and instance creation), returning values, and throwing exceptions.

The details of approximating the lock state are shown in the next section.

Phase 4: Policy constraint generation. The constraint generation phase will result in a set of constraints on the form p ⊑ LS q where p and q are policy expressions and LS is the lock state (calculated in Phase 3) at the program point where the constraint was generated (omitted if empty). Intuitively, this is the ordinary ⊑ operator presented in Section 2, but where the locks that are open in LS are removed from the policies. As argued in Section 4.1 the lock state is only taken into account for direct flows. Due to inference of policies for local variables, the policy expressions possibly contain meta-variables, for which the constraint solving phase then solves.

The full details of constraint generation are shown in the next section.

Phase 5: Policy constraint solving. The last phase solves the generated constraints, on a per-method basis. A solution to a set of constraints is an assignment of policies to constraint variables that satisfies all the policy comparison constraints. The algorithm needs only determine whether there exists a solution, and does not need to actually produce one. The constraint solver is based on the algorithm presented by Rehof and Mogensen [38].

5.2. Paragon type system

In this section we present the formal type system for the parts of the analysis corresponding to lock state approximation and policy constraint generation, for a sizeable subset of Java. Our implementation covers a larger subset still, but here we leave out a number of features that do not add anything to the presentation. More specifically, the features left out are enums, static fields, arrays (as in the syntactic sugar), inner classes, casts, most operators, labeled statements, as well as expressions and statements whose typing would be very similar to those already covered (e.g. do is very similar to while ). We will further leave out discussion of Paragon’s scoped open statements; these are not difficult to handle in practice, but introduce significant notational overhead to the presentation, so we omit them for clarity.

Lock state approximation. Let us first look at lock states, and define some convenient operations. First, in our analysis a lock state is represented concretely as the set of locks being open in that state. We will also have use for the concept of an unreachable state, represented with the distinguished value ⊥ . We let LS range over values in the domain of lock states including ⊥ .

Next, we will have use for the concept of a lock modification, representing a set of changes to be applied to a lock state. We model this concretely as a pair ( L o , L c ) , where L o is a set of locks to be opened, and L c is a set of locks to be closed. Here we overload ⊥ and identify it with the tuple ( ∅ , ∅ ) , i.e. no modifications.

We now need two (overloaded) operations, ⊳ and ◇, respectively corresponding to sequential and parallel composition of lock states and lock modifications. We have that: LS 1 ◇ LS 2 = LS 1 ∩ LS 2 , LS ⊳ ( L o , L c ) = ( LS ∖ { L ( a 1 , … , a n ) | L ( b 1 , … , b n ) ∈ L c , b i ≃ a i } ) ∪ L o , ( L o 1 , L c 1 ) ◇ ( L o 2 , L c 2 ) = ( L o 1 ∩ L o 2 , L c 1 ∪ L c 2 ) , ( L o 1 , L c 1 ) ⊳ ( L o 2 , L c 2 ) = ( L o 2 ∪ ( L o 1 ⊳ ( ∅ , L c 2 ) ) , L c 2 ∪ ( L c 1 ∖ L o 1 ) ) . Note that the a i listed in the second definition are abstract actor identities, and that we here appeal to the ≃ operation; this operation arises from the alias analysis performed in the previous phase, and simply tests whether two actor identities may be aliases. Thus, b ≃ a only returns false if we have been able to statically determine that b and a cannot be aliases for the same object. The above definitions hold when the lock state operands are not ⊥ . We have that ⊥ is the identity element for ◇, and the 0-element (annihilator) when appearing as the left-hand operand of ⊳.

Now we can turn to the analysis itself. The behaviour of the analysis is captured by the following declarative judgment, covering both expressions and statements: LS ⊢ e ⇝ LS ′ ; X , where

LS and LS ′ are the lock states prior to and after evaluating e;

Further, a rule for this judgment is valid only if each occurence of the mentioned language constructs is annotated with the correct lock state.

We will consistently use superscripts (sometimes in conjunction with square brackets for scoping) to denote annotated information, while subscripts or primes serve to disambiguate terms. Technically, an expression e will also be annotated with information from previous passes. We will omit such annotations when they are not needed by the rule.

Looking at expressions first, we omit the rules for literals, the expressions this and null , and variables; they do nothing interesting in this context. We further omit the rules for binary operators as they do nothing but inductively call their sub-components, and for instance creation which is very similar to method calls. This leaves the rules for method calls, assignments, and the conditional ?: operator. The rule for assignments is as follows, where the only interesting part to note is the lock state that the assignment gets annotated with, which will later be used by the constraint generation.

This rule deals with variable assignment. The rule for field assignments is analogous; for primary field assignments (where the object is calculated from an expression) or array updates, the only difference is that the sub-expressions of those left-hand sides are analysed first.

The rule for method calls is more involved:

where LS ′ = LS n ⊳ ( L o , L c ) , and X ′ = X 0 ◇ ⋯ ◇ X n ◇ LX . Again, note the lock state annotation on the method call. As noted, the rule for instance creation is near identical (assuming that M also stores lock state signatures for constructors).

Finally (for expressions), the rule for the conditional operator:

The interesting thing to note here is that we expect the condition to be annotated, from a previous phase, with any locks known to be open or closed if the condition is true and false, respectively, and we take this into account when analysing and annotating the expressions in the branches. The annotation ( L 1 , L 2 ) here is thus input to this phase computed in the previous phase, unlike the annotations in the previous two rules which are the result of this phase.

Turning to statements, empty statements and expression statements add nothing interesting, and if statements are very similar to the conditional operator, so we omit these. Further, many of the pseudo-exceptions all follow the same pattern: continue , break and return without a value – we show only the first of these. Apart from these we have while , throw , return with a value, try-catch-finally , and the Paragon-specific open and close statements.

Most central to this phase are the open and close statements, contrasted below:

The open statement opens the lock for exactly the listed identities, while the close statement must assume that the lock may have been closed for any choice of identities that the listed ones may alias, as per the definition of the ⊳ operation.

The rule for while -loops is as follows:

where X ′ = X c [ continue ↦ ⊥ , break ↦ ⊥ ] . First, note the annotations on the condition from the previous phase, which affect the analysis of both the loop body and the lock state after the loop ends. Second, note the circular dependency between the lock state in effect after the body is executed and the lock state at the beginning of the condition (it is possible to unroll the loop and check the condition twice, to get an algorithmic version – only one unrolling is necessary, due to the pessimistic approximation of lock states). Third, the evaluation of the body s may have been prematurely aborted through a continue or break , and execution continued at the relevant places. In the exception state after the loop we want to reset the registered lock states for these pseudo-exceptions to what they were before the loop, in case there are nested loops. In effect, the while -loop serves as (two nested) try-catch for the two pseudo-exceptions.

For thrown exceptions we have the following rule:

Three things to note: first, the lock state after this point is ⊥ , marking an unreachable state (“dead code”); second, the throw is annotated with the lock state; third, we register in the outgoing exception map that an enclosing catch block might start in the lock state in effect here, LS e . Since an exception of the same type could be thrown in several places within the same try-catch , we must also take previously registered exception states into account.

Finally we have the rules for try-catch-finally blocks. Here we assume for simplicity that all such statements are unrolled to have either a single catch block, or a finally block. We then look at the two cases separately:

where X ′ = X c ◇ X t [ T ↦ ⊥ ] . If we reach the start of the catch-block, the lock state in effect must be that which was registered by a corresponding throw (or several) inside s t . All exceptions are still valid after the whole try-catch completes, except the one caught, as mirrored by the outgoing exception map.

The rule for try-finally is then as follows:

where LS ′ = LS t ◇ { X t ( T ) | T ∈ dom ( X t ) } . The finally -block will be executed regardless of what exceptions that may have been thrown inside the try -block, so we must assume that any of them may be the cause of the lock state in effect.

Policy constraint generation. This phase is captured by the following judgment, where we assume that the expression e has been properly annotated from the lock state approximation phase: EX ; pcB ; PCE ⊢ e : p ⇝ PCE ′ , θ where

p is the effective policy of the expression (i.e., the policy of the value of the expression);

We implicitly assume an environment E containing policy signatures for fields, variables, methods and locks, as well as the declared return policy of the enclosing method. We also assume a set of global lock properties G, which would formally be added as a subscript to every constraint, e.g. p ⊑ G , LS q , however we omit it since it appears the same everywhere.

The rules for literals, this and null are uninteresting. The rule for field dereferencing is as follows:

The only interesting thing to note is that the policy is the join of the policies of the containing object and the field. The rule for binary operators is very similar:

In the rule for conditionals we extend the branch PC to constrain indirect flows in the branches:

An assignment constitutes an actual information flow, so the rule for assignments is where many of the constraints arise:

where p f = E ( τ , f ) and θ = { p e ⊑ LS p f , ⨆ PCE e ⊔ pcB ⊑ p f , p o ⊑ p f } . The three constraints generated at this rule have the following purposes:

Finally, the rule for method calls:

Here we assume E ( τ , m ) = ( p m , p w , PP , PX ) , where PP is a mapping from parameter positions to the parameter policy signatures of the method, and PX is a mapping from the method’s checked exception types (and pseudo-exceptions) to policies. We then have that θ = { p i ⊑ LS PX ( i ) , pcB ⊔ PCE n ⊑ p w , p o ⊑ p w } , θ x = ⋃ { { PX ( τ ) ⊑ EX ( τ ) , EX ( τ ) ⊑ PX ( τ ) } | τ is an exception type } , and PCE ′ ( τ ) = PCE n ( τ ) ⊔ PX ( τ ) for all exception types τ.

The constraints in θ here are similar in spirit to the ones for assignment, only here the write effect of the method, p w , is used instead of the policy of the updated field, and there are several direct flows from argument values to parameters. The constraints in θ x check that the policies of the exceptions potentially thrown by the method match those expected by the environment. Since the policies are used both as constraints of effects in the area of influence, and as the effective policy of the exception value being thrown, the inequality must hold in both directions.

The outgoing exception PC map is updated to take into account all exceptions potentially thrown by the method.

For statements, the rules for empty statements and expression statements are uninteresting, and the rule for if statements mirrors that for conditional expressions.

The rule for while -loops is as follows:

where

Note in particular that the entire loop, including the condition itself, is constrained by the policy of the condition.

The rules for return and throw are near identical, we show only that for return:

where θ = { p e ⊑ LS EX ( return ) } . Here we have a direct flow of the returned value back to the caller of the enclosing method, and thus the lock state is taken into account. The expected policy of the returned value is found in the enclosing exception environment.

The rules for the pseudo-exceptions are even simpler, so we omit them.

For try-catch-finally , again we assume an unrolling so that each block is either try-catch or try-finally .

Note first that we assume the parameter of the catch block to be annotated with its calculated policy p x from a previous phase. This policy then serves as the expected policy of thrown exceptions of type T in the try block. The catch block is only in the area of influence from exceptions of type T if they were already thrown before reaching this try-catch .

where PCE ′ ( τ ) = PCE t ( τ ) ⊔ PCE f ( τ ) . Here, the interesting thing to note is that we analyse the finally -block under the same exception PC map, PCE , as the try -block. The reason is that the finally -block will always be executed no matter what exceptions are thrown in the try -block, so it will not be in the area of influence of any of those. Any code following this try-finally statement will still be within the area of influence of any as-of-yet uncaught exceptions from within the try -block, which is mirrored by the outgoing exception PC map, PCE ′ .

Finally we look at the Paragon-specific statements open and close . Locks too have policies, and opening or closing a lock is an effect visible at the level of that policy, hence we must take implicit flows into consideration:

The rule for closing is identical. Note the similarity to the rule for assignments.

This concludes our presentation of the formal type system for the two most interesting phases, from the perspective of Paragon policy checking.

5.3. Paragon implementation

We have implemented Paragon in a compiler that performs type checking for policies, and compiles policy-compliant programs into vanilla Java code. While the enforcement system was presented in a modular fashion above, for efficiency the current implementation performs most of the phases simultaneously.

Once we know that a given program satisfies the intended information flow properties, we can safely remove all Paragon-specific type-level aspects of policies, locks and actors. We must still retain the runtime aspects, such as querying the lock state and performing inequality comparisons between policies.

The Paragon runtime library provides Java implementations for locks and properties, including operations for opening, closing and querying locks to which the Paragon open , close and query statements are compiled. Similarly, the library provides Java implementations for policies and operations for performing runtime inequality comparisons between them.

Compiler statistics. Our Paragon compiler is written in Haskell and comprises roughly 16k lines of code, including comments. Approximately half of that code is due to our policy type checker, and only a small fraction, just over 600 lines of code, deals with generation of Java code and the Paragon interface files needed for modular compilation. Of the roughly 8k lines of code for the type checker, slightly less than 1k are used for the policy language, including constraint solving. Most of the complexity for the remainder comes simply from the fact that Java is a large language, with many syntactic constructs. Note that, as per phase 1, our policy type checker includes a (superset of a) full type checker for ordinary Java types.

On top of the compiler itself, some 1500 lines of Java code are written for our runtime representations of Paragon entities.

Runtime overhead. Supporting lock queries and policy comparisons at runtime yields a negligible overhead on Paragon programs. Most of the additional generated code handles the initialisation of policies and locks upon class or object instantiation, as well as the opening and closing of locks, which does not give any significant performance penalty. More involved are the lock queries and policy comparisons themselves since they resemble essentially Datalog program evaluation and respectively containment [50]. However, our experience shows that clause bodies consist of just a few atoms, and have yet to find an example involving locks with arity higher than two, so in practice we posit that this overhead is negligible as well.