Publications by Kai Engelhardt (~) in reverse chronological order

[1]

Toby Murray, Robert Sison, and ~. Covern: A logic for compositional verification of information flow control. In Frank Piessens and Matthew Smith, editors, IEEE European Symposium on Security and Privacy (EuroS&P), April 2018. [ bib | DOI | .pdf ]

Shared memory concurrency is pervasive in modern programming, including in systems that must protect highly sensitive data. Recently, verification has finally emerged as a practical tool for proving interesting security properties of real programs, particularly information flow control (IFC) security. Yet there remain no general logics for verifying IFC security of shared-memory concurrent programs. In this paper we present the first such logic, Covern (Compositional Verification of Noninterference) and its proof of soundness via a new generic framework for general rely-guarantee IFC reasoning. We apply Covern to model and verify the security-critical software functionality of the Cross Domain Desktop Compositor, an embedded device that facilitates simultaneous and intuitive user interaction with multiple classified networks while preventing leakage between them. To our knowledge this is the first foundational, machine-checked proof of IFC security for a non-trivial shared-memory concurrent program in the literature.

[2]

~. A better composition operator for quantitative information flow analyses. In Simon N. Foley, Dieter Gollmann, and Einar Snekkenes, editors, Computer Security – ESORICS 2017, 22nd European Symposium on Research in Computer Security Oslo, Norway, September 11–15, 2017, Proceedings, Part I, volume 10492 of LNCS, pages 446–463, Oslo, Norway, September 11–13 2017. Springer-Verlag. [ bib | DOI ]

Given a description of the quantitative information flow (qif) for components, how can we determine the qif of a system composed from components? We explore this fundamental question mathematically and provide an answer based on a new composition operator. We investigate its properties and prove that it generalises existing composition operators. We illustrate the results with a fresh look on Chaum's dining cryptographers. We show that the new operator enjoys various convenient algebraic properties and that it is well-behaved under composition refinement.

[3]

Peter Gammie, Antony L. Hosking, and ~. Relaxing safely: Verified on-the-fly garbage collection for x86-TSO. In Steve Blackburn, editor, PLDI 2015, 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation, pages 99–109, Portland, OR, May 2015. ACM. [ bib ]

We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. The abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward.

[4]

Peter Gammie, Tony Hosking, and ~. Relaxing safely: Verified on-the-fly garbage collection for x86-TSO. Archive of Formal Proofs, 2015. [ bib | http ]

We use ConcurrentIMP to model Schism, a state-of-the-art real-time garbage collection scheme for weak memory, and show that it is safe on x86-TSO. This development accompanies the PLDI 2015 paper of the same name.

[5]

~, Ron van der Meyden, and Chenyi Zhang. Intransitive noninterference in nondeterministic systems. In Ting Yu, George Danezis, and Virgil D. Gligor, editors, 19th ACM Conference on Computer and Communications Security. ACM, October 2012. [ bib ]

This paper addresses the question of how TA-security, a semantics for intransitive information-flow policies in deterministic systems, can be generalized to nondeterministic systems. Various definitions are proposed, including definitions that state that the system enforces as much of the policy as possible in the context of attacks in which groups of agents collude by sharing information through channels that lie outside the system. Relationships between the various definitions proposed are characterized, and an unwinding-based proof technique is developed. Finally, it is shown that on a specific class of systems, access control systems with local non-determinism, the strongest definition can be verified by checking a simple static property.

[6]

Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, ~, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an operating-system kernel. Communications of the ACM, 53(6):107–115, June 2010. [ bib | DOI ]

We report on the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, hardware, and boot code. seL4 is a third-generation microkernel of L4 provenance, comprising 8,700 lines of C and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels. We prove that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as that the kernel will never crash, and it will never perform an unsafe operation. It also implies much more: we can predict precisely how the kernel will behave in every possible situation.

[7]

~. A note on noninterference in the presence of colluding adversaries (preliminary report). Presented at Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS'10, March 27–28 2010. [ bib ]

Whether adversaries can glean information from a distributed system in a formal sense hinges on the definition of such a system and what can be observed by those agents. In the presence of colluding adversaries, the standard definition of non-interference by Goguen and Meseguer and its many variants proposed in the literature fail in a very intuitive sense to capture a simple collusion attack. The crucial difference between what is modelled in those definitions and what we argue needs to be modelled is that teams can observe pomsets as Plotkin and Pratt stated. In this note we expose what goes wrong in the known approaches and explain how to fix the problem.

[8]

~ and Ralf Huuck. Smaller abstractions for ∀CTL^* without Next. In Dennis Dams, Ulrich Hannemann, and Martin Steffen, editors, Concurrency, Compositionality, and Correctness: Essays in Honor of Willem-Paul de Roever, volume 5930 of LNCS, pages 250–259. Springer-Verlag, 2010. [ bib ]

The success of applying model-checking to large systems depends crucially on the choice of good abstractions. In this work we present an approach for constructing abstractions when checking next-free universal CTL^* properties. It is known that functional abstractions are safe and that next-free universal CTL^* is insensitive to finite stuttering. We exploit these results by introducing a safe next-free abstraction that is typically smaller than the usual functional one while at the same time more precise, i.e., it has less spurious counter-examples.

[9]

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, ~, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), pages 207–220, Big Sky, MT, USA, October 2009. ACM. [ bib | PDF ]

[10]

~ and Yoram Moses. Causing communication closure: safe program composition with reliable non-FIFO channels. Distributed Computing, 22(2):73–91, October 2009. [ bib | DOI ]

A rigorous framework for analyzing safe composition of distributed programs is presented. It facilitates specifying notions of safe sequential execution of distributed programs in various models of communication. A notion of sealing is defined, where if a program P is immediately followed by a program Q that seals P then P will be communication-closed—it will execute as if it runs in isolation. None of its send or receive actions will match or interact with actions outside P. The applicability of sealing is illustrated by a study of program composition when communication is reliable but not necessarily FIFO . In this model, special care must be taken to ensure that messages do not accidentally overtake one another in the composed program. In this model no program that sends or receives messages can be composed automatically with arbitrary programs without jeopardizing their intended behavior. Safety of composition becomes context-sensitive and new tools are needed for ensuring it. The investigation of sealing in this model reveals a novel connection between Lamport causality and safe composition. A characterization of sealable programs is given, as well as efficient algorithms for testing if Q seals P and for constructing a seal for a class of straight-line programs. It is shown that every sealable program can be sealed using O(n) messages. In fact, 3n-4 messages are necessary and sufficient in the worst case, despite the fact that a sealable program may be open to interference on Ω(n²) channels.

[11]

~ and Yoram Moses. Single-bit messages are insufficient for data link over duplicating channels. Information Processing Letters, 107(6):235–239, August 2008. [ bib | DOI ]

Ideal communication channels in asynchronous systems are reliable, deliver messages in FIFO order, and do not deliver spurious or duplicate messages. A message vocabulary of size two (i.e., single-bit messages) suffices to encode and transmit messages of arbitrary finite length over such channels. This note proves that single-bit messages are insufficient once channels potentially deliver duplicate messages. In particular, it is shown that no protocol allows the sender to notify the receiver which of three values it holds, over a bidirectional, reliable, FIFO channel that may duplicate messages. This implies that messages must encode some additional control information, e.g., in the form of headers or tags.

[12]

~, Peter Gammie, and Ron van der Meyden. Model checking knowledge and linear time: PSPACE cases. In Sergei N. Artëmov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, NY, USA, June 4-7, 2007, Proceedings, volume 4514 of LNCS, pages 195–211. Springer-Verlag, June 2007. [ bib ]

We present a general algorithm scheme for model checking logics of knowledge, common knowledge and linear time, based on simulations to a class of structures that capture the way that agents update their knowledge. We show that the scheme leads to PSPACE implementations of model checking the logic of knowledge and linear time in several special cases: perfect recall systems with a single agent or in which all communication is by synchronous broadcast, and systems in which knowledge is interpreted using either the agents' current observation only or its current observation and clock value. In all these results, common knowledge operators may be included in the language. Matching lower bounds are provided, and it is shown that although the complexity bound matches the PSPACE complexity of the linear time temporal logic LTL, as a function of the model size the problems considered have a higher complexity than LTL.

[13]

~ and Yoram Moses. Single-bit messages are insufficient in the presence of duplication. In Ajit Pal, Ajay Kshemkalyani, Rajeev Kumar, and Arobinda Gupta, editors, 7th International Workshop on Distributed Computing IWDC 2005, volume 3741 of LNCS, pages 25–31. Springer-Verlag, December 27–30 2005. [ bib | DOI ]

Ideal communication channels in asynchronous systems are reliable, deliver messages in FIFO order, and do not deliver spurious or duplicate messages. A message vocabulary of size two (i.e., single-bit messages) suffices to encode and transmit messages of arbitrary finite length over such channels. This note proves that single-bit messages are insufficient once channels potentially deliver duplicate messages. In particular, it is shown that no protocol allows the sender to notify the receiver which of three values it holds, over a bidirectional, reliable, FIFO channel that may duplicate messages. This implies that messages must encode some additional control information, e.g., in the form of headers or tags.

[14]

~ and Yoram Moses. Safe composition of distributed programs communicating over order-preserving imperfect channels. In Ajit Pal, Ajay Kshemkalyani, Rajeev Kumar, and Arobinda Gupta, editors, 7th International Workshop on Distributed Computing IWDC 2005, volume 3741 of LNCS, pages 32–44. Springer-Verlag, December 27–30 2005. [ bib | DOI ]

The fundamental question considered in this paper is when program Q, if executed immediately after program P, is guaranteed not to interfere with P and be safe from interference by P. If a message sent by one of these programs is received by the other, it may affect and modify the other's execution. The notion of communication-closed layers (CCLs) introduced by Elrad and Francez in 1982 is a useful tool for studying such interference. CCLs have been considered mainly in the context of reliable FIFO channels (without duplication), where one can design programs layers that do not interfere with any other layer. When channels are less than perfect such programs are no longer feasible. The absence of interference between layers becomes context-dependent. In this paper we study the impact of message duplication and loss on the safety on the safety of layer composition. Using a communication phase operator, the fits after relation among programs is defined. If program Q fits after P then P and Q will not interfere with each other in executions of P*Q. For programs P and Q in a natural class of programs we outline efficient algorithms for the following: (1) deciding whether Q fits after P; (2) deciding whether Q seals P, meaning that Q fits after P and no following program can communicate with P; and (3) constructing a separator S that both fits after P and satisfies that Q fits after P*S.

[15]

~ and Yoram Moses. Causing communication closure: Safe program composition with non-FIFO channels. In Pierre Fraigniaud, editor, DISC 2005 19th International Symposium on Distributed Computing, volume 3724 of LNCS, pages 229–243. Springer-Verlag, September 26–29 2005. [ bib | DOI ]

A semantic framework for analyzing safe composition of distributed programs is presented. Its applicability is illustrated by a study of program composition when communication is reliable but not necessarily FIFO . In this model, special care must be taken to ensure that messages do not accidentally overtake one another in the composed program. We show that barriers do not exist in this model. Indeed, no program that sends or receives messages can automatically be composed with arbitrary programs without jeopardizing their intended behavior. Safety of composition becomes context-sensitive and new tools are needed for ensuring it. A notion of sealing is defined, where if a program P is immediately followed by a program Q that seals P then P will be communication-closed—it will execute as if it runs in isolation. The investigation of sealing in this model reveals a novel connection between Lamport causality and safe composition. A characterization of sealable programs is given, as well as efficient algorithms for testing if Q seals P and for constructing a seal for a significant class of programs. It is shown that every sealable program that is open to interference on O(n²) channels can be sealed using O(n) messages.

[16]

~, Ron van der Meyden, and Kaile Su. Modal logics with a linear hierarchy of local propositional quantifiers. In Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev, editors, Advances in Modal Logic, volume 4, pages 9–30. King's College London Publications, 2003. [ bib ]

Local propositions arise in the context of the semantics for logics of knowledge in multi-agent systems. A proposition is local to an agent when it depends only on that agent's local state. We consider a logic, LLP, that extends S5, the modal logic of necessity (in which the modality refers to truth at all worlds) by adding a quantifier ranging over the set of all propositions and, for each agent, a propositional quantifier ranging over the agent's local propositions. LLP is able to express a large variety of epistemic modalities, including knowledge, common knowledge and distributed knowledge. However, this expressiveness comes at a cost: the logic is equivalent to second order predicate logic when two independent agents are present [22], hence undecidable and not axiomatizable. This paper identifies a class of multi-agent S5 structures, hierarchical structures, in which the agents' information has the structure of a linear hierarchy. All systems with just a single agent are hierarchical. It is shown that LLP becomes decidable with respect to hierarchical systems. The main result of the paper is the completeness of an axiomatization for the hierarchical case.

[17]

~, Ron van der Meyden, and Kaile Su. Modal logics with a linear hierarchy of local propositional quantifiers (preliminary version). In Nobu-Yuki Suzuki and Frank Wolter, editors, Advances in Modal Logic 2002 (AiML), pages 63–76. Institut de recherche en informatique de Toulouse, Université Paul Sabatier, September 2002. [ bib ]

[18]

~. Towards a refinement theory that supports reasoning about knowledge and time for multiple agents (work in progress). In John Derrick, Eerke Boiten, Jim Woodcock, and Joakim von Wright, editors, REFINE '02 An FME sponsored Refinement Workshop in collaboration with BCS FACS, page 23. Computing Laboratory, University of Kent at Canterbury, UK, July 2002. Preliminary Proceedings. [ bib ]

[19]

~, Ron van der Meyden, and Yoram Moses. A refinement theory that supports reasoning about knowledge and time for synchronous agents. In Robert Nieuwenhuis and Andrei Voronkov, editors, Proceedings LPAR 2001, volume 2250 of LNAI, pages 125–141. Springer-Verlag, December 2001. [ bib | DOI ]

An expressive semantic framework for program refinement that supports both temporal reasoning and reasoning about the knowledge of multiple agents is developed. The refinement calculus owes the cleanliness of its decomposition rules for all programming language constructs and the relative simplicity of its semantic model to a rigid synchrony assumption which requires all agents and the environment to proceed in lockstep. The new features of the calculus are illustrated in a derivation of the two-phase-commit protocol.

[20]

~, Ron van der Meyden, and Yoram Moses. A program refinement framework supporting reasoning about knowledge and time. In Jerzy Tiuryn, editor, Foundations of Software Science and Computation Structures, volume 1784 of LNCS, pages 114–129. Springer-Verlag, March 2000. [ bib ]

This paper develops a highly expressive semantic framework for program refinement that supports both temporal reasoning and reasoning about the knowledge of a single agent. The framework generalizes a previously developed temporal refinement framework by amalgamating it with a logic of quantified local propositions, a generalization of the logic of knowledge. The combined framework provides a formal setting for development of knowledge-based programs, and addresses two problems of existing theories of such programs: lack of compositionality and the fact that such programs often have only implementations of high computational complexity. Use of the framework is illustrated by a control theoretic example concerning a robot operating with an imprecise position sensor.

[21]

~ and Ron van der Meyden. Modal logics with a hierarchy of local propositional quantifiers (extended abstract). In Thomas Eiter, Georg Gottlob, Victor Marek, and Jeffrey Remmel, editors, Proceedings of the FLoC'99 Workshop Complexity-Theoretic and Recursion-Theoretic Methods in Databases and Artificial Intelligence, pages 81–90, July 6 1999. [ bib ]

[22]

~, Ron van der Meyden, and Yoram Moses. Knowledge and the logic of local propositions. In Itzhak Gilboa, editor, Theoretical Aspects of Rationality and Knowledge, Proceedings of the Seventh Conference (TARK 1998), pages 29–41. Morgan Kaufmann, July 1998. [ bib ]

An agent's limited view of the state of a distributed system may render globally different situations indistinguishable. A proposition is local for this agent whenever his view suffices to decide this proposition. Motivated by a framework for the development of distributed programs from knowledge-based specifications, we introduce a modal logic of local propositions, in which it is possible to quantify over such propositions. We show that this logic is able to represent a rich set of epistemic notions. Under the usual strong semantics, this logic is not recursively axiomatizable, however. We show that by weakening the semantics of quantification, it is possible to obtain a logic that is axiomatizable and is still able to express interesting epistemic notions.

[23]

Willem-Paul de Roever and ~. Data Refinement: Model-Oriented Proof Methods and their Comparison. Number 47 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998. Paperback re-issue 2009. Errata at https://kai-e.github.io/pubs/dRE1998/errata.pdf. [ bib ]

[24]

~. Model-Oriented Data Refinement. PhD thesis, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, July 1997. [ bib ]

The goal of this thesis is to provide a comprehensive and systematic introduction to the important and highly applicable method of data refinement and proving simulation. We concentrate in the first part on the general principles needed to prove data refinement correct, and begin with an explanation of the fundamental notions, showing that data refinement proofs reduce to proving simulation. The topics of Hoare Logic and the Refinement Calculus are then introduced and a general theory of simulations is developed and related to them. Accessibility and comprehension are emphasised in order to guide newcomers to the area. The second part of this thesis contains a detailed survey of important methods in this area, such as VDM, and the methods due to Abadi & Lamport, Hehner, Lynch and Reynolds, and Back's refinement calculus. All these methods are carefully analysed, and shown to be either incomplete, with counterexamples to their application, or to be always applicable whenever data refinement holds. This is shown by proving, for the first time, that all of them can be described and analysed in terms of two simple notions: forward and backward simulation.

[25]

~ and Willem-Paul de Roever. New win[e/d] for old bags. In John Tromp, editor, A dynamic and quick intellect, Paul Vitányi 25 years @ CWI, pages 59–66. CWI, Amsterdam, November 1996. [ bib ]

[26]

~ and Willem-Paul de Roever. Simulation of specification statements in Hoare logic. In Wojciech Penczek and Andrzej Szalas, editors, Mathematical Foundations of Computer Science 1996, 21st International Symposium, MFCS '96, Cracow, Poland, Proceedings, volume 1113 of LNCS, pages 324–335. Springer-Verlag, September 1996. [ bib ]

Data refinement is a powerful technique to derive implementations in terms of low-level data structures like bytes from specification in terms of high-level data structures like queues. The higher level operations need not be coded as ordinary programs; it is more convenient to introduce specification statements to the programming language and use them instead of actual code. Specification statements represent the maximal program satisfying a given Hoare-triple. Sound and (relatively) complete simulation techniques allow for proving data refinement by local arguments. A major challenge for simulation consists of expressing the weakest lower level specification simulating a given higher level specification w.r.t. a given relation between these two levels of abstraction. We present solutions to this challenge for upward and downward simulation in both partial and total correctness frameworks, thus reducing the task of proving data refinement to proving validity of certain Hoare-triples.

[27]

~ and Willem-Paul de Roever. Towards a practitioners' approach to Abadi and Lamport's method. Formal Aspects of Computing, 7(5):550–575, 1995. [ bib ]

Our own basic intuitions are presented when introducing the method developed by Abadi and Lamport in [?] for proving refinement between specifications of nondeterministic programs correct to people unacquainted with it. The example we use to illustrate this method is a nontrivial communication protocol that provides a mechanism analogous to message passing between migrating processes within a fixed finite network of nodes due to Kleinman, Moscowitz, Pnueli, and Shapiro [?]. Especially the cruel last step of a three step refinement proof of that protocol gives rise to a deeper understanding of, and some small enhancements to, Abadi and Lamport's 1988 method.

[28]

~ and Willem-Paul de Roever. Generalizing Abadi & Lamport's method to solve a problem posed by A. Pnueli. In Jim C.P. Woodcock and Peter Gorm Larsen, editors, FME '93: Industrial-Strength Formal Methods, volume 670 of LNCS, pages 294–313. Springer-Verlag, April 1993. [ bib ]

[29]

~. Verallgemeinerungen der Methode von Abadi und Lamport um ein von A. Pnueli gestelltes Problem zu lösen. Master's thesis, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, January 1993. [ bib ]

By adding a new technique and a simple proof strategy to Abadi & Lamport's 1988 method [?] for proving refinement between specifications of distributed programs correct, the inherent limitation of their method, occurring when the abstract level of specification features so-called infinite invisible nondeterminism or internal discontinuity, can be sometimes overcome. This technique is applied to the cruel last step of a three step correctness proof for an algorithm for communication between migrating processes within a finite network due to Kleinman, Moscowitz, Pnueli & Shapiro [?].