From languages to systems:
Understanding practical application development in security-typed languages

Motivation

Eli Lilly Releases Confidential Info

A new software application unintentionally Emailed the names of 669 Prozac users out to each user on the listserve. Although they maintain a clear privacy policy, they unintentionally violated their own policy...more...

US secrets leaked by insider.

Leandro Aragoncillo, a marine working on the staff of then-Vice President Al Gore, leaked over 100 classified, FBI documents by sending them out over email. "Of course, it is a source of embarrassment when you find out that this kind of activity has been carried out literally right under your nose," said Martin, the former espionage prosecutor (quoted from ABC article). more...

An experiment in secure programming

Problem Security-typed languages are still in development. The most feature-full security-typed language, Jif, provides a security-typed variant of much of the Java language. Unfortunately, some practical tools are lacking in order to use this language to build real-world systems.

Goal: Improve Jif's capacity for building real-world systems.

How: Develop a practical application in Jif. Develop and supply needed tools.

Results: We found it possible to build a practical application, an email client, in Jif. We also found that tools were needed in three categories:

• Software engineering: Developing an application in Jif was complex and time-consuming. Just the edit/compile/repair cycle was tedious because of the surprisingly large number of possible information leaks in typical programs. Jif prevents all possible leaks, forcing very particular programming styles.. There are also opportunities for other refactorings to aid the programmer in labeling and re-labeling data. These developments are still in progress.
• High-level policy construction: Jif policy consists essentially of 3 parts: (1) principals, (2) delegations, (3) declassifiers. Modelling different security environments (a business, research lab, or military MLS setting, e.g.) should be possible at a high-level. This policy should be configurable at the application level rather than only at the level of each line of code. No such policy infrastructure exists for Jif.
• Distributed policy: Jif aims to be useful for building distributed, secure applications. This requires that policy be able to remain consistent across a distributed framework. Furthermore, Jif applications must be able to interact with other components, such as the operating system, network, foreign servers, etc. Currently, there is no way to maintain a policy across a distributed system involving non-Jif components.

We concluded that Jif holds great promise for building provably secure, distributed applications, but more development is needed before this goal may be realized.