Information Flow Security
Susmit Jha and Sanjit A. Seshia
Security-typed languages can be used to build programs that are information-flow secure, meaning that they do not allow secret data to leak. Declassification allows programs to leak secret information in carefully prescribed ways. Manually placing declassifiers to authorize certain flows of information can be dangerous because an incorrectly placed declassifier can leak far more secure data than intended. Additionally, the sheer number of runtime flows that can cause an error means that determining where to place declassifiers can be difficult. This project involves development of a new constraint solver-based approach for diagnosing the source of information leaks in programs  and constructing information-flow secure programs by an optimized placement of declassifiers . Leakage restrictions are specified using hard constraints and potential declassifier locations are ranked using soft constraints. Finally, the placement problem is submitted to a pseudo-Boolean optimizing SAT solver that selects a minimal set of declassifiers that prevent unauthorized data leakage. These declassifiers can be reviewed by the programmer to ensure that they correspond with acceptable declassification points: if not, new hard constraints can be added and the optimization framework can be reinvoked. More recently we have also explored a graph-theoretic approach to placing declassifiers and endorsers .
The experimental results indicate that our analysis suggests declassifiers that will cause no more leakage than those placed by programmers in a fraction of the time it would take to perform a manual analysis. This work provides a foundation for less expert programmers to build information-flow secure programs and to convert existing programs to be information-flow secure.
Currently, we are trying to develop a technique which can quantitatively track the flow of information. The goal of declassification in this quantitative setting would be to minimize the mutual entropy of the secret data and the public output.
- Dave King, Trent Jaeger, Somesh Jha, and Sanjit A. Seshia, "Effective Blame for Information-Flow Violations," Proceedings of the ACM Conference on Foundations of Software Engineering (FSE), November 2008. Pre-print version available at http://www.eecs.berkeley.edu/~sseshia/pubdir/fse08-blame.pdf
- Dave King, Susmit Jha, Trent Jaeger, Somesh Jha, and Sanjit A. Seshia, "On Automatic Placement of Declassifiers for Information-Flow Security," Available at http://www.eecs.berkeley.edu/~jha/ifc.pdf
- Dave King, Susmit Jha, Divya Muthukumaran, Trent Jaeger, Somesh Jha, and Sanjit A. Seshia, "Automating Security Mediation Placement", Proceedings of the 19th European Symposium on Programming (ESOP) 2010, to appear.