Giving Semantics to Program-Counter Labels via Secure Effects
| Autor: | Andrew K. Hirsch, Ethan Cecchetti |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Cryptography and Security Computer science Semantics (computer science) Context (language use) D.4.6 F.3.2 0102 computer and information sciences 02 engineering and technology Type (model theory) Mathematical proof computer.software_genre 01 natural sciences Program counter 0202 electrical engineering electronic engineering information engineering Safety Risk Reliability and Quality Control (linguistics) Computer Science - Programming Languages Programming language 020207 software engineering 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Core (graph theory) State (computer science) Cryptography and Security (cs.CR) computer Software Programming Languages (cs.PL) |
| Popis: | Type systems designed for information-flow control commonly use a program-counter label to track the sensitivity of the context and rule out data leakage arising from effectful computation in a sensitive context. Currently, type-system designers reason about this label informally except in security proofs, where they use ad-hoc techniques. We develop a framework based on monadic semantics for effects to give semantics to program-counter labels. This framework leads to three results about program-counter labels. First, we develop a new proof technique for noninterference, the core security theorem for information-flow control in effectful languages. Second, we unify notions of security for different types of effects, including state, exceptions, and nontermination. Finally, we formalize the folklore that program-counter labels are a lower bound on effects. We show that, while not universally true, this folklore has a good semantic foundation. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|