On the Complexity of Pointer Arithmetic in Separation Logic.

Kanovich Max; Brotherston James

Book chapter

On the Complexity of Pointer Arithmetic in Separation Logic.

P. 329-349.

Kanovich M., Brotherston J.

We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study an extension of the points-to fragment of symbolic-heap separation logic with sets of simple “difference constraints” of the form x≤y+k

, where x and y are pointer variables and k is an integer offset. This extension can be considered a practically minimal language for separation logic with pointer arithmetic.

Most significantly, we find that, even for this minimal language, polynomial-time decidability is already impossible: satisfiability becomes NP

-complete, while quantifier-free entailment becomes coNP-complete and quantified entailment becomes ΠP2-complete (where ΠP2

is the second class in the polynomial-time hierarchy).

However, the language does satisfy the small model property, meaning that any satisfiable formula has a model, and any invalid entailment has a countermodel, of polynomial size, whereas this property fails when richer forms of arithmetical constraints are permitted.

Language: English

Keywords: computer science Computer Science Applications computer science logic

In book

Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings. Lecture Notes in Computer Science 11275, Springer 2018, ISBN 978-3-030-02767-4

Edited by: S. R. Sukyoung Ryu:. Netherlands: Springer, 2018.

Undecidability of Propositional Separation Logic and Its Neighbours

Brotherston J., Kanovich M. Journal of the ACM. 2014. Vol. 61. No. 2. P. 14:1-14:43.

In this article, we investigate the logical structure of memory models of theoretical and practical interest. Our main interest is in “the logic behind a fixed memory model”, rather than in “a model of any kind behind a given logical system”. As an effective language for reasoning about such memory models, we use the formalism of separation logic. Our main result is that for any concrete choice of heap-like memory model, validity in that model is undecidable even for purely propositional formulas in this language.

The main novelty of our approach to the problem is that we focus on validity in specific, concrete memory models, as opposed to validity in general classes of models.

Besides its intrinsic technical interest, this result also provides new insights into the nature of their decidable fragments. In particular, we show that, in order to obtain such decidable fragments, either the formula language must be severely restricted or the valuations of propositional variables must be constrained.

In addition, we show that a number of propositional systems that approximate separation logic are undecidable as well. In particular, this resolves the open problems of decidability for Boolean BI and Classical BI.

Moreover, we provide one of the simplest undecidable propositional systems currently known in the literature, called “Minimal Boolean BI”, by combining the purely positive implication-conjunction fragment of Boolean logic with the laws of multiplicative *-conjunction, its unit and its adjoint implication, originally provided by intuitionistic multiplicative linear logic. Each of these two components is individually decidable: the implication-conjunction fragment of Boolean logic is co-NP-complete, and intuitionistic multiplicative linear logic is NP-complete.

All of our undecidability results are obtained by means of a direct encoding of Minsky machines.

Key Words and Phrases: Separation logic, undecidability, memory models, bunched logic

Added: Mar 23, 2015

Foundations for Decision Problems in Separation Logic with General Inductive Predicates

Antonopoulos T., Gorogiannis N., Haase C. et al. In bk.: Lecture Notes in Computer Science. 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Berlin: Springer, 2014. Ch. 27. P. 411-425.

We establish foundational results on the computational complexity of deciding entailment in Separation Logic with general inductive predicates whose underlying base language allows for pure formulas, pointers and existentially quantified variables. We show that entailment is in general undecidable, and ExpTime-hard in a fragment recently shown to be decidable by Iosif et al. Moreover, entailment in the base language is PI_2^p complete, the upper bound even holds in the presence of list predicates. We additionally show that entailment in essentially any fragment of Separation Logic allowing for general inductive predicates is intractable even when strong syntactic restrictions are imposed.

Added: Mar 24, 2015

Bounded memory Dolev-Yao adversaries in collaborative systems

Kanovich M., Ban Kirigin T., Nigam V. et al. Information and Computation. 2014. No. 238. P. 233-261.

In a collaborative system, the agents collaborate to achieve a common goal, but they are not willing to share some sensitive private information.

The question is how much damage can be done by a malicious participant sitting inside the system.

We assume that all the participants (including internal adversaries) have bounded memory – at any moment, they can store only a fixed number of messages of a fixed size. The Dolev–Yao adversaries can compose, decompose, eavesdrop, and intercept messages, and create fresh values (nonces), but within their bounded memory.

We prove that the secrecy problem is PSPACE-complete in the bounded memory model where all actions are balanced and a potentially infinite number of the nonce updates is allowed.

We also show that the well-known security protocol anomalies (starting from the Lowe attack to the Needham–Schroeder protocol) can be rephrased within the bounded memory paradigm with the explicit memory bounds.

Added: Mar 23, 2015

Linear logic with idempotent exponential modalities: a note

Sergey Slavnov. arxiv.org. math. Cornell University, 2014

In this note we discuss a variant of linear logic with idempotent exponential modalities. We propose a sequent calculus system and discuss its semantics. We also give a concrete relational model for this calculus.

Added: Dec 23, 2015

Bracket Induction for Lambek Calculus with Bracket Modalities

Kuznetsov S., Kanovich M., Scedrov A. In bk.: International Conference on Formal Grammar FG 2018: Formal Grammar 2018. Netherlands: Springer, 2018. P. 84-101.

Abstract

Relativisation involves dependencies which, although unbounded, are constrained with respect to certain island domains. The Lambek calculus L can provide a very rudimentary account of relativisation limited to unbounded peripheral extraction; the Lambek calculus with bracket modalities Lb can further condition this account according to island domains. However in naïve parsing/theorem-proving by backward chaining sequent proof search for Lb the bracketed island domains, which can be indefinitely nested, have to be specified in the linguistic input. In realistic parsing word order is given but such hierarchical bracketing structure cannot be assumed to be given. In this paper we show how parsing can be realised which induces the bracketing structure in backward chaining sequent proof search with Lb.

Added: Dec 5, 2018

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Edited by: J. Wiedermann, A. Tjoa, S. Biffl et al. Vol. 10706. Springer, 2018.

Added: Mar 5, 2018

Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

NY: ACM, 2014.

This volume contains the proceedings of the Joint Meeting of the Twenty-Third Annual EACSL Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/ IEEE Symposium on Logic in Computer Science (LICS). CSL is the annual meeting of the European Association for Computer Science Logic (EACSL) intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. LICS is an annual international forum on theoretical and practical topics in computer science that relate to logic. Every 3--4 years, LICS has been part of the Federated Logic Conference (FLoC). Given that FLoC was to be held as part of the Vienna Summer of Logic (VSL) during July 2014, the organizers of CSL and LICS have chosen to merge the 2014 editions of these meetings into a single event within FLoC and VSL. Thus, in 2014, the joint meeting had one program committee, one program, and one proceedings.

Added: Oct 20, 2014

Bounded Memory Protocols and Progressing Collaborative Systems

Kanovich M., Ban Kirigin T., Nigam V. et al. In bk.: Lecture Notes in Computer Science. Computer Security – ESORICS 2013 18th European Symposium on Research in Computer Security, Egham, UK, September 9-13, 2013. Proceedings. Berlin: Springer, 2013. Ch. 18. P. 309-326.

It is well-known that the Dolev-Yao adversary is a powerful adversary. Besides acting as the network, intercepting, sending, and composing messages, he can remember as much information as he needs. That is, his memory is unbounded.

We recently proposed a weaker Dolev-Yao like adversary, which also acts as the network, but whose memory is bounded. We showed that this Bounded Memory Dolev-Yao adversary, when given enough memory, can carry out many existing protocol anomalies. In particular, the known anomalies arise for bounded memory protocols, where there is only a bounded number of concurrent sessions and the honest participants of the protocol cannot remember an unbounded number of facts nor an unbounded number of nonces at a time. This led us to the question of whether it is possible to infer an upper-bound on the memory required by the Dolev-Yao adversary to carry out an anomaly from the memory restrictions of the bounded protocol. This paper answers this question negatively (Theorem 2).

The second contribution of this paper is the formalization of Progressing Collaborative Systems that may create fresh values, such as nonces. In this setting there is no unbounded adversary, although bounded memory adversaries may be present. We prove the NP-completeness of the reachability problem for Progressing Collaborative Systems that may create fresh values.

Added: Mar 24, 2015

Proceedings of the 34th Annual IEEE Conference on Computer Communications (INFOCOM 2015)

Hong Cong: IEEE, 2015.

Added: Feb 23, 2017