eCommons

 

Semantics for Secure Software

Other Titles

Abstract

In 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.

Journal / Series

Volume & Issue

Description

Supplemental file(s) description: Coq Code for FOCAL, Coq code for FLAFOL

Sponsorship

Date Issued

2019-08-30

Publisher

Keywords

authorization; Logic; Comonad; Flow-Limited Authorization; Monad; Computer science; Programming Languages

Location

Effective Date

Expiration Date

Sector

Employer

Union

Union Local

NAICS

Number of Workers

Committee Chair

Tate, Ross Everett

Committee Co-Chair

Committee Member

Kozen, Dexter Campbell
Shore, Richard A.
Morrisett, John Gregory

Degree Discipline

Computer Science

Degree Name

Ph.D., Computer Science

Degree Level

Doctor of Philosophy

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)

References

Link(s) to Reference(s)

Previously Published As

Government Document

ISBN

ISMN

ISSN

Other Identifiers

Rights

Attribution 4.0 International

Types

dissertation or thesis

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record