Links

Home

Results

People

Publications

Software

Jeddak Language

The Jeddak language is an extension of the Java language, intended to incorporate KDLM and related abstractions into distributed Java applications.

Security Type Abstractions

The key idea of Jeddak is to model security policies in the type system, using cryptographic keys as run-time witnesses for policies and principals. Some of the abstractions of the language are given below:

Security Type Abstractions in Jeddak
Abstraction
Example
anonymous policy alice : { bob, carol }
policy spec policyspec KT [alice : { bob, carol }]
named policy policy KT K
security label {K1, … , Kn}
security type {K1, … , Kn} T

Policies may be named or anonymous. Named policies are a distinct feature of KDLM, and are motivated by KDLM's support for distributed declassification based on declassification certificates. Following the example set by the decentralized label model, a policy identifies a principal that controls that policy (i.e., can relax the policy) as well as the principals that are allowed access to data under the policy. In the anonymous policy above, Alice controls the policy, and Bob and Carol are allowed access to data controlled by this policy.

More generally Jeddak has named policies, as exemplified by the third example above. The identifier K is the name of the policy that is defined, where the actual policy is provided by the policy specification KT (the second example above). For those familiar with rich type systems, policy names are type-level atomic names, with security information provided by policy specifications in their kinds. Introducing named policy specifications is helpful to support abstracting over such specifications, providing kind genericity (in addition to the type genericity already available in Java).

Security labels are the basis for associating access control policies with data. A label is a collection of policies, and access is restricted to principals allowed by the intersection of the policies in the label. For example, if we have:

K1 specifies policy [Joe: {Joe,Mary,Sam}] 
K2 specifies policy [Mary: {Mary,Sue,Sam}] 
{K1,K2}int w; 

Then the variable w is only accessible to Mary and Sam.

Cryptographic APIs and Type Modules

One of the principal foci of the Jeddak language design is the proper handling of principals (and policies) where we are modeling security policies in the type system. We deliberately model policies in the type system so that a we can erase this type information at runtime. Any runtime security checks require explicit witnesses that must be implemented by application developers, e.g., using cryptographic keys. This is a design decision in the development of Jeddak. The intention is that Jeddak programming will layer explication of security policies, and static checking of compliance with those policies, on top of existing practice in developing distributed applications in Java.

Actual policies are named, and are represented by cryptographic keys. The normal Java types for keys are parameterized, indexed by the policies they enforce at run-time, for example:

class PublicKey <policyspec KT> ... 
PublicKey<KT=KT1> x; 
PublicKey<KT=KT2> y; 

Since keys are generated at run-time, policy names must also be dynamically generated; they cannot be global types. So the question is, where do policy names come from and how are they represented? Our answer to this is to introduce type parameters in class declarations that are existentially quantified, in addition to the universally quantified parameters associated with generics in Java. We modify the above declaration of the public key class:

class PublicKey <policyspec KT, policy KT K> ... 
PublicKey <KT=KT1> x; 
PublicKey <KT=KT2> y; 
{x.K,y.K}int w; 

The generic class PublicKey has two parameters, a policy specification KT and a policy name K that is specified to have this policy specification. The instantiations of PublicKey in the types of x and y only specify the instantiation of the first of these parameters, the policy specification KT. The second parameter, K, is left locally opaque in the type of the object in which it appears. Jeddak allows reference to this locally opaque type-level entity via a dot-notation. So in the above example, x.K and y.K are both type-level names for distinct policy names, where the distinction is due to the different “roots” to their paths, x and y respectively. In this case the two policy names have different specification, but they would still have distinct identity if they had the same specification, due to their different paths. In the above example, the type of w is labelled with the security policies x.K and y.K, so (ultimately) only principals in the intersection of these policies have access to the data.

In general we expect cryptographic libraries to be provided as part of the trusted computing base, presumably in Java. Jeddak then layers parameterized types on top of the types of objects created by these libraries. Although clients of these libraries may assume that the policy names are instantiated in the library, in fact this is a fiction that serves its purpose since the opaque policy names can never be exposed in Jeddak. So for example the Java JCE classes:

class KeyPair { 
   PrivateKey getPrivate (); 
   PublicKey getPublic (); 
} 
class KeyPairFactory { 
   KeyPair generateKeyPair (); 
} 

can be represented in Jeddak as:

class KeyPair <policyspec KT, policy KT K> {
   PrivateKey <KT=KT,K=K> getPrivate ();
   PublicKey <KT=KT,K=K> getPublic ();
} class KeyPairFactory <policyspec KT, policy KT K> { KeyPair<KT=KT,K=K> generateKeyPair (); }

where the classes are parameterized by policy specifications KT and policy name K. The following represents the use of these classes:

KeyPairFactory<KT=KT1> f = new KeyPairFactory<KT=KT1>(...); 
KeyPair<KT=KT1> x1 = f.generateKeyPair ();
KeyPair<KT=KT1> x2 = f.generateKeyPair ();
PublicKey<KT=KT1> x1Pub = x1.getPublic();
PublicKey<KT=KT1> x2Pub = x2.getPublic();
{x1Pub.K}int y;
{x2Pub.K}int z = y;

In the types of the variables x1, x2, x2Pub and x2Pub, the type component K is left locally opaque in their interfaces. The type syntax x1.K allows reference to the name of the locally opaque policy name in the interface of x1. The last assignment fails because y and z have different declares a public key class, parameterized by a kind (policy) specification and the policy name K.

Associating policies with public keys is one among several alternatives in the design spaces. We do not commit to any one of these choices in the Jeddak language design, but focus instead on providing mechanisms for allowing application developers to make their own choices in this design space. They do this by providing Jeddak APIs to existing trusted cryptographic libraries. For example, another point in the design space allows session keys to be associated with labels (sets of policies).

Type Revelations and Type Sharing

Consider the following example:

KeyPair <KT=KT1> x = f.generateKeyPair(); 
PublicKey <KT=KT1> xPub = x.getPublic(); 
PublicKey <KT=KT1> xPriv = x.getPrivate(); 
KeyPair <KT=KT1> y = new KeyPair<KT=KT1,K=x.K>(xPub,xPriv); 

This example fails to type-check. The problem is that the opaque types x.K, xPub.K and xPriv.K are all distinct, so the call to the constructor for KeyPair fails. This is a problem with using existential types in general, and is the reason they were initially rejected as a foundation for ML modules. Type revelations overcome this problem by allowing modules (or, in our case, objects) to reveal information about locally opaque types in interfaces. In particular it allows the identity of a locally opaque type to be shared with copies of the corresponding object. We can retype the example as follows:

KeyPair <KT=KT1> x = f.generateKeyPair (); 
PublicKey <KT=KT1,K=x.K> xPub = x.getPublic(); 
PublicKey <KT=KT1,K=x.K> xPriv = x.getPrivate(); 
KeyPair <KT=KT1,K=x.K> y = new KeyPair<KT=KT1,K=x.K>(xPub,xPriv); 

In this case the type sharing constraint K=x.K propagates through the various copies of the keys in the key pair object x. This propagation begins with a type rule that says that if x has type

KeyPair <KT=KT1>

then it has the type

KeyPair <KT=x.KT,K=x.K>

that makes the identity of each type field explicit in the object interface. Then for example the type of the getPrivate field

PrivateKey <KT=KT,K=K> getPrivate ();      

propagates this into the type of the private key object returned.

Type sharing constraints that allow locally abstract types (policy names) to share identity are one example of type revelations that expose information about otherwise opaque types. Here is another example, taken from an API for sockets that places label constraints on the data being transmitted over the secure link:

class Socket <label L> { ... } 
class TCPSocket <label L={}> extends Socket <L> { ... }
class SSLSocket <
    prin Local, prin Remote, 
    policyspec KTlocal=[Local:{Remote}], 
    policyspec KTremote=[Remote:{Local}], 
    policy KTlocal Kloc, policy KTremote Krem, 
    label L={Kloc,Krem}
> extends Socket <L> { ... } 

A generic socket class is parameterized by the security label for data transmitted on the socket connection. A TCP socket has the empty label, reflecting the fact that there are no security guarantees for data transmitted on the connection. An SSL socket has a security label that reflects two policies, one for each of the two parties in the connection (Local and Remote) that grants the other party access to the data on the connection1.

In a TCP socket, there are no further instantiations of the type parameters allowed, since the label has been fully instantiated (to the empty label). For the SSL socket, the identities of the principals and the names of the policies must still be instantiated. The label and the policy specifications are fully determined by the class declaration.

This generates a general facility to specialize the instantiations of the type parameters in subclasses, which is a fundamental part of structuring classes with security annotations: subclasses provide more specific security guarantees. In this case the KTLocal, KTremote and L parameters of the SSL socket class, for example, should be considered as “exports” from an object interface rather than “imports” that are provided at the point that such an object is created. Of course all “imports” are also “exports” by virtue of treating type parameters as universally quantified before instantiation and existentially quantified after instantiation.

The structure of imports and exports can sometimes be complicated. Taking again from the SSL example, we have the following pattern of instantiations for when a socket is created by the server socket class:

class SSLKeysSocket <
   prin Local, prin Remote, 
   policyspec KTlocal=[Local:{Remote}], 
   policyspec KTremote=[Remote:{Local}], 
   policy KTlocal Kloc=kloc.K, 
   policy KTremote Krem=krem.K, 
   label L={kloc.K,krem.K} 
> extends Socket <...> {
   PublicKey <KT=KTlocal> kloc = null; 
   PublicKey <KT=KTremote> krem = null; 
   GroupKey <L={Kloc,Krem}> sessionKey = null; 
}

An instantiation of this implementation class need only provide an instantiation of the principals, since the policy names are now determined with reference to the public key fields that provide locally opaque names for the policies. The reason for using these fields for names is that, when the SSLKeysSocket object is initially created, these fields are null, and their contents are determined as key agreement is performed during establishment of the secure connection. Again the way to think about this is that the Kloc and Krem fields are exports from the object interface. There is no circularity among the exports because it is possible to order the exports to break any apparent cycles; the type rules rely on such a well-foundedness condition to ensure that there is always a finite type derivation for the well-formedness of an object type.

The sessionKey field in the above example is a symmetric encryption key. There are several ways to handle symmetric keys, so we expect several different libraries depending on how an application expects to use such keys. For example we have developed an API for the Java JCE key agreement library (based on Diffie-Helman key agreement) that parameterizes a symmetric key type by a security label, reflecting the different individually controlled policies that went into the generation of that session key. The type GroupKey is the type of such session keys.

The ability to mutate variables with locally opaque types must be treated carefully. Consider the following example (using types to demonstrate a potential unsoundness in the type system):

class C <type T> { 
   T f(int); 
   int g(T x); 
} 
class C1 <T=Integer> extends C<T> ... 
class C2 <T=String> extends C<T> ... 
C<> x = new C1<T=Integer>(); 
x.T y = x.f(3); 
x = new C2<T=String>(); 
x.g(y); 

Assuming C1 and C2 use different representations for the state they provide to clients, confusing the implementations (via the mutation of the implementation that x is bound to) can give rise to unsoundness in the type system. There are several possibilities for handling this situation. Requiring such fields to be final is clearly useless for the above example, since the fields are initially undefined and subsequently redefined during key negotation. Another possibility is to require a field to be final (immutable) if there are any negative occurrences of the type parameters in the method types. However there are still problems with sharing constraints that relate opaque types in different object-assigned variables, that may be violated after-the-fact by a mutation of the original variable after it has been copied. Our solution is to allow such fields to be “single-assignable”: initially null and subsequently assigned a non-null value once. In general this requires a run-time check on every assignment (because of the non-local nature of the data flow); this check should be cheap, since the assignment should only be performed once. In general therefore we only allow mutation on fields whose type parameters are completely exposed in their interface.

Secure Transport

SSL and TLS sockets are widely used to secure Internet transport connections for e-commerce. We consider their implementation an important consideration for Jeddak because of the latter’s motivation, to place large parts of the security protocol stack inside the application. The following provides an interface for standard Internet sockets, with the type indexed by a label that specifies who is allowed to read and write on the transport connection:

abstract class Socket <label L> { 
   Socket (InetAddress address, int port); 
   InputStream<L> getInputStream(); 
   OutputStream<L> getOutputStream(); 
   void close(); 
} 
abstract class ServerSocket<label L> { 
   ServerSocket (int port); 
   void Socket<L> accept(); 
   void implAccept (Socket<L> s); 
   void close(); 
} 
class TCPSocket <label L, L= {}> extends Socket<L> { ... } 
class TCPServerSocket <label L, L= {}> extends ServerSocket<L> { ... } 
abstract class SSLSocket <
   prin Local, prin Remote, 
   policyspec KTlocal=(Local:{Remote}), 
   policyspec KTremote=(Remote:{Local}), 
   policy KTlocal Kloc, policy KTremote Krem, 
   label L={Kloc,Krem}
> extends Socket<L> {...}
 
class SSLKeysSocket <
   prin Local, prin Remote, 
   policyspec KTlocal=(Local:{Remote}), 
   policyspec KTremote=(Remote:{Local}), 
   policy KTlocal Kloc=kloc.K, 
   policy KTremote Krem=krem.K, 
   label L={kloc.K,krem.K} 
> extends SSLSocket<Local,Remote,KTlocal,KTremote,Kloc,Krem,L> {
   sa PublicKey<KTlocal> kloc; 
   sa PublicKey<KTremote> krem; 
   sa SecretGroupKey<L={Kloc,Krem}> sessionKey; 
   ... 
} 

class SSLServerSocket <
   prin Local, prin Remote, 
   policyspec KTlocal=(Local:{Remote}), 
   policyspec KTremote=(Remote:{Local}) > { 
   ...
   SSLSocket<Local,Remote> accept () { 
      SSLsocket <Local,Remote> s = new SSLKeysSocket <Local, Remote> (); 
      implAccept (s); 
      s.beginHandshake(); 
      return s; 
   } 
}

The Socket class is defined as an abstract class because it would be unsafe to allow unrestricted access to socket instantiation using this class. For example:

PublicKey<KT=[Alice:{Bob}]> k0;
PublicKey<KT=[Bob:{Alice}]> k1;
ServerSocket<L={k0.K,k1.K}> socket = … 
Socket<L={k0.K,k1.K}> connection = socket.accept();
OutputStream<L={k0.K,k1.K}> out = connection.getOutputStream();
PrintWriter<L={k0.K,k1.K}> wr = new PrintWriter<L={k0.K,k1.K}>(out);
wr.print("Some amazingly sensitive piece of data");

This is an unsafe use of the Socket API because the principals Alice and Bob may exchange data in cleartext over a TCP/IP socket, fooled by the security label on the stream into believing that their communication is secure. If we allowed the ServerSocket class to be instantiated directly, with an arbitrary label, then data with security guarantees could be transmitted in cleartext over the Internet, as demonstrated by the example above. Preventing this in the ServerSocket class would require some reasoning in the runtime about (a) the relative sensitivity of the data (as reflected in the label of the data channel) and (b) the relative trustworthiness of the medium (as reflected in the address being connected to). For example it might (under some circumstances) be considered reasonable to transmit data in cleartext over Unix domain sockets (i.e., on the local machine). We have done some investigations in this direction, but we have not incorporated it into the general Jeddak framework.

The approach instead is to offer two subclasses of Socket. The TCPSocket class specifies that the label is empty. This prevents the transmission of sensitive data over such a connection. The only way to instantiate TCP sockets is with an empty label, reflecting that all communication using such sockets is insecure.

ServerSocket <L={}> svr = new ServerSocket <L={}> (...); 
Socket <L={}> connection = svr.accept(); 
OutputStream <L={}> out = connection.getOutputStream(); 
PrintWriter <L={}> wr = new PrintWriter <L={}> (out); 
{k0.K,k1.K}String privData; 
wr.print(privData); // type failure 

Secure data is transmitted via a SSLSocket connection. To explain this API, consider first the SSLFTOSocket definition below:

 class SSLFTOSocket <
   prin Local, prin Remote, 
   policyspec KTlocal=(Local:{Remote}), 
   policyspec KTremote=(Remote:{Local}), 
   policy KTlocal Kloc, policy KTremote Krem, 
   label L={Kloc,Krem}
> extends Socket<L> { 
    SecretGroupKey<L={Kloc,Krem}> sessionKey; 
    ... 
} 
class SSLFTOServerSocket <
    prin Local, prin Remote, 
    policyspec KTlocal=(Local:{Remote}), 
    policyspec KTremote=(Remote:{Local})> { 
    PrivateKey <KTlocal> kloc; 
    SSLFTOSocket (PrivateKey<KTlocal> k) { this.kloc = k; } 
    SSLFTOSocket <Local, Remote, KTlocal, KTremote> accept () 
    { 
    implAccept(); 
    PublicKey<KT=KTremote> krem = handshake(); 
    SSLsocket<KTlocal,KTremote> s = 
        new SSLFTOSocket 
            <Kloc=kloc.K, Krem=krem.K, L= {kloc.K, krem.K}> (this); 
    return s; 
    }

The SSLFTOSocket class extends the Socket class with further parameters to specialize the label L. There are two policies (more precisely, policy names), Kloc and Krem, for the policies specified by the local and remote peers, respectively (identified by the Local and Remote principals provided as parameters). The label parameter L is constrained to be {Kloc,Krem}. The SSLFTOServerSocket class provides an implementation of the server side of the socket stream protocol. The server socket is assumed to be provided with the local principal private key (more precisely, the local secret for the key exchange) at the point that it is created. The method for accepting client connections calls the base class implAccept to actually accept transport connections from clients3 . Once this is done, a handshake method actually establishes the exchange of secrets between local and remote peers. These secrets are handed off to the constructor for the stream socket, which generates the session key(s) for the connection.

Both this and the SSLServerSocket class assume the class is instantiated with the remote principal. Obviously more general several principals might establish connections to the server. We only make this assumption for perspecuity, it can be fixed by having a locally opaque remote principal in the socket interface returned by accept.

This API is unrealistic because this is not in practice how SSL connections are established. Rather, the server socket accept method returns immediately with the stream socket, and the handshake protocol runs in parallel with the calling program. Furthermore, it is highly unrealistic to assume that the server socket has a single local secret (Kloc in the example) that it uses to secure all connections. Rather the local peer has a suite of ciphers that it can choose from in securing the connection, and part of the SSL protocol consists of the peers negotiating which ciphers they are going to use. The choice of secret may depend on which cipher they agree to use. The choice of a single secret at the point of establishment of the server socket also severely limits the API, since this secret restricts communications on all transport connections to this server port to a particular remote principal (Remote in the API).

The SSLServerSocket API above fixes this API, with the addition of single-assignment variables to the language semantics:

class SSLKeysSocket <
   prin Local, prin Remote, 
   policyspec KTlocal=(Local:{Remote}), 
   policyspec KTremote=(Remote:{Local}), 
   policy KTlocal Kloc=kloc.K, 
   policy KTremote Krem=krem.K, 
   label L={kloc.K,krem.K} 
> extends SSLSocket<Local,Remote,KTlocal,KTremote,Kloc,Krem,L> {
   sa PublicKey<KTlocal> kloc; 
   sa PublicKey<KTremote> krem; 
   sa SecretGroupKey<L={Kloc,Krem}> sessionKey; 
   ... 
} 

A single-assignment variable is one that can initially be null, but should eventually be instantiated to a non-null object reference. Any access to the variable while null is considered an error. Any attempt to mutate the variable once it has been set to a non-null object reference is similarly an error. So all references to single-assignment variables must be checked. This does not pose performance problems, since they exist in our semantics purely to provide placeholders for policy names that have not yet been determined. Once determined, the corresponding object reference can be copied to a final variable for processing without requiring further checking, with type sharing allowing policy names in the copy to share identity with policy names in the original.

Single-assignment variables are used in the SSLKeysSocket, which is the implementation class for the SSLSocket class (the latter is an interface to hide the local names of the policies). In the former class, the policies for the connection label are named by local single-assignment variables kloc and krem. The keyword sa denotes that they are single-assignment: initially null, inaccessible at run-time until they are assigned to a non-null value, and thereafter immutable. We now allow the class parameter specifications to refer to these local fields in constraining the bindings of the Kloc and Krem policy names. In case it might appear strange to have the class parameter specifications referring to the fields, consider a class in Jeddak as both a functor (parameterized module) and structure (implementation module) in ML module terminology. The fact that the Kloc and Krem parameters of the SSLKeysSocket class are completely defined by the sharing constraints means that no further instantiation of them is necessary, so we may consider them as only exports rather than imports from the module (object). The local fields kloc and krem can therefore be viewed as embedded modules (substructures in ML terminology). The only extra complication added here is the addition of single-assignedness, which allows the type components of such fields to be referred to in other types before their value fields are defined. The immutability of type definitions is what makes this sound (this in turn relies on variables bound to objects with local type fields being declared final).

The SSLServerSocket class uses this definition in the accept method. The socket object can now be created immediately, rather than waiting until after the handshake as with the SSLFTOServerSocket implementation. The only type-level fields that need to specified in the instantiation of the SSLKeysSocket are the local and remote principals; all other parameters are completely specified by the interface. The base class connection acceptance implementation then operates directly on this socket. Once the connection is established, the handshake protocol for key exchange and secret generation is started, and the socket returned immediately. The socket interface identifies via its label the policies that control access to the resulting byte stream, despite the fact that the secrets establishing the identity of those policies will not be known until after the conclusion of the handshaking. At that point, the local kloc and krem fields in the socket will be set, as well as the session key.