40 million credit cards leaked

Policy is not enough

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...

Lax Security Compromised Thousands of Credit and Debit Cards.

BJ'S Wholesale Club Settles FTC Charges. It was not a problem with policy, but rather with enforcing the policy...more...

Company Disclosed Personal Information of Nearly One Million Consumers

"Privacy policy: It's simple. We don't sell, trade, or lend any information on our customers or visitors to anyone.” But CartManager collected and rented the personal information of nearly one million consumers who shopped at merchant sites..." more...

Provable Confidentiality Guarantees

Although security policy dictates acceptable information flows, provable guarantees are needed for critical software systems. Even extensive manual certification processes cannot provide enough confidence that software is implemented according to security policy specifications. This was seen clearly in the Diebold electronic voting software which passed certification, but was later discovered to contain serious security flaws.

data leakage

End-to-End Information Flow Control

How to prevent information leaks?

Problem: private data (like credit card numbers) are 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; type-secure programming languages provably 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.
Advantages:
  1. Using static analysis can enforce stronger properties than the common runtime approach of using reference monitors.
  2. Runtime performance is improved by being able to perform the analysis at compile time.
  3. The type properties could be used to generate proof-carrying code for verification of the security of untrusted applications.
A new approach to secure program development

A New Approach

Intermediate-level Security Policy Information Flow Framework

This program and policy structure will be low level enough so that it can be automatically generated from a security-typed program using our program policy abstraction tool.

The intermediate-level representation will be high-level enough that it will facilitate an automatic mapping of policy labels from a high-level security policy language.

By using our refactoring tools, the intermediate level framework and a high level policy can be combined to generate policy labels automatically for a security-typed program.

This intermediate-level security policy flow framework will bridge the semantic gap and allow for high-level security policies to be implemented efficiently in real applications with provable guarantees of compliance.

New Developer Tools

A Jif IDE using Eclipse

Jif development is prohibitive for large applications, as two recent case studies (including our own) have shown. If Jif programming is to become practical, some tools are needed to aid in application development.

IBM's Eclipse framework has been used for building various Integrated Development Environments, notably for Java and C. We are developing a new IDE for secure programming in Jif.

Visualization Tools

  1. One of the most challenging parts of Jif programming is visualizing information flows. Color syntax and integrated graphing tools will aid in this.
  2. The complexity of Jif annotations can become confusing. The ability to hide and expose annotations simplifies the task of the programmer.

Automation Tools

  1. The Jif programmer faces both tedious and challenging tasks. Automation tools assist in both. Assisted annotation of native Java methods is an example of reducing tedious tasks.
  2. Refactoring tools will provide automated inference of security labels, derived from an intermediate-level security policy flow graph.