Undecidability of Propositional Separation Logic and Its Neighbours
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
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.
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.
We consider the quantifier-free languages, Bc and Bc°, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of Rn (n ≥ 2) and, additionally, over the regular closed semilinear sets of Rn. The resulting logics are examples of formalisms that have recently been proposed in the Artificial Intelligence literature under the rubric Qualitative Spatial Reasoning. We prove that the satisfiability problem for Bc is undecidable over the regular closed semilinear sets in all dimensions greater than 1, and that the satisfiability problem for Bc and Bc° is undecidable over both the regular closed sets and the regular closed semilinear sets in the Euclidean plane. However, we also prove that the satisfiability problem for Bc° is NP-complete over the regular closed sets in all dimensions greater than 2, while the corresponding problem for the regular closed semilinear sets is ExpTime-complete. Our results show, in particular, that spatial reasoning is much harder over Euclidean spaces than over arbitrary topological spaces.
This volume contains the papers selected for presentation at the 18th European Symposium on Research in Computer Security (ESORICS 2013), held during September 9–13, 2013, in Egham, UK. In response to the symposium’s call for papers, 242 papers were submitted to the conference from 38 countries. These papers were evaluated on the basis of their significance, novelty, technical quality, as well as on their practical impact and/or their level of advancement of the field’s foundations. The Program Committee’s work was carri ed out electronically, yielding in- tensive discussions over a period of a few weeks. Of the papers submitted, 43 were selected for presentation at the conf erence (resulting in an acceptance rate of 18%). We note that many top-quality submissions were not selected for pre- sentation because of the high technical level of the overall submissions, and we are certain that many of these submissions will, nevertheless, be published at other competitive forums in the future.
It is well-known that the Dolev–Yao adversary is a powerful adversary. Besides acting as the network, intercepting, decomposing, composing and sending 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 although the total number of sessions is unbounded, there are only a bounded number of concurrent sessions and the honest participants of the protocol cannot remember an unbounded number of facts or 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 8).
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.
This volume contains the proceedings of the 17th International Conference on the Foundations of Software Science and Computation Structures, FOSSACS 2014, held in Grenoble, France, 5–13 April 2014. FOSSACS is an event of the Joint European Conferences on Theory and Practice of Software (ETAPS).
FOSSACS presents original papers on the foundations of software science. The conference invited submissions on theories and methods to support analysis, synthesis, transformation, and verification of programs and software systems.
We received 128 abstracts and 106 full paper s ubmissions; of these, 28 were selected for presentation at FOSSACS and inclusion in the proceedings.
The PC members, and the external experts they consulted, wrote over 320 paper reviews, and the discussion phase of the meeting included a 3-day author rebuttal phase. The competition was very strong, and unfortunately many good papers could not be accepted.
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.
We consider certain spaces of functions on the circle, which naturally appear in harmonic analysis, and superposition operators on these spaces. We study the following question: which functions have the property that each their superposition with a homeomorphism of the circle belongs to a given space? We also study the multidimensional case.
We consider the spaces of functions on the m-dimensional torus, whose Fourier transform is p -summable. We obtain estimates for the norms of the exponential functions deformed by a C1 -smooth phase. The results generalize to the multidimensional case the one-dimensional results obtained by the author earlier in “Quantitative estimates in the Beurling—Helson theorem”, Sbornik: Mathematics, 201:12 (2010), 1811 – 1836.
We consider the spaces of function on the circle whose Fourier transform is p-summable. We obtain estimates for the norms of exponential functions deformed by a C1 -smooth phase.
This proceedings publication is a compilation of selected contributions from the “Third International Conference on the Dynamics of Information Systems” which took place at the University of Florida, Gainesville, February 16–18, 2011. The purpose of this conference was to bring together scientists and engineers from industry, government, and academia in order to exchange new discoveries and results in a broad range of topics relevant to the theory and practice of dynamics of information systems. Dynamics of Information Systems: Mathematical Foundation presents state-of-the art research and is intended for graduate students and researchers interested in some of the most recent discoveries in information theory and dynamical systems. Scientists in other disciplines may also benefit from the applications of new developments to their own area of study.