A system-level game semantics

Research output: Contribution to journalArticlepeer-review

Standard

A system-level game semantics. / Ghica, Dan R.; Tzevelekos, Nikos.

In: Electronic Notes in Theoretical Computer Science, Vol. 286, 24.09.2012, p. 191-211.

Research output: Contribution to journalArticlepeer-review

Harvard

APA

Vancouver

Author

Ghica, Dan R. ; Tzevelekos, Nikos. / A system-level game semantics. In: Electronic Notes in Theoretical Computer Science. 2012 ; Vol. 286. pp. 191-211.

Bibtex

@article{8e3a1fae8f7c41c89c46f8cef0234220,
title = "A system-level game semantics",
abstract = "Game semantics is a trace-like denotational semantics for programming languages where the notion of legal observable behaviour of a term is defined combinatorially, by means of rules of a game between the term (the Proponent) and its context (the Opponent). In general, the richer the computational features a language has the less constrained the rules of the semantic game. In this paper we consider the consequences of taking this relaxation of rules to the limit, by granting the Opponent omnipotence, that is, permission to play any move without combinatorial restrictions. However, we impose an epistemic restriction by not granting Opponent omniscience, so that Proponent can have undisclosed secret moves. We introduce a basic C-like programming language and we define such a semantic model for it. We argue that the resulting semantics is an appealingly simple combination of operational and game semantics and we show how certain traces explain system-level attacks, i.e. plausible attacks that are realisable outside of the programming language itself. We also show how allowing Proponent to have secrets ensures that some desirable equivalences in the programming language are preserved.",
keywords = "Game semantics, Omnipotent opponent, Omniscient opponent",
author = "Ghica, {Dan R.} and Nikos Tzevelekos",
year = "2012",
month = sep,
day = "24",
doi = "10.1016/j.entcs.2012.08.013",
language = "English",
volume = "286",
pages = "191--211",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

RIS

TY - JOUR

T1 - A system-level game semantics

AU - Ghica, Dan R.

AU - Tzevelekos, Nikos

PY - 2012/9/24

Y1 - 2012/9/24

N2 - Game semantics is a trace-like denotational semantics for programming languages where the notion of legal observable behaviour of a term is defined combinatorially, by means of rules of a game between the term (the Proponent) and its context (the Opponent). In general, the richer the computational features a language has the less constrained the rules of the semantic game. In this paper we consider the consequences of taking this relaxation of rules to the limit, by granting the Opponent omnipotence, that is, permission to play any move without combinatorial restrictions. However, we impose an epistemic restriction by not granting Opponent omniscience, so that Proponent can have undisclosed secret moves. We introduce a basic C-like programming language and we define such a semantic model for it. We argue that the resulting semantics is an appealingly simple combination of operational and game semantics and we show how certain traces explain system-level attacks, i.e. plausible attacks that are realisable outside of the programming language itself. We also show how allowing Proponent to have secrets ensures that some desirable equivalences in the programming language are preserved.

AB - Game semantics is a trace-like denotational semantics for programming languages where the notion of legal observable behaviour of a term is defined combinatorially, by means of rules of a game between the term (the Proponent) and its context (the Opponent). In general, the richer the computational features a language has the less constrained the rules of the semantic game. In this paper we consider the consequences of taking this relaxation of rules to the limit, by granting the Opponent omnipotence, that is, permission to play any move without combinatorial restrictions. However, we impose an epistemic restriction by not granting Opponent omniscience, so that Proponent can have undisclosed secret moves. We introduce a basic C-like programming language and we define such a semantic model for it. We argue that the resulting semantics is an appealingly simple combination of operational and game semantics and we show how certain traces explain system-level attacks, i.e. plausible attacks that are realisable outside of the programming language itself. We also show how allowing Proponent to have secrets ensures that some desirable equivalences in the programming language are preserved.

KW - Game semantics

KW - Omnipotent opponent

KW - Omniscient opponent

UR - http://www.scopus.com/inward/record.url?scp=84879245003&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2012.08.013

DO - 10.1016/j.entcs.2012.08.013

M3 - Article

AN - SCOPUS:84879245003

VL - 286

SP - 191

EP - 211

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -