Flow-limited authorization for consensus,replication,and secret sharing 1

1. Introduction

Failure is inevitable in distributed systems, but its consequences may vary. The consequences of failure are particularly severe in centralized system designs, where single points-of-failure can render the entire system inoperable. Even distributed systems are sometimes built using a single, centralized authority to execute security-critical tasks. If this trusted entity is compromised, the security of the entire system may be compromised as well.

Building reliable decentralized systems, which have no single point-of-failure, is a complex task. Quorum replication protocols such as Paxos [16] and PBFT [7], and blockchains such as Bitcoin [21] replicate state and computation at independent hosts and use consensus protocols to ensure the integrity and availability of operations on system state. In these protocols, there is neither centralization of function nor centralization of trust: all honest hosts work to replicate the same computation on the same data, and this redundancy helps the system tolerate a bounded number of node failures and corruptions.

Within a single trust domain such as a corporate data center, replicas likely have uniform trust relationships and may be treated interchangeably. However, many large-scale systems depend on services hosted by multiple external services. Even when a service’s internal components are replicated, developers must take into account the failure properties of external dependencies when considering their own robustness.

Information flow control (IFC) has been used to enforce decentralized security in distributed systems for confidentiality and integrity (e.g., Fabric [18] and DStar [28]). Less attention has been paid to enforcing decentralized availability policies with IFC. In particular, no language (or protocol) we are aware of addresses systems that compose multiple quorums or consider quorum participants with arbitrary trust relationships.

To build a formal foundation for such languages, we present FLAQR, a core calculus for Flow-Limited Authorization [3] for Quorum Replication. FLAQR uses high-level abstractions for replication and consensus that help manage tradeoffs between the availability and integrity of computation and data.

OPEN IN VIEWER

Fig. 1.

Integrity-availability trade-off.

Consider the scenarios in Fig. 1. Shaded boxes represent hosts in a distributed system. Dashed lines denote outputs that contribute to the final result, a value v. Dotted lines denote ignored outputs and solid lines indicate the flow of data from an initial expression e distributed to hosts to the collected result. Results are accompanied by labels that indicate which hosts influenced the final result.

In Fig. 1(b), e is distributed to hosts alice and bob . The hosts’ results are compared and, if they match, the result is produced. Since a value is output only if the values match, we can treat the output of this protocol as having more integrity than just alice or bob . While both alice and bob technically influence the output, neither host can unilaterally control its value. However, either host can cause the protocol to fail.

By contrast, the protocol in Fig. 1(a) prioritizes availability over integrity: if either alice or bob produce a value, the protocol outputs a value – in this case alice ’s. Here, neither host can unilaterally cause a failure; the protocol only fails if both alice and bob fail. Either alice or bob (but not both) has complete control over the result in the event of the other’s failure, so we should treat the output as having less integrity than just alice or bob .

With an adequate number of hosts, we can combine these two techniques to form the essential components of a quorum system. In Fig. 1(c), e is replicated to alice , bob , and carol . This protocol outputs a value if any two hosts have matching outputs. Since alice and bob both output v, the protocol outputs v and attaches alice and bob ’s signatures. The non-matching value v ′ from carol is ignored. Hence, this protocol prevents any single host from unilaterally controlling the failure of the protocol or its output.

Figure 1(c) is similar in spirit to consensus protocols such as Paxos or PBFT where quorums of independent replicas are used to tolerate a bounded number of failures. FLAQR also permits us to write protocols where principals have differing trust relationships. Figure 1(d) illustrates a protocol that tolerates failure (or corruption) of either alice or bob , but requires dave ’s output to be part of any quorum. This protocol will fail if both alice and bob fail to produce matching outputs, but can also fail if dave fails to produce a matching output. This example illustrates the distributed systems where the hosts do not have homogeneous trust.

The main contributions of this paper are:

This paper is an expanded and updated version of an article previously published in the proceedings of the 35th Computer Security Foundations Symposium [19]. This version adds support for secret sharing (Section 9) and extensions of our previous results that demonstrate these new terms neither impact integrity and availability noninterference, nor majority liveness, despite introducing an additional source of failure. In addition, we corrected a minor issue in the original blame semantics, and include complete rule sets and proofs for our formalization and theoretical results.

Non-goals. The design of FLAQR is motivated by application-agnostic consensus protocols such as Paxos [16] and PBFT [7], but our present goal is not to develop a framework for verifying implementations of such protocols (although it would be interesting future work). Rather, the goal is to develop security abstractions that make it easier to create components with application-specific integrity and availability guarantees, and compose them in a secure and principled way.

In particular, the FLAQR system model lacks some features that a protocol verification model would require, most notably a concurrent semantics, asynchronous message delivery, and arbitrary communication patterns. Although this simplifies some aspects of consensus protocols, our model retains many of the core challenges present in fault tolerance models. For example, perfect fault detection is impossible and faulty hosts can manipulate data to cause failures to manifest at other hosts. We argue that even in a synchronous, deterministic model with RPC-style communication, the challenges of specifying and enforcing policies remain quite difficult to solve, and are among the primary security concerns of high-level application developers.

In this section we present two motivating examples. The first example highlights the trade-off between integrity and availability. The second example highlights the need for availability policies in distributed systems.

2.1. Tolerating failure and corruption

If a bank’s deposit records are stored in a single node, then customers will be unable to access their accounts if that node is unavailable or is compromised. To eliminate this single point-of-failure, banks can replicate their records on multiple hosts as illustrated in Fig. 1(c). If a majority of hosts agree on an account balance, then the system can tolerate the remaining minority of hosts failing or returning corrupted results.

Consider a quorum system with three hosts: alice , bob , and carol . To tolerate the failure of a single node, balance queries attempt to contact all three hosts and compare the responses. As long as the client receives two responses with the same balance, the client can be confident the balance is correct even if one node is compromised or has failed.

OPEN IN VIEWER

Fig. 2.

Majority quorum.

Figure 2 illustrates a pseudocode implementation of getBalance in this system. The code fetches balances from the three hosts (lines 2–4). The function returns the balance if each fetched value matches, otherwise the function returns fail (lines 6–12).

The downside of this approach is that it is quite verbose and repetitive compared to a single-line fetch without any fault tolerance. Small mistakes in any of these lines could have significant consequences. For example, suppose a programmer typed bal _ b instead of bal _ c on line 8. This small change gives bob (or an attacker in control of bob ’s node) the ability to unilaterally choose the return value of the function, even when alice and carol agree on a different value.

2.2. Using best available services

Real world applications often consist of communication between entities with mutual distrust. The pseudocode in Fig. 3 communicates with two banks, represented by b and b ′ , during a distributed computation. A user has two accounts acc _ 1 , and acc _ 2 with b and b ′ respectively. The user has linked both accounts to a service and specifies the bill should be paid

as long as at least one account is available

using the highest-balance account, if available

Lines 7–10 take care of point (1), ensuring the comparison on line 12 does not get stuck if a fetch returns fail . Lines 12–15 cover point (2), returning the account with the highest balance when both balances are available.

OPEN IN VIEWER

Fig. 3.

Available largest balance.

This example shows how availability of data can effect the final result of an application and thus highlights the importance of enforcing availability in distributed computations. As in the previous example, the programmer must reason about failures due to unavailable hosts and make the correct comparisons to implement the (implicitly) desired policy. Furthermore, the programmer may be unaware of the availability guarantees offered by b and b ′ . For example, if b and b ′ rely on the same replicas to implement getBalance , the availability of highestBalance may be lower than expected.

Finally, in both of the above examples, an attacker should not be able to read an account balance, or infer which account balance was greater. With the FLAQR type-system, programmers can not only specify and enforce availability and integrity, but also confidentiality – crucial for dealing with sensitive information. Moreover, FLAQR enables programmers to write fault-tolerant code concisely, with explicit primitives for consensus and replication operations that clarify the programmer’s intentions.

FLAQR policies are specified using an extension of the FLAM [2,3] principal algebra that includes availability policies.2

We can write the conjunction of two principals with the Boolean connective ∧ as alice ∧ bob , denoting the combined authority of Alice and Bob. Put another way, alice ∧ bob is a principal both Alice and Bob trust. The disjunction of two principals’ authority is written using the connective ∨ as alice ∨ bob . This is a principal whose authority is less than both Alice and Bob; either Alice or Bob can act on behalf of the principal alice ∨ bob . Put another way alice ∨ bob is a principal that trusts both Alice and Bob. Authority projections distribute over ∧ and ∨, so for example ( alice ∧ bob ) i ≡ alice i ∧ bob i .

The confidentiality, integrity, and availability authorities make up the totality of a principal’s authority, so writing alice c ∧ alice i ∧ alice a is equivalent to writing alice . For brevity, we sometimes write alice c i as a shorthand for alice c ∧ alice i when we wish to include all but one kind of authority. Our complete formalization of the acts-for relation is presented in Figs 39 and 40 in Appendix A.

In addition to conjunctions and disjunctions of authority, FLAQR also introduce two new operators: partial conjunction ( ⊞ ), and partial disjunction ( ⊟ ). These operations are necessary to represent the tradeoffs between integrity and availability mediated by consensus and replication. Consider the “more integrity” protocol from Fig. 1(b). It is reasonable to think of the consensus value v as having more integrity than (or at least, “not less integrity than”) Alice or Bob alone, but it turns out to be useful to distinguish between this authority and the combined integrity authority of Alice and Bob, ( alice i ∧ bob i ). A principal with integrity authority ( alice i ∧ bob i ) may act arbitrarily on behalf of both Alice and Bob since it is trusted by them. In contrast, the integrity of the value produced in Fig. 1(b) is not fully trusted by Alice and Bob. Instead, Alice and Bob only trust the value when Alice and Bob agree on it. If they do not agree, that trust is revoked and no value is produced. For this reason, we describe the integrity of consensus values such as v as the partial conjunction of Alice and Bob, written alice i ⊞ bob i .

Similarly, for replication protocols like that in Fig. 1(a), we want to distinguish the integrity of values that may have been received from either Alice or Bob due to failure, from the integrity of values that may have been influenced by both Alice and Bob: alice i ∨ bob i . The integrity of a value produced by either Alice or Bob is written as the partial disjunction alice i ⊟ bob i . This principal does not have the same integrity authority as Alice or Bob alone since we cannot guarantee which host’s value will be used in the event of a failure. However, the value does have more integrity than alice i ∨ bob i , since only Alice or Bob (and not both) may have influenced it.

We compare the authority of principals using the acts-for relation ≽, which partially orders (equivalence classes of) principals by increasing authority. We form the set of all principals P as the closure of the set N ∪ { ⊤ , ⊥ } over the operations ∧, ∨, ⊞ , ⊟ , and authority projections c , i , and a . We say Alice acts for Bob (or equivalently, Bob trusts Alice) and write alice ≽ bob when Alice has at least as much authority as Bob. The ≽ relation forms a lattice with join ∧, meet ∨, greatest element ⊤, and least element ⊥.

In addition to the trust relationships such as p ∧ q ≽ p and p ≽ p i implied by the principal algebra, explicit delegations of trust such as p ≽ q (for any p, q in P ) may expressed using a delegation context Π. An acts-for judgment has the form Π ⊩ p ≽ q and means that p acts for q in context Π. While FLAC has a feature that allows dynamic extensions of Π, for simplicity we fix Π to a static set of delegations in FLAQR.

OPEN IN VIEWER

Fig. 4.

Selected acts-for rules for partial conjunction and disjunction.

OPEN IN VIEWER

Fig. 5.

The FLAQR authority lattice for the principal set { ⊥ , x , y , ⊤ } .

We extend the acts-for relation defined by Arden et al. [2] with new rules for availability authority and partial conjunction and disjunction. Figure 4 presents a selection of these rules – we have omitted the distributivity rules for brevity. In Fig. 4, an acts for judgement of form Π ⊩ p ≽ q , states that p has at least as much authority as q in delegation context Π. Figures 39 and 40 in Appendix A together present the complete formalization of the ≽ relation. In Fig. 40 we present only the extensions to this relation introduced by FLAQR.

As a consequence of these new acts-for rules we have additional distinct points in the authority lattice. Figure 5 illustrates the authority sublattice over elements { ⊥ , x , y , ⊤ } . Figure 5 shows the trust ordering of all possible distinct combinations of elements that can be formed on the set { ⊥ , x , y , ⊤ } with operations ∧, ∨, ⊞ and ⊟ over them. The relationship between principals ⊥ , x , y , x ∧ y , x ∨ y , and ⊤ is the same as in FLAM, but Fig. 5 also includes principals constructed using partial conjunctions and disjunctions. For example, x ∧ ( x ⊞ y ) is the least upper bound of x ∧ ( x ⊟ y ) and x ⊞ y . This is due to rule PAndPOr in Fig. 4, which lets us simplify x ∧ ( x ⊟ y ) ∧ x ⊞ y to x ∧ ( x ⊞ y ) .

To compare the restrictiveness of information flow policies, we use the flows-to relation ⊑, which partially orders principals by increasing policy restrictiveness, rather than by authority. For example, we say Alice’s integrity flows to Bob’s integrity and write alice i ⊑ bob i if Bob trusts information influenced by Alice at least as much as information he influenced himself. Likewise, we write alice c ⊑ bob c if Alice trusts Bob to protect the confidentiality of her information, and alice a ⊑ bob a if Bob is trusted to keep Alice’s data available. The flows-to relation behaves similarly to a sub-typing relation. Treating information labeled alice c i a (i.e. alice ) as though it was labeled bob c i a (i.e. bob ) is only safe (doesn’t violate anyone’s policies) if alice c i a ⊑ bob c i a (i.e. alice ⊑ bob ).

One advantage of the FLAM principal algebra is that we can define the flows-to relation, as well as the upper and lower bounds of information flow policies, in terms of the acts-for relation, simplifying our formalism. p ⊑ q ⇔ q c ≽ p c and p i ≽ q i and p a ≽ q a p ⊔ q ≜ ( p c ∧ q c ) ∧ ( p i ∨ q i ) ∧ ( p a ∨ q a ) p ⊓ q ≜ ( p c ∨ q c ) ∧ ( p i ∧ q i ) ∧ ( p a ∧ q a ) Based on this, the equivalence classes of ≽ and ⊑ are identical, meaning that the lattice formed by ⊑ with joins ⊔ and meets ⊓ has the same elements as the acts-for lattice. A flow from p to q is secure only when q c is at least as confidential as p c , q i trusts information influenced by p i , and q a cannot cause failures that p a cannot.

OPEN IN VIEWER

Fig. 6.

FLAQR syntax. Shaded terms are new to FLAQR. Underlined terms are used during evaluation and not available at the source level.

OPEN IN VIEWER

Fig. 7.

FLAQR local semantics.

OPEN IN VIEWER

Fig. 8.

FLAQR evaluation context.

Figures 6 and 7 present the FLAQR syntax and selected evaluation rules. Figure 8 presents the evaluation context. For space and exposition purposes, we omit some term annotations and standard lambda calculus rules in order to focus on FLAQR’s contributions, but the complete, annotated FLAQR syntax and semantics can be found in Figs 29 and 31 in the Appendix.

FLAQR is based on FLAC [2,5], a monadic calculus in the style of Abadi’s Polymorphic DCC [1]. In addition to standard extensions to System F [12,13,23] such as pairs and tagged unions, an Abadi-style calculus supports monadic operations on values in a monad indexed by a lattice of security labels. Such a value has a type of the form ℓ says τ , meaning that it is a value of type τ, protected at level ℓ, where ℓ is an element of the security lattice. Here we focus on FLAQR’s additions to FLAC and DCC, and refer the readers to Figs 33 and 34 in the Appendix for our complete formalization.

FLAQR builds on FLAC’s expressive principal algebra and type system to model distributed security policies for applications that use replication and consensus. FLAC supports arbitrary policy downgrades through dynamic delegations of authority, but for simplicity we omit these features in FLAQR.

The monadic unit or return term η ℓ e protects the value that e evaluates to at level ℓ (E-Sealed).4

The primary novelty in the FLAQR calculus is the introduction of compare and select terms for expressing consensus and replication operations. We represent the consensus problem as a comparison of two values with the same underlying type but distinct outer security labels. In other words, we want to check the equality of values produced by two different principals. If the values match, we can treat them as having the (partially) combined integrity of the principals. If not, then the principals failed to reach consensus.

Rule E-Compare defines the former case: two syntactically equal values protected at different labels evaluate to a value that combines labels using the compare action on labels ⊕ . Intuitively, ℓ 1 ⊕ ℓ 2 determines the increase in integrity and the corresponding decrease in availability inherent in requiring a consensus. We define ⊕ formally in Definition 1.

We also lift this notation to says types by defining ℓ 1 says τ ⊕ ℓ 2 says τ ≜ ( ℓ 1 ⊕ ℓ 2 ) says τ

As discussed in Section 3, the integrity authority of compare is not as trusted as the conjunction of ℓ 1 and ℓ 2 ’s integrity. Instead, we represent the limited “increase” in integrity authority5

OPEN IN VIEWER

Fig. 9.

fail propagation rules.

The decreased availability resulting from applying compare is more apparent in rules E-CompareFail, E-CompareFailL and E-CompareFailR. In E-CompareFail, two unequal values are compared, resulting in a failure. Failure is represented syntactically using a fail τ term. We use a type annotation τ on many terms in our formal definitions so that our semantics is well defined with respect to failure terms, but we omit most of these annotations in Fig. 7. These annotations are only necessary for our formalization and would be unnecessary in a FLAQR implementation.

A compare term may also result in failure if either subexpression fails. Rule E-CompareFailL and E-CompareFailR, defines how failure of an input propagates to the output. In fact, most FLAQR terms result in failure when a subexpression fails. Figure 9 presents selected failure propagation rules (complete failure propagation rules are presented in Fig. 32). Note that fail terms are treated similarly to values, but are distinct from them. For example, in E-AppFail, applying a lambda term to a fail term substitutes the failure as it would a value, but in E-SealedFail the failure is propagated beyond the monadic unit term. This latter behavior captures the idea that failures cannot be hidden or isolated in the same way as secrets or untrusted data.

Failures are tolerated using replication. A select term will evaluate to a value as long as at least one of its subexpressions does not fail. For example, rule E-SelectL returns its left subexpression when the right subexpression fails. In contrast to compare , applying select increases availability since either subexpression can be used, but reduces integrity since influencing only one of the subexpressions is potentially sufficient to influence the result of evaluating select . The effect of a select statement on the labels of its sub-expressions is captured with the select action ⊖ .

We define the select action on types similarly to compare: ℓ 1 says τ ⊖ ℓ 2 says τ = ( ℓ 1 ⊖ ℓ 2 ) says τ

The end result of a select statement, select ( η ‾ ℓ 1 v ) or ( η ‾ ℓ 2 v ) , will have integrity of either ℓ 1 i or ℓ 2 i since only one of the two possible values will be used. We use a partial disjunction to represent this integrity since the result does not have the same integrity as ℓ 1 or ℓ 2 , but does have more integrity than ℓ 1 ∨ ℓ 2 since it is never the case that both principals influence the output.

OPEN IN VIEWER

Fig. 10.

Global semantics.

OPEN IN VIEWER

Fig. 11.

Global configuration stack.

5. FLAQR typing rules

OPEN IN VIEWER

Fig. 12.

Typing rules for expressions.

As we have a local and global semantics, we have two corresponding forms of typing judgements: local typing judgments for expressions and global typing judgments for the stack. Local typing judgments have the form Π ; Γ ; p c ; c ⊢ e : τ . Π is the program’s delegation context and is used to derive acts-for relationships with the rules in Figs 4 and 40. Γ is the typing context containing in-scope variable names and their types. The p c label tracks the information flow policy on the program counter (due to control flow) and on unsealed protected values such as in the body of a bind .

Figure 12 presents a selection of local typing rules. Each typing rule includes an acts-for premise of the form Π ⊩ c ≽ p c . This enforces the invariant that each host principal c has control of the program it executes locally. Thus for any judgment Π ; Γ ; p c ; c ⊢ e : τ pc should never exceed the authority of c, the principal executing the expression. Rules Fail and Expect type fail and expect terms according to their type annotation τ. Rule Lam types lambda abstractions. Since functions are first-class values, we have to ensure that the pc annotation on the lambda term preserves the invariant Π ⊩ c ≽ p c . The clearance of a type τ, written C ( τ ) , is an upper bound on the pc annotations of the function types in τ. By checking that Π ⊩ c ≽ C ( τ 1 → p c ′ τ 2 ) holds (along with similar checks in Run and Ret), we ensure the contents of the lambda term is protected when sending or receiving lambda expressions, and that hosts never receive a function they cannot securely execute. Due to space constraints, the definition of C ( · ) is presented in Appendix A, in Fig. 35. The App rule requires the pc label at any function application to flow to the function’s pc label annotation. Hence the premise Π ⊩ p c ⊑ p c ′ .

Protected terms η ℓ e are typed by rule UnitM as ℓ says τ where τ is the type of e. Additionally, it requires that Π ⊩ p c ⊑ ℓ . This ensures that any unsealed values in the context are adequately protected by policy ℓ if they are used by e. The Sealed rule types protected values ( η ‾ ℓ v ) . These values are well-typed at any host, and does not require Π ⊩ p c ⊑ ℓ since no unsealed values in the context could be captured by the (closed) value v.

Computation on protected values occurs in bind terms bind x = e ′ in e . The policy protecting e must be at least as restrictive as the policy on e ′ so that the occurrences of x in e are adequately protected. Thus, rule BindM requires Π ⊩ ℓ ⊔ p c ⊑ τ , and furthermore e is typed at a more restrictive program counter label ℓ ⊔ pc to reflect the dependency of e on the value bound to x.

Rule Run requires that the pc at the local host flow to the pc ′ of the remote host, and that e be well-typed at c ′ , which implies that c ′ acts for pc ′ . Additionally, c must act for the clearance of the remote return type τ ′ to ensure c is authorized to receive the return value. The type of the run expression is p c ′ i a says τ ′ , which reflects the fact that c ′ controls the availability of the return value and also has some influence on which value of type τ ′ is returned. Although c ′ may not be able to create a value of type τ ′ unless p c ′ i a flows to τ ′ , if c ′ has access to more than one value of type τ ′ , it could choose which one to return. Rule Ret requires that expression e is welltyped at c and that c ′ is authorized to receive the return value based on the clearance of τ.

The Compare rule gives type ( ℓ 1 ⊕ ℓ 2 ) says τ to the expression compare e 1 and e 2 where e 1 and e 2 have types ℓ 1 says τ and ℓ 2 says τ respectively. Additionally, it requires that c, the host executing the compare , is authorized to fully examine the results of evaluating e 1 and e 2 so that they may be checked for equality.6

Finally, the Select rule gives type ( ℓ 1 ⊖ ℓ 2 ) says τ to the expression select e 1 or e 2 where e 1 and e 2 have types ℓ 1 says τ and ℓ 2 says τ respectively.

The typing judgment for the global configuration is presented in Fig. 13 and consists of three rules. Rule Head shows that the global configuration ⟨ e , c ⟩ & t , is well-typed if the expression e is well-typed at host c with program counter p c ′ where Π ⊩ p c ⊑ p c ′ and the tail t is well-typed. [ τ ′ ] τ means that the tail of the stack is of type τ while the expression in the head of the configuration is of type τ ′ . We introduced rules Tail(when t ≠ empty ) and Emp(when t = empty ) to typecheck the tail t.

⟨ E [ expect τ ′ ] , c ⟩ : : t is well-typed with type [ τ ′ ] τ , if expression E [ expect τ ′ ] is well-typed with type τ ˆ at host c. And, the rest of the stack t needs to be well-typed with type [ τ ˆ ] τ . Rule Emp says the tail is empty and the type of the expression in the head of the configuration is τ, in which case the type of the whole stack is [ τ ] τ .

OPEN IN VIEWER

Fig. 13.

Typing rules for configuration stack.

Availability attackers are different from traditional integrity and confidentiality attackers. While an integrity attacker’s goal is to manipulate data and a confidentiality attacker’s goal is to learn secrets, an availability attacker’s goal is to cause failures. In our model, an availability attacker can substitute a value only with a fail term. Integrity attackers may also cause failures in consensus based protocols when consensus is not reached because of data manipulation. In FLAQR this scenario is relevant during executing a compare statement: if one of the values in the compare statement is substituted with a wrong (mismatching) value then a fail term is returned. Thus we need to consider an availability attacker’s integrity authority when reasoning about its power to fail a program. Specifically, the authority of principal ℓ as an availability attacker is ℓ i a .

We consider a static but active attacker model similar to those used in Byzantine consensus protocols. By static we mean which principal or collection of principals can act maliciously is fixed prior to program execution. By active we mean that the attackers may manipulate inputs (including higher-order functions) during run time. We formally define the power of an availability attacker with respect to quorum systems.

Availability attackers in FLAQR are somewhat different than integrity and confidentiality attackers because we want to represent multiple possible attackers but limit which attackers are active for a particular execution. This goal supports the bounded fault assumptions found in consensus protocols where system configurations assume an upper bound on the number of faults possible.

A quorum system Q is represented as set of sets of hosts (or principals) e.g. Q = { q 1 , q 2 , … , q n } . Here each q i represents a set of principals whose consensus is adequate for the system to make progress. We define availability attackers in terms of the toleration set ⟦ Q ⟧ of a quorum system Q . The toleration set is a set of principals where each principal represents an upper bound on the authority of an attacker the quorum can tolerate without failing.

Example.

If Q = { q 1 : = { a , b } ; q 2 : = { b , c } ; q 3 : = { a , c } } and ℓ Q = ( a ⊕ b ) ⊖ ( b ⊕ c ) ⊖ ( a ⊕ c ) then ℓ Q says ( a says τ ) is not a valid quorum type because Π ⊮ Q g u a r d s ( ℓ Q says ( a says τ ) ) as Π ⊩ a i a ⋗ ℓ Q says ( a says τ ) and a i a ∈ A ⟦ Q ⟧ . But it is a valid quorum type for heterogeneous quorum system Q ′ = { q 1 : = { a , b } ; q 2 : = { a , c } } as a i a ∉ A ⟦ Q ′ ⟧ .

7. Security properties

To evaluate the formal properties of FLAQR, we prove that FLAQR preserves noninterference for confidentiality, integrity, and availability (Section 7.2). These theorems state that attackers cannot learn secret inputs, influence trusted outputs, or control the failure behavior of well-typed FLAQR programs. In addition, we also prove additional theorems that formalize the soundness of our type system with respect to a program’s failure behavior.

7.1. Soundness of failure

FLAQR’s semantics uses the compare and select security abstractions and the failure propagation rules to model failure and failure-tolerance in distributed programs, and FLAQR’s type system lets us reason statically about this failure behavior. To verify that such reasoning is sound, we prove two related theorems regarding the type of a program and the causes of potential failures.

In pursuit of this goal, this section introduces our blame semantics which reasons about failure-causing (faulty) principals during program execution. The goal is to record the set of principals which may cause run-time failures as a constraint on the set of faulty hosts F . Figure 15 presents the syntax of blame constraints, which are boolean formulas representing a lower bound on the contents of F . Atomic constraints ℓ ∈ F denote that label ℓ is in faulty set F . This initial blame constraint ( C init ) is represented using the toleration set of the implied quorum system.

OPEN IN VIEWER

Fig. 15.

Blame constraint syntax.

OPEN IN VIEWER

Fig. 16.

Blame membership: to apply C-In, C-Or and C-And the label p needs to be a primitive principal in N ∪ { ⊥ , ⊤ } . The blame semantics rules ensure all statements added to the blame set only refer to primitive principals. This rule set differs from the originally published one [19], which didn’t correctly handle compound principals such as p ∧ q .

Definition 4 (Initial blame constraint).

For toleration set ⟦ Q ⟧ of the form { ( p 1 1 ∧ ... ∧ p m 1 1 ) i a , …, ( p 1 k ∧ ... ∧ p m k k ) i a } the initial blame constraint C init is defined as a (logical) disjunction of conjunctions: C init ≜ ( p 1 1 ∈ F AND ... AND p m 1 1 ∈ F ) OR ... OR ( p 1 k ∈ F AND ... AND p m k k ∈ F )

Each disjunction represents a minimal subset of a possible satisfying assignment for the faulty set F . For brevity, we will refer to these subsets as the possible faulty sets implied by a particular blame constraint. Observe that for quorum system Q , there is a one-to-one correspondence between every t i ∈ ⟦ Q ⟧ and every possible faulty set F 1 , … , F k in C init where F i is the set implied by the ith disjunction in C init such that t i = b i i a , where b i = ⋀ p ∈ F i p .

Evaluation rule C-CompareFail, in Fig. 17, shows how function L (discussed below) updates the blame constraint from C to C ′ . We omit the blame-enabled versions of other evaluation rules since they simply propagate the blame constraint without modification.

OPEN IN VIEWER

Fig. 17.

E-CompareFail with blame semantics.

Example.

Quorum system Q 1 = { q 1 = { a , b } ; q 2 = { b , c } ; q 3 = { a , c } } has toleration set ⟦ Q 1 ⟧ = { a i a , b i a , c i a } and three possible faulty sets in C init : F = { a } or F = { b } or F = { c }

Quorum system Q 2 = { q 1 : = { p , q } ; q 2 : = { r } } has toleration set ⟦ Q 2 ⟧ = { p i a ∧ q i a , r i a } and two possible faulty sets in C init : F = { p , q } or F = { r } .

While C init is defined statically according to the type of the program, rule C-CompareFail updates these constraints according to actual failures that occur during the program’s execution. This approach identifies “unexpected” failures not implied by C init .

For example, Q 2 = { q 1 : = { p , q } ; q 2 : = { r } } has two possible faulty sets F = { p , q } or F = { r } . The initial blame constraint is C init : : = ( p ∈ F AND q ∈ F ) OR ( r ∈ F )

Placing blame for a specific failure in a distributed system is challenging, (and often impossible!). For example, when a comparison of values signed by ℓ 1 and ℓ 2 fails, it is unclear who to blame since either principal (or a principal acting on their behalf) could have influenced the values that led to the failure. We do know, however, that at least one of them is faulty; recording this information helps constrain the contents of possible faulty sets.

We can reason about principals that must be in F by considering all possible faulty sets implied by the blame constraints. We write C ⊨ ℓ ∈ F (read as C entails ℓ ∈ F ), when every possible faulty set in C , has the ℓ ∈ F clause. Figure 16 presents inference rules for the ⊨ relation.

The rules C-In, C-Or and C-And are defined for a primitive principal p π in N ∪ { ⊥ , ⊤ } , where π ∈ { i , a } . Whereas rules C-Conj, C-Disj, C-ParAnd and C-ParOr are defined for compound principals such as p ∧ q and p ⊟ q . The blame semantics rules (particularly, the L and NORM functions) ensure all statementss added to the blame set only refer to primitive principals. This rule set differs from the rule set presented in the originally published one [19], which didn’t correctly handle compound principals such as p ∧ q . For example, if C ⊨ p and C ⊨ q , then with the old ruleset from [19], we can not prove C ⊨ p ∧ q , because the blame semantics did not add the compound principal p ∧ q to F . Instead the blame semantics add p ∈ F and q ∈ F to the blame set as two different statements. But with our corrected ruleset we can prove C ⊨ p ∧ q , given C ⊨ p and C ⊨ q (using C-Conj and C-In).

Let us see another example. Since ℓ 1 is included in all satisfying choices of F below, we can say C ⊨ ℓ 1 ∈ F (using C-Conj,C-In, and possibly C-In). C = ( ℓ 1 ∈ F AND ℓ 2 ∈ F ) OR ( ℓ 1 ∈ F AND ℓ 3 ∈ F ) OR ( ℓ 1 ∈ F AND ℓ 4 ∈ F ) OR ( ℓ 1 ∈ F AND ℓ 5 ∈ F )

The L function (full definition in Fig. 45) is used by rule C-CompareFail to update C . For an expression: compare ( η ‾ ℓ 1 v 1 ) and ( η ‾ ℓ 2 v 2 ) with v 1 ≠ v 2 , L ( v 1 , v 2 , C , ℓ 1 , ℓ 2 ) updates the formulas in C to reflect that either ℓ 1 or ℓ 2 is faulty. If ℓ 1 or ℓ 2 already must be faulty, specifically if C ⊨ ℓ 1 ∈ F or C ⊨ ℓ 2 ∈ F , then the function does not update any formulas. This approach avoids blaming honest principals when the other principal is already known to be faulty.

If neither ℓ 1 nor ℓ 2 are known to be faulty. then function L is called recursively on inner layers (i.e., nested ( η ‾ ) expressions) of v 1 and v 2 until a subexpression protected by a known-faulty principal is found. If no such layer is present, then the principal protecting the innermost layer is added to C (or the outer principals if there are no inner layers). Only this principal has seen the unprotected value and thus could have knowingly protected the wrong value. Observe that for well-typed compare expressions, only the outer layer of compare d terms may differ in protection level, so there is less ambiguity when blaming an inner principal.

Updated constraints are kept in disjunctive normal form. Specifically, for compared terms ( η ‾ ℓ 1 v 1 ) and ( η ‾ ℓ 2 v 2 ) , with v 1 ≠ v 2 , with initial constraint: C init : : = ( p ∈ F AND q ∈ F ) OR ( r ∈ F ) , then L ( v 1 , v 2 , C init , ℓ 1 , ℓ 2 ) returns C ′ = ( p ∈ F AND q ∈ F AND ℓ 1 ∈ F ) OR ( p ∈ F AND q ∈ F AND ℓ 2 ∈ F ) OR ( r ∈ F AND ℓ 1 ∈ F ) OR ( r ∈ F AND ℓ 2 ∈ F )

We can now state the soundness theorem for our blame semantics, and apply it to prove a liveness result. Theorem 1 states that for any well-typed FLAQR program with a failing execution, and the faulty sets F i implied by C ′ (the final constraint computed by the blame semantics), it must be the case that the program’s type τ reflects the ability of the (possibly colluding) principals in F i to fail the program.

Theorem 1 (Sound blame).

Given,

Π ; Γ ; pc ; c ⊢ ⟨ ⟨ e , c ⟩ & empty ⟩ C init : τ

⟨ ⟨ e , c ⟩ & empty ⟩ C init ⟶ ∗ ⟨ ⟨ fail τ , c ⟩ & empty ⟩ C ′

where e is a source-level expression, 7

⁷

In other words, e does not contain any fail terms.

then for each possible faulty set F i implied by C ′ , there is a principal b i = ⋀ p ∈ F i p such that Π ⊩ b i i a ⋗ τ .

Proof.

Either e takes single step or multiple steps to produce the fail τ term as the end result. For both the cases we prove it by induction over structure of e. See Appendix B for full proof. □

While Theorem 1 characterizes the relationship between a program’s type and the possible faulty sets for a failing execution, it does not explicitly tell us anything about the fault-tolerance of a particular program. Since the type of a FLAQR program specifies its availability policy (in addition to its confidentiality and integrity), different FLAQR types will be tolerant of different failures. Below, we prove a liveness result for a common case, majority quorum protocols.

Definition 5 (Majority quorum system).

An m / n majority quorum system is a quorum system that always requires at least m of its hosts to reach consensus, where m > n − m .

Theorem 2 (Majority Liveness).

If e is a source-level expression and:

Π ; Γ ; pc ; c ⊢ ⟨ ⟨ e , c ⟩ & empty ⟩ C init : τ

Π ⊩ Q g u a r d s τ

Q is a m / n majority quorum system

⟨ ⟨ e , c ⟩ & empty ⟩ C init ⟶ ∗ ⟨ ⟨ fail τ , c ⟩ & empty ⟩ C ′

then for every possible faulty set F ′ implied by C ′ , | F ′ | > ( n − m ) .

Proof.

From (2), we know τ is a valid quorum type for Q so ∀ ℓ ∈ A ⟦ Q ⟧ . Π ⊮ ℓ ⋗ τ . Since A ⟦ Q ⟧ is a superset of ⟦ Q ⟧ , we also have ∀ t ∈ ⟦ Q ⟧ . Π ⊮ t ⋗ τ . Furthermore, from Definition 4, for each possible faulty set F i implied by C init , we know there is a principal t i ∈ ⟦ Q ⟧ such that t i = b i i a , where b i = ⋀ p ∈ F i p . Therefore, for each such b i , we know Π ⊮ b i i a ⋗ τ .

Since Q is an m / n majority quorum system, every quorum is of size m and every faulty set in C init is of size ( n − m ) . For contradiction, assume there exists a faulty set F ′ satisfying C ′ that has size ( n − m ) . Then by the definition of L , all possible faulty sets implied by C ′ also have size ( n − m ) since L monotonically increases the size of all possible faulty sets or none of them. Furthermore, each possible faulty set implied by C init is a subset (or equal to) a possible faulty set implied by C ′ , so | F ′ | = ( n − m ) implies C init = C ′ .

From Theorem 1 we know for every possible faulty set F ′ i implied by C ′ , it must be the case that Π ⊩ b ′ i i a ⋗ τ , where ⋀ p ∈ F ′ i p . However, since C init = C ′ , we have a contradiction since (2) implies Π ⊮ b ′ i i a ⋗ τ . Thus there cannot exist a possible faulty set of size (at least) ( n − m ) implied by C ′ , and all possible faulty sets must have size greater than ( n − m ) . □

7.2. Noninterference

We prove noninterference by extending the FLAQR syntax with bracketed expressions in the style of Pottier and Simonet [22]. Figure 43 shows selected bracketed evaluation rules and Fig. 42a and 42b show the typing rules for bracketed terms. The soundness and completeness of the bracketed semantics are proved the Appendix A (Lemmata 16–21).

Noninterference often is expressed with a distinct attacker label. We use H to denote the attacker. This means the attacker can read data with label ℓ if Π ⊩ ℓ c ⊑ H c and can forge or influence it if Π ⊩ H i ⊑ ℓ i and can make it unavailable if Π ⊩ H a ⊑ ℓ a

An issue in typing brackets is how to deal with fail terms. Our confidentiality and integrity results are failure-insensitive in the sense that they only apply to terminating executions. This is similar to how termination-insensitive noninterference is typically characterized for potentially non-terminating programs.

Traditionally, bracketed typing rules require that bracketed terms have a restrictive type, ensuring that only values derived from secret (or untrusted) inputs are bracketed. In FLAQR, there are several scenarios where a bracketed value may not have a restrictive type. For example, when a run expression is evaluated within a bracket, it pushes an element onto the configuration stack, but only in one of the executions. Another example is when a bracketed value occurs in a compare expression, but the result is no longer influenceable by the attacker H. For these scenarios, several of the typing rules in Fig. 42a permit bracketed values to have less restrictive types. Because of these rules, subject reduction does not directly imply noninterference as it does in most bracketed approaches, but the additional proof obligations are relatively easy to discharge.

OPEN IN VIEWER

The table above summarizes how bracketed terms are typed depending on whether we are concerned with integrity or availability. For integrity, unequal bracketed values must have a restrictive type (i.e., one that protects H), but equal bracketed values may have a less restrictive type. For availability, only bracketed terms where one side contains a value and the other a failure must have a restrictive type.

7.2.1. Confidentiality and integrity noninterference

To prove confidentiality (integrity) noninterference we need to show that given two different secret (untrusted) inputs to an expression e the evaluated public (trusted) outputs are equivalent. Equivalence is defined in terms of an observation function O adapted from FLAC [2] in Appendix A, Fig. 44.

Theorem 3 ( c - i Noninterference).

If Π ; Γ , x : ℓ ′ says τ ′ ⊢ ⟨ e , c ⟩ & empty : ℓ says τ where

Π ; Γ ; pc ; c ⊢ v i : ℓ ′ says τ ′ , i ∈ { 1 , 2 }

⟨ e [ x ↦ ( v 1 | v 2 ) ] , c ⟩ & empty ⟶ ∗ ⟨ v , c ⟩ & empty

Π ⊩ H π ⊑ ℓ ′ and Π ⊮ H π ⊑ ℓ , π ∈ { c , i } .

then, O ( ⌊ v ⌋ 1 , Π , ℓ , π ) = O ( ⌊ v ⌋ 2 , Π , ℓ , π )

Proof.

From subject reduction we can prove that ⌊ v ⌋ 1 and ⌊ v ⌋ 2 have same type. By induction over the structure of projected values, ⌊ v ⌋ i , we can show O ( ⌊ v ⌋ 1 , Π , ℓ , π ) = O ( ⌊ v ⌋ 2 , Π , ℓ , π ) Please refer to the Appendix A for full proof. □

7.2.2. Availability noninterference

Similar to [30] our end-to-end availability guarantee is also expressed as noninterference property. Specifically, if one run of a well-typed FLAQR program running on a quorum system terminates successfully (does not fail), then all other runs of the program also terminate.

This approach treats “buggy” programs where every execution returns fail regardless of the choice of inputs as noninterfering. This behavior is desirable because here we are concerned with proving the absence of failures that attackers can control. For structured quorum systems with a liveness result such as Theorem 2 for m / n majority quorums, we can further constrain when failures may occur. For example, Theorem 2 proves failures can only occur when more than ( n − m ) principals are faulty. In contrast, Theorem 4 applies to arbitrary quorum systems provided they guard the program’s type, but cannot distinguish programs where all executions fail.

Theorem 4 (Availability Noninterference).

If Π ; Γ , x : ℓ says τ ′ ⊢ ⟨ e , c ⟩ & empty : ℓ Q says τ where

Π ; Γ ; pc ; c ⊢ f i : ℓ says τ ′ , i ∈ { 1 , 2 }

⟨ e [ x ↦ ( f 1 | f 2 ) ] , c ⟩ & empty ⟶ ∗ ⟨ f , c ⟩ & empty

Π ⊩ H ⋗ ℓ says τ ′ and H i a ∈ A ⟦ Q ⟧ and Π ⊩ Q g u a r d s ( ℓ Q says τ )

then ⌊ f ⌋ 1 ≠ fail ℓ Q says τ ⟺ ⌊ f ⌋ 2 ≠ fail ℓ Q says τ

Proof.

From subject reduction (see Lemma 25 in the Appendix) we know, Π ; Γ ; pc ; c ⊢ ⌊ f ⌋ i : ℓ Q says τ . Because Π ⊩ Q g u a r d s ( ℓ Q says τ ) and H i a ∈ A ⟦ Q ⟧ we can write Π ⊮ H i a ⋗ ℓ Q says τ from rule Q-Guard. This ensures if ⌊ f ⌋ 1 ≠ fail ℓ Q says τ , then ⌊ f ⌋ 2 ≠ fail ℓ Q says τ , and vice-versa. □

8. Examples revisited

We are now ready to implement the examples from Section 2 with FLAQR semantics. To make these implementations intuitive we assume that our language supports integer ( i n t ) types, a mathematical operator > (greater than), and ternary operator : ? . Beacuse int is a base type C ( int ) returns ⊥. The examples also read from the local state of the participating principals. Which is fine because there are standard ways to encode memory (reads/writes) into lambda-calculus.

8.1. Tolerating failure and corruption

In this FLAQR implementation (Fig. 18) of 2 / 3 majority quorum example of Section 2.1, we refer principals representing alice , bob and carol as a, b and c respectively. The program is executed at host c ′ with program counter p c . Which means condition Π ⊩ c ′ ≽ p c holds. The program body consists of a function of type τ f = ( τ a → p c τ b → p c τ c → p c ( ( ( a i a ⊕ b i a ) ⊖ ( b i a ⊕ c i a ) ⊖ ( a i a ⊕ c i a ) ) says τ ) ) and the three arguments to the function are run statements. Here τ is ( a ∧ b ∧ c ) c says int . Which means C ( τ f ) = p c . The function body can be evaluated at c ′ , as condition Π ⊩ c ′ ≽ p c is true.

OPEN IN VIEWER

Fig. 18.

FLAQR implementation of majority quorum example.

Here e a , e b and e c are the expressions that read the balances for account a c c t from the local states of a, b and c respectively. The program counter at a, b, and c are a, b and c respectively. The data returned from a has type τ a , which is basically a i a says τ . Similarly τ b is b i a says τ and τ c is c i a says τ . Because each run returns a balance, the base type of τ is an i n t type, and it is protected with confidentiality label ( a ∧ b ∧ c ) c , meaning anyone who can read all the three labels (a, b and c), can read the returned balances.

In order to typecheck the run statements the conditions Π ⊩ p c ⊑ a , Π ⊩ p c ⊑ b , and Π ⊩ p c ⊑ c need to hold. The condition Π ⊩ c ′ ≽ C ( τ a ) is trivially true as C ( τ a ) = ⊥ . Similarly C ( τ b ) = ⊥ and C ( τ c ) = ⊥ as well.

The host executing the code need to be able to read the return values from the three hosts. This means conditions Π ⊩ c ′ ⊳ a i a says τ Π ⊩ c ′ ⊳ b i a says τ and Π ⊩ c ′ ⊳ c i a says τ need to hold in order to typecheck the compare statements. The type of the whole program is ( ( ( a i a ⊕ b i a ) ⊖ ( b i a ⊕ c i a ) ⊖ ( a i a ⊕ c i a ) ) says τ ) , which is a valid quorum type for Q = { q 1 : = { a , b } ; q 2 : = { b , c } ; q 3 : = { a , c } } .

Based on the security properties defined in Section 7 this program offers the confidentiality, integrity and availability guaranteed by quorum system Q . Therefore, the result cannot be learned or influenced by unauthorized principals, and will be available as long as two hosts out of a, b, and c are non-faulty.

The toleration set here is ⟦ Q ⟧ = { a i a , b i a , c i a } . So, the program is not safe against an attacker with label l a = a i a ∧ b i a (or, a i ∧ b a ), for example. This is because ∄ t ∈ ⟦ Q ⟧ . Π ⊩ t ≽ l a . Since Π ⊩ l a ≽ a i a , principal l a can fail two compare statements on lines 3 and 8. And, because Π ⊩ l a ≽ b i a , l a can also fail another two compare statements (one overlapping compare statment) on lines 3 and 6. Thus the whole program evaluates to fail . This FLAQR code also helps prevent incorrect comparisons. For instance, replacing z with y on line 8 will not typecheck.

OPEN IN VIEWER

Fig. 19.

FLAQR implementation of available largest balance example.

8.2. Using best available services

The code in Fig. 19 is the FLAQR implementation of Fig. 3. The program runs at a host c with program counter p c . The expressions e and e ′ read account balances from principals b and b ′ , representing the banks. The values returned from b and b ′ have types τ b = ( b i a says ( b c ∧ b ′ c ) says int ) and τ b ′ = ( b ′ i a says ( b c ∧ b ′ c ) says int ) respectively.

The type of the whole program is ( ( d ⊖ b i a ⊖ b ′ i a ) says ( b c ∧ b ′ c ) says i n t ) . Here d = p c ⊔ b ⊔ b ′ . In order to typecheck the run statements, the conditions Π ⊩ p c ⊑ b and Π ⊩ p c ⊑ b ′ need to hold. The program counter at b is b and b ′ is b ′ . The bind statements (lines 3–4) typecheck because conditions Π ⊩ p c ⊔ b i a ⊑ d , Π ⊩ p c ⊔ b i a ⊔ b ′ i a ⊑ d , Π ⊩ p c ⊔ b i a ⊔ b ′ i a ⊔ b c ⊑ d , and Π ⊩ p c ⊔ b i a ⊔ b ′ i a ⊔ b c ⊔ b ′ c ⊑ d hold, because of our choice of d.

9. Secret sharing with FLAQR

Secret sharing is a cryptographic mechanism used in several distributed systems protocols such as oblivious transfer, multiparty communication, and Byzantine agreement. In this section we extend FLAQR with two new language constructs to support secret sharing. We call this extended version of our programming model FLAQR + . Secret sharing is a process of splitting a secret into n shares and distributing the shares among n hosts (or principals in our setting). When an adequate number of hosts, say t, combine their respective shares, the secret is reconstructed [10,24]. Sometimes this process is referred as (t,n)-threshold secret sharing scheme [24,26], i.e. a quorum of t hosts (where 1 < t ⩽ n ) out of those n hosts need to combine their shares to retrieve the initial secret value. With ( t − 1 ) or fewer shares, adversaries learn nothing about the secret.

Secret sharing is most commonly described in terms of a mathematical polynomial, say p ( x ) , of degree ( t − 1 ) , p ( 0 ) being the secret value [24]. The polynomial’s values at n different co-ordinates are distributed as the secret shares, and by knowing t of these values one can reconstruct8

⁸

Typically using Lagrange interpolation [10].

the polynomial and find the secret value p ( 0 ) .

For simplicity, we extend FLAQR to support (2,2)-threshold secret sharing, but later sketch how support for (t,n)-threshold secret sharing where 2 < n and t < n would be straightforward. We model secret shares abstractly using a value sealed by new kinds of principals k . L and k . R . We call k a key principal because, unlike the principals in P , a new, unique key principal k is created each time secret shares are created. In contrast, the principals in P are statically known. The principals k . L and k . R represent the two associated shares of the key principal k. We will be refering to (2,2)-threshold secret sharing simply as (2,2) secret sharing in the following sections.

9.1. Motivating example of secret sharing : Password splitting

Figure 20 presents a simple (2,2) secret sharing example and the corresponding pseudocode is shown in Fig. 21. A (secret) password s belongs to bob who wants keep a backup of it. Bob creates two secret-shares of s as s _ 1 and s _ 2 and sends them to alice and carol respectively. That is, anyone who wants to get access to s has to either get it directly from bob , or needs to get both s _ 1 and s _ 2 from alice and carol and reproduce it. Later, dave fetches the secret shares from alice and carol and combines them to produce the password s .

An advantage of secret sharing is that it permits the secure transmission of secrets without requiring key distribution or public-key infrastructure (PKI). Instead, any party who possesses t shares may recover the secret. This can also be a liability, however, since an adversary needs to only obtain the shares to access the secret, too. Thus, considering the flow of shares between principals is central to the security of a secret sharing scheme. In the example in Fig. 21, alice and carol are unable to access the secret because they only possess a single share, but a coding error could transmit both shares to alice or carol , obviating the cryptographic protection. For this reason, embedding secret sharing in a language like FLAQR makes sense because the type system ensures the code only permits authorized flows.

OPEN IN VIEWER

Fig. 20.

Overview of ( 2 , 2 ) secret sharing: bob shares his secret shares with alice and carol . Later, alice and carol forward their respective shares to dave . Finally, dave reproduces the initial secret s with the shares he received from alice and carol .

OPEN IN VIEWER

Fig. 21.

Creating two secret shares from a secret and then reconstructing the secret from the two secret shares using functions of a ( 2 , 2 ) secret sharing protocol.

9.2. ( 2 , 2 ) secret sharing in FLAQR +

Our abstractions for secret sharing in FLAQR + make use of the η ‾ ℓ term to represent sealed secret shares. However, aspects of secret sharing schemes differ from the use of η ‾ ℓ in prior FLAC-based languages [2,8,14]. Here, in addition to the sealed values generated by the η ℓ term, sealed values may also be created when splitting a secret into shares. In the previous approaches, a value sealed by η ℓ serves as a reasonable model for signed and encrypted values. Specifically, the confidentiality component ℓ c behaves like a public-key encrypted value: anyone can encrypt values at ℓ c , but only authorized parties (which possess the associated private key) can distinguish the values protected at ℓ c . Since η ℓ can only be applied in contexts where pc ≽ ℓ i (see UnitM), the integrity component behaves like a digitally signed value: only authorized principals can cause a value to be signed with ℓ i integrity, but anyone can use high-integrity values.9

⁹

There doesn’t appear to be a natural cryptographic analog for the availability component.

Obviously then, enforcing these policies cryptographically would require public-key infrastructure.

Secret sharing behaves differently from the above interpretations: rather than authorization being based on possession of a long-lived private key (a reasonable proxy for identity), secret sharing implicitly authorizes any party possessing t shares. Therefore using identity-based principals such as alice or bob is inappropriate since, even if a shared secret is intended for alice , anyone with t shares will be able to distinguish the secret. Even alice must have t shares to access the secret. An abstraction for secret sharing should capture this behavior, but doing so in FLAQR + requires new concepts.

We extend the set of principals P  with new primitive principals L and R representing the left and right shares of our ( 2 , 2 ) secret sharing scheme. The set of all principals P for FLAQR + is thus the closure of the set N ∪ { ⊤ , ⊥ , L , R } over the same operations as FLAQR. In the following we are only interested in the confidentiality projections L c and R c , since secret sharing only concerns enforcing the confidentiality of the secret.

Another aspect of secret sharing that departs from prior uses of FLAC principals is that each time shares are created, they are protected by a different secret. Consequently, shares created from different invocations cannot be mixed, even when the underlying value is the same. For this reason, we define key principals, a new type of principal generated dynamically at runtime. For our purposes, each k ∈ K , where K is the set of all key principals, is equipped with a left and right principal, k . L c and k . R c . Importantly, since key principals are generated dynamically, they are not directly representable statically. The principals L c and R c are the static representation for the left and right principals of any key principal, but the shares of different key principals cannot be distinguished at the type level.

9.3. Semantics and types for secret sharing OPEN IN VIEWER

Fig. 22.

FLAQR⁺ semantics for secret sharing (splitting secrets and combining shares).

OPEN IN VIEWER

Fig. 23.

FLAQR⁺ typing rules for secret sharing.

Figure 22 presents the semantic rules added to FLAQR + . Expression split ℓ v produces two secret shares, sealed with principals k . L c ∧ ℓ and k . R c ∧ ℓ from the secret value v (rule E-Split) using a fresh key principal k. The ℓ annotation specifies an additional policy to seal the secret with an addition to the key principal. Primarily ℓ is used for integrity and availability components since k . L c and k . R c are confidentiality projections.

Two shares are combined with expression combine x = ⟨ ( η ‾ k . L c ∧ ℓ v ) , ( η ‾ k . R c ∧ ℓ v ) ⟩ @ p c in e Rule E-Combine evaluates these terms to e [ x ↦ v ] revealing the secret v and substituting it for x in the body e. Notice that the key principal is the same on both sides of the pair. As discussed below in Section 9.4, mismatched key principals result in failure. The additional pc annotation on combine terms is used by the extended blame semantics, discussed in Section 9.4.

For simplicity, our extension only supports (2,2)-threshold secret sharing, but we believe extending this framework to support (t,n)-threshold secret sharing for 2 < n and t < n would be straightforward. For example, given some t and n, we could redefine E-Split to generate a tuple containing n shares sealed by principals k . S 1 c , k . S 2 c , … , k . S n c . E-Combine would be replaced by n t rules: one for each valid t-sized subset of shares.

Figure 23 presents the FLAQR +  typing rules for split and combine . The last premise in the Split rule involves the view of the pc ’s integrity, △ ( pc i ) . The view of a principal was introduced by Ceccetti et al. [8] to specify an upper bound on the confidentiality that may be robustly declassified [27] based on the integrity of the context performing the declassification and the data itself. These restrictions ensure an attacker cannot influence what (or whether) information is declassified. Below, we extend the definition of view with the principals’ availability projection counterpart as well.

Definition 6 (view of a principal).

Let ℓ = p c ∧ q i ∧ r a be a FLAM [3] label (principal) expressed in normal form. The view of ℓ, written as △ ( ℓ ) , is defined as △ ( p c ∧ q i ∧ r a ) ≜ q c .

The premise Π ⊩ p c ⊑ ℓ ⊔ △ ( p c i ) in Split serves two purposes. First, it ensures the confidentiality of control flow and the unsealed values in the context, represented by pc , are no more restrictive than the upper bound on declassification △ ( pc i ) (or the confidentiality of ℓ if no declassification takes place). Second, it ensures the label ℓ protects the availability and integrity of the context; only confidentiality may be downgraded by split terms.

When shares are combined to reveal the secret, the rule Combine ensures the combined pair contains a left and right share (although not which key principal they are associated with), and that the body of the combine term protects the result with a principal at least as restrictive as the upper bound of ℓ and the context pc the combine occurs in.

In some sense, split ℓ and combine function as an alternative to η ℓ and bind . The difference is that split seals values using a key principal in addition to a label ℓ, and permits secrets more restrictive than ℓ to be sealed. Combine is similar to a bind that declassifies its bound value, dropping the key principals k . L and k . R from the protection requirements on the body of the combine . Note that it is not possible for a type-safe program to bind a secret share. Since a premise of bind would require the body accessing the unsealed share on host c to typecheck at pc ⊔ ( L c ∧ ℓ ) , this would violate the invariant that c must act for the pc of the programs it executes.10

¹⁰

Recall this invariant is enforced by the Π ⊩ c ≽ p c premise included in all typing rules.

We need one more typing rule, SealedK, to preserve the types of the values sealed with labels k . L c and k . R c , for any freshly generated key k ∈ K . The existing Sealed rule is not enough as it does not handle the values protected with these new key principals. A consequence of this rule is that well-typed FLAQR +  programs can produce mismatching shares with two different keys (say k 1 and k 2 ) during run-time. We handle mismatching shares with our extended blame semantics, discussed in Section 9.4.

9.4. Extending the blame semantics

As with other FLAQR terms, fail values propagate through split and combine . Figure 24 presents fail propagation rules for split and combine statements. These rules are straightforward propagation rules except for E-CombineFail (see Figure 25), which evaluates to fail if the key principals sealing the shares are mismatched.

OPEN IN VIEWER

Fig. 24.

fail propagation rules in FLAQR + .

OPEN IN VIEWER

Fig. 25.

E-CombineFail with blame semantics.

The introduction of E-CombineFail rule creates an additional source of failure besides compare terms with mismatched values. Rule C-CombineFail extends FLAQR’s blame semantics to account for this. Unlike the case for compare , we cannot blame the failure on the principal that sealed the mismatched values given to combine . The failure in this case is due to pairing together shares generated by different split evaluations. Rather than blaming the creators of the sealed value, we instead want to blame the principals that influenced this pairing. This influence is represented by the label of the pc . Hence, when k 1 and k 2 do not match, C-CombineFail adds pc to the blame set. The function L used in C-CompareFail is unnecessary here because it is unnecessary to examine any subterms of the combined pair – only the outer key principals contribute to a combine failure.

The NORM function11

¹¹

This normalization function was not present in the original FLAQR publication [19], which is an error. Normalization of the statements added to the blame set is required to ensure compound principals are correctly handled.

in the premise of C-CombineFail is used to add the new (potentially malicious) principal p c in the exisiting blame set C in normalized form. For example, if p c = ( a ∧ b ) ∨ c and if C : = ( ℓ 1 ∈ F ) OR ( ℓ 2 ∈ F ) , then calling NORM ( p c , C ) will return a blame set C ′ : = ( a ∈ F AND b ∈ F AND ℓ 1 ∈ F ) OR ( a ∈ F AND b ∈ F AND ℓ 2 ∈ F ) OR ( c ∈ F AND ℓ 1 ∈ F ) OR ( c ∈ F AND ℓ 1 ∈ F ) In case of C-CompareFail (Fig. 17), the NORM function was called from within the L function (see Fig. 45). Figure 46 contains the complete definition of the NORM function.

9.5. Security properties

By design, split and combine are interfering with respect to confidentiality: they can cause secret values to be declassified. However, we would like to ensure that integrity and availability noninterference are unaffected.

In order to prove integrity and availability noninterference for FLAQR +  programs we extend the bracketed semantics (Fig. 26) and observation function (Fig. 27) with rules for split and combine , and add the corresponding cases for split and combine terms to the proofs for the lemmas and theorems of FLAQR + . The noninterference theorem statements for FLAQR + are identical to Theorems 3 and 4, though Theorem 3 only holds for π = i in FLAQR + . Since the new static principals L and R are only used in confidentiality projections, rules such as Q-Guard and the fails are unaffected by the new terms for secret sharing, the proofs of these theorems is largely unchanged from those for FLAQR. However, ensuring the new terms did not break an essential lemma such as subject reduction (Lemma 24) required careful design of the new rules for evaluation, failure propagation, bracketed semantics, and typing.

Although we protect the robustness (in theory) of what values may be declassified via split and combine , secret sharing is inherently non-robust since the party possessing the shares decides whether to reveal the secret. To formalize the protections that split and combine do offer, a weaker form of robust declassification would be required that permits secure uses of split and prohibits insecure ones (such as those violating the premise Π ⊩ p c ⊑ ℓ ⊔ △ ( p c i ) ). Such a definition is not immediately clear12

¹²

One reason such a definition is challenging in FLAC-based languages is that the pc label not only protects control flow, but also any values that have been unsealed using bind (which raises the pc label for its body).

to us, and we leave further investigation to future work. Since split and combine permit non-robust declassification, they could potentially permit malleability attacks [8]. Since secret shares cannot be unsealed via bind , the possibility for such attacks is limited, but we leave formalization of the strength of these limitations to future work.

For compare statements, failures are generated because of two mismatching values. In contrast, the contents of the secret shares are irrelevant in combine statements. Instead, combine failures happen due to mismatching keys of the secret shares. Hence, we should only blame the control flow of the program for putting the two mismatching secret shares together. Since the program counter tracks the control flow of the program, we blame the program counter annotation pc in the C-CombineFail rule by adding it to the blame set when a fail term is returned while combining two shares. Our Theorem 1 (Sound blame) still holds, even though combine statement adds a new source of failure. The new cases hold because the premise Π ⊩ pc ⊑ ℓ ′ says τ in Combine allows us to show Π ⊩ p c ⋗ ℓ ′ says τ (using P-Lbl and A-Avail). Since, Theorem 1 holds, Theorem 2 (Majority liveness) holds as well, as it depends on Theorem 1.

OPEN IN VIEWER

Fig. 26.

Bracketed semantics for FLAQR +  terms.

OPEN IN VIEWER

Fig. 27.

Observation function for intermediate FLAQR +  terms (extended from FLAC [2]).

9.6. Password splitting example with FLAQR +

Figure 28 presents the FLAQR + implementation of the example discussed in Section 9.1. The program executes at host c ′ with program counter p c , such that Π ⊩ c ′ ≽ p c . The host a has program counter a, host b has program counter b and host c has program counter c. The program consists of a function body (lines 1–5) and an argument to it (line 6). The function body is of type τ b → p c ℓ ′ says int , where τ b = b i a says ( L c ∧ b says int × R c ∧ b says int ) , and takes the value of running a split statement at host b (i.e. run τ b ( split b v ) @ b ), which splits b’s secret v. The argument type is τ b . This means the pair of the secret shares created at and returned by b is tainted with b’s integrity and availability. In order to typecheck the run statement p c needs to flow to b, i.e. the condition Π ⊩ p c ⊑ b needs to hold. The condition Π ⊩ c ≽ C ( ( L c ∧ b says int × R c ∧ b says int ) ) satisfies trivially, as C ( ( L c ∧ b says int × R c ∧ b says int ) ) = ⊥ . The function body can be executed at c ′ as C ( τ b → p c ℓ ′ says int ) = p c and we mentioned earlier that the condition Π ⊩ c ′ ≽ p c is true. The run statements on line 3 and 4 indicates that the left share is tainted by a’s and the right share is tainted by c’s integrity and availability. Which means a and c have seen and approved on the secret shares created by b. To make the run statements on lines 3 and 4 well-typed, the conditions Π ⊩ p c ⊑ a Π ⊩ p c ⊑ c should satisfy. We choose label ℓ such that Π ⊩ p c ⊔ a i a ⊔ b i a ⊔ c i a ⊑ ℓ . The bind statements (lines 2–4) typecheck because the conditions Π ⊩ p c ⊔ b i a ⊑ ℓ , Π ⊩ p c ⊔ b i a ⊔ a i a ⊑ ℓ and Π ⊩ p c ⊔ b i a ⊔ a i a ⊔ c i a ⊑ ℓ hold due to our choice of ℓ.

OPEN IN VIEWER

Fig. 28.

A simple example of secret sharing in FLAQR + .

10. Related work

FLAM [3,4] offers an algebra to integrate authorization logics and information flow control policies. FLAM also introduces a security condition, robust authorization, that is useful to ensure security when delegations and revocations change the meaning of confidentiality and integrity policies. In FLAQR we extend FLAM algebra with availability policies, and new binary operations to represent integrity and availability policies of the output of quorum based protocols. FLAC [2,5] embeds its types with FLAM information flow policies. FLAC supports dynamic delegation of authority, but this feature is omitted in FLAQR.

A limited number of previous approaches [29,30] combine availability with more common confidentiality and integrity policies in distributed systems. Zheng and Myers [29] extend the Decentralized Label Model [20] with availability policies, but focus primarily tracking dependencies rather than applying mechanisms such as consensus and replication to improve availability and integrity. Zheng and Myers later introduce the language Qimp [30] with a type system explicitly parameterized on a quorum system for offloading computation while enforcing availability policies. Instead of treating quorums specially, FLAQR quorums emerge naturally using compare and select and enable application-specific integrity and availability policies that are secure by construction.

Hunt and Sands [15] present a novel generalisation of information flow lattices that captures disjunctive flows similar to the influence of replicas in FLAQR on a select result. Our partial-or operation was inspired by their treatment of disjunctive dependencies.

Models of distributed system protocols are often verified with model checking approaches such as TLA+ [17]. Model checking programs is typically undecidable, making it ill-suited to integrate directly into a programming model in the same manner as a (decidable) type system. To make verification tractable, TLA+ models are often simplified versions of the implementations they represent, potentially leading to discrepancies. FLAQR is designed as a core calculus for a distributed programming model, making direct verification of implementations more feasible.

BFT protocols [6,7] use consensus and replication to protect the integrity and availability of operations on a system’s state. Each instance of a BFT protocol essentially enforces a single availability policy and a single integrity policy. While composing multiple instances is possible, doing so provides no end-to-end availability or integrity guarantees for the system as a whole. FLAQR programs, by constrast, routinely compose consensus and replication primitives to enforce multiple policies while also providing end-to-end system guarantees.

Our blame semantics presented in Section 7.1 has some resemblance to the idea of blame used to detect contract violations [11] and applied to gradual typing [25]. In our system, blame is necessarily ambiguous since perfect fault detection is not possible. Hence, rather than identifying a single program point responsible for a contract or type violation, our semantics builds constraints that specify a set of principals that may be responsible for a given failure.

In [9] Clarkson and Schneider talks about integrity measures such as contamination and suppression. The idea of suppression can be equivalent to the idea of unavailability. Although in [9] suppression happens due to untrusted input making trusted output unavailable. In FLAQR, unavailibity is caused by both unavailable and untrusted (via compare statement) inputs.

11. Conclusion

In this work, we extend Flow Limited Authorization Model [3] with availability policies. We introduce a core calculus and type-system, FLAQR, for building decentralized applications that are secure by construction. We identify a trade-off relation between integrity and availability, and introduce two binary operations partial-and and partial-or, specifically to express integrities of quorum based replicated programs. We define f a i l s relation and judgments that help us reason about a principal’s authority over availability of a type. We introduce blame semantics that associate failures with malicious hosts of a quorum system to ensure that quorums can not exceed a bounded number of failures without causing the whole system to fail. FLAQR ensures end-to-end information security with noninterference for confidentiality, integrity and availability. Finally we present FLAQR + , which is an extension of FLAQR with language constructs that support secret sharing between hosts with mutual distrust. We extend our failure propagation rules and blame semantics to assign blame to appropriate principals when a secret sharing round fails.