Formalization and analysis of privacy and web security policies
Abstract/Contents
- Abstract
- The privacy regulations and policies for healthcare and other industries are often complex, and the design and implementation of effective compliance systems call for precise analysis of the policies and understanding of their consequences. Similarly, the Web as a complex platform for sophisticated distributed applications has multifaceted security requirements. Its security specifications may involve unstated and unverified assumptions about other components of the web, and may introduce new vulnerabilities and break security invariants assumed by web applications. This work describes two formalization frameworks designed for privacy and web security policies, shows that abstract yet informed models of privacy and security policies can be amenable to automation, detect policy violations, and support useful evaluation of alternate designs. Formalization of applicable privacy policies that regulate business processes can facilitate policy compliance in certain computer applications. In this study, a stratified fragment of Datalog with limited use of negation is used to formalize a portion of the US Health Insurance Portability and Accountability Act (HIPAA). Each communication of Protected Health Information (PHI) is modeled as a mathematical tuple, the privacy policies are modeled as logic rules, and rule combination and conflict resolution are discussed. Federal and State policy makers have called for both education to increase stakeholder understanding of complex policies and improved systems that impose policy restrictions on the access and transmission of Electronic Health Information (EHI). Building on the work of formalizing privacy laws as logic programs, the existence of a representative finite model that exhibits precisely how the policy applies in all the cases it governs is proved for policies that conform to certain acyclicity pattern evident in HIPAA. This representative finite model could facilitate education and training on policy compliance, and support policy development and debugging. To address the need for secure transmission of usable EHI, a formalization of policy expressed as a logic program is used to automatically generate a form of access control policy used for Attribute-Based Encryption (ABE). This approach, testable using the representative finite model, makes it possible to share policy-encrypted data on untrusted cloud servers, or send strategically encrypted data across potentially insecure networks. As part of the study, a prototype is built to secure Health Information Exchanges (HIEs) using automatically generates ABE policies, and its performance is measured. For web security policies, a formal model of web security based on an abstraction of the web platform is described and partially implemented in the Alloy programming language. Three distinct threat models are identified that can be used to analyze web applications, ranging from a web attacker who controls malicious web sites and clients, to stronger attackers who can control the network or leverage sites designed to display user-supplied content. Two broadly applicable security goals are proposed, and certain security mechanisms are studied in detail. In the case studies, a SAT-based model-checking tool is used to find both previously known vulnerabilities and new vulnerabilities. The case study of a Kerberos-based single sign-on system illustrates the differences between a secure network protocol using custom client software and a similar but vulnerable web protocol that uses cookies, redirects, and embedded links instead.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2015 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Lam, Peifung E | |
|---|---|---|
| Associated with | Stanford University, Department of Computer Science. | |
| Primary advisor | Mitchell, John | |
| Thesis advisor | Mitchell, John | |
| Thesis advisor | Boneh, Dan | |
| Thesis advisor | Williams, Ryan (Richard Ryan) | |
| Advisor | Boneh, Dan | |
| Advisor | Williams, Ryan (Richard Ryan) |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | Peifung E. Lam. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Thesis (Ph.D.)--Stanford University, 2015. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2015 by Peifung Eric Lam
- License
- This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).
Also listed in
Loading usage metrics...