Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Dan Ghica

LFCS Seminar: Dan Ghica

— filed under:

Towards a system-level semantics

  • LFCS Seminar
When Jan 20, 2012
from 02:00 PM to 03:00 PM
Add event to calendar vCal

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
(Proponent) and its context (Opponent).  In general, the richer
the computational features a language has, the less constrained the
rules of the semantic game. In this talk 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
realizable 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.

(joint work with Nikos Tzevelekos, Queen Mary University, London)

Document Actions