Wait‐freedom guarantees that all processes complete their operations in a finite number of steps regardless of the delay of any process. Combinatorial topology has been proposed in the literature as a formal verification technique to prove the wait‐free computability of decision tasks. Wait‐freedom is proved through the properties of a static topological structure that expresses all possible combinations of execution paths of the protocol solving the decision task. The practical application of combinatorial topology as a formal verification technique is limited because the existing theory only considers protocols in which the manner of communication between processes is through read‐write memory. This research proposes an extension to the existing theory, called the CAS‐extended model. The extended theory includes Compare‐And‐Swap (CAS) and Load‐Link/Store‐Conditional (LL/SC), which are atomic primitives used to achieve wait‐freedom in state‐of‐the‐art protocols. The CAS‐extended model theory can be used to formally verify wait‐free algorithms used in practice, such as concurrent data structures. We present new definitions detailing the construction of a protocol complex in the CAS‐extended model. As a proof‐of‐concept, we formally verify a wait‐free queue with three processes using the CAS‐extended combinatorial topology.
Why extensionbased proofs fail
It is impossible to deterministically solve waitfree consensus in an asynchronous system. The classic proof uses a valency argument, which constructs an infinite execution by repeatedly extending a finite execution. We introduce extensionbased proofs, a class of impossibility proofs that are modelled as an interaction between a prover and a protocol and that include valency arguments.
Using proofs based on combinatorial topology, it has been shown that it is impossible to deterministically solve kset agreement among n > k ≥ 2 processes in a waitfree manner. However, it was unknown whether proofs based on simpler techniques were possible. We show that this impossibility result cannot be obtained by an extensionbased proof and, hence, extensionbased proofs are limited in power.
 Publication Date:
 NSFPAR ID:
 10120533
 Journal Name:
 51st Annual ACM SIGACT Symposium on Theory of Computing
 Page Range or eLocationID:
 986 to 996
 Sponsoring Org:
 National Science Foundation
More Like this

Summary 
Intel SGX promises powerful security: an arbitrary number of usermode enclaves protected against physical attacks and privileged software adversaries. However, to achieve this, Intel extended the x86 architecture with an isolation mechanism approaching the complexity of an OS microkernel, implemented by an inscrutable mix of silicon and microcode. While hardwarebased security can offer performance and features that are difficult or impossible to achieve in pure software, hardwareonly solutions are difficult to update, either to patch security flaws or introduce new features. Komodo illustrates an alternative approach to attested, ondemand, usermode, concurrent isolated execution. We decouple the core hardware mechanisms such as memory encryption, addressspace isolation and attestation from the management thereof, which Komodo delegates to a privileged software monitor that in turn implements enclaves. The monitor's correctness is ensured by a machinecheckable proof of both functional correctness and highlevel security properties of enclave integrity and confidentiality. We show that the approach is practical and performant with a concrete implementation of a prototype in verified assembly code on ARM TrustZone. Our ultimate goal is to achieve security equivalent to or better than SGX while enabling deployment of new enclave features independently of CPU upgrades. The Komodo specification, prototype implementation, and proofsmore »

A proof of work (PoW) is an important cryptographic construct enabling a party to convince others that they invested some effort in solving a computational task. Arguably, its main impact has been in the setting of cryptocurrencies such as Bitcoin and its underlying blockchain protocol, which received significant attention in recent years due to its potential for various applications as well as for solving fundamental distributed computing questions in novel threat models. PoWs enable the linking of blocks in the blockchain data structure and thus the problem of interest is the feasibility of obtaining a sequence (chain) of such proofs. In this work, we examine the hardness of finding such chain of PoWs against quantum strategies. We prove that the chain of PoWs problem reduces to a problem we call multisolution Bernoulli search, for which we establish its quantum query complexity. Effectively, this is an extension of a threshold direct product theorem to an averagecase unstructured search problem. Our proof, adding to active recent efforts, simplifies and generalizes the recording technique of Zhandry (Crypto'19). As an application, we revisit the formal treatment of security of the core of the Bitcoin consensus protocol, the Bitcoin backbone (Eurocrypt'15), against quantum adversaries, whilemore »

We develop a new semialgebraic proof system called Stabbing Planes which formalizes modern branchandcut algorithms for integer programming and is in the style of DPLLbased modern SAT solvers. As with DPLL there is only a single rule: the current polytope can be subdivided by branching on an inequality and its “integer negation.” That is, we can (nondeterministically choose) a hyperplane ax ≥ b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying ax ≥ b, the points satisfying ax ≤ b, and the middle slab b − 1 < ax < b. Since the middle slab contains no integer points it can be safely discarded, and the algorithm proceeds recursively on the other two branches. Each path terminates when the current polytope is empty, which is polynomialtime checkable. Among our results, we show that Stabbing Planes can efficiently simulate the Cutting Planes proof system, and is equivalent to a treelike variant of the R(CP) system of Krajicek [54]. As well, we show that it possesses short proofs of the canonical family of systems of F_2linear equations known as the Tseitin formulas. Finally, we prove linear lower bounds on the rank of Stabbing Planesmore »

A collection of sets displays a proximity gap with respect to some property if for every set in the collection, either (i) all members are δclose to the property in relative Hamming distance or (ii) only a tiny fraction of members are δclose to the property. In particular, no set in the collection has roughly half of its members δclose to the property and the others δfar from it. We show that the collection of affine spaces displays a proximity gap with respect to ReedSolomon (RS) codes, even over small fields, of size polynomial in the dimension of the code, and the gap applies to any δ smaller than the Johnson/GuruswamiSudan listdecoding bound of the RS code. We also show nearoptimal gap results, over fields of (at least) linear size in the RS code dimension, for δ smaller than the unique decoding radius. Concretely, if δ is smaller than half the minimal distance of an RS code V ⊂ Fq n , every affine space is either entirely δclose to the code, or alternatively at most an ( n/q)fraction of it is δclose to the code. Finally, we discuss several applications of our proximity gap results to distributed storage, multipartymore »