系统级语义
A System-Level Semantics
摘要：
博弈语义是一种用于程序设计语言的类迹指称语义，其中术语的合法可观察行为的概念通过术语（“Proponent”）及其上下文（“Opponent”）之间的博弈规则来组合地定义。一般来说，一种语言的计算特性越丰富，语义游戏规则的约束就越少。在本文中，我们考虑的后果，采取这种放宽规则的限制，通过授予对手的omnipulations，也就是说，允许发挥任何移动没有组合的限制。然而，我们施加了一个认识上的限制，不授予对手全知，使支持者可以有未公开的秘密行动。我们介绍了一个基本的C-样的程序设计语言，我们定义这样一个语义模型，我们认为，由此产生的语义是一个有吸引力的简单组合的操作和游戏语义，我们展示了某些痕迹如何解释系统级的攻击，即似是而非的攻击是可实现的程序设计语言本身之外。我们还展示了如何允许Proponent有秘密，确保在程序设计语言的一些理想的等价物被保存。
英文摘要：
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 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
