Precise, dynamic information flow for database-backed applications

We present an approach for dynamic information flow control across the application and database. Our approach reduces the amount of policy code required, yields formal guarantees across the application and database, works with existing relational database implementations, and scales for realistic ap...

Full description

Bibliographic Details
Main Authors: Yang, Jean (Author), Hance, Travis (Author), Austin, Thomas H. (Author), Flanagan, Cormac (Author), Chong, Stephen (Author), Solar Lezama, Armando (Contributor)
Other Authors: Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor)
Format: Article
Language:English
Published: Association for Computing Machinery, 2017-12-29T19:45:12Z.
Subjects:
Online Access:Get fulltext
LEADER 02430 am a22003133u 4500
001 112990
042 |a dc 
100 1 0 |a Yang, Jean  |e author 
100 1 0 |a Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science  |e contributor 
100 1 0 |a Solar Lezama, Armando  |e contributor 
700 1 0 |a Hance, Travis  |e author 
700 1 0 |a Austin, Thomas H.  |e author 
700 1 0 |a Flanagan, Cormac  |e author 
700 1 0 |a Chong, Stephen  |e author 
700 1 0 |a Solar Lezama, Armando  |e author 
245 0 0 |a Precise, dynamic information flow for database-backed applications 
260 |b Association for Computing Machinery,   |c 2017-12-29T19:45:12Z. 
856 |z Get fulltext  |u http://hdl.handle.net/1721.1/112990 
520 |a We present an approach for dynamic information flow control across the application and database. Our approach reduces the amount of policy code required, yields formal guarantees across the application and database, works with existing relational database implementations, and scales for realistic applications. In this paper, we present a programming model that factors out information flow policies from application code and database queries, a dynamic semantics for the underlying $^JDB$ core language, and proofs of termination-insensitive non-interference and policy compliance for the semantics. We implement these ideas in Jacqueline, a Python web framework, and demonstrate feasibility through three application case studies: a course manager, a health record system, and a conference management system used to run an academic workshop. We show that in comparison to traditional applications with hand-coded policy checks, Jacqueline applications have 1) a smaller trusted computing base, 2) fewer lines of policy code, and 2) reasonable, often negligible, additional overheads. Keywords: Web frameworks, information flow 
520 |a Facebook (Fellowship) 
520 |a Levine (Fellowship) 
520 |a Qatar Computing Research Institute 
520 |a National Science Foundation (U.S.) (Grant 1054172) 
520 |a National Science Foundation (U.S.) (Grant CCF-1139056) 
520 |a National Science Foundation (U.S.) (Grant CCF-1337278) 
520 |a National Science Foundation (U.S.) (Grant CCF-1421016) 
546 |a en_US 
655 7 |a Article 
773 |t Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI 2016