Static Information Flow and
Secure Program Partitioning

Protecting Confidential Data

Problems

Policies vs. Mechanisms

 Access Control?

Standard Mechanisms

Static information flow

Information Leaks

Noninterference

Intentional Leaks

Decentralized Label Model

Principals

Labels

Assignment

Assignment Example

Computation

Selective Declassification

Tax Preparer Example

Implicit Flows

Static Assignment Rule

Run-time Checking?

Jif: Java + Information Flow

Type checking

Convenience/Expressiveness

Annotated Class Example

Labeling the Program

actsFor & declassify

Secure distributed systems?

Example: Battleship

Secure partitioning

Security for distrusting principals

Integrity Policies

Battleship example

Replication

Host labels

Secure replication condition

Downgrading in Jif

Downgrading in Battleship

Replicating computation

Results

Related work

Program partitioning

Conclusions

Slide 44

Restoring integrity

Capability tokens

Splitting capability tokens

Theoretical results