Links

Home

Results

People

Publications

Software

Cryptographic Types

Programming of wide-area networks and the Internet has gained a great deal of interest with the success of the Web. WANs and the Internet introduce or emphasize new issues that receive less priority in programming local area networks. One of these issues is the fact that communication is typically over untrusted networks, and so a security infrastructure is required to protect computations over such networks. Cryptography, for protection and for integrity, plays an important role in any such infrastructure, potentially at various levels in the network protocol stack. One way to deploy cryptography is to use it everywhere. An obvious problem with this is the runtime overhead of running cryptographic algorithms over network traffic. This might be an issue in low-power mobile wireless devices, for example. A potentially much more important problem is the loss of reliability: if cryptographic checks (decryption, authentication) are happening ubiqituously around the system, these are all potential failure points. A dual problem to this is determining when it is safe not to perform a crypto-
graphic check. Removing a check will remove a potential failure point, but at the risk of compromising the security of the systen if that check was sometimes useful.

In many cases, the ubiquitous application of cryptography is unnecessary. Wide-area networks, including the Internet, are not a single flat homogeneous namespace, with every host given the same level of trust.
Rather, networks are organized into administrative domains, with the boundaries of such domains often delineated by firewalls. Different levels of trust may be assigned to different parts of the network, based on the
application that is using the network and its relationship to those parts of the network. Blindly applying cryptography to secure all traffic is appropriate if no part of the network is trusted. This is analogous to dynamic type checking in a strongly typed language that performs all of its type-checking at runtime. Most modern programming languages perform some static checking at compile-time, with dynamic checking left for those properties that it is too difficult or impossible to check at compile time (e.g., array bounds checks, null pointer checks, checked downcasts). It is a thesis of this work that some degree of static checking can bring benefits to network
communication analogous to the case for statically typed programming languages. First, static checking improves the trustworthiness of the run-time behaviour of code because it provides static guarantees of the absence of failures of run-time checks. Second, static checking can improve efficiency by demonstrating where run-time type checks can be safely omitted (because network traffic is over trusted subnets or through
a trusted medium such as same-machine IPC). Finally, it allows layers in the security protocol stack to be moved out of the trusted computing base, relying on static checking of the security guarantees offered by such layers to upper layers.

Cryptographic types are a way to replace the ubiquitous use of cryptographic techniques with a combination of static and dynamic techniques for secure communication:

  1. Values have types that include encryption types and signature types. The former denotes a value that has been encrypted, and the type is annotated with the key that was used for encryption. The latter denotes a value that has been digitally signed, and the type is annotated with the key that was used for signing.
  2. In the case where a message is sent over an untrusted network, this is reflected by a channel type that masks the identities of keys in cryptographic types in the channel message type. Cryptographic
    types include an (unchecked) hiding rule that allows such masking be done via a coercion. There is a corresponding (checked) exposure rule that exposes key identities that have been masked by hiding. The check in the exposure rule is realized concretely by decryption and signature verification. Hiding and exposure are analogous to type widening (upcasting) and narrowing (checked downcasting), respectively, in typed object-oriented programming languages. This is with the proviso that in general
    both hiding and exposure also perform some transformation of the value, based on the application of cryptographic algorithms.

An analogy can be made between our approach and the use of types in type-safe distributed communication. Type-safe communication over an untyped channel can be achieved using an API that “forgets” type information, and then uses dynamic type-checking at run-time to reassert the expected types:

// Java example 
class Chan { 
       void send (Object x) { ... } 
       Object receive () { ... } 
} 

// Sender side 
Chan ch = new Chan(...); 
ch.send(new Integer(3)); 

// Receiver side 
Chan ch = new Chan(...); 
Object x = ch.receive(); 
Integer ix = (Integer)x; 

In this case the sending operation uses type widening to lose the type of the object being sent over the untyped channel. At the receiving site a checked cast is used to coerce the receive value to the expected type. This checked casting can be avoided if the API for the Chan class is modified to preserve the types of the values being transmitted:

class Chan { 
       void send (Integer x) { ... } 
       Integer receive () { ... } 
} 

If the type-preserving API is implemented atop an untrusted network, then there will still be checked casting “under the hood.” However there is at least the possibility of avoiding checked casts for communication that does not go over the untyped network (for example, between processes that share memory on the same machine). Also static type-safety gives a static assurance of application reliability, guaranteeing that there is no possibility of run-time type errors except where the application explicitly resorts to dynamic typing.

If the language has parameterized types or type templates, then a generic statically-typed channel API can be provided. For example the following posits a generic channel implementation, parameterized over a message type A. The sender and receiver instantiate this channel class to a channel of Integer objects. There is no loss of type information in the sending receive operation, and there is no need for a checked cast in the message receive operation:

class Chan ⟨ A ⟩ { 
       void send (A x) { ... } 
       A receive () { ... } 
} 
// Sender side 
Chan ⟨ Integer ⟩ ch = new Chan⟨ Integer ⟩(...); 
ch.send(new Integer(3)); 
// Receiver side 
Chan ⟨ Integer ⟩ ch = new Chan⟨ Integer ⟩(...); 
Integer ix = ch.receive(); 

Cryptographic types extends this approach, of combining static and dynamic checking, from type-checking of distributed communication to the checking of cryptographic properties of the communication. The cryptographic properties denote that parts of messages are signed for authentication or encrypted for privacy. Cryptographic algorithms can be used in insecure environments to ensure authentication and privacy. However if trusted communication channels can be established, for example through a trusted operating system kernel, then the application of these algorithms is unnecessary. A type system reflects when trusted communication channels can be established, and ensures that authentication and privacy properties are preserved when dynamic cryptographic checks are omitted.

Cryptographic types consider two formal systems for cryptographic types:

  1. The first system, the sec-calculus, adds “virtual” cryptographic operations (encryption, decryption, etc) as a complement to the usual “actual” cryptographic operations.
  2. The sec-calculus, although simple, has a fundamental problem that in some cases limits its usefulness. The second formal system, the ec-calculus, addresses this problem by replacing the cryptographic operations (both actual and virtual) with type-based cryptographic “hiding” and “exposing” coercions. Like upcasting, hiding never fails, while exposure may fail due to the failure of a run-time check, like checked downcasting.

Java Examples

We use Java as an example of how these approaches could be incorporated into a high-level language. Our extensions of Java include a new type Prin, the type of principals underlying computation. Every process executes under a principal. A principal can be viewed as an implicit pair of (public, private) key pairs, one for encryption and another for signing, where references to the private part are only available through signing and decryption, and otherwise references are implicitly to the public part of the keys. A process can sign messages with its underlying principal’s signing key, and a process can read messages “hidden” with the underlying principal’s encryption key. The special identifier thisPrin is provided to designate the principal underlying the current process (just as this designates the current object and currentThread() denotes the current thread; thisPrin is provided as an identifier to facilitate static checking).

The actual formal systems for the sec-calculus and ec-calculus both differentiate encryption and signing, using the key types EKey and SKey, the types of keys (key pairs) for encryption and signing, respectively. A value of one of these types is interpreted as the public key of the corresponding (public, private) key pair, with the manipulation of the private key kept implicit. The sec-calculus and ec-calculus also allow each process to execute with a collection of private keys. We use the current more limited model in the examples below for economy. Interpreting the simple sec-calculus system in Java, types may be annotated with specifications of expected cryptographic properties:

Integer vsealed a x; // x is “virtually” encrypted for a
Integer vsigned a x; // x is “virtually” signed by a
Integer sealed x; // x is “actually” encrypted
Integer signed x; // x is “actually” signed

If the underlying communication system can build a trusted channel between two processes, this is
reflected in the cryptographic type of the channel. In the following example, the currently executing process
builds a channel to the process b that will carry messages signed by itself and sealed for b:

Chan ⟨ Integer vsigned thisPrin vsealed b ⟩ chan = 
       new Chan ⟨ Integer vsigned thisPrin vsealed b ⟩; 
chan.send (vseal b (vsign thisPrin (new Integer(3))));

where vseal and vsign are the virtual cryptographic operatons for encryption and signing, respectively. These operations are “no-ops” at run-time; they serve only to annotate the static types of values with crypto- graphic specifications. The corresponding decryption and authentication operations at the receiving site are guaranteed by the type system to succeed. If the underlying communication system cannot build a trusted channel between two processes, this is again reflected in the cryptographic type of the channel:

Chan ⟨ Integer signed sealed ⟩ chan = new Chan ⟨ Integer signed sealed ⟩; 
chan.send (seal b (sign thisPrin (new Integer(3))));       

where seal and sign are the actual cryptographic operatons for encryption and signing, respectively. These operations have actual effect at run-time. Since the type system no longer tracks the identities of the princi- pals in the types, the decryption and authentication of values received on this channel may fail at run-time.

We now consider how the second formal system of cryptographic types, the ec-calculus, could be interpreted in Java. Message payloads are represented by objects. We extend class declarations with signing and sealing declarations for fields: a field can be declared to be signed by a principal and/or sealed (encrypted with the public key of) a principal. For example a request type for a client-server application may include both the request datum (say an integer) and a private reply channel. Using cryptographic types we can fur- thermore specify that reply data are signed by the server and sealed for the client. The request datum is sealed for the server, and both it and the reply channel are signed by the client. All of this is specified by the following special kinds of class templates (parameterized over the principal for the client a and the server b):

class Reply ⟨⟨a, b⟩⟩ { 
      Integer val sealed a signed b;         
}        
class ReqPayLoad ⟨⟨a, b⟩⟩ {        
      Integer data;        
      Chan ⟨ Reply⟨⟨a,b⟩⟩ ⟩ replyChan;        
}        
class Request ⟨⟨a, b⟩⟩ {        
      ReqPayLoad ⟨⟨a,b⟩⟩ payload sealed b signed a;        
} 

If the underlying communication system can build a trusted channel that satisfies these cryptographic properties, this is reflected in the type of the channel. In the following example, the server creates a reply that is virtually encrypted for the client and signed by its own key. This reply is sent to the client on a secure reply channel (i.e., one that ensures the cryptographic guarantees specified by the reply type) that was provided by the client:

// Server side    
Prin a = ... Chan ⟨ Reply⟨⟨a=a,b=thisPrin⟩⟩ ⟩ replyCh;
// received from the client Reply ⟨⟨a=a,b=thisPrin⟩⟩ reply = new Reply⟨⟨a=a,b=thisPrin⟩⟩(new Integer (3)); replyCh.send(reply); // Client side Prin b = ... Chan ⟨ Reply⟨⟨a=thisPrin,b=b⟩⟩ ⟩ replyCh = new Chan⟨ Reply⟨⟨a=thisPrin,b=b⟩⟩ ⟩(...); // ... send replyCh to the server as part of a request.... Reply ⟨⟨a=thisPrin,b=b⟩⟩ reply = replyCh.receive(); Integer data = reply.data;

If it is not possible to obtain a trusted channel, this is again reflected in the type of request and reply channels. For example a trusted reply channel has type:

Chan ⟨ Reply⟨⟨a=a,b=thisPrin⟩⟩ ⟩

The syntax b=thisPrin reflects that the principal parameter b in the type of Reply (in the server) is bound to thisPrin. On the other hand, an untrusted reply channel has type:

Chan ⟨ Reply⟨⟨ ⟩⟩ ⟩

where the type of the reply message now elides the identity of the principals. To transmit messages over these channels, the parties build values of the full types, and a hiding operation then “forgets” the principal information that is available in the full type:

// Server side 
Prin a = ... 
Chan ⟨ Reply⟨⟨ ⟩⟩ ⟩ replyCh; // received from the client 
Reply ⟨⟨a=a,b=thisPrin⟩⟩ reply = 
		new Reply⟨⟨a=a,b=thisPrin⟩⟩(new Integer (3)); 
Reply ⟨⟨ ⟩⟩ secReply = hide ⟨⟨ ⟩⟩ reply; 
replyCh.send(secReply); 

// Client side 
Prin b = ... 
Chan ⟨ Reply⟨⟨ ⟩⟩ ⟩ replyCh = new Chan⟨ Reply⟨⟨ ⟩⟩ ⟩(...); 
// ... send replyCh to the server as part of a request.... 
Reply ⟨⟨ ⟩⟩ secReply = replyCh.receive(); 
Reply ⟨⟨a=thisPrin,b=b⟩⟩ reply = expose ⟨⟨a=thisPrin,b=b⟩⟩ secReply; 
Integer data = reply.data; 

In sending the reply message, the server provides a message of type Reply ⟨⟨a=a,b=thisPrin⟩⟩, statically signed with its own private key and encrypted with the public key of the client. The communication channel only accepts values of type Reply ⟨⟨ ⟩⟩, where the signing and encryption keys are elided. This loss of static type information is reflected at runtime by a coercion from an object of type Reply ⟨⟨a=a,b=thisPrin⟩⟩ to an object of type Reply ⟨⟨ ⟩⟩. This coercion performs the actual signing and encryption of the request mes- sage. At the receiving side, the receiver performs a coercion from type Reply ⟨⟨ ⟩⟩ to type Reply ⟨⟨a=thisPrin,b=b⟩⟩. The use of thisPrin is used here to denote the private keys that only this principal has, to perform dynamic decryption of the reply message. It is also possible to consider channels that are partially secure, for example, Chan ⟨ Reply⟨⟨a=a⟩⟩ ⟩. If a reply of type Reply ⟨⟨a=a,b=thisPrin⟩⟩ is coerced to this channel type for sending, then the integrity of the data is guaranteed by a digital signature, but the secrecy of the data relies on the trustworthiness of the channel. This may reflect different tradeoffs between performance and trustworthiness for the integrity and secrecy of reply messages.