{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/123144"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/123144","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"A framework for specifying and formally verifying application security policies","abstract":"One challenge of building software applications that handle sensitive information is ensuring that they meet certain security and privacy policies, which guide how the application should be written in order to satisfy particular security properties. Common examples of security policies include information-flow control and access control. In complex applications, which can be composed of many stateful components, it is hard to reason about all possible interactions and check that a policy is satisfied in every case. In this thesis, we present work on a new static-analysis framework in the Coq proof assistant to verify that implementations of applications meet their specified security policies, using proofs of indistinguishability of labeled transition systems. The primary goal of our framework is to be applicable to a wide variety of applications and policies, moreso than existing analysis tools. In addition to a formalization of applications and policies, we discuss some theorems to reduce manual proof effort and enable modular development. Finally, we apply our framework to some simple examples.","abstract_html":"One challenge of building software applications that handle sensitive information is ensuring that they meet certain security and privacy policies, which guide how the application should be written in order to satisfy particular security properties. Common examples of security policies include information-flow control and access control. In complex applications, which can be composed of many stateful components, it is hard to reason about all possible interactions and check that a policy is satisfied in every case. In this thesis, we present work on a new static-analysis framework in the Coq proof assistant to verify that implementations of applications meet their specified security policies, using proofs of indistinguishability of labeled transition systems. The primary goal of our framework is to be applicable to a wide variety of applications and policies, moreso than existing analysis tools. In addition to a formalization of applications and policies, we discuss some theorems to reduce manual proof effort and enable modular development. Finally, we apply our framework to some simple examples.","abstract_has_math":false,"creators":["Shao, Christopher,M. Eng.Massachusetts Institute of Technology."],"institution":"Massachusetts Institute of Technology","degree_name":"Master","degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","school":null,"contributors":[],"advisors":["Adam Chlipala."],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019","date_published":"2019","updated_at":"2026-07-22T22:21:04Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"rights":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/123144","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Adam Chlipala."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","EECS"]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Shao, Christopher,M. Eng.Massachusetts Institute of Technology."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2019-12-05T18:05:54Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2019-12-05T18:05:54Z"]},{"key":"dc:date.issued","label":"Date","values":["2019"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/123144"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2019","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 59-60)."]},{"key":"dc:description.abstract","label":"Abstract","values":["One challenge of building software applications that handle sensitive information is ensuring that they meet certain security and privacy policies, which guide how the application should be written in order to satisfy particular security properties. Common examples of security policies include information-flow control and access control. In complex applications, which can be composed of many stateful components, it is hard to reason about all possible interactions and check that a policy is satisfied in every case. In this thesis, we present work on a new static-analysis framework in the Coq proof assistant to verify that implementations of applications meet their specified security policies, using proofs of indistinguishability of labeled transition systems. The primary goal of our framework is to be applicable to a wide variety of applications and policies, moreso than existing analysis tools. In addition to a formalization of applications and policies, we discuss some theorems to reduce manual proof effort and enable modular development. Finally, we apply our framework to some simple examples."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M. Eng."]},{"key":"dc:title","label":"Title","values":["A framework for specifying and formally verifying application security policies"]}]}],"canonical_facts":{"dc:contributor.advisor":["Adam Chlipala."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","EECS"],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Shao, Christopher,M. Eng.Massachusetts Institute of Technology."],"dc:date.accessioned":["2019-12-05T18:05:54Z"],"dc:date.available":["2019-12-05T18:05:54Z"],"dc:date.issued":["2019"],"dc:description":["This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2019","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 59-60)."],"dc:description.abstract":["One challenge of building software applications that handle sensitive information is ensuring that they meet certain security and privacy policies, which guide how the application should be written in order to satisfy particular security properties. Common examples of security policies include information-flow control and access control. In complex applications, which can be composed of many stateful components, it is hard to reason about all possible interactions and check that a policy is satisfied in every case. In this thesis, we present work on a new static-analysis framework in the Coq proof assistant to verify that implementations of applications meet their specified security policies, using proofs of indistinguishability of labeled transition systems. The primary goal of our framework is to be applicable to a wide variety of applications and policies, moreso than existing analysis tools. In addition to a formalization of applications and policies, we discuss some theorems to reduce manual proof effort and enable modular development. Finally, we apply our framework to some simple examples."],"dc:description.degree":["M. Eng."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/123144"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["A framework for specifying and formally verifying application security policies"],"dc:type":["Thesis"],"thesis:degree_name":["Master"]},"updated_at":"2026-07-22T22:21:04Z"}