Macquarie University
Browse
01whole.pdf (1.03 MB)

Game semantics for non-deterministic security

Download (1.03 MB)
thesis
posted on 2022-11-03, 01:02 authored by Chris Chen

The Shadow Semantics [47, 48, 50] models secure refinement, i.e. preservation of privacy under adversarial inference attacks. Previous work has given a structural (affirmative) account of secure refinement and its primitives, with some progress towards a testing (refutational) account. At the same time, (mutable-state) programs in the Shadow Se- mantics can be modelled readily as functions, but lack ‘healthiness conditions’ [11, 53] to characterise the underlying properties of information flow. Our contributions are twofold. First, we provide a testing (refutational) account of secure refinement as a game semantics for a certain adversarial game. In so doing we develop and characterise the ‘predicates’ first proposed in [47]. This game semantics provides an interpretation of the Shadow Semantics in terms of a security threat model. Its structure hints at connections to the quantitative analogue, qif [4]. Second, we give an order-theoretic account of the Shadow Semantics, adapting a recently developed framework from category theory [27, 32]. The Shadow Semantics’s main primitives are shown to arise from an adjunction on a certain ‘lax’ category. This account gives an alternative ‘first-principles’ derivation of the Shadow Semantics, and hints at future foundational work in the category theory of inference attacks.

History

Table of Contents

1. Introduction -- 2. Preliminaries and notation -- 3. Orders and refinement -- 4. The Shadow Semantics -- 5. Lattices and P+-algebras -- 6. Attacks and predicates -- 7. Shadow semantics – game model -- 8. Healthiness -- 9. Hyper-shadows and categorical duality -- 10. Significance and further work -- Bibliography

Notes

A thesis submitted to Macquarie University for the degree of Master of Research

Awarding Institution

Macquarie University

Degree Type

Thesis MRes

Degree

Thesis (MRes), Macquarie University, Faculty of Science and Engineering, Department of Computing, 2022

Department, Centre or School

Department of Computing

Year of Award

2022

Principal Supervisor

Annabelle McIver

Additional Supervisor 1

Richard Garner

Rights

Copyright: The Author Copyright disclaimer: https://www.mq.edu.au/copyright-disclaimer

Language

English

Extent

65 pages

Usage metrics

    Macquarie University Theses

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC