상세정보
Export to Refworks부가기능
Semantics for Secure Software
상세 프로파일
| 자료유형 | 학위논문 |
|---|---|
| 서명/저자사항 | Semantics for Secure Software. |
| 개인저자 | Hirsch, Andrew Karl. |
| 단체저자명 | Cornell University. Computer Science. |
| 발행사항 | [S.l.]: Cornell University., 2019. |
| 발행사항 | Ann Arbor: ProQuest Dissertations & Theses, 2019. |
| 형태사항 | 231 p. |
| 기본자료 저록 | Dissertations Abstracts International 81-04B. Dissertation Abstract International |
| ISBN | 9781088379950 |
| 학위논문주기 | Thesis (Ph.D.)--Cornell University, 2019. |
| 일반주기 |
Source: Dissertations Abstracts International, Volume: 81-04, Section: B.
Includes supplementary digital materials. Advisor: Tate, Ross E. |
| 이용제한사항 | This item must not be sold to any third party vendors. |
| 요약 | In order to build machine-checked proven-secure software, we need formal security 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. |
| 일반주제명 | Computer science. |
| 언어 | 영어 |
| 바로가기 | 
: 이 자료의 원문은 한국교육학술정보원에서 제공합니다. |
