ORA-TM-98-030 1 A Test for Non-Disclosure in Security Level Translations David Rosenthal and Francis Fung Odyssey Research Associates 33 Thornwood Dr, Suite 500 Ithaca, NY 14850 Abstract Two security domains that want to exchange information securely may need to agree on translations of Mandatory Access Control (MAC) labels of their information, if their MAC labels have a different syntax or semantics. It is desirable that these translations do not introduce any confidentiality violations. In this paper we present a property, the Security Level Translation Property (SLTP), which must hold if the security level translation functions satisfy MAC confidentiality. This property is in some sense the best possible test of the level translations in the absence of a “common domain” that gives the real relationships among the levels of the two domains. 1 Introduction The need for constructing translations between MAC security levels arises when two security domains need to communicate, but the representation of the levels of those domains is not the same. Each domain may have its own syntax for assigning labels to objects and clearances to users; these labels and clearances do not necessarily have the same meaning in both domains. In order to securely send a message from one domain to the other, the two domains must agree on some method of translating the levels of one domain into those of the other domain, so that a user in the second domain can interpret the first domain’s level appropriately. The translations can either be done on object labels, which are then compared with untranslated clearances, or the translations can be done on clearances, which are then compared to labels. The methods and analysis, although not identical, are essentially the same, and we examine only the object label translation method. The Multilevel Information System Security Initiative (MISSI) [MISSI KPCMP] architecture, developed by the NSA, provides support for translations between security policies. MISSI is an architecture that enables efficient and secure communications across insecure channels, such as the Internet. The MISSI architecture is structured around the use of hierarchical domains, in which trust is propagated from a top-level root authority by the use of certificates. Part of this architecture supports communication between different domains. When two domains want to 1 This work was supported by the National Security Agency under the direction of the Air Force Research Laboratory at Rome for contract F30602-96-C-0348 1 Report Documentation Page Form Approved OMB No. 0704-0188 Public reporting burden for the collection of information is estimated to average 1 hour per response, including the time for reviewing instructions, searching existing data sources, gathering and maintaining the data needed, and completing and reviewing the collection of information. Send comments regarding this burden estimate or any other aspect of this collection of information, including suggestions for reducing this burden, to Washington Headquarters Services, Directorate for Information Operations and Reports, 1215 Jefferson Davis Highway, Suite 1204, Arlington VA 22202-4302. Respondents should be aware that notwithstanding any other provision of law, no person shall be subject to a penalty for failing to comply with a collection of information if it does not display a currently valid OMB control number. 1. REPORT DATE 3. DATES COVERED 2005 2. REPORT TYPE - 4. TITLE AND SUBTITLE 5a. CONTRACT NUMBER A Test for Non-Disclosure in Security Level Translations 5b. GRANT NUMBER 5c. PROGRAM ELEMENT NUMBER 6. AUTHOR(S) 5d. PROJECT NUMBER 5e. TASK NUMBER 5f. WORK UNIT NUMBER 7. PERFORMING ORGANIZATION NAME(S) AND ADDRESS(ES) 8. PERFORMING ORGANIZATION Defense Advanced Research Projects Agency,3701 N. Fairfax REPORT NUMBER Dr,Arlington,VA,22203 9. SPONSORING/MONITORING AGENCY NAME(S) AND ADDRESS(ES) 10. SPONSOR/MONITOR’S ACRONYM(S) 11. SPONSOR/MONITOR’S REPORT NUMBER(S) 12. DISTRIBUTION/AVAILABILITY STATEMENT Approved for public release; distribution unlimited 13. SUPPLEMENTARY NOTES 14. ABSTRACT Two security domains that want to exchange information securely may need to agree on translations of Mandatory Access Control (MAC) labels of their information, if their MAC labels have a different syntax or semantics. It is desirable that these translations do not introduce any confidentiality violations. In this paper we present a property, the Security Level Translation Property (SLTP), which must hold if the security level translation functions satisfy MAC confidentiality. This property is in some sense the best possible test of the level translations in the absence of a "common domain" that gives the real relationships among the levels of the two domains. 15. SUBJECT TERMS 16. SECURITY CLASSIFICATION OF: 17. LIMITATION OF 18. NUMBER 19a. NAME OF ABSTRACT OF PAGES RESPONSIBLE PERSON a. REPORT b. ABSTRACT c. THIS PAGE 16 unclassified unclassified unclassified Standard Form 298 (Rev. 8-98) Prescribed by ANSI Std Z39-18 interoperate, they use the mechanism of cross-certificates. A cross-certificate is a certificate issued by a Certificate Authority (CA) in a certain domain, whose subject lies in some other domain. Cross-certificates enable domains to convey trust in each other, without forcing them to commit their trust to a higher-level root. The MISSI level translations associated with cross- certified domains are not contained in the cross-certificate itself. Instead, the translations are contained in a file called the Security Policy Information File (SPIF), which is used to compare object labels to authorizations. The translations allow object labels from other domains to be compared with local authorizations, and local object labels to be compared with another domain’s authorizations. A translation of security labels should not result in a security leak. In particular, messages should only be sent to users that have the proper authorization to view that information. (The Bell- LaPadula Simple Security Property [BLP] should be satisfied.) In this paper, we describe a security check that can be applied to given pair of level translation functions. A complete non- disclosure analysis of translation functions requires a “common domain” that describes the “real” relationships between the levels. Such an analysis would require more information than is available in the representation of the functions and domain level orderings, i.e. in the SPIF. However, in the absence of full information about the common domain, we can still perform a partial analysis. We formulate the Security Level Translation Property (SLTP) for a pair of translations, which must be satisfied for the translations to be secure. SLTP is in some sense the best possible check for non-disclosure that can be done without knowledge of the real relationships among the labels. If SLTP is satisfied, then there exists a “comparison domain” into which both label orderings embed, such that non-disclosure is satisfied with respect to the comparison domain. There is, however, no guarantee that the constructed comparison domain will reflect the actual relationships among the levels of the two domains. The rest of this paper is structured as follows. In section 2, we consider the representation of object labels as a partially ordered set and translations as partial functions between these orderings, and we discuss the notion of a common domain. Then, in section 3, we formulate the Security Level Translation Property (SLTP) and show that a pair of functions satisfies SLTP if and only if there exists some partially ordered set with the formal properties of a common domain in which the translation functions do not downgrade data. We also consider a simplified form that SLTP takes on when the functions are total and “order-compatible.” In section 4, we formulate an equivalent form of SLTP for SDN.801 [MISSI SDN.801] military message labels. 2 Modeling the Security Level Translations For the analysis that we describe here, we assume that the orderings on each domain are available, but that no information about the real relationships among the levels of the two domains is known. We will introduce the term comparison domain to mean a partially ordered set of levels containing copies of the two domains. Our analysis will use comparison domains in establishing the appropriateness of the desired security properties. Suppose (A,<) and (B,<) are the partial orders of the security levels for the two domains. Let f represent the translation function from A to B and let f ' represent the translation function from B to A. Note that f and f ' might be only partial functions. We want to analyze the appropriateness of f and f '. A comparison domain is a partially ordered set (C,<) with (A,<) and (B,<) properly embedded into (C,<), i.e., we have maps p and p from A to C, and B to C respectively, that satisfy: A B 2 For x, y ˛ A, x < y (cid:219) p (x) < p (y) and for x, y ˛ B, x < y (cid:219) p (x) < p (y) and A A B B for x, y ˛ A, x = y (cid:219) p (x) = p (y) and for x, y ˛ B, x = y (cid:219) p (x) = p (y). A A B B f A B f ' p p A B C Figure 1: Relationship of translation functions Any proper embedding of A and B into some C expresses an ordering relationship between levels in A and B. It may or may not represent the relationships of the common domain, i.e., the real relationships between A and B. What security properties should the translation functions, f and f ', have with respect to a comparison domain for A and B? The translation functions should not allow a downgrade to occur. Hence we want if x is in the domain of f, p (x) = p (f(x)) and A B if y is in the domain of f ', p (y) = p (f '(y)). B A This formula merely states that the translation functions can only raise levels. So, given a comparison domain C, we call f and f ' level increasing (relative to C), if the above two conditions hold for the proper embeddings p and p of A and B into C. If f and f ' are level A B increasing with respect to the common domain of A and B, then translating a label cannot cause a security leak, since a translated label is at least as a restrictive in who can view the object as the untranslated one. 3 Analysis of the Translation Functions 3.1 Analysis of the security level translation functions 3.1.1 Need for a common domain As noted above, a complete analysis of the f and f ' translation functions requires using the common domain that captures the actual relationships between the levels of A and B. Analysis of just the translation functions in the SPIF (i.e., looking at just A, B, f, and f ') will not produce a total answer. 3 Consider the following example. Suppose A={S,TS} with the natural ordering and B={protect}. Let f(S)=protect, f(TS)=protect and f ' (protect)=TS. This completely specifies A, B, f and f ', but does not provide enough information to determine if the translation functions are in fact secure (i.e., whether f and f ' are level increasing in the common domain). If protect is equivalent to S (in the common domain) then TS information might be viewed by the equivalent of an S user. On the other hand, if protect is equivalent to TS then the level of the information may increase when translated, but there is no non-disclosure problem. Without a means to check the real relationship between the security levels (that is, using the common domain), we cannot guarantee that there is no non-disclosure violation. 3.1.2 Security Level Translation Property Even though analysis without the common domain is only partial, it provides a way to identify non-disclosure violations with the information that is available. We define the Security Level Translation Property (SLTP) as the following pair of conditions: Condition 1: If x is in domain of f, y is in the domain of f ', and f(x) = y , then x = f ' (y). Condition 2: If y is in domain of f ', x is in the domain of f, and f ' (y) = x, then y = f(x). The two conditions represent the same property applied to the two different directions of the translation functions. f ' (y) y KEY: mapping: less than: x f(x) Figure 2: SLTP rule, condition 1 f(x) x y f’(y) Figure 3: SLTP rule, condition 2 4 3.1.3 Main theorem for SLTP Theorem: For any two partially ordered sets (A,<), (B,<) , and functions f, f ' between them: SLTP holds if and only if there exists a partially ordered set (C,<), with A and B properly embedded into C (i.e., a comparison domain C) and f, f ' satisfying the level increasing property with respect to C. This theorem shows that SLTP is necessary for non-disclosure; whenever a comparison domain C exists for which f and f ' are level increasing with respect to C, then SLTP holds. The other direction shows that, with only the limited information of A, B, f, and f ', SLTP is the best possible sufficiency condition for non-disclosure. If SLTP is satisfied, there is a possible common interpretation of levels, namely C, for which the functions have the correct non- disclosure property (that is, they are level increasing). Hence, in the absence of additional criteria about the common domain (i.e., what are the real relationships between A and B), the translation functions are plausibly secure. Note, however, that SLTP is not a sufficient condition to ensure that there is no non-disclosure problem, since the comparison domain C that is shown to exist in the theorem may not provide the real ordering relationships between the security levels in A and B (as shown in section 3.1.1). Proof of Theorem: <= Let A and B be properly embedded into C, with f and f ' satisfying the level increasing property. We will show SLTP. Suppose x is in the domain of f, y is in the domain of f ', and f(x) = y. By the level increasing property, we have p (x) = p (f(x)) and p (y) = p (f ' (y)). Also, since p is a proper embedding, A B B A B we have p (f(x)) = p (y). Hence, B B p (x) = p (f(x)) = p (y) = p (f ' (y)) and thus p (x) = p (f '(y)). A B B A A A Since p is a proper embedding, we see that x = f '(y). This proves SLTP condition 1. A similar A proof holds for condition 2. => Assuming SLTP, we construct a comparison domain C satisfying the level increasing property, with A and B properly embedded into C. Let C' be the disjoint union of A and B with the relation = defined as follows: C If x in A and y in A, then x = y iff x = y. C A If x in B and y in B, then x = y iff x = y. C B If x in A and y in B, then x = y iff there is some z in A such that z is in the domain of f and C x = z and f(z) = y (see Figure 4). A B If x in B and y in A, then x = y iff there is some z in B such that z is in the domain of f ' and C x = z and f(z) = y. B A 5 y z f(z) x Figure 4: Part of inequality definition Because the orderings = = agree on elements of A and = = agree on element of B, we can A, C B, C unambiguously drop the subscripts. We will eventually construct a partially ordered set C that satisfies the conditions of the theorem by identifying elements of C'. First, we show some properties of C'. Reflexive: It is easy to see that x = x for any x in C'. Transitive: We next show transitivity of the partial order =. There are several cases to consider. Suppose we have x, y, z such that x = y and y = z. We must show that x = z. First, suppose x is in A. Case: y is in A and z is in A: Then x = z by transitivity of = in A. Case: y is in A and z is in B: Expanding the definition of y = z, we can find a q in A such that y = q and f(q) = z. By transitivity in A and the hypotheses that x = y and y = q, we obtain x = q. Since we have f(q) = z, by the definition of = in C, we conclude that x = z. Case: y is in B and z is in B: Expanding the definition of x = y, we can find a q in A such that x = q and f(q) = y. Since y = z, we have f(q) = z by transitivity in B. So, by the definition of = in C, x = z. Case: y is B and z is in A: Expanding the definition of x = y, we can find a q in A such that x = q and f(q) = y. Expanding the definition of y = z, we obtain an r in B such that y = r and f '(r) = z. 6 (See Figure 5.) By transitivity in B, we conclude that f(q) = r. By the property SLTP, we have q = f '(r). Then, since x = q and f '(r) = z, we find that x = z by transitivity in A. z r f’(r) y q f(q) x Figure 5: Relationship of x, y, and z This completes the cases for x in A. The cases for x in B are similar. Hence the relation = is transitive. Now, define x ˜ y iff x = y and y = x. It is easy to check that this is an equivalence relation. We denote the equivalence class of x by [x]. Let C = (C'/˜,<) be the set of equivalence classes of C' with respect to ˜, where [a] < [b] iff (a = b in C' and not [a] = [b] in C). Note that this is well defined. First, observe that C is indeed a partially ordered set. We now show C satisfies proper embedding and the level increasing property. Proper Embedding: We show that the maps p (a) = [a] and p (b) = [b] are proper embeddings of A and B into C. A B If x, y in A, then (p (x) = p (y)) iff ([x] = [y]) iff (x = y and y = x in C') iff (x = y and y = x in A) A A iff (x = y in A). If x, y in A then (p (x) < p (y)) iff ([x] < [y]) iff (x = y in C' and not [x] = [y] in C) iff A A (x = y in A and not x = y in A) iff (x < y in A). A similar argument holds for the map p from B to C. B So, A and B are properly embedded in C. 7 Level Increasing: For all a in the domain of f, a = f(a) in C by the definition of =. Similarly, b = f ' (b) in C. So, C satisfies the level increasing property. Thus we have constructed a comparison domain C with the desired properties. This proves the theorem. ? We now note that the comparison domain C constructed in the theorem satisfies the property that an element of A is identified with an element of B exactly when the functions translate them to each other. Proposition: Let C be a comparison domain as constructed in the theorem. For any x in A and y in B, [x] = [y] iff (y = f(x) and x = f '(y)). <=: If y = f(x) then x = x, x maps to f(x), and f(x) = y. Hence, by the definition of the partial order in C', we find that x = y. Similarly, y = x. Hence, [x] = [y]. =>: If [x] = [y] in C, then x = y and y = x in C'. So, there exists q in A such that x = q and f(q) = y and r in B such that y = r and f '(r) = y. We combine these inequalities to conclude that x = q = f '(r) and y = f(q) = r (see Figure 6). This produces the desired result. ? y q f(q) x r f ' (r) y q f(q) x Figure 6: x = f(y) and y = f ' (x) 8 3.1.4 Total Functions The natural interpretation of a partial translation function is that when an element is not in the domain of the function, the message is not sent. (There may, or may not, be some notification to the sender.) We can convert such partial functions to total functions by: 1) Introducing a new level in A and B which is higher than any possible clearance. 2) Extending the functions to take this value whenever they are partial. If the modified functions are used, the effect is that any message with a label not in the domain of the partial function will still not be sent, since it will fail the access constraint. So from an abstract point of view, the security analysis of the translation functions could assume only total functions. However, there are some practical differences and, to avoid confusion, we have used partial functions. 3.1.5 Simplification of SLTP under order compatibility In some cases, it may be reasonable to impose some other constraints on the translation functions that are not strictly necessary for non-disclosure. Consider the following property, which we call order compatibility: For x and y in the domain of f, x < y => f(x) = f(y), and for x and y in the domain of f ', x < y => f '(x) = f '(y). Order compatibility says that the B’s view of the ordering on A is compatible with A’s view, although there may be some collapse. Similarly, this holds for A’s view of B’s ordering. Order compatibility is not strictly necessary to satisfy non-disclosure (and hence not inferable from the property SLTP). For example, A could be {U, C}, B could be {S, TS} and C could be {U, C, S, TS} with the natural orderings. The translation function f(U) = TS and f(C) = S would not cause a leak, even though it violates order compatibility. However, it is desirable to construct translation functions which are as faithful as possible. In particular, translation functions should generally not send a level to a level that is higher than necessary. If order compatibility is not satisfied, then this principle is violated. We show that if a level increasing function f does not satisfy order compatibility, then there is another function that is still level increasing but does not increase the level as much. Suppose there are elements x and y such that x < y, f(x) > f(y), where f is level increasing. Let g be the same as f, but with g(x) = f(y). Then g is still level increasing, by the following argument. For all other elements except x, it follows because g agrees with f. And for x, since p (y) = p (f(y)) and p (x)< p (y), we see that p (x) < p (f(y)). Hence, p (x) < p (g(x)), so g A B A A A B A B is still level increasing. Further, for any y in the domain of f, g(y) = f(y) and g(x) < f(x). Thus g is a more faithful alternative to f. If the translation functions are total and they satisfy order compatibility, then SLTP can be expressed in a simple form. 9