Jif Java Information Flow Steve Zdancewic University of Pennsylvania Andrew Myers Lantian Zheng Nate Nystrom Cornell University Confidential Data Networked information systems PCs store passwords e mail finances Businesses rely on computing infrastructure Military government communications Security of data and infrastructure is critical Trust in Cyberspace Schneider et al 99 2 1 Problems in Practice Eli Lilly major pharmaceutical company leaks the names of 669 Prozac users Oops Which is essentially what the company said when it found out about the error ComputerUser magazine CartManager leaks personal info of millions BJ s wholesale club leaks 1000 s of credit cards 3 Technical Challenges Software is large and complex Security policies are complex Requires tools automation Existing mechanisms are crucial but OS Coarse granularity of access control Cryptography must be applied appropriately 4 2 High level Policy HIPAA Sarbanes Oxley Penn State Visa 5 High level policy As in all medical matters these tests and services are confidential in accordance with Pennsylvania Act 148 from Penn State Policy AD43 6 3 Low level security As in all medical matters these tests and services are confidential in accordance with Pennsylvania Act 148 void checkHIV Patient id MedRecord mr getRecord id if mr tests HIVpositive out print HIV pos Information leak 7 Jif Java Information Flow Myers Nystrom Zdancewic Zheng Java With some restrictions Information Flow Policy Language Principals and Labels Principal Hierarchy delegation Confidentiality Integrity constraints Robust Declassification Endorsement Language features i e polymorphism 8 4 Benefits Explicit fine grained policies Program abstractions Regulate end to end behavior Information Flow vs Access Control Tools increased confidence in security 9 Information flow Policy Downloadable financial planner Disk Network Accounting Software Access control insufficient 10 5 Noninterference Reynolds 78 Goguen Meseguer 82 84 Disk Network Accounting Software Private data does not interfere with network communication Baseline confidentiality policy 11 Principals Principals users groups etc Express constraints on data usage Distinct from hosts Alice Bob etc are principals Jif runtime represents principals as Java classes 12 6 Decentralized Labels Myers Liskov 97 00 Simple Component owner readers Alice Bob Eve Alice owns this data and she permits Bob Eve to read it Compound Labels Alice Charles Bob Charles Alice Bob own this data but only Charles can read it 13 Label Lattice T Order Join Alice Labels higher in the lattice are more restrictive Alice Bob Alice Bob Charles Alice Bob Eve 14 7 Integrity Constraints Specify who can write to a piece of data Alice Bob Alice owns this data and she permits Bob to change it Both kinds of constraints Alice Bob Alice 15 Extended Types Jif augments Java s types with labels int Alice Bob x Object L o Subtyping Inherited from the lattice order Inference All Jif expressions have labeled types Programmers may elide types 16 8 Implicit Flows PC Label Alice Alice Alice Bob Alice Bob int Alice a int Bob b if a 0 then b 4 Assignment leaks information contained in the program counter 17 Implicit Flows PC Label Alice Alice Alice Bob Alice Bob int Alice a int Bob b if a 0 then b 4 To assign to variable with label X must have PC X 18 9 Function Calls PC Label Alice Alice Alice Bob Alice int Alice a int Bob b if a 0 then f 4 Bob Effects inside the function can leak information about the program counter 19 Method Types int L1 method B int L2 arg E where authority Alice Constrain begin and end PC labels To call PC B On return PC E May include where clauses to specify Authority set of principals Caller s Authority 20 10 Richer Security Policies More complex policies Alice will release her data to Bob but only after he has paid 10 Noninterference too restrictive In practice programs do leak some information Justification lies outside the model i e cryptography 21 Declassification int Alice a int Paid compute Paid if Paid 10 int Alice Bob b declassify a Alice Bob down cast int Alice to int Alice Bob 22 11 Robust Declassification Zdancewic Myers CSFW 01 int Alice a Alice needs to trust the contents int Alice Paid of paid compute Paid if Paid 10 int Alice Bob b declassify a Alice Bob Introduces constraint PC Alice 23 First Class Labels Principals Two new primitive datatypes principal Can be bound to different users at run time Programmer can ask whether p actsfor q label A value that can be used as a dynamic tag If x is a label value then x is the type Can use switchlabel l to examine run time labels 24 12 Parameterized Classes Jif allows classes to be parameterized by labels and principals Code reuse e g Containers parameterized by labels class MyClass label L int L x 25 Unix cat in Jif public static void main String args String filename args 0 final principal p Runtime user final label lb lb new label p Runtime p runtime Runtime getRuntime p FileInputStream lb fis runtime openFileRead filename lb InputStreamReader lb reader new InputStreamReader lb fis BufferedReader lb br new BufferedReader lb reader PrintStream lb out runtime out String line br readLine while line null out println line line br readLine 26 13 Caveats No threads Information flow hard to control Active area of research still preliminary Timing channels not controlled Explicit choice for practicality See Agat 01 for alternatives Other differences from Java Some exceptions are fatal Restricted access to some System calls 27 Language based Security Denning 75 77 Reynolds 78 Smith Volpano 96 01 Abadi Banerjee Heintz and Riecke 99 Sabelfeld Sands 01 Honda Yoshida 01 02 Pottier et al 01 02 Banerjee Naumann 02 Many others 28 14 Jif Project Status Complete implementation of Jif Implemented several thousand LOC Mostly small test cases Port of Java s io package Hashtable implementation Tax simulation 300 LOC Battleship program 300 LOC Poker 5000 LOC Mail client 5000 LOC 29 Jif Project Home www cs cornell edu jif 30 15
View Full Document
Unlocking...