A Framework for Composing Security-typed Languages
| dc.contributor.advisor | von Ronne, Jeffery | |
| dc.contributor.author | Gampe, Andreas Robert | |
| dc.contributor.committeeMember | Krishnan, Ram | |
| dc.contributor.committeeMember | Niu, Jianwei | |
| dc.contributor.committeeMember | Sandhu, Ravi | |
| dc.contributor.committeeMember | Wang, Xiaoyin | |
| dc.contributor.committeeMember | White, Gregory B. | |
| dc.date.accessioned | 2024-02-09T21:10:49Z | |
| dc.date.available | 2024-02-09T21:10:49Z | |
| dc.date.issued | 2013 | |
| dc.description | This item is available only to currently enrolled UTSA students, faculty or staff. To download, navigate to Log In in the top right-hand corner of this screen, then select Log in with my UTSA ID. | |
| dc.description.abstract | Ensuring that software protects its users' privacy has become an increasingly pressing challenge. Requiring software to be certified with a secure type system is one enforcement mechanism. Protecting privacy with type systems, however, has only been studied for programs written entirely in a single language, whereas software is frequently implemented using multiple languages specialized for different tasks. We present a framework that facilitates reasoning over composite languages. In it, guarantees of sufficiently related component languages can be lifted to the composed language. This can significantly lower the burden necessary to certify that such composite programs are safe. Our simple but powerful approach relies, at its core, on computability. We argue that a composition is secure when we can show that an equivalent single-language program is secure. This reasoning can be applied to noninterference, the standard notion of language-based security, as well as declassification, which is a weaker security guarantee necessary for practical uses. We introduce Security Completeness as the main technical tool to satisfy our framework requirements. Informally, a security-typed languages is security-complete if every secure and computable function can be implemented as a well-typed program in the language. We formally study security completeness and derive sufficient, and in some cases necessary, requirements for a language to be security-complete. A case study of three seminal languages from the literature investigates the three main paradigms of secure languages: imperative, functional and object-oriented languages. We show that, with reasonable assumptions, all case studies are security complete. To demonstrate the applicability of this framework, we completely show that a standard secure while language satisfies all necessary requirements of a composition host, and present an expressive, security-typed fragment of SQL for embedding. We finish the thesis with an investigation of dynamically loaded code. A special interpretation of the framework allows it to be used to lift guaranties to programs containing components that are incrementally loaded and verified. This has three benefits. First, incremental loading means a lower start-up time for programs, as the full program is not necessary to start executing. Second, only code that is really necessary for the current computation will be loaded. This results in a decreased bandwidth or time requirement for the application. Third and finally, incremental verification distributes the verification time over the runtime of the program. | |
| dc.description.department | Computer Science | |
| dc.format.extent | 230 pages | |
| dc.format.mimetype | application/pdf | |
| dc.identifier.uri | https://hdl.handle.net/20.500.12588/3457 | |
| dc.language | en | |
| dc.subject | Computer Security | |
| dc.subject | Language Composition | |
| dc.subject | Programming Languages | |
| dc.subject | Security-typed Languages | |
| dc.subject.classification | Computer science | |
| dc.title | A Framework for Composing Security-typed Languages | |
| dc.type | Thesis | |
| dc.type.dcmi | Text | |
| dcterms.accessRights | pq_closed | |
| thesis.degree.department | Computer Science | |
| thesis.degree.grantor | University of Texas at San Antonio | |
| thesis.degree.level | Doctoral | |
| thesis.degree.name | Doctor of Philosophy |
Files
Original bundle
1 - 1 of 1
No Thumbnail Available
- Name:
- Gampe_utsa_1283D_11207.pdf
- Size:
- 1.3 MB
- Format:
- Adobe Portable Document Format