Primer on lattices in access & information flow control

[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.