Only Connect, Securely

Abstract

The lattice model proposed by Denning in her seminal work provided secure information flow analyses with an intuitive and uniform mathematical foundation. Different organisations, however, may employ quite different security lattices. In this paper, we propose a connection framework that permits different organisations to exchange information while maintaining both security of information flow as well as their autonomy in formulating and maintaining security policies. Our prescriptive framework is based on the rigorous mathematical framework of Lagois connections given by Melton, together with a simple operational model for transferring object data between domains. The merit of this formulation is that it is simple, minimal, adaptable and intuitive, and provides a formal framework for establishing secure information flow across autonomous interacting organisations. We show that our framework is semantically sound, by proving that the connections proposed preserve standard correctness notions such as non-interference.

Supported by Indo-Japanese project Security in the IoT Space, DST, Govt of India.

1 Introduction

Denning’s seminal work [7] proposed complete lattices¹ as the appropriate mathematical framework for questions regarding secure information flow (SIF), i.e., only authorised flows of information are possible. An information flow model (IFM) is characterised as $\langle N, P, SC, \sqcup , \sqsubseteq \rangle$ where: Storage objects in N are assigned security classes drawn from a (finite) complete lattice SC. P is a set of processes (also assigned security classes as clearances). The partial ordering $\sqsubseteq$ represents permitted flows between classes; reflexivity and transitivity capture intuitive aspects of information flow; antisymmetry helps avoid redundancies in the framework, and the join operation $\sqcup$ succinctly captures the combination of information belonging to different security classes in arithmetic, logical and computational operations. This lattice model provides an abstract uniform framework that identifies the commonalities of the variety of analyses for different applications – e.g., confidentiality and trust – whether at the language level or at a system level. In the ensuing decades, the vast body of secure information flow analyses has been built on these mathematical foundations, with the development of a plethora of static and dynamic analysis techniques for programming languages [13, 15, 17, 19,20,21], operating systems [2, 8, 12, 20, 25], databases [22], and hardware architectures [9, 27], etc.

The soundness of this lattice model was expressed in terms of semantic notions of system behaviour, for instance, as properties like non-interference [10] by Volpano et al. [23] and others. Alternative semantic notions of security such as safety properties have been proposed as well, e.g., [1], but for brevity we will not explore these further.

The objective of this paper is to propose a simple way in which large-scale distributed secure systems can be built by connecting component systems in a secure and modular manner. Our work begins with the observation that large information systems are not monolithic: Different organisations define their own information flow policies independently, and subsequently collaborate or federate with one another to exchange information. In general, the security classes and the lattices of any two organisations may be quite different—there is no single universal security class lattice. Moreover, modularity and autonomy are important requirements since each organisation would naturally wish to retain control over its own security policies and the ability to redefine them. Therefore, fusing different lattices by taking their union is an unsatisfactory approach, more so since the security properties of application programs would have to be re-established in this possibly enormous lattice.

When sharing information, most organisations limit the cross-domain communications to a limited set of security classes (which we call transfer classes). In order to ensure that shared data are not improperly divulged, two organisations usually negotiate agreements or memorandums of understanding (MoUs), promising that they will respect the security policies of the other organisation. We argue that a good notion of secure connection should require reasoning only about those flows from just the transfer classes mentioned in a MoU. Usually, cross-domain communication involves downgrading the security class of privileged information to public information using primitives such as encryption, and then upgrading the information to a suitable security class in the other domain. Such approaches, however, do not gel well with correctness notions such as non-interference. Indeed the question of how to translate information between security classes of different lattices is interesting [6].

Contributions of This Paper. In this paper, we propose a simple framework and sufficient conditions under which secure flow guarantees can be enforced without exposing the complexities and details of the component information flow models. The framework consists of (1) a way to connect security classes of one organisation to those in another while satisfying intuitive requirements; (2) a simple language that extends the operations within an organisation with primitives for transferring data between organisations; and (3) a type system and operational model for these constructs, which we use to establish that the framework conserves security.

In Sect. 2, we first identify, using intuitive examples, violations in secure flow that may arise when two secure systems are permitted to exchange information in both directions. Based on these lacunae, we formulate security and precision requirements for secure bidirectional flow. We then propose a framework that guarantees the absence of such policy violations, without impinging on the autonomy of the individual systems, without the need for re-verifying the security of the application procedures in either of the domains, and confining the analysis to only the transfer classes involved in potential exchange of data. Our approach is based on monotone functions and an elegant theory of connections [16] between the security lattices. Theorem 1 shows that Lagois connections between the security lattices satisfy the security and precision requirements.

We present in Sect. 3 a minimal operational language consisting of a small set of atomic primitives for effecting the transfer of data between domains. The framework is simple and can be adapted for establishing secure connections between distributed systems at any level of abstraction (language, system, database, ...). We assume each domain uses atomic transactional operations for object manipulation and intra-domain computation. The primitives of our model include reliable communication between two systems, transferring object data in designated output variables of one domain to designated input variables of a specified security class in the other domain. We also assume a generic set of operations in each domain for copying data from input variables to domain objects, and from domain objects to output variables. To avoid interference between inter-domain communication and the computations within the domains, we assume that the sets of designated input and output variables are all mutually exclusive of one another, and also with the program/system variables used in the computations within each domain. Thus by design we avoid the usual suspects that cause interference and insecure transfer of data. The operational description of the language consists of the primitives together with their execution rules (Sect. 3.1).

The correctness of our framework is demonstrated by expressing soundness (with respect to the operational semantics) of a type system (Sect. 3.2), stated in terms of the security lattices and their connecting functions. In particular, Theorem 7 shows the standard semantic property of non-interference in both domains holds of all operational behaviours. We adapt and extend the approach taken by Volpano et al. [23] to encompass systems coupled using the Lagois connection conditions, and (assuming atomicity of the data transfer operations) show that security is conserved. Since our language is a minimal imperative model with atomic transactions, reads and writes as the basic elements, we are able to work with a simplified version of the type system of Volpano et al.. In particular, our language does not include conditional constructs in the transfer of data between domains, and assumes all conditional computation is absorbed within atomic intradomain transactions. Thus, we do not have to concern ourselves with issues of implicit flows that arise due to branching structures (e.g., conditionals and loops in programming language level security, pipeline mispredictions at the architectural level, etc.) While non-interference is the property addressed in this paper, we believe that our formulation is general enough to be applicable to other behavioural notions of secure information flow as a safety property [1].

In Sect. 4, we briefly review some related work. We conclude in Sect. 5 with a discussion on our approach and directions for future work.

2 Lagois Connections and All that

Motivating Examples. Consider a university system in which students study in semi-autonomously administered colleges (one such is ) that are affiliated to a university (). The university also has “university professors” with whom students can take classes. We assume each institution has established the security of its information flow mechanisms and policies.

We first observe that formulating an agreement between the institutions which respects the flow policies within each institution is not entirely trivial. Consider an arrangement where the College Faculty and University Faculty can share information (say, course material and examinations), and the Dean of Colleges in the University can exchange information (e.g., students’ official grade-sheets) with the college’s Dean of Students. Even such an apparently reasonable arrangement suffers from insecurities, as illustrated in Fig. 1 by the flow depicted using dashed red arrows, where information can flow from the college’s Faculty to the college’s Dean of Students. (Moral: internal structure of the lattices matters.)

Fig. 1.

Solid green arrows represent permitted flows according to the information exchange arrangement between a college and a university. Red dash-dotted arrows highlight a new flow that is a security violation. (Color figure online)

Fig. 2.

Unidirectional flow: If the solid blue arrows denote identified flows connecting important classes, then the dashed green arrows are constrained by monotonicity to lie between them. (Color figure online)

As long as information flows unidirectionally from colleges to the University, monotone functions from the security classes of the college lattice to those in the university security lattice suffice to ensure secure information flow. A function is called monotone if whenever in then in .² Monotonicity also constrains possible flows between classes of the two domains, once certain important flows between certain classes have been identified (see Fig. 2). Moreover, since monotone functions are closed under composition, one can chain them to create secure unidirectional information flow connections through a series of administrative domains. Monotonicity is a basic principle adopted for information flow analyses, e.g. [13].

Fig. 3.

The solid blue/green and dashed brown/red arrows respectively define monotone functions in each direction. However, the dash-dotted red arrow highlights a flow that is a security violation. (Color figure online)

Fig. 4.

The arrows define a secure and precise connection. However, the security classification escalates quickly in a few round-trips when information can flow in both directions.

However, when there is “blowback” of information, mere monotonicity is inadequate for ensuring SIF. Consider the bidirectional flow situation in Fig. 3, where data return to the original domain. Monotonicity of both functions and does not suffice for security because the composition may not be non-decreasing. In Fig. 3, both and are monotone but their composition can lead to information leaking from a higher class, e.g., College Principal, to a lower class, e.g., Faculty within —an outright violation of the college’s security policy. Similarly, composition may lead to violation of the University’s security policy.

Fig. 5.

Secure flow conditions: (sc1)   (sc2) .

Requirements. We want to ensure that any “round-trip” flow of information, e.g., from a domain to and back to , is a permitted flow in the lattice , from where the data originated. Thus we require the following (tersely stated) “security conditions” SC1 and SC2 on and , which preclude any violation of the security policies of both the administrative domains (see Fig. 5):

In other words, the data can flow only in accordance with the flows permitted by the ordering relations of the two lattices.

We also desire precision, based on a principle of least privilege escalation—if data are exchanged between the two domains without any computation done on them, then the security level should not be needlessly raised. Precision is important for meaningful and useful analyses; otherwise data would be escalated to security classes which permit very restricted access.

Further, if the data were to go back and forth between two domains more than once, the security classes to which data belong should not become increasingly restrictive after consecutive bidirectional data sharing (See Fig. 4, which shows monotone functions that keep climbing up to the top). This convergence requirement may be stated informally as conditions CC1 and CC2, requiring fixed points for the compositions and . Since security lattices are finite, CC1 and CC2 necessarily hold – such fixed points exist, though perhaps only at the topmost elements of the lattice. We would therefore desire a stronger requirement, where fixed points are reached as low in the orderings as possible.

Fig. 6.

The arrows between the domains define a Galois Connection. However, the red dash-dotted arrows highlight flow security violations when information can flow in both directions. (Color figure online)

Fig. 7.

A useful increasing Lagois connection for sharing data. Dashed black arrows define permissible flows between buds.

Galois Connections Aren’t the Answer. Any discussion on a pair of partial orders linked by a pair of monotone functions suggests the notion of a Galois connection, an elegant and ubiquitous mathematical structure that finds use in computing, particularly in static analyses. However, Galois connections are not the appropriate structure for bidirectional informational flow control.

Let and be two complete security class lattices, and and be two monotone functions such that forms a Galois connection. Recall that a Galois connection satisfies the condition

So in a Galois connection we have . Since holds trivially, we get . If then (strictly), which would violate secure flow requirement SC2. Figure 6 illustrates such a situation.

Why Not Galois Insertions? Now suppose and are two complete security class lattices, and and be two monotone functions such that forms a Galois insertion, i.e., a Galois connection where $\alpha$ is surjective:

Then the flow of information permitted by and is guaranteed to be secure. However, Galois insertions mandate conditions on the definitions of functions and that are much too strong, i.e.,

• is injective, i.e.,

• is surjective, i.e., .

Typically data are shared only from a few security classes of any organisation. Organisations rarely make public their entire security class structure and permitted flow policies. Organisations also typically do not want any external influences on some subsets of its security classes. Thus, if not all elements of are transfer classes, it may be impossible to define a Galois insertion because we cannot force to be surjective.

Lagois Connections. Further, the connection we seek to make between two domains should allow us to transpose them. Fortunately there is an elegant structure, i.e., Lagois Connections [16], which exactly satisfies this as well as the requirements of security and bidirectional sharing (SC1, SC2, PC1, PC2, CC1 and CC2). They also conveniently generalise Galois insertions.

Definition 1

(Lagois Connection [16]). If and are two partially ordered sets, and and are order-preserving functions, then we call the quadruple an increasing Lagois connection, if it satisfies the following properties:

LC3 ensures that is the least upper bound of all security classes in that are mapped to the same security class, say in .

The main result of this section is that if the negotiated monotone functions and form a Lagois connection between the security lattices and , then information flows permitted are secure and precise.

Theorem 1

Let and be two complete security class lattices, and be two monotone functions. Then the flow of information permitted by , satisfies conditions SC1, SC2, PC1, PC2, CC1 and CC2 if is an increasing Lagois connection.

Proof

Condition SC1 holds because if , by monotonicity of , . But by LC1, . So . (A symmetric argument holds for SC2.) Conditions PC1 and PC2 are shown in Proposition 3.7 of [16]. Conditions CC1 and CC2 hold since the compositions and are closure operators, i.e., idempotent, extensive, order-preserving endo-functions on and .

In fact, Lagois connections (e.g. Fig. 7) ensure that information in a security class in the original domain remains accessible even after doing a round-trip from the other domain (Proposition 3.8 in [16]):

(1)

(2)

Properties of Lagois Connections. We list some properties of Lagois connections that assist in the construction of a secure connection, and in identifying those security classes that play an important role in the connection. Proposition 2 says that the two functions and uniquely determine each other.

Proposition 2

(Proposition 3.9 in [16]). If is a Lagois connection, then the functions and uniquely determine each other; in fact

(3)

(4)

Proposition 3 shows the existence of dominating members in their pre-images, which act as equivalence-class representatives of the equivalence relations and induced by the functions and .

Proposition 3

(Proposition 3.7 in [16]). Let be a Lagois connection and let and . Then has a largest member, which is , and has a largest member, which is .

That is, for all and , and exist. Also, the images and are isomorphic lattices. and define a system of representatives for and . Element in , called a budpoint, acts as the representative of the equivalence class in the following sense:

(5)

Symmetrically, defines a system of representatives for . These budpoints play a significant role in delineating the connection between the transfer classes in the two lattices.

Further, Proposition 4 shows that these budpoints are closed under meets. This property enables us to confine our analysis to just these classes when reasoning about bidirectional flows.

Proposition 4

(Proposition 3.11 in [16]). If is a Lagois connection and , then

• 1. the meet of in exists if and only if the meet of in exists, and whenever either exists, they are equal.

• 2. the join of in exists if the join of in exists, and in this case

3 An Operational Model

3.1 Computational Model

Let us consider two different organisations and that want to share data with each other. We start with the assumptions that the two domains comprise storage objects and respectively, which are manipulated using their own sets of atomic transactional operations, ranged over by and respectively. We further assume that these transactions within each domain are internally secure with respect to their flow models, and have no insecure or interfering interactions with the environment. Thus, we are agnostic to the level of abstraction of the systems we aim to connect securely, and since our approach treats the application domains as “black boxes”, it is readily adaptable to any level of discourse (language, system, OS, database) found in the security literature.

We extend these operations with a minimal set of operations to transfer data between the two domains. To avoid any concurrency effects, interference or race conditions arising from inter-domain transfer, we augment the storage objects of both domains with a fresh set of export and import variables into/from which the data of the domain objects can be copied atomically. We designate these sets as the respective export variables, and as the respective import variables, with the corresponding variable instances written as , and , . These export and import variables form mutually disjoint sets, and are distinct from any extant domain objects manipulated by the applications within a domain. These variables are used exclusively for transfer, and are manipulated atomically. We let range over all variables in (respectively over ). Domain objects are copied to export variables and from import variables by special operations and (and and in the other domain). We assume atomic transfer operations (trusted by both domains) $T_{RL}, T_{LR}$ that copy data from the export variables of one domain to the import variables of the other domain as the only mechanism for inter-domain flow of data. Let “phrase” p denote a command in either domain or a transfer operation, and let s be any (empty or non-empty) sequence of phrases.

Fig. 8.

Execution rules

A store (typically ) is a finite-domain function from variables to a set of values (not further specified). We write, e.g., for the contents of the store at variable , and for the store that is the same as everywhere except at variable , where it now takes value .

The rules specifying execution of commands are given in Fig. 8. Assuming the specification of intradomain transactions () of the form and , our rules allow us to specify judgments of the form for phrases, and the reflexive-transitive closure for sequences of phrases. Note that phrase execution occurs atomically, and the intra-domain transactions, as well as copying to and from the export/import variables affect the store in only one domain, whereas the atomic transfer is only between export variables of one domain and the import variables of the other.

3.2 Typing Rules

Let the two domains have the respective different IFMs:

such that the flow policies in both are defined over different sets of security classes and .³

The (security) types of the core language are as follows. Metavariables and range over the sets of security classes, and respectively, which are partially ordered by and . A type assignment is a finite-domain function from variables to (respectively, from to ). The important restriction we place on and is that they map export and import variables only to points in the security lattices and respectively which are in the domains of and , i.e., these points participate in the Lagois connection. Intuitively, a variable w mapped to security class can store information of security class or lower. The type system works with respect to a given type assignment. Given a security level, e.g., , the typing rules track for each command within that domain whether all written-to variables in that domain are of security classes “above” , and additionally for transactions within a domain, they ensure “simple security”, i.e., that all variables which may have been read belong to security classes “below” . We assume for the transactions within a domain, e.g., , we have a type system that will give us judgments of the form . The novelty of our approach is to extend this framework to work over two connected domains, i.e., given implicit security levels of the contexts in the respective domains. Cross-domain transfers will require pairing such judgments, and thus our type system will have judgments of the form

We introduce a set of typing rules for the core language, given in Fig. 9. In many of the rules, the type for one of the domains is not constrained by the rule, and so any suitable type may be chosen as determined by the context, e.g., in the rules , , and , and both and in Com0.

Fig. 9.

Typing rules

For transactions e.g., entirely within domain , the typing rule constrains the type in the left domain to be at a level that dominates all variables read in , and which is dominated by all variables written to in , but places no constraints on the type in the other domain . In the rule , since a value in import variable is copied to the variable , we have , and the type in the domain is with no constraint on the type in the other domain. Conversely, in the rule , since a value in variable is copied to the export variable , we have , and the type in the domain is with no constraint on the type in the other domain. In the rule , since the contents of a variable in domain are copied into a variable in domain , we require , and constrain the type in domain to . The constraint in the other domain is unimportant (but for the sake of convenience, we peg it at ). Finally, for the types of sequences of phrases, we take the meets of the collected types in each domain respectively, so that we can guarantee that no variable of type lower than these meets has been written into during the sequence. Note that Proposition 4 ensures that these types have the desired properties for participating in the Lagois connection.

3.3 Soundness

We now establish soundness of our scheme by showing a non-interference theorem with respect to operational semantics and the type system built on the security lattices. This theorem may be viewed as a conservative adaptation (to a minimal secure data transfer framework in a Lagois-connected pair of domains) of the main result of Volpano et al. [23].

We assume that underlying base transactional languages in each of the domains have the following simple property (stated for , but an analogous property is assumed for ). Within each transaction , for each assignment of an expression to any variable , the following holds: If , are two stores such that for all , we have , then after executing the assignment, we will get . That is, if two stores are equal for all variables appearing in the expression , then the value assigned to the variable will be the same. This assumption plays the rôle of “Simple Security” of expressions in [23] in the proof of the main theorem. The type system plays the rôle of “Confinement”. We start with two obvious lemmas about the operational semantics, namely preservation of domains, and a “frame” lemma:

Lemma 5

(Domain preservation). If , then , and .

Proof

By induction on the length of the derivation of .

Lemma 6

(Frame). If , and w is not assigned to in s, then and .

Proof

By induction on the length of the derivation of .

The main result of the paper assumes an “adversary” that operates at a security level in domain and at security level in domain . Note however, that these two levels are interconnected by the monotone functions and , since these levels are connected by the ability of information at one level in one domain to flow to the other level in the other domain. The following theorem says that if (a) a sequence of phrases is well-typed, and (b, c) we start its execution in two store configurations that are (e) indistinguishable with respect to all objects having security class below and in the respective domains, then the corresponding resulting stores after execution continue to remain indistinguishable on all variables with security classes below these adversarial levels.

Theorem 7

(Type Soundness). Suppose are the “adversarial” type levels in the respective domains, which satisfy the condition and . Let

• (a) ;     (s has security type )

• (b) ;   (execution of s starting from )

• (c) ;   (execution of s starting from )

• (d) and ;

• (e) for all such that , and for all such that .

Then for all such that , and for all such that .

Proof

By induction on the length of sequence s. The base case is vacuously true. We now consider a sequence $s_1; p$. and and and By induction hypothesis applied to $s_1$, we have for all such that , and for all such that .

Let , and . We examine four cases for p (the remaining cases are symmetrical).

Case p is : Consider any such that . If (i.e., it doesn’t appear in ), or if but is not assigned to in , then by Lemma 6 and the induction hypothesis, .

Now suppose is assigned to in . From the condition , we know that for all assigned in , and for all read in , . Now if , then since in no variables such that are assigned to. Therefore by Lemma 6, , for all such that .

If , then for all read in , . Therefore, by assumption on transaction , if any variable is assigned an expression , since , are two stores such that for all , , the value of will be the same. By this simple security argument, after the transaction , we have . Since the transaction happened entirely and atomically in domain , we do not have to worry ourselves with changes in the other domain , and do not need to concern ourselves with the adversarial level .

Case p is : Thus , which means . If , there is nothing to prove (Lemma 6, again). If , then since by I.H., , we have .

Case p is : Thus , which means . If , there is nothing to prove (Lemma 6, again). If , then since by I.H., , we have .

Case p is : So , and . If , there is nothing to prove (Lemma 6, again). If , then by transitivity, . By monotonicity of : (By our assumption on and ). But by LC2, . So by transitivity, . Now, by I.H., since , we have .

4 Related Work

The notion of Lagois connections [16] has surprisingly not been employed much in computer science. The only cited use of this idea seems to be the work of Huth [11] in establishing the correctness of programming language implementations. To our knowledge, our work is the only one to propose their use in secure information flow control.

Abstract Interpretation and type systems [5] have been used in secure flow analyses, e.g., [3, 4] and [24], where security types are defined using Galois connections employing, for instance, a standard collecting semantics. Their use of two domains, concrete and abstract, with a Galois connection between them, for performing static analyses within a single domain should not be confused with our idea of secure connections between independently-defined security lattices of two organisations.

There has been substantial work on SIF in a distributed setting at the systems level. DStar [26] for example, uses sets of opaque identifiers to define security classes. The DStar framework extends a particular Decentralized Information Flow Control (DIFC) model [12, 25] for operating systems to a distributed network. The only partial order that is considered in DStar’s security lattice is subset inclusion. So it is not clear if DStar can work on general IFC mechanisms such as FlowCaml [19], which can use any partial ordering. Nor can it express the labels of JiF [17] or Fabric [13] completely. DStar allows bidirectional communication between processes R and S only if $L_R \sqsubseteq _{O_R} L_S$ and $L_S \sqsubseteq _{O_S} L_R$, i.e., if there is an order-isomorphism between the labels. Our motivating examples indicate such a requirement is far too restrictive for most practical arrangements for data sharing between organisations.

Fabric [13, 14] adds trust relationships directly derived from a principal hierarchy to support federated systems with mutually distrustful nodes and allows dynamic delegation of authority.

Most of the previous DIFC mechanisms [2, 8, 12, 17, 20, 25] including Fabric are susceptible to the vulnerabilities illustrated in our motivating examples, which we will mention in the concluding discussion.

5 Conclusions and Future Work

Our work is similar in spirit to Denning’s motivation for proposing lattices, namely to identify a simple and mathematically elegant structure in which to frame the construction of scalable secure information flow in a modular manner that preserved the autonomy of the individual organisations. From the basic requirements, we identified the elegant theory of Lagois connections as an appropriate structure. Lagois connections provide us a way to connect the security lattices of two (secure) systems in a manner that does not expose their entire internal structure and allows us to reason only in terms of the interfaced security classes. We believe that this framework is also applicable in more intricate information flow control formulations such as decentralised IFC [18] and models with declassification, as well as formulations with data-dependent security classes [15]. We intend to explore these aspects in the future.

In this paper, we also proposed a minimal operational model for the transfer of data between the two domains. This formulation is spare enough to be adaptable at various levels of abstraction (programming language, systems, databases), and is intended to illustrate that the Lagois connection framework can conserve security, using non-interference as the semantic notion of soundness. The choice of non-interference and the use of a type system in the manner of Volpano et al. [23] was to illustrate in familiar terms how those techniques (removed from a particular language formulation) could be readily adapted to work in the context of secure connections between lattices. In this exercise, we made suitable assumptions of atomicity and the use of fresh variables for communication, so as to avoid usual sources of interference. By assuming that the basic intra-domain transactions are atomic and by not permitting conditional transfer of information across domains in the language, we have avoided dealing with issues related to implicit flows. We believe that the Lagois connection framework for secure flows between systems is readily adaptable for notions of semantic correctness other than non-interference, though that is an exercise for the future.

In the future we intend to explore how the theory of Lagois connections constitutes a robust framework that can support the discovery, decomposition, update and maintenance of secure MoUs for exchanging information. In this paper, we concerned ourselves only with two domains and bidirectional information exchange. Compositionality of Lagois connections allows these results to extend to chaining connections across several domains. In the future, we also intend to explore how one may secure more complicated information exchange arrangements than merely chains of bidirectional flow.

We close this discussion with a reminder of why it is important to have a framework in which secure flows should be treated in a modular and autonomous manner. Consider Myer’s DIFC model described in [18], where a principal can delegate to others the capacity to act on its behalf. We believe that this notion does not scale well to large, networked systems since a principal may repose different levels of trust in the various hosts in the network. For this reason, we believe that frameworks such as Fabric [13, 14] may provide more power than mandated by a principle of least privilege. In general, since a principal rarely vests unqualified trust in another in all contexts and situations, one should confine the influence of the principals possessing delegated authority to only specific domains. A mathematical framework that can deal with localising trust and delegation of authority in different domains and controlling the manner in which information flow can be secured deserves a deeper study. We believe that algebraic theories such as Lagois connections can provide the necessary structure for articulating these concepts.