Primer on lattices in access & information flow control

[graphomath]

If you wonder why we do not only consider access control, note that a “practical system needs both access and flow control to satisfy all security requirements”^[1]. Thus, we naturally will be lead to information flow control once we start thinking about access control.

In this post, let us focus on a concept that is shared between access control and information flow control. Looking on Wikipedia, we find lattice-based access control as a natural starting point; in particular, we have a lattice of security classes. Evidently, more than four decades later, a lot of research has been done. However, let us go back to the 70ies to get a feeling for the lattice-based approach.

One kind of access control mechanism

Denning introduces flow models for objects (in a set N), processes (in a set P), security classes (in a set SC), which come with a suitable operator for combining classes (written \oplus); most notably, we have a flow relation, modelling the allowed flow of information, in particular “direct” access, denoted \to. Thus, a full information flow model is a 5-tuple.

FM = \langle N, P, SC, \oplus , \to \rangle

Denning explains this model in one short paragraph, showing how it related to access control, referencing two pre-existing approaches to access control (from the early days of computer science).

In both the Case system [22] and the MITRE system [2], each process p has an associated clearance class \underline{\smash p} specifying the highest class p can read from (observe) and the lowest class p can write into (modify or extend). Security is enforced by a run-time mechanism that permits p to acquire read access to an object a only if \underline a \to \underline{\smash p}, and write access to an object b only if \underline{\smash p} \to \underline b. Hence, p can read from a_1,\ldots, a_m and write into b_,\ldots , b_n only if \underline a_1 \oplus \ldots \oplus \underline a_m \to \underline{\smash p} \to \underline b_1 \otimes \ldots \otimes \underline b_n,. This mechanism automatically guarantees the security of all flows, explicit or implicit, since no flow from an object a to an object b can occur unless \underline{\smash a} \to \underline{\smash p} \to \underline b, which implies \underline a \to \underline b.

Here, we see that the lattice of security classes is distinct from the set of processes. In fact, all information flow information congregate into a unifying lattice of IFC labels.

What next?

One of the many advances is the unification of all information flow information into a a unifying lattice^[2] This is where we shall continue in follow up posts. Finally, developers and user will benefit from good languages for expressing access control and information flow policies (see, e.g., SecureUML). Then there are questions of how we can “lift” access control from single method invocations to hierarchical transactions while avoiding side-channels.

Last, but not least: comments and questions are more than welcome!

---

References

• Model driven security: from UML models to access control infrastructures
• A Lattice Model of Secure Information Flow
• Flow-Limited Authorization
• SecureUML

---

1. This quote is from Denning’s paper A Lattice Model of Secure Information Flow. ↩︎

2. In particular, § 3.5.2 describes how access control is captured. ↩︎

[cwgoes]

Thank you for the write-up! I am wondering how best to connect this prior art to (a) the theoretical structure of the AVM and (b) the practical operational details of the resource machine and distributed network. I’m not quite sure how to synthesize all of this yet, so I will start here with a practical proposal for simple access control annotations at the AVM level which can be implemented with verifiable encryption and authorization checks at the resource level.

Let’s take as an example everybody’s favourite application: shielded kudos (a simple version).

Read permissions

First, read permissions. Recall the structure of balance queries: the user calls getBalance on the application (simple kudos) object, which results in scanning all kudo resources owned by the user, adding up their amounts, and returning the total, like (abstractly) so:

Now, suppose that we want to make this balance private (shielded), so that only the user who owns the kudos resources (A in the diagram) can read their balance. Suppose that we have some way to label methods (specific messages sent to objects) with metadata that specifies a restriction on “who” can call those methods (however exactly we might implement this). Which metadata would we need here? Let’s assume for now that we put metadata on all the methods, like so:

Note that here the metadata for the top-level “SimpleKudos” object is dependent, in that A is both part of the message data and part of the metadata, while for all the other objects A is fixed, so the metadata is too.

How could we operationalize this? Luckily, A is already in the right form – an external identity which defines an encryption function – so we could simply enforce in the resource logic that newly created kudo resources owned by A verifiably encrypt their data to A. Presto!

Write permissions

What about write permissions? In the simple shielded kudos app, we want kudos to be transferable only by whoever “owns” them – this “ownership” is really just a write permission. How should we represent this, exactly? Let’s start with the simple “transfer” message diagram:

Now, we want only A to be able to effect a transfer from A, let’s label that:

What else do we need to label? In some form, probably any subtraction from A’s balance / consumption of resources owned by A:

Note: here we’re assuming that the receiver’s authorization is not required to receive a transfer – we may well want this for the “real” shielded kudos application, but we don’t need it for this simplified example.

So far, so good, but how do we operationalize this? A is an external identity, with a verify method, which we should use, but what exactly do we call verify on? Semantically, at a high level, we just need to call verify on some commitment to the transfer(A, B, 6) message sent to the SimpleKudos object, such that the SimpleKudos object will not accept/process that message unless a valid commitment was produced by A. Clear enough for the SimpleKudos object, but what about for the A balance object and the specific resources? Here I think hierarchical object compilation will need to come into play – we want to translate this high-level picture into checks in the low-level resource logics which will ultimately indeed check a commitment to transfer(A, B, 6) but without “SimpleKudos” itself needing to be represented as a resource.

Many details to figure out here, but to me some high-level takeaways are:

• Initially, we’re just talking about access control in the sense of “which principals [represented by external identities] can call a particular method on a particular object”. This is actually the same for “read permissions” and “write permissions” – the difference between read and write permissions is whether the method in question can mutate (consume/create resources) or just read, but in both cases, it’s a permission defined in terms of which principal(s) can call the method.
• Two lattice structures are already implied by the external identity type, where A \lt B w.r.t. encryption iff. B can decrypt anything that A can decrypt, A \lt B w.r.t. authorization if B can authorize anything that A can authorize, and the join/meet are given by conjunction/disjunction. This should be formalized more, I think there are many similarities with the FLA paper.
• Read access control can be implemented with verifiable encryption using the encrypt function of the external identity.
• Write access control can be implemented with authorization using the verify function of the external identity. What exactly all of the checks should be is related to the question of hierarchical transactional object compilation/representation.
• There are hierarchical access control relations implied by the hierarchical transactional object system model – at minimum, we should perform some consistency-checks on labels, and we might be able to perform certain kinds of inference (on what labels low-level object methods need to have in order to implement desired higher-level labels) – more research is needed here.