Usable security as a static-analysis problem

The privacy policies of many websites, especially those designed for sharing data, are a product of many inputs. They are defined by the program underlying the website, by user configurations (such as privacy settings), and by the interactions that interfaces enable with the site. A website's security thus depends partly on users' ability to effectively use security mechanisms provided through the interface.Questions about the effectiveness of an interface are typically left to manual evaluation by user-experience experts. However, interfaces are generated by programs and user input is received and processed by programs. This suggests that aspects of usable security could also be approached as a program-analysis problem.This paper establishes a foundation on which to build formal analyses for usable security. We define a formal model for data-sharing websites. We adapt a set of design principles for usable security to modern websites and formalize them with respect to our model. In the formalization, we decompose each principle into two parts: one amenable to formal analysis, and another that requires manual evaluation by a designer. We demonstrate the potential of this approach through a preliminary analysis of models of actual sites.