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:
A dataflow diagram
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.).
Bob retrieves his email from a POP3 server using the MailReader class.
Securing email from end to end
This application seeks to enforce a single real-world security policy. It is seemingly simple:
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.
INSR | SIIS | CSE | Penn State | Copyright 2014 SIIS Lab