CAREER: Building Secure Applications with Non-Static Information Flow Policies

Many security concerns in computer systems can be understood in terms of information flows: private and untrusted data, as well as data derived from them, should never flow to unintended channels in a computer system. In real-world systems, such security concerns typically change over time. For example, a payment system is allowed to use credit card details during a transaction, but it should not retain any record of credit card details once the transaction is complete. The dynamic nature of security concerns makes it challenging to build, verify and debug applications with non-static information flow policies. Consequently, the information flow policies of many security-sensitive applications are currently either unspecified at all, or being treated in an ad-hoc manner, resulting in large trusted computing bases and many security bugs in real applications. This award investigates an integrated research and education plan designed to transform the way that programmers understand, specify, verify and debug non-static information flow policies. It contains three components to address the key obstacles of building secure applications with non-static policy: (1) Dependent policy gives a simple, declarative and unified view of non-static policies, including dynamic policy, downgrading policy and erasure policy that are currently formalized and checked with unconnected semantic goals, (2) CONST, a constraint language for analyzing non-static policies in applications, and (3) An error diagnosis module that provides useful feedbacks when a program violates the specified non-static policy. This research will also develop and open-source a new toolchain that integrates the three novel components, making it feasible to specify, verify and debug real applications with non-static information flow policy. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.