Show simple item record

dc.contributor.authorHirsch, Andrew Karl
dc.date.accessioned2019-10-15T16:49:13Z
dc.date.available2019-10-15T16:49:13Z
dc.date.issued2019-08-30
dc.identifier.otherHirsch_cornellgrad_0058F_11681
dc.identifier.otherhttp://dissertations.umi.com/cornellgrad:11681
dc.identifier.otherbibid: 11050625
dc.identifier.urihttps://hdl.handle.net/1813/67641
dc.descriptionSupplemental file(s) description: Coq Code for FOCAL, Coq code for FLAFOL
dc.description.abstractIn order to build machine-checked proven-secure software, we need formal se curity policies that express what it means to be “secure.” We must then show that the semantics of our software matches the semantics of those policies. This requires formal semantics for both programs and policies. In this dissertation, we explore the semantics of effectful programs and the semantics of authorization policies. The most well-known class of effects are those that can be given semantics via a monad, though current research also focuses on those that can be given a semantics via a comonad. We compare three methods for combining these two popular options: one method requires extra semantic structure, whereas the other methods can be applied to any monadic and comonadic effects. If the extra semantic structure needed for the first method exists then the three semantics are equivalent. Otherwise, we show that the two remaining semantics correspond to strict and lazy interpretations of the effects. On the other side, we use authorization logics to express authorization policies. Authorization logics can be given semantics using either models or a proof system. We build a model theory for an authorization logic that more-closely expresses how authorization logics are used by systems than traditional models. We also build a proof system for an authorization logic that ensures that proofs of authorization respect information-security policies.
dc.language.isoen_US
dc.rightsAttribution 4.0 International
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.subjectauthorization
dc.subjectLogic
dc.subjectComonad
dc.subjectFlow-Limited Authorization
dc.subjectMonad
dc.subjectComputer science
dc.subjectProgramming Languages
dc.titleSemantics for Secure Software
dc.typedissertation or thesis
thesis.degree.disciplineComputer Science
thesis.degree.grantorCornell University
thesis.degree.levelDoctor of Philosophy
thesis.degree.namePh.D., Computer Science
dc.contributor.chairTate, Ross Everett
dc.contributor.committeeMemberKozen, Dexter Campbell
dc.contributor.committeeMemberShore, Richard A.
dc.contributor.committeeMemberMorrisett, John Gregory
dcterms.licensehttps://hdl.handle.net/1813/59810
dc.identifier.doihttps://doi.org/10.7298/6grg-xc95


Files in this item

Thumbnail
Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Except where otherwise noted, this item's license is described as Attribution 4.0 International

Statistics