JPmail: The details

An Email Client with Information-flow Control

How to prevent information leaks? Security-typed languages!

Problem: private data (like email content) is handled by applications and can be leaked maliciously or accidentally, contrary to high-level policy.

Goal: to ensure the confidentiality of private data (to enforce high-level policy) as it passes from one application to another.

How: tag data types with a security level; security-typed programming languages guarantee noninterference, i.e., that high-secure data and low-secure data don't interact.

Tools: security-typed languages automatically enforce noninterference. By using type analysis, strong security properties can be verified at compile-time.

Illustrated in the Figure, the JPmail system consists of three main components: JPmail clients, the Internet and public mail servers. Written in Jif, the JPmail client (or just JPmail throughout) is a functional email client implementing a subset of the MIME protocol. The JPmail client software consists of three software components: a POP3-based mail reader, an SMTP-based mail sender and a policy store. The client provably enforces security policy from end to end (sender to recipient). Policy is defined with respect to a principal hierarchy. Each environment defines principal hierarchies representative of their organizational rights structure.

Sending email requires three steps:

1. Alice enters email and sends through the Internet to an SMTP server
2. The SMTP Server sends the email to the POP3 server associated with Bob's address
3. Bob retrieves the mail from his POP3 server.

A dataflow diagram

Sending email

Alice initializes a MailSender with a policy and her principal name as well the necessary parameters for the outgoing mail server (address, user name, etc.).

1. Then Alice enters an email, including the header information and the text for the body of the email. This email is labeled as alice since it came from an input stream owned by Alice.
2. The email must then undergo two transformations. First, in order to send out an email, the headers must be readable by the mail server. This requires that they be declassified to public. Secondly, the body must be readable by the recipient, Bob, without being readable by the public. These two steps are performed by a reclassifier, as shown. At this point, the email headers are visible to the server while the body is visible only to the recipient.
3. The next step is to make the entire email visible to the server so that it can be sent out. At the same time, we must not compromise the policy on the body, which requires that it should only be visible to bob. To do this, we use a random one-time symmetric key approach. The one-time key (k) is generated, used to encrypt the email body (b), and encrypted with bob's public key (k⁺_bob). Then the original body is replaced with the encrypted body along with the encrypted, one-time key, i.e. the message body contains E(k, b),E(k⁺_bob, k). The encrypted values can be declassified to be visible by the server without compromising bob's privacy.
4. Finally, the email is sent to the SMTP server, which in turn delivers it to the POP3 server.

Reading email

Bob retrieves his email from a POP3 server using the MailReader class.

5. After connecting to the server, the mail reader takes in each email and examines the label field in the header (Label in the figure). The header information can remain public, but the text of the body must be decrypted and reclassified according to the label field.
6. To do this, we require Bob's private key. Since Bob has access to his own private key, it can be read in from the file system, labeled as bob. If another user were trying to impersonate Bob, the private key would not be available and the attempted decryption would fail.
7. Since Bob's private key is labeled as bob, decrypting the body of the email automatically raises the plaintext's security level to bob. Now that the body is safely in the confines of the Jif sandbox, it can be decrypted without fear that it will be leaked.
8. Finally, since the user who is running the mail reader is bob, this email can be printed to bob's terminal window.

Securing email from end to end

This application seeks to enforce a single real-world security policy. It is seemingly simple:
The body of an email should be visible only to the authorized senders and receivers.
However, provably realizing this policy was more complex than it would initially appear.

We make two clarifications about this policy. Firstly, we are only concerned with privacy (confidentiality). This is because the most recent release of Jif only handles confidentiality properties. As Jif evolves (the next release will include integrity), our models will also evolve. Secondly, our email client is not inherently limited to sending email only to authorized receivers. The way the client handles unauthorized recipients depends on the user-defined policy that is in place.

We centrally enforce policy within the client through noninterference modulo trusted declassification. Developed in our prior work, this property parameterizes a security policy based on the declassifiers that are explicitly trusted by the principals in an application. Declassifiers are the set of declassifying filters that must be used in order for an application to function (such as the filters which make the headers public or make the body public through encryption). The allowed declassifiers for each principal are defined in a separate policy file which is integrated into our Jif application using policy tools developed for this work. This security policy states that all leakage occurs through explicitly allowed declassifiers. This has the benefit of reducing security analysis to an analysis of only trusted declassifiers.

There are caveats to security that must not be overlooked. Firstly, the security properties of a program are dependent on the correctness of the Jif compiler (and our policy compiler). Secondly, the security properties may also be dependent on supporting infrastructures. This includes the correctness of encryption libraries and the strength of used cryptographic algorithms, the protection on keystores and correctness of public-key cryptographic libraries as well as the security enforced by the local file system. Moreover, for the system to be secure, the enforced policy must be consistent across all clients.

One advantage of Jif is that it forces the programmer to think in terms of information flows and to consider security concerns from the outset. Although designing security in from the beginning often complicates development, there is a strong consensus in the security community that this is the ideal approach. Furthermore, it quickly exposes the places in which filters are necessary and informs the policy that is needed to govern an application.

Finally, we observed that the policy tool was effective in decoupling policy from the programs that they govern. This allowed us to change policy easily in order to accommodate different security models. By instrumenting the code during development with different options for each filter, we could implement distinct security models without further modifying the code. Furthermore, by gathering the policy into a single file, it was easier to do a security analysis and gauge what information flows could take place for a given principal, in contrast to leaving declassify statements littered throughout the code.